/**CFile**************************************************************** FileName [abcSaucy.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Symmetry Detection Package.] Synopsis [Finds symmetries under permutation (but not negation) of I/Os.] Author [Hadi Katebi] Affiliation [University of Michigan] Date [Ver. 1.0. Started - April, 2012.] Revision [No revisions so far] Comments [] Debugging [There are some part of the code that are commented out. Those parts mostly print the contents of the data structures to the standard output. Un-comment them if you find them useful for debugging.] ***********************************************************************/ #include "base/abc/abc.h" #include "opt/sim/sim.h" ABC_NAMESPACE_IMPL_START /* on/off switches */ #define REFINE_BY_SIM_1 0 #define REFINE_BY_SIM_2 0 #define BACKTRACK_BY_SAT 1 #define SELECT_DYNAMICALLY 0 /* number of iterations for sim1 and sim2 refinements */ int NUM_SIM1_ITERATION; int NUM_SIM2_ITERATION; /* conflict analysis */ #define CLAUSE_DECAY 0.9 #define MAX_LEARNTS 50 /* * saucy.c * * by Paul T. Darga * and Mark Liffiton * and Hadi Katebi * * Copyright (C) 2004, The Regents of the University of Michigan * See the LICENSE file for details. */ struct saucy_stats { double grpsize_base; int grpsize_exp; int levels; int nodes; int bads; int gens; int support; }; struct saucy_graph { int n; int e; int *adj; int *edg; }; struct coloring { int *lab; /* Labelling of objects */ int *unlab; /* Inverse of lab */ int *cfront; /* Pointer to front of cells */ int *clen; /* Length of cells (defined for cfront's) */ }; struct sim_result { int *inVec; int *outVec; int inVecSignature; int outVecOnes; double activity; }; struct saucy { /* Graph data */ int n; /* Size of domain */ int *adj; /* Neighbors of k: edg[adj[k]]..edg[adj[k+1]] */ int *edg; /* Actual neighbor data */ int *dadj; /* Fanin neighbor indices, for digraphs */ int *dedg; /* Fanin neighbor data, for digraphs */ /* Coloring data */ struct coloring left, right; int *nextnon; /* Forward next-nonsingleton pointers */ int *prevnon; /* Backward next-nonsingleton pointers */ /* Refinement: inducers */ char *indmark; /* Induce marks */ int *ninduce; /* Nonsingletons that might induce refinement */ int *sinduce; /* Singletons that might induce refinement */ int nninduce; /* Size of ninduce stack */ int nsinduce; /* Size of sinduce stack */ /* Refinement: marked cells */ int *clist; /* List of cells marked for refining */ int csize; /* Number of cells in clist */ /* Refinement: workspace */ char *stuff; /* Bit vector, but one char per bit */ int *ccount; /* Number of connections to refining cell */ int *bucket; /* Workspace */ int *count; /* Num vertices with same adj count to ref cell */ int *junk; /* More workspace */ int *gamma; /* Working permutation */ int *conncnts; /* Connection counts for cell fronts */ /* Search data */ int lev; /* Current search tree level */ int anc; /* Level of greatest common ancestor with zeta */ int *anctar; /* Copy of target cell at anc */ int kanctar; /* Location within anctar to iterate from */ int *start; /* Location of target at each level */ int indmin; /* Used for group size computation */ int match; /* Have we not diverged from previous left? */ /* Search: orbit partition */ int *theta; /* Running approximation of orbit partition */ int *thsize; /* Size of cells in theta, defined for mcrs */ int *thnext; /* Next rep in list (circular list) */ int *thprev; /* Previous rep in list */ int *threp; /* First rep for a given cell front */ int *thfront; /* The cell front associated with this rep */ /* Search: split record */ int *splitvar; /* The actual value of the splits on the left-most branch */ int *splitwho; /* List of where splits occurred */ int *splitfrom; /* List of cells which were split */ int *splitlev; /* Where splitwho/from begins for each level */ int nsplits; /* Number of splits at this point */ /* Search: differences from leftmost */ char *diffmark; /* Marked for diff labels */ int *diffs; /* List of diff labels */ int *difflev; /* How many labels diffed at each level */ int ndiffs; /* Current number of diffs */ int *undifflev; /* How many diff labels fixed at each level */ int nundiffs; /* Current number of diffs in singletons (fixed) */ int *unsupp; /* Inverted diff array */ int *specmin; /* Speculated mappings */ int *pairs; /* Not-undiffed diffs that can make two-cycles */ int *unpairs; /* Indices into pairs */ int npairs; /* Number of such pairs */ int *diffnons; /* Diffs that haven't been undiffed */ int *undiffnons; /* Inverse of that */ int ndiffnons; /* Number of such diffs */ /* Polymorphic functions */ int (*split)(struct saucy *, struct coloring *, int, int); int (*is_automorphism)(struct saucy *); int (*ref_singleton)(struct saucy *, struct coloring *, int); int (*ref_nonsingle)(struct saucy *, struct coloring *, int); void (*select_decomposition)(struct saucy *, int *, int *, int *); /* Statistics structure */ struct saucy_stats *stats; /* New data structures for Boolean formulas */ Abc_Ntk_t * pNtk; Abc_Ntk_t * pNtk_permuted; int * depAdj; int * depEdg; Vec_Int_t ** iDep, ** oDep; Vec_Int_t ** obs, ** ctrl; Vec_Ptr_t ** topOrder; Vec_Ptr_t * randomVectorArray_sim1; int * randomVectorSplit_sim1; Vec_Ptr_t * randomVectorArray_sim2; int * randomVectorSplit_sim2; char * marks; int * pModel; Vec_Ptr_t * satCounterExamples; double activityInc; int fBooleanMatching; int fPrintTree; int fLookForSwaps; FILE * gFile; int (*refineBySim1)(struct saucy *, struct coloring *); int (*refineBySim2)(struct saucy *, struct coloring *); int (*print_automorphism)(FILE *f, int n, const int *gamma, int nsupp, const int *support, char * marks, Abc_Ntk_t * pNtk); }; static int *ints(int n) { return ABC_ALLOC(int, n); } static int *zeros(int n) { return ABC_CALLOC(int, n); } static char *bits(int n) { return ABC_CALLOC(char, n); } static char * getVertexName(Abc_Ntk_t *pNtk, int v); static int * generateProperInputVector(Abc_Ntk_t * pNtk, struct coloring *c, Vec_Int_t * randomVector); static int ifInputVectorsAreConsistent(struct saucy * s, int * leftVec, int * rightVec); static int ifOutputVectorsAreConsistent(struct saucy * s, int * leftVec, int * rightVec); static Vec_Ptr_t ** findTopologicalOrder(Abc_Ntk_t * pNtk); static void getDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep); static struct saucy_graph * buildDepGraph (Abc_Ntk_t *pNtk, Vec_Int_t ** iDep, Vec_Int_t ** oDep); static struct saucy_graph * buildSim1Graph(Abc_Ntk_t * pNtk, struct coloring *c, Vec_Int_t * randVec, Vec_Int_t ** iDep, Vec_Int_t ** oDep); static struct saucy_graph * buildSim2Graph(Abc_Ntk_t * pNtk, struct coloring *c, Vec_Int_t * randVec, Vec_Int_t ** iDep, Vec_Int_t ** oDep, Vec_Ptr_t ** topOrder, Vec_Int_t ** obs, Vec_Int_t ** ctrl); static Vec_Int_t * assignRandomBitsToCells(Abc_Ntk_t * pNtk, struct coloring *c); static int Abc_NtkCecSat_saucy(Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel); static struct sim_result * analyzeConflict(Abc_Ntk_t * pNtk, int * pModel, int fVerbose); static void bumpActivity (struct saucy * s, struct sim_result * cex); static void reduceDB(struct saucy * s); static int print_automorphism_ntk(FILE *f, int n, const int *gamma, int nsupp, const int *support, char * marks, Abc_Ntk_t * pNtk) { int i, j, k; /* We presume support is already sorted */ for (i = 0; i < nsupp; ++i) { k = support[i]; /* Skip elements already seen */ if (marks[k]) continue; /* Start an orbit */ marks[k] = 1; fprintf(f, "(%s", getVertexName(pNtk, k)); /* Mark and notify elements in this orbit */ for (j = gamma[k]; j != k; j = gamma[j]) { marks[j] = 1; fprintf(f, " %s", getVertexName(pNtk, j)); } /* Finish off the orbit */ fprintf(f, ")"); } fprintf(f, "\n"); /* Clean up after ourselves */ for (i = 0; i < nsupp; ++i) { marks[support[i]] = 0; } return 1; } static int print_automorphism_ntk2(FILE *f, int n, const int *gamma, int nsupp, const int *support, char * marks, Abc_Ntk_t * pNtk) { int i, j, k; /* We presume support is already sorted */ for (i = 0; i < nsupp; ++i) { k = support[i]; /* Skip elements already seen */ if (marks[k]) continue; /* Start an orbit */ marks[k] = 1; fprintf(f, "%d", k-1); /* Mark and notify elements in this orbit */ for (j = gamma[k]; j != k; j = gamma[j]) { marks[j] = 1; fprintf(f, " %d ", j-1); } /* Finish off the orbit */ } fprintf(f, "-1\n"); /* Clean up after ourselves */ for (i = 0; i < nsupp; ++i) { marks[support[i]] = 0; } return 1; } static int print_automorphism_quiet(FILE *f, int n, const int *gamma, int nsupp, const int *support, char * marks, Abc_Ntk_t * pNtk) { return 1; } static int array_find_min(const int *a, int n) { const int *start = a, *end = a + n, *min = a; while (++a != end) { if (*a < *min) min = a; } return min - start; } static void swap(int *a, int x, int y) { int tmp = a[x]; a[x] = a[y]; a[y] = tmp; } static void sift_up(int *a, int k) { int p; do { p = k / 2; if (a[k] <= a[p]) { return; } else { swap(a, k, p); k = p; } } while (k > 1); } static void sift_down(int *a, int n) { int p = 1, k = 2; while (k <= n) { if (k < n && a[k] < a[k+1]) ++k; if (a[p] < a[k]) { swap(a, p, k); p = k; k = 2 * p; } else { return; } } } static void heap_sort(int *a, int n) { int i; for (i = 1; i < n; ++i) { sift_up(a-1, i+1); } --i; while (i > 0) { swap(a, 0, i); sift_down(a-1, i--); } } static void insertion_sort(int *a, int n) { int i, j, k; for (i = 1; i < n; ++i) { k = a[i]; for (j = i; j > 0 && a[j-1] > k; --j) { a[j] = a[j-1]; } a[j] = k; } } static int partition(int *a, int n, int m) { int f = 0, b = n; for (;;) { while (a[f] <= m) ++f; do --b; while (m <= a[b]); if (f < b) { swap(a, f, b); ++f; } else break; } return f; } static int log_base2(int n) { int k = 0; while (n > 1) { ++k; n >>= 1; } return k; } static int median(int a, int b, int c) { if (a <= b) { if (b <= c) return b; if (a <= c) return c; return a; } else { if (a <= c) return a; if (b <= c) return c; return b; } } static void introsort_loop(int *a, int n, int lim) { int p; while (n > 16) { if (lim == 0) { heap_sort(a, n); return; } --lim; p = partition(a, n, median(a[0], a[n/2], a[n-1])); introsort_loop(a + p, n - p, lim); n = p; } } static void introsort(int *a, int n) { introsort_loop(a, n, 2 * log_base2(n)); insertion_sort(a, n); } static int do_find_min(struct coloring *c, int t) { return array_find_min(c->lab + t, c->clen[t] + 1) + t; } static int find_min(struct saucy *s, int t) { return do_find_min(&s->right, t); } static void set_label(struct coloring *c, int index, int value) { c->lab[index] = value; c->unlab[value] = index; } static void swap_labels(struct coloring *c, int a, int b) { int tmp = c->lab[a]; set_label(c, a, c->lab[b]); set_label(c, b, tmp); } static void move_to_back(struct saucy *s, struct coloring *c, int k) { int cf = c->cfront[k]; int cb = cf + c->clen[cf]; int offset = s->conncnts[cf]++; /* Move this connected label to the back of its cell */ swap_labels(c, cb - offset, c->unlab[k]); /* Add it to the cell list if it's the first one swapped */ if (!offset) s->clist[s->csize++] = cf; } static void data_mark(struct saucy *s, struct coloring *c, int k) { int cf = c->cfront[k]; /* Move connects to the back of nonsingletons */ if (c->clen[cf]) move_to_back(s, c, k); } static void data_count(struct saucy *s, struct coloring *c, int k) { int cf = c->cfront[k]; /* Move to back and count the number of connections */ if (c->clen[cf] && !s->ccount[k]++) move_to_back(s, c, k); } static int check_mapping(struct saucy *s, const int *adj, const int *edg, int k) { int i, gk, ret = 1; /* Mark gamma of neighbors */ for (i = adj[k]; i != adj[k+1]; ++i) { s->stuff[s->gamma[edg[i]]] = 1; } /* Check neighbors of gamma */ gk = s->gamma[k]; for (i = adj[gk]; ret && i != adj[gk+1]; ++i) { ret = s->stuff[edg[i]]; } /* Clear out bit vector before we leave */ for (i = adj[k]; i != adj[k+1]; ++i) { s->stuff[s->gamma[edg[i]]] = 0; } return ret; } static int add_conterexample(struct saucy *s, struct sim_result * cex) { int i; int nins = Abc_NtkPiNum(s->pNtk); struct sim_result * savedcex; cex->inVecSignature = 0; for (i = 0; i < nins; i++) { if (cex->inVec[i]) { cex->inVecSignature += (cex->inVec[i] * i * i); cex->inVecSignature ^= 0xABCD; } } for (i = 0; i < Vec_PtrSize(s->satCounterExamples); i++) { savedcex = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, i); if (savedcex->inVecSignature == cex->inVecSignature) { //bumpActivity(s, savedcex); return 0; } } Vec_PtrPush(s->satCounterExamples, cex); bumpActivity(s, cex); return 1; } static int is_undirected_automorphism(struct saucy *s) { int i, j, ret; for (i = 0; i < s->ndiffs; ++i) { j = s->unsupp[i]; if (!check_mapping(s, s->adj, s->edg, j)) return 0; } ret = Abc_NtkCecSat_saucy(s->pNtk, s->pNtk_permuted, s->pModel); if( BACKTRACK_BY_SAT && !ret ) { struct sim_result * cex; cex = analyzeConflict( s->pNtk, s->pModel, s->fPrintTree ); add_conterexample(s, cex); cex = analyzeConflict( s->pNtk_permuted, s->pModel, s->fPrintTree ); add_conterexample(s, cex); s->activityInc *= (1 / CLAUSE_DECAY); if (Vec_PtrSize(s->satCounterExamples) >= MAX_LEARNTS) reduceDB(s); } return ret; } static int is_directed_automorphism(struct saucy *s) { int i, j; for (i = 0; i < s->ndiffs; ++i) { j = s->unsupp[i]; if (!check_mapping(s, s->adj, s->edg, j)) return 0; if (!check_mapping(s, s->dadj, s->dedg, j)) return 0; } return 1; } static void add_induce(struct saucy *s, struct coloring *c, int who) { if (!c->clen[who]) { s->sinduce[s->nsinduce++] = who; } else { s->ninduce[s->nninduce++] = who; } s->indmark[who] = 1; } static void fix_fronts(struct coloring *c, int cf, int ff) { int i, end = cf + c->clen[cf]; for (i = ff; i <= end; ++i) { c->cfront[c->lab[i]] = cf; } } static void array_indirect_sort(int *a, const int *b, int n) { int h, i, j, k; /* Shell sort, as implemented in nauty, (C) Brendan McKay */ j = n / 3; h = 1; do { h = 3 * h + 1; } while (h < j); do { for (i = h; i < n; ++i) { k = a[i]; for (j = i; b[a[j-h]] > b[k]; ) { a[j] = a[j-h]; if ((j -= h) < h) break; } a[j] = k; } h /= 3; } while (h > 0); } static int at_terminal(struct saucy *s) { return s->nsplits == s->n; } static void add_diffnon(struct saucy *s, int k) { /* Only add if we're in a consistent state */ if (s->ndiffnons == -1) return; s->undiffnons[k] = s->ndiffnons; s->diffnons[s->ndiffnons++] = k; } static void remove_diffnon(struct saucy *s, int k) { int j; if (s->undiffnons[k] == -1) return; j = s->diffnons[--s->ndiffnons]; s->diffnons[s->undiffnons[k]] = j; s->undiffnons[j] = s->undiffnons[k]; s->undiffnons[k] = -1; } static void add_diff(struct saucy *s, int k) { if (!s->diffmark[k]) { s->diffmark[k] = 1; s->diffs[s->ndiffs++] = k; add_diffnon(s, k); } } static int is_a_pair(struct saucy *s, int k) { return s->unpairs[k] != -1; } static int in_cell_range(struct coloring *c, int ff, int cf) { int cb = cf + c->clen[cf]; return cf <= ff && ff <= cb; } static void add_pair(struct saucy *s, int k) { if (s->npairs != -1) { s->unpairs[k] = s->npairs; s->pairs[s->npairs++] = k; } } static void eat_pair(struct saucy *s, int k) { int j; j = s->pairs[--s->npairs]; s->pairs[s->unpairs[k]] = j; s->unpairs[j] = s->unpairs[k]; s->unpairs[k] = -1; } static void pick_all_the_pairs(struct saucy *s) { int i; for (i = 0; i < s->npairs; ++i) { s->unpairs[s->pairs[i]] = -1; } s->npairs = 0; } static void clear_undiffnons(struct saucy *s) { int i; for (i = 0 ; i < s->ndiffnons ; ++i) { s->undiffnons[s->diffnons[i]] = -1; } } static void fix_diff_singleton(struct saucy *s, int cf) { int r = s->right.lab[cf]; int l = s->left.lab[cf]; int rcfl; if (!s->right.clen[cf] && r != l) { /* Make sure diff is marked */ add_diff(s, r); /* It is now undiffed since it is singleton */ ++s->nundiffs; remove_diffnon(s, r); /* Mark the other if not singleton already */ rcfl = s->right.cfront[l]; if (s->right.clen[rcfl]) { add_diff(s, l); /* Check for pairs */ if (in_cell_range(&s->right, s->left.unlab[r], rcfl)) { add_pair(s, l); } } /* Otherwise we might be eating a pair */ else if (is_a_pair(s, r)) { eat_pair(s, r); } } } static void fix_diff_subtract(struct saucy *s, int cf, const int *a, const int *b) { int i, k; int cb = cf + s->right.clen[cf]; /* Mark the contents of the first set */ for (i = cf; i <= cb; ++i) { s->stuff[a[i]] = 1; } /* Add elements from second set not present in the first */ for (i = cf; i <= cb; ++i) { k = b[i]; if (!s->stuff[k]) add_diff(s, k); } /* Clear the marks of the first set */ for (i = cf; i <= cb; ++i) { s->stuff[a[i]] = 0; } } static void fix_diffs(struct saucy *s, int cf, int ff) { int min; /* Check for singleton cases in both cells */ fix_diff_singleton(s, cf); fix_diff_singleton(s, ff); /* If they're both nonsingleton, do subtraction on smaller */ if (s->right.clen[cf] && s->right.clen[ff]) { min = s->right.clen[cf] < s->right.clen[ff] ? cf : ff; fix_diff_subtract(s, min, s->left.lab, s->right.lab); fix_diff_subtract(s, min, s->right.lab, s->left.lab); } } static void split_color(struct coloring *c, int cf, int ff) { int cb, fb; /* Fix lengths */ fb = ff - 1; cb = cf + c->clen[cf]; c->clen[cf] = fb - cf; c->clen[ff] = cb - ff; /* Fix cell front pointers */ fix_fronts(c, ff, ff); } static void split_common(struct saucy *s, struct coloring *c, int cf, int ff) { split_color(c, cf, ff); /* Add to refinement */ if (s->indmark[cf] || c->clen[ff] < c->clen[cf]) { add_induce(s, c, ff); } else { add_induce(s, c, cf); } } static int split_left(struct saucy *s, struct coloring *c, int cf, int ff) { /* Record the split */ s->splitwho[s->nsplits] = ff; s->splitfrom[s->nsplits] = cf; ++s->nsplits; /* Do common splitting tasks */ split_common(s, c, cf, ff); /* Always succeeds */ return 1; } static int split_init(struct saucy *s, struct coloring *c, int cf, int ff) { split_left(s, c, cf, ff); /* Maintain nonsingleton list for finding new targets */ if (c->clen[ff]) { s->prevnon[s->nextnon[cf]] = ff; s->nextnon[ff] = s->nextnon[cf]; s->prevnon[ff] = cf; s->nextnon[cf] = ff; } if (!c->clen[cf]) { s->nextnon[s->prevnon[cf]] = s->nextnon[cf]; s->prevnon[s->nextnon[cf]] = s->prevnon[cf]; } /* Always succeeds */ return 1; } static int split_other(struct saucy *s, struct coloring *c, int cf, int ff) { int k = s->nsplits; /* Verify the split with init */ if (s->splitwho[k] != ff || s->splitfrom[k] != cf || k >= s->splitlev[s->lev]) { return 0; } ++s->nsplits; /* Do common splitting tasks */ split_common(s, c, cf, ff); /* Fix differences with init */ fix_diffs(s, cf, ff); /* If we got this far we succeeded */ return 1; } static int print_partition(struct coloring *left, struct coloring *right, int n, Abc_Ntk_t * pNtk, int fNames) { int i, j; printf("top = |"); for(i = 0; i < n; i += (left->clen[i]+1)) { for(j = 0; j < (left->clen[i]+1); j++) { if (fNames) printf("%s ", getVertexName(pNtk, left->lab[i+j])); else printf("%d ", left->lab[i+j]); } if((i+left->clen[i]+1) < n) printf("|"); } printf("|\n"); /*printf("(cfront = {"); for (i = 0; i < n; i++) printf("%d ", left->cfront[i]); printf("})\n");*/ if (right == NULL) return 1; printf("bot = |"); for(i = 0; i < n; i += (right->clen[i]+1)) { for(j = 0; j < (right->clen[i]+1); j++) { if (fNames) printf("%s ", getVertexName(pNtk, right->lab[i+j])); else printf("%d ", right->lab[i+j]); } if((i+right->clen[i]+1) < n) printf("|"); } printf("|\n"); /*printf("(cfront = {"); for (i = 0; i < n; i++) printf("%d ", right->cfront[i]); printf("})\n");*/ return 1; } static int refine_cell(struct saucy *s, struct coloring *c, int (*refine)(struct saucy *, struct coloring *, int)) { int i, cf, ret = 1; /* * The connected list must be consistent. This is for * detecting mappings across nodes at a given level. However, * at the root of the tree, we never have to map with another * node, so we lack this consistency constraint in that case. */ if (s->lev > 1) introsort(s->clist, s->csize); /* Now iterate over the marked cells */ for (i = 0; ret && i < s->csize; ++i) { cf = s->clist[i]; ret = refine(s, c, cf); } /* Clear the connected marks */ for (i = 0; i < s->csize; ++i) { cf = s->clist[i]; s->conncnts[cf] = 0; } s->csize = 0; return ret; } static int maybe_split(struct saucy *s, struct coloring *c, int cf, int ff) { return cf == ff ? 1 : s->split(s, c, cf, ff); } static int ref_single_cell(struct saucy *s, struct coloring *c, int cf) { int zcnt = c->clen[cf] + 1 - s->conncnts[cf]; return maybe_split(s, c, cf, cf + zcnt); } static int ref_singleton(struct saucy *s, struct coloring *c, const int *adj, const int *edg, int cf) { int i, k = c->lab[cf]; /* Find the cells we're connected to, and mark our neighbors */ for (i = adj[k]; i != adj[k+1]; ++i) { data_mark(s, c, edg[i]); } /* Refine the cells we're connected to */ return refine_cell(s, c, ref_single_cell); } static int ref_singleton_directed(struct saucy *s, struct coloring *c, int cf) { return ref_singleton(s, c, s->adj, s->edg, cf) && ref_singleton(s, c, s->dadj, s->dedg, cf); } static int ref_singleton_undirected(struct saucy *s, struct coloring *c, int cf) { return ref_singleton(s, c, s->adj, s->edg, cf); } static int ref_nonsingle_cell(struct saucy *s, struct coloring *c, int cf) { int cnt, i, cb, nzf, ff, fb, bmin, bmax; /* Find the front and back */ cb = cf + c->clen[cf]; nzf = cb - s->conncnts[cf] + 1; /* Prepare the buckets */ ff = nzf; cnt = s->ccount[c->lab[ff]]; s->count[ff] = bmin = bmax = cnt; s->bucket[cnt] = 1; /* Iterate through the rest of the vertices */ while (++ff <= cb) { cnt = s->ccount[c->lab[ff]]; /* Initialize intermediate buckets */ while (bmin > cnt) s->bucket[--bmin] = 0; while (bmax < cnt) s->bucket[++bmax] = 0; /* Mark this count */ ++s->bucket[cnt]; s->count[ff] = cnt; } /* If they all had the same count, bail */ if (bmin == bmax && cf == nzf) return 1; ff = fb = nzf; /* Calculate bucket locations, sizes */ for (i = bmin; i <= bmax; ++i, ff = fb) { if (!s->bucket[i]) continue; fb = ff + s->bucket[i]; s->bucket[i] = fb; } /* Repair the partition nest */ for (i = nzf; i <= cb; ++i) { s->junk[--s->bucket[s->count[i]]] = c->lab[i]; } for (i = nzf; i <= cb; ++i) { set_label(c, i, s->junk[i]); } /* Split; induce */ for (i = bmax; i > bmin; --i) { ff = s->bucket[i]; if (ff && !s->split(s, c, cf, ff)) return 0; } /* If there was a zero area, then there's one more cell */ return maybe_split(s, c, cf, s->bucket[bmin]); } static int ref_nonsingle(struct saucy *s, struct coloring *c, const int *adj, const int *edg, int cf) { int i, j, k, ret; const int cb = cf + c->clen[cf]; const int size = cb - cf + 1; /* Double check for nonsingles which became singles later */ if (cf == cb) { return ref_singleton(s, c, adj, edg, cf); } /* Establish connected list */ memcpy(s->junk, c->lab + cf, size * sizeof(int)); for (i = 0; i < size; ++i) { k = s->junk[i]; for (j = adj[k]; j != adj[k+1]; ++j) { data_count(s, c, edg[j]); } } /* Refine the cells we're connected to */ ret = refine_cell(s, c, ref_nonsingle_cell); /* Clear the counts; use lab because junk was overwritten */ for (i = cf; i <= cb; ++i) { k = c->lab[i]; for (j = adj[k]; j != adj[k+1]; ++j) { s->ccount[edg[j]] = 0; } } return ret; } static int ref_nonsingle_directed(struct saucy *s, struct coloring *c, int cf) { return ref_nonsingle(s, c, s->adj, s->edg, cf) && ref_nonsingle(s, c, s->dadj, s->dedg, cf); } static int ref_nonsingle_undirected(struct saucy *s, struct coloring *c, int cf) { return ref_nonsingle(s, c, s->adj, s->edg, cf); } static void clear_refine(struct saucy *s) { int i; for (i = 0; i < s->nninduce; ++i) { s->indmark[s->ninduce[i]] = 0; } for (i = 0; i < s->nsinduce; ++i) { s->indmark[s->sinduce[i]] = 0; } s->nninduce = s->nsinduce = 0; } static int refine(struct saucy *s, struct coloring *c) { int front; /* Keep going until refinement stops */ while (1) { /* If discrete, bail */ if (at_terminal(s)) { clear_refine(s); return 1; }; /* Look for something else to refine on */ if (s->nsinduce) { front = s->sinduce[--s->nsinduce]; s->indmark[front] = 0; if (!s->ref_singleton(s, c, front)) break; } else if (s->nninduce) { front = s->ninduce[--s->nninduce]; s->indmark[front] = 0; if (!s->ref_nonsingle(s, c, front)) break; } else { return 1; }; } clear_refine(s); return 0; } static int refineByDepGraph(struct saucy *s, struct coloring *c) { s->adj = s->depAdj; s->edg = s->depEdg; return refine(s, c); } static int backtrackBysatCounterExamples(struct saucy *s, struct coloring *c) { int i, j, res; struct sim_result * cex1, * cex2; int * flag = zeros(Vec_PtrSize(s->satCounterExamples)); if (c == &s->left) return 1; if (Vec_PtrSize(s->satCounterExamples) == 0) return 1; for (i = 0; i < Vec_PtrSize(s->satCounterExamples); i++) { cex1 = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, i); for (j = 0; j < Vec_PtrSize(s->satCounterExamples); j++) { if (flag[j]) continue; cex2 = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, j); res = ifInputVectorsAreConsistent(s, cex1->inVec, cex2->inVec); if (res == -2) { flag[j] = 1; continue; } if (res == -1) break; if (res == 0) continue; if (cex1->outVecOnes != cex2->outVecOnes) { bumpActivity(s, cex1); bumpActivity(s, cex2); ABC_FREE(flag); return 0; } /* if two input vectors produce the same number of ones (look above), and * pNtk's number of outputs is 1, then output vectors are definitely consistent. */ if (Abc_NtkPoNum(s->pNtk) == 1) continue; if (!ifOutputVectorsAreConsistent(s, cex1->outVec, cex2->outVec)) { bumpActivity(s, cex1); bumpActivity(s, cex2); ABC_FREE(flag); return 0; } } } ABC_FREE(flag); return 1; } static int refineBySim1_init(struct saucy *s, struct coloring *c) { struct saucy_graph *g; Vec_Int_t * randVec; int i, j; int allOutputsAreDistinguished; int nsplits; if (Abc_NtkPoNum(s->pNtk) == 1) return 1; for (i = 0; i < NUM_SIM1_ITERATION; i++) { /* if all outputs are distinguished, quit */ allOutputsAreDistinguished = 1; for (j = 0; j < Abc_NtkPoNum(s->pNtk); j++) { if (c->clen[j]) { allOutputsAreDistinguished = 0; break; } } if (allOutputsAreDistinguished) break; randVec = assignRandomBitsToCells(s->pNtk, c); g = buildSim1Graph(s->pNtk, c, randVec, s->iDep, s->oDep); assert(g != NULL); s->adj = g->adj; s->edg = g->edg; nsplits = s->nsplits; for (j = 0; j < s->n; j += c->clen[j]+1) add_induce(s, c, j); refine(s, c); if (s->nsplits > nsplits) { i = 0; /* reset i */ /* do more refinement by dependency graph */ for (j = 0; j < s->n; j += c->clen[j]+1) add_induce(s, c, j); refineByDepGraph(s, c); } Vec_IntFree(randVec); ABC_FREE( g->adj ); ABC_FREE( g->edg ); ABC_FREE( g ); } return 1; } static int refineBySim1_left(struct saucy *s, struct coloring *c) { struct saucy_graph *g; Vec_Int_t * randVec; int i, j; int allOutputsAreDistinguished; int nsplits; if (Abc_NtkPoNum(s->pNtk) == 1) return 1; for (i = 0; i < NUM_SIM1_ITERATION; i++) { /* if all outputs are distinguished, quit */ allOutputsAreDistinguished = 1; for (j = 0; j < Abc_NtkPoNum(s->pNtk); j++) { if (c->clen[j]) { allOutputsAreDistinguished = 0; break; } } if (allOutputsAreDistinguished) break; randVec = assignRandomBitsToCells(s->pNtk, c); g = buildSim1Graph(s->pNtk, c, randVec, s->iDep, s->oDep); assert(g != NULL); s->adj = g->adj; s->edg = g->edg; nsplits = s->nsplits; for (j = 0; j < s->n; j += c->clen[j]+1) add_induce(s, c, j); refine(s, c); if (s->nsplits > nsplits) { /* save the random vector */ Vec_PtrPush(s->randomVectorArray_sim1, randVec); i = 0; /* reset i */ /* do more refinement by dependency graph */ for (j = 0; j < s->n; j += c->clen[j]+1) add_induce(s, c, j); refineByDepGraph(s, c); } else Vec_IntFree(randVec); ABC_FREE( g->adj ); ABC_FREE( g->edg ); ABC_FREE( g ); } s->randomVectorSplit_sim1[s->lev] = Vec_PtrSize(s->randomVectorArray_sim1); return 1; } static int refineBySim1_other(struct saucy *s, struct coloring *c) { struct saucy_graph *g; Vec_Int_t * randVec; int i, j; int ret, nsplits; for (i = s->randomVectorSplit_sim1[s->lev-1]; i < s->randomVectorSplit_sim1[s->lev]; i++) { randVec = (Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim1, i); g = buildSim1Graph(s->pNtk, c, randVec, s->iDep, s->oDep); if (g == NULL) { assert(c == &s->right); return 0; } s->adj = g->adj; s->edg = g->edg; nsplits = s->nsplits; for (j = 0; j < s->n; j += c->clen[j]+1) add_induce(s, c, j); ret = refine(s, c); if (s->nsplits == nsplits) { assert(c == &s->right); ret = 0; } if (ret) { /* do more refinement now by dependency graph */ for (j = 0; j < s->n; j += c->clen[j]+1) add_induce(s, c, j); ret = refineByDepGraph(s, c); } ABC_FREE( g->adj ); ABC_FREE( g->edg ); ABC_FREE( g ); if (!ret) return 0; } return 1; } static int refineBySim2_init(struct saucy *s, struct coloring *c) { struct saucy_graph *g; Vec_Int_t * randVec; int i, j; int nsplits; for (i = 0; i < NUM_SIM2_ITERATION; i++) { randVec = assignRandomBitsToCells(s->pNtk, c); g = buildSim2Graph(s->pNtk, c, randVec, s->iDep, s->oDep, s->topOrder, s->obs, s->ctrl); assert(g != NULL); s->adj = g->adj; s->edg = g->edg; nsplits = s->nsplits; for (j = 0; j < s->n; j += c->clen[j]+1) add_induce(s, c, j); refine(s, c); if (s->nsplits > nsplits) { i = 0; /* reset i */ /* do more refinement by dependency graph */ for (j = 0; j < s->n; j += c->clen[j]+1) add_induce(s, c, j); refineByDepGraph(s, c); } Vec_IntFree(randVec); ABC_FREE( g->adj ); ABC_FREE( g->edg ); ABC_FREE( g ); } return 1; } static int refineBySim2_left(struct saucy *s, struct coloring *c) { struct saucy_graph *g; Vec_Int_t * randVec; int i, j; int nsplits; for (i = 0; i < NUM_SIM2_ITERATION; i++) { randVec = assignRandomBitsToCells(s->pNtk, c); g = buildSim2Graph(s->pNtk, c, randVec, s->iDep, s->oDep, s->topOrder, s->obs, s->ctrl); assert(g != NULL); s->adj = g->adj; s->edg = g->edg; nsplits = s->nsplits; for (j = 0; j < s->n; j += c->clen[j]+1) add_induce(s, c, j); refine(s, c); if (s->nsplits > nsplits) { /* save the random vector */ Vec_PtrPush(s->randomVectorArray_sim2, randVec); i = 0; /* reset i */ /* do more refinement by dependency graph */ for (j = 0; j < s->n; j += c->clen[j]+1) add_induce(s, c, j); refineByDepGraph(s, c); } else Vec_IntFree(randVec); ABC_FREE( g->adj ); ABC_FREE( g->edg ); ABC_FREE( g ); } s->randomVectorSplit_sim2[s->lev] = Vec_PtrSize(s->randomVectorArray_sim2); return 1; } static int refineBySim2_other(struct saucy *s, struct coloring *c) { struct saucy_graph *g; Vec_Int_t * randVec; int i, j; int ret, nsplits; for (i = s->randomVectorSplit_sim2[s->lev-1]; i < s->randomVectorSplit_sim2[s->lev]; i++) { randVec = (Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim2, i); g = buildSim2Graph(s->pNtk, c, randVec, s->iDep, s->oDep, s->topOrder, s->obs, s->ctrl); if (g == NULL) { assert(c == &s->right); return 0; } s->adj = g->adj; s->edg = g->edg; nsplits = s->nsplits; for (j = 0; j < s->n; j += c->clen[j]+1) add_induce(s, c, j); ret = refine(s, c); if (s->nsplits == nsplits) { assert(c == &s->right); ret = 0; } if (ret) { /* do more refinement by dependency graph */ for (j = 0; j < s->n; j += c->clen[j]+1) add_induce(s, c, j); ret = refineByDepGraph(s, c); } ABC_FREE( g->adj ); ABC_FREE( g->edg ); ABC_FREE( g ); if (!ret) { assert(c == &s->right); return 0; } } return 1; } static int check_OPP_only_has_swaps(struct saucy *s, struct coloring *c) { int j, cell; Vec_Int_t * left_cfront, * right_cfront; if (c == &s->left) return 1; left_cfront = Vec_IntAlloc (1); right_cfront = Vec_IntAlloc (1); for (cell = 0; cell < s->n; cell += (s->left.clen[cell]+1)) { for (j = cell; j <= (cell+s->left.clen[cell]); j++) { Vec_IntPush(left_cfront, s->left.cfront[s->right.lab[j]]); Vec_IntPush(right_cfront, s->right.cfront[s->left.lab[j]]); } Vec_IntSortUnsigned(left_cfront); Vec_IntSortUnsigned(right_cfront); for (j = 0; j < Vec_IntSize(left_cfront); j++) { if (Vec_IntEntry(left_cfront, j) != Vec_IntEntry(right_cfront, j)) { Vec_IntFree(left_cfront); Vec_IntFree(right_cfront); return 0; } } Vec_IntClear(left_cfront); Vec_IntClear(right_cfront); } Vec_IntFree(left_cfront); Vec_IntFree(right_cfront); return 1; } static int check_OPP_for_Boolean_matching(struct saucy *s, struct coloring *c) { int j, cell; int countN1Left, countN2Left; int countN1Right, countN2Right; char *name; if (c == &s->left) return 1; for (cell = 0; cell < s->n; cell += (s->right.clen[cell]+1)) { countN1Left = countN2Left = countN1Right = countN2Right = 0; for (j = cell; j <= (cell+s->right.clen[cell]); j++) { name = getVertexName(s->pNtk, s->left.lab[j]); assert(name[0] == 'N' && name[2] == ':'); if (name[1] == '1') countN1Left++; else { assert(name[1] == '2'); countN2Left++; } name = getVertexName(s->pNtk, s->right.lab[j]); assert(name[0] == 'N' && name[2] == ':'); if (name[1] == '1') countN1Right++; else { assert(name[1] == '2'); countN2Right++; } } if (countN1Left != countN2Right || countN2Left != countN1Right) return 0; } return 1; } static int double_check_OPP_isomorphism(struct saucy *s, struct coloring * c) { /* This is the new enhancement in saucy 3.0 */ int i, j, v, sum1, sum2, xor1, xor2; if (c == &s->left) return 1; for (i = s->nsplits - 1; i > s->splitlev[s->lev-1]; --i) { v = c->lab[s->splitwho[i]]; sum1 = xor1 = 0; for (j = s->adj[v]; j < s->adj[v+1]; j++) { sum1 += c->cfront[s->edg[j]]; xor1 ^= c->cfront[s->edg[j]]; } v = s->left.lab[s->splitwho[i]]; sum2 = xor2 = 0; for (j = s->adj[v]; j < s->adj[v+1]; j++) { sum2 += s->left.cfront[s->edg[j]]; xor2 ^= s->left.cfront[s->edg[j]]; } if ((sum1 != sum2) || (xor1 != xor2)) return 0; v = c->lab[s->splitfrom[i]]; sum1 = xor1 = 0; for (j = s->adj[v]; j < s->adj[v+1]; j++) { sum1 += c->cfront[s->edg[j]]; xor1 ^= c->cfront[s->edg[j]]; } v = s->left.lab[s->splitfrom[i]]; sum2 = xor2 = 0; for (j = s->adj[v]; j < s->adj[v+1]; j++) { sum2 += s->left.cfront[s->edg[j]]; xor2 ^= s->left.cfront[s->edg[j]]; } if ((sum1 != sum2) || (xor1 != xor2)) return 0; } return 1; } static int descend(struct saucy *s, struct coloring *c, int target, int min) { int back = target + c->clen[target]; /* Count this node */ ++s->stats->nodes; /* Move the minimum label to the back */ swap_labels(c, min, back); /* Split the cell */ s->difflev[s->lev] = s->ndiffs; s->undifflev[s->lev] = s->nundiffs; ++s->lev; s->split(s, c, target, back); /* Now go and do some work */ //print_partition(&s->left, NULL, s->n, s->pNtk, 1); if (!refineByDepGraph(s, c)) return 0; /* if we are looking for a Boolean matching, check the OPP and * backtrack if the OPP maps part of one network to itself */ if (s->fBooleanMatching && !check_OPP_for_Boolean_matching(s, c)) return 0; //print_partition(&s->left, NULL, s->n, s->pNtk, 1); if (REFINE_BY_SIM_1 && !s->refineBySim1(s, c)) return 0; //print_partition(&s->left, NULL, s->n, s->pNtk, 1); if (REFINE_BY_SIM_2 && !s->refineBySim2(s, c)) return 0; /* do the check once more, maybe the check fails, now that refinement is complete */ if (s->fBooleanMatching && !check_OPP_for_Boolean_matching(s, c)) return 0; if (s->fLookForSwaps && !check_OPP_only_has_swaps(s, c)) return 0; if (!double_check_OPP_isomorphism(s, c)) return 0; return 1; } static int select_smallest_max_connected_cell(struct saucy *s, int start, int end) { int smallest_cell = -1, cell; int smallest_cell_size = s->n; int max_connections = -1; int * connection_list = zeros(s->n); cell = start; while( !s->left.clen[cell] ) cell++; while( cell < end ) { if (s->left.clen[cell] <= smallest_cell_size) { int i, connections = 0;; for (i = s->depAdj[s->left.lab[cell]]; i < s->depAdj[s->left.lab[cell]+1]; i++) { if (!connection_list[s->depEdg[i]]) { connections++; connection_list[s->depEdg[i]] = 1; } } if ((s->left.clen[cell] < smallest_cell_size) || (connections > max_connections)) { smallest_cell_size = s->left.clen[cell]; max_connections = connections; smallest_cell = cell; } for (i = s->depAdj[s->left.lab[cell]]; i < s->depAdj[s->left.lab[cell]+1]; i++) connection_list[s->depEdg[i]] = 0; } cell = s->nextnon[cell]; } ABC_FREE( connection_list ); return smallest_cell; } static int descend_leftmost(struct saucy *s) { int target, min; /* Keep going until we're discrete */ //print_partition(&s->left, NULL, s->n, s->pNtk, 1); while (!at_terminal(s)) { //target = min = s->nextnon[-1]; if (s->nextnon[-1] < Abc_NtkPoNum(s->pNtk)) target = min = select_smallest_max_connected_cell(s, s->nextnon[-1], Abc_NtkPoNum(s->pNtk)); else target = min = select_smallest_max_connected_cell(s, Abc_NtkPoNum(s->pNtk), s->n); if (s->fPrintTree) printf("%s->%s\n", getVertexName(s->pNtk, s->left.lab[min]), getVertexName(s->pNtk, s->left.lab[min])); s->splitvar[s->lev] = s->left.lab[min]; s->start[s->lev] = target; s->splitlev[s->lev] = s->nsplits; if (!descend(s, &s->left, target, min)) return 0; } s->splitlev[s->lev] = s->n; return 1; } /* * If the remaining nonsingletons in this partition match exactly * those nonsingletons from the leftmost branch of the search tree, * then there is no point in continuing descent. */ static int zeta_fixed(struct saucy *s) { return s->ndiffs == s->nundiffs; } static void select_dynamically(struct saucy *s, int *target, int *lmin, int *rmin) { /* Both clens are equal; this clarifies the code a bit */ const int *clen = s->left.clen; int i, k; //int cf; /* * If there's a pair, use it. pairs[0] should always work, * but we use a checked loop instead because I'm not 100% sure * I'm "unpairing" at every point I should be. */ for (i = 0; i < s->npairs; ++i) { k = s->pairs[i]; *target = s->right.cfront[k]; *lmin = s->left.unlab[s->right.lab[s->left.unlab[k]]]; *rmin = s->right.unlab[k]; if (clen[*target] && in_cell_range(&s->left, *lmin, *target) && in_cell_range(&s->right, *rmin, *target)) return; } /* Diffnons is only consistent when there are no baddies */ /*if (s->ndiffnons != -1) { *target = *lmin = *rmin = s->right.cfront[s->diffnons[0]]; return; }*/ /* Pick any old target cell and element */ /*for (i = 0; i < s->ndiffs; ++i) { cf = s->right.cfront[s->diffs[i]]; if (clen[cf]) { *lmin = *rmin = *target = cf; return; } }*/ for (i = 0; i < s->n; i += (clen[i]+1)) { if (!clen[i]) continue; *rmin = *lmin = *target = i; if (s->right.cfront[s->left.lab[*lmin]] == *target) *rmin = s->right.unlab[s->left.lab[*lmin]]; return; } /* we should never get here */ abort(); } static void select_statically(struct saucy *s, int *target, int *lmin, int *rmin) { int i; *target = *rmin = s->left.cfront[s->splitvar[s->lev]]; *lmin = s->left.unlab[s->splitvar[s->lev]]; /* try to map identically! */ for (i = *rmin; i <= (*rmin + s->right.clen[*target]); i++) if (s->right.lab[*rmin] == s->left.lab[*lmin]) { *rmin = i; break; } } static int descend_left(struct saucy *s) { int target, lmin, rmin; /* Check that we ended at the right spot */ if (s->nsplits != s->splitlev[s->lev]) return 0; /* Keep going until we're discrete */ while (!at_terminal(s) /*&& !zeta_fixed(s)*/) { /* We can pick any old target cell and element */ s->select_decomposition(s, &target, &lmin, &rmin); if (s->fPrintTree) { //printf("in level %d: %d->%d\n", s->lev, s->left.lab[lmin], s->right.lab[rmin]); printf("in level %d: %s->%s\n", s->lev, getVertexName(s->pNtk, s->left.lab[lmin]), getVertexName(s->pNtk, s->right.lab[rmin])); } /* Check if we need to refine on the left */ s->match = 0; s->start[s->lev] = target; s->split = split_left; if (SELECT_DYNAMICALLY) { s->refineBySim1 = refineBySim1_left; s->refineBySim2 = refineBySim2_left; } descend(s, &s->left, target, lmin); s->splitlev[s->lev] = s->nsplits; s->split = split_other; if (SELECT_DYNAMICALLY) { s->refineBySim1 = refineBySim1_other; s->refineBySim2 = refineBySim2_other; } --s->lev; s->nsplits = s->splitlev[s->lev]; /* Now refine on the right and ensure matching */ s->specmin[s->lev] = s->right.lab[rmin]; if (!descend(s, &s->right, target, rmin)) return 0; if (s->nsplits != s->splitlev[s->lev]) return 0; } return 1; } static int find_representative(int k, int *theta) { int rep, tmp; /* Find the minimum cell representative */ for (rep = k; rep != theta[rep]; rep = theta[rep]); /* Update all intermediaries */ while (theta[k] != rep) { tmp = theta[k]; theta[k] = rep; k = tmp; } return rep; } static void update_theta(struct saucy *s) { int i, k, x, y, tmp; for (i = 0; i < s->ndiffs; ++i) { k = s->unsupp[i]; x = find_representative(k, s->theta); y = find_representative(s->gamma[k], s->theta); if (x != y) { if (x > y) { tmp = x; x = y; y = tmp; } s->theta[y] = x; s->thsize[x] += s->thsize[y]; s->thnext[s->thprev[y]] = s->thnext[y]; s->thprev[s->thnext[y]] = s->thprev[y]; s->threp[s->thfront[y]] = s->thnext[y]; } } } static int theta_prune(struct saucy *s) { int start = s->start[s->lev]; int label, rep, irep; irep = find_representative(s->indmin, s->theta); while (s->kanctar) { label = s->anctar[--s->kanctar]; rep = find_representative(label, s->theta); if (rep == label && rep != irep) { return s->right.unlab[label] - start; } } return -1; } static int orbit_prune(struct saucy *s) { int i, label, fixed, min = -1; int k = s->start[s->lev]; int size = s->right.clen[k] + 1; int *cell = s->right.lab + k; /* The previously fixed value */ fixed = cell[size-1]; /* Look for the next minimum cell representative */ for (i = 0; i < size-1; ++i) { label = cell[i]; /* Skip things we've already considered */ if (label <= fixed) continue; /* Skip things that we'll consider later */ if (min != -1 && label > cell[min]) continue; /* New candidate minimum */ min = i; } return min; } static void note_anctar_reps(struct saucy *s) { int i, j, k, m, f, rep, tmp; /* * Undo the previous level's splits along leftmost so that we * join the appropriate lists of theta reps. */ for (i = s->splitlev[s->anc+1]-1; i >= s->splitlev[s->anc]; --i) { f = s->splitfrom[i]; j = s->threp[f]; k = s->threp[s->splitwho[i]]; s->thnext[s->thprev[j]] = k; s->thnext[s->thprev[k]] = j; tmp = s->thprev[j]; s->thprev[j] = s->thprev[k]; s->thprev[k] = tmp; for (m = k; m != j; m = s->thnext[m]) { s->thfront[m] = f; } } /* * Just copy over the target's reps and sort by cell size, in * the hopes of trimming some otherwise redundant generators. */ s->kanctar = 0; s->anctar[s->kanctar++] = rep = s->threp[s->start[s->lev]]; for (k = s->thnext[rep]; k != rep; k = s->thnext[k]) { s->anctar[s->kanctar++] = k; } array_indirect_sort(s->anctar, s->thsize, s->kanctar); } static void multiply_index(struct saucy *s, int k) { if ((s->stats->grpsize_base *= k) > 1e10) { s->stats->grpsize_base /= 1e10; s->stats->grpsize_exp += 10; } } static int backtrack_leftmost(struct saucy *s) { int rep = find_representative(s->indmin, s->theta); int repsize = s->thsize[rep]; int min = -1; pick_all_the_pairs(s); clear_undiffnons(s); s->ndiffs = s->nundiffs = s->npairs = s->ndiffnons = 0; if (repsize != s->right.clen[s->start[s->lev]]+1) { min = theta_prune(s); } if (min == -1) { multiply_index(s, repsize); } return min; } static int backtrack_other(struct saucy *s) { int cf = s->start[s->lev]; int cb = cf + s->right.clen[cf]; int spec = s->specmin[s->lev]; int min; /* Avoid using pairs until we get back to leftmost. */ pick_all_the_pairs(s); clear_undiffnons(s); s->npairs = s->ndiffnons = -1; if (s->right.lab[cb] == spec) { min = find_min(s, cf); if (min == cb) { min = orbit_prune(s); } else { min -= cf; } } else { min = orbit_prune(s); if (min != -1 && s->right.lab[min + cf] == spec) { swap_labels(&s->right, min + cf, cb); min = orbit_prune(s); } } return min; } static void rewind_coloring(struct saucy *s, struct coloring *c, int lev) { int i, cf, ff, splits = s->splitlev[lev]; for (i = s->nsplits - 1; i >= splits; --i) { cf = s->splitfrom[i]; ff = s->splitwho[i]; c->clen[cf] += c->clen[ff] + 1; fix_fronts(c, cf, ff); } } static void rewind_simulation_vectors(struct saucy *s, int lev) { int i; for (i = s->randomVectorSplit_sim1[lev]; i < Vec_PtrSize(s->randomVectorArray_sim1); i++) Vec_IntFree((Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim1, i)); Vec_PtrShrink(s->randomVectorArray_sim1, s->randomVectorSplit_sim1[lev]); for (i = s->randomVectorSplit_sim2[lev]; i < Vec_PtrSize(s->randomVectorArray_sim2); i++) Vec_IntFree((Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim2, i)); Vec_PtrShrink(s->randomVectorArray_sim2, s->randomVectorSplit_sim2[lev]); } static int do_backtrack(struct saucy *s) { int i, cf, cb; /* Undo the splits up to this level */ rewind_coloring(s, &s->right, s->lev); s->nsplits = s->splitlev[s->lev]; /* Rewind diff information */ for (i = s->ndiffs - 1; i >= s->difflev[s->lev]; --i) { s->diffmark[s->diffs[i]] = 0; } s->ndiffs = s->difflev[s->lev]; s->nundiffs = s->undifflev[s->lev]; /* Point to the target cell */ cf = s->start[s->lev]; cb = cf + s->right.clen[cf]; /* Update ancestor with zeta if we've rewound more */ if (s->anc > s->lev) { s->anc = s->lev; s->indmin = s->left.lab[cb]; s->match = 1; note_anctar_reps(s); } /* Perform backtracking appropriate to our location */ return s->lev == s->anc ? backtrack_leftmost(s) : backtrack_other(s); } static int backtrack_loop(struct saucy *s) { int min; /* Backtrack as long as we're exhausting target cells */ for (--s->lev; s->lev; --s->lev) { min = do_backtrack(s); if (min != -1) return min + s->start[s->lev]; } return -1; } static int backtrack(struct saucy *s) { int min, old, tmp; old = s->nsplits; min = backtrack_loop(s); tmp = s->nsplits; s->nsplits = old; rewind_coloring(s, &s->left, s->lev+1); s->nsplits = tmp; if (SELECT_DYNAMICALLY) rewind_simulation_vectors(s, s->lev+1); return min; } static int backtrack_bad(struct saucy *s) { int min, old, tmp; old = s->lev; min = backtrack_loop(s); if (BACKTRACK_BY_SAT) { int oldLev = s->lev; while (!backtrackBysatCounterExamples(s, &s->right)) { min = backtrack_loop(s); if (!s->lev) { if (s->fPrintTree) printf("Backtrack by SAT from level %d to %d\n", oldLev, 0); return -1; } } if (s->fPrintTree) if (s->lev < oldLev) printf("Backtrack by SAT from level %d to %d\n", oldLev, s->lev); } tmp = s->nsplits; s->nsplits = s->splitlev[old]; rewind_coloring(s, &s->left, s->lev+1); s->nsplits = tmp; if (SELECT_DYNAMICALLY) rewind_simulation_vectors(s, s->lev+1); return min; } void prepare_permutation_ntk(struct saucy *s) { int i; Abc_Obj_t * pObj, * pObjPerm; int numouts = Abc_NtkPoNum(s->pNtk); Nm_ManFree( s->pNtk_permuted->pManName ); s->pNtk_permuted->pManName = Nm_ManCreate( Abc_NtkCiNum(s->pNtk) + Abc_NtkCoNum(s->pNtk) + Abc_NtkBoxNum(s->pNtk) ); for (i = 0; i < s->n; ++i) { if (i < numouts) { pObj = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk->vPos, i); pObjPerm = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk_permuted->vPos, s->gamma[i]); } else { pObj = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk->vPis, i - numouts); pObjPerm = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk_permuted->vPis, s->gamma[i] - numouts); } Abc_ObjAssignName( pObjPerm, Abc_ObjName(pObj), NULL ); } Abc_NtkOrderObjsByName( s->pNtk_permuted, 1 ); /* print the permutation */ /*for (i = 0; i < s->ndiffs; ++i) printf(" %d->%d", s->unsupp[i], s->diffs[i]); printf("\n"); Abc_NtkForEachCo( s->pNtk, pObj, i ) printf (" %d", Abc_ObjId(pObj)-1-Abc_NtkPiNum(s->pNtk)); Abc_NtkForEachCi( s->pNtk, pObj, i ) printf (" %d", Abc_ObjId(pObj)-1+Abc_NtkPoNum(s->pNtk)); printf("\n"); Abc_NtkForEachCo( s->pNtk_permuted, pObj, i ) printf (" %d", Abc_ObjId(pObj)-1-Abc_NtkPiNum(s->pNtk_permuted)); Abc_NtkForEachCi( s->pNtk_permuted, pObj, i ) printf (" %d", Abc_ObjId(pObj)-1+Abc_NtkPoNum(s->pNtk_permuted)); printf("\n");*/ } static void prepare_permutation(struct saucy *s) { int i, k; for (i = 0; i < s->ndiffs; ++i) { k = s->right.unlab[s->diffs[i]]; s->unsupp[i] = s->left.lab[k]; s->gamma[s->left.lab[k]] = s->right.lab[k]; } prepare_permutation_ntk(s); } void unprepare_permutation_ntk(struct saucy *s) { int i; Abc_Obj_t * pObj, * pObjPerm; int numouts = Abc_NtkPoNum(s->pNtk); Nm_ManFree( s->pNtk_permuted->pManName ); s->pNtk_permuted->pManName = Nm_ManCreate( Abc_NtkCiNum(s->pNtk) + Abc_NtkCoNum(s->pNtk) + Abc_NtkBoxNum(s->pNtk) ); for (i = 0; i < s->n; ++i) { if (i < numouts) { pObj = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk->vPos, s->gamma[i]); pObjPerm = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk_permuted->vPos, i); } else { pObj = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk->vPis, s->gamma[i] - numouts); pObjPerm = (Abc_Obj_t *)Vec_PtrEntry(s->pNtk_permuted->vPis, i - numouts); } Abc_ObjAssignName( pObjPerm, Abc_ObjName(pObj), NULL ); } Abc_NtkOrderObjsByName( s->pNtk_permuted, 1 ); } static void unprepare_permutation(struct saucy *s) { int i; unprepare_permutation_ntk(s); for (i = 0; i < s->ndiffs; ++i) { s->gamma[s->unsupp[i]] = s->unsupp[i]; } } static int do_search(struct saucy *s) { int min; unprepare_permutation(s); /* Backtrack to the ancestor with zeta */ if (s->lev > s->anc) s->lev = s->anc + 1; /* Perform additional backtracking */ min = backtrack(s); if (s->fBooleanMatching && (s->stats->grpsize_base > 1 || s->stats->grpsize_exp > 0)) return 0; if (s->fPrintTree && s->lev > 0) { //printf("in level %d: %d->%d\n", s->lev, s->left.lab[s->splitwho[s->nsplits]], s->right.lab[min]); printf("in level %d: %s->%s\n", s->lev, getVertexName(s->pNtk, s->left.lab[s->splitwho[s->nsplits]]), getVertexName(s->pNtk, s->right.lab[min])); } /* Keep going while there are tree nodes to expand */ while (s->lev) { /* Descend to a new leaf node */ if (descend(s, &s->right, s->start[s->lev], min) && descend_left(s)) { /* Prepare permutation */ prepare_permutation(s); /* If we found an automorphism, return it */ if (s->is_automorphism(s)) { ++s->stats->gens; s->stats->support += s->ndiffs; update_theta(s); s->print_automorphism(s->gFile, s->n, s->gamma, s->ndiffs, s->unsupp, s->marks, s->pNtk); unprepare_permutation(s); return 1; } else { unprepare_permutation(s); } } /* If we get here, something went wrong; backtrack */ ++s->stats->bads; min = backtrack_bad(s); if (s->fPrintTree) { printf("BAD NODE\n"); if (s->lev > 0) { //printf("in level %d: %d->%d\n", s->lev, s->left.lab[s->splitwho[s->nsplits]], s->right.lab[min]); printf("in level %d: %s->%s\n", s->lev, getVertexName(s->pNtk, s->left.lab[s->splitwho[s->nsplits]]), getVertexName(s->pNtk, s->right.lab[min])); } } } /* Normalize group size */ while (s->stats->grpsize_base >= 10.0) { s->stats->grpsize_base /= 10; ++s->stats->grpsize_exp; } return 0; } void saucy_search( Abc_Ntk_t * pNtk, struct saucy *s, int directed, const int *colors, struct saucy_stats *stats) { int i, j, max = 0; struct saucy_graph *g; extern Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ); /* Save network information */ s->pNtk = pNtk; s->pNtk_permuted = Abc_NtkDup( pNtk ); /* Builde dependency graph */ g = buildDepGraph(pNtk, s->iDep, s->oDep); /* Save graph information */ s->n = g->n; s->depAdj = g->adj; s->depEdg = g->edg; /*s->dadj = g->adj + g->n + 1; s->dedg = g->edg + g->e;*/ /* Save client information */ s->stats = stats; /* Polymorphism */ if (directed) { s->is_automorphism = is_directed_automorphism; s->ref_singleton = ref_singleton_directed; s->ref_nonsingle = ref_nonsingle_directed; } else { s->is_automorphism = is_undirected_automorphism; s->ref_singleton = ref_singleton_undirected; s->ref_nonsingle = ref_nonsingle_undirected; } /* Initialize scalars */ s->indmin = 0; s->lev = s->anc = 1; s->ndiffs = s->nundiffs = s->ndiffnons = 0; s->activityInc = 1; /* The initial orbit partition is discrete */ for (i = 0; i < s->n; ++i) { s->theta[i] = i; } /* The initial permutation is the identity */ for (i = 0; i < s->n; ++i) { s->gamma[i] = i; } /* Initially every cell of theta has one element */ for (i = 0; i < s->n; ++i) { s->thsize[i] = 1; } /* Every theta rep list is singleton */ for (i = 0; i < s->n; ++i) { s->thprev[i] = s->thnext[i] = i; } /* We have no pairs yet */ s->npairs = 0; for (i = 0; i < s->n; ++i) { s->unpairs[i] = -1; } /* Ensure no stray pointers in undiffnons, which is checked by removed_diffnon() */ for (i = 0; i < s->n; ++i) { s->undiffnons[i] = -1; } /* Initialize stats */ s->stats->grpsize_base = 1.0; s->stats->grpsize_exp = 0; s->stats->nodes = 1; s->stats->bads = s->stats->gens = s->stats->support = 0; /* Prepare for refinement */ s->nninduce = s->nsinduce = 0; s->csize = 0; /* Count cell sizes */ for (i = 0; i < s->n; ++i) { s->ccount[colors[i]]++; if (max < colors[i]) max = colors[i]; } s->nsplits = max + 1; /* Build cell lengths */ s->left.clen[0] = s->ccount[0] - 1; for (i = 0; i < max; ++i) { s->left.clen[s->ccount[i]] = s->ccount[i+1] - 1; s->ccount[i+1] += s->ccount[i]; } /* Build the label array */ for (i = 0; i < s->n; ++i) { set_label(&s->left, --s->ccount[colors[i]], i); } /* Clear out ccount */ for (i = 0; i <= max; ++i) { s->ccount[i] = 0; } /* Update refinement stuff based on initial partition */ for (i = 0; i < s->n; i += s->left.clen[i]+1) { add_induce(s, &s->left, i); fix_fronts(&s->left, i, i); } /* Prepare lists based on cell lengths */ for (i = 0, j = -1; i < s->n; i += s->left.clen[i] + 1) { if (!s->left.clen[i]) continue; s->prevnon[i] = j; s->nextnon[j] = i; j = i; } /* Fix the end */ s->prevnon[s->n] = j; s->nextnon[j] = s->n; /* Preprocessing after initial coloring */ s->split = split_init; s->refineBySim1 = refineBySim1_init; s->refineBySim2 = refineBySim2_init; //print_partition(&s->left, NULL, s->n, s->pNtk, 1); printf("Initial Refine by Dependency graph ... "); refineByDepGraph(s, &s->left); //print_partition(&s->left, NULL, s->n, s->pNtk, 1); printf("done!\n"); printf("Initial Refine by Simulation ... "); if (REFINE_BY_SIM_1) s->refineBySim1(s, &s->left); //print_partition(&s->left, NULL, s->n, s->pNtk, 1); if (REFINE_BY_SIM_2) s->refineBySim2(s, &s->left); //print_partition(&s->left, NULL, s->n, s->pNtk, 1); printf("done!\n\t--------------------\n"); /* Descend along the leftmost branch and compute zeta */ s->refineBySim1 = refineBySim1_left; s->refineBySim2 = refineBySim2_left; descend_leftmost(s); s->split = split_other; s->refineBySim1 = refineBySim1_other; s->refineBySim2 = refineBySim2_other; /* Our common ancestor with zeta is the current level */ s->stats->levels = s->anc = s->lev; /* Copy over this data to our non-leftmost coloring */ memcpy(s->right.lab, s->left.lab, s->n * sizeof(int)); memcpy(s->right.unlab, s->left.unlab, s->n * sizeof(int)); memcpy(s->right.clen, s->left.clen, s->n * sizeof(int)); memcpy(s->right.cfront, s->left.cfront, s->n * sizeof(int)); /* The reps are just the labels at this point */ memcpy(s->threp, s->left.lab, s->n * sizeof(int)); memcpy(s->thfront, s->left.unlab, s->n * sizeof(int)); /* choose cell selection method */ if (SELECT_DYNAMICALLY) s->select_decomposition = select_dynamically; else s->select_decomposition = select_statically; /* Keep running till we're out of automorphisms */ while (do_search(s)); } void saucy_free(struct saucy *s) { int i; ABC_FREE(s->undiffnons); ABC_FREE(s->diffnons); ABC_FREE(s->unpairs); ABC_FREE(s->pairs); ABC_FREE(s->thfront); ABC_FREE(s->threp); ABC_FREE(s->thnext); ABC_FREE(s->thprev); ABC_FREE(s->specmin); ABC_FREE(s->anctar); ABC_FREE(s->thsize); ABC_FREE(s->undifflev); ABC_FREE(s->difflev); ABC_FREE(s->diffs); ABC_FREE(s->diffmark); ABC_FREE(s->conncnts); ABC_FREE(s->unsupp); ABC_FREE(s->splitlev); ABC_FREE(s->splitfrom); ABC_FREE(s->splitwho); ABC_FREE(s->splitvar); ABC_FREE(s->right.unlab); ABC_FREE(s->right.lab); ABC_FREE(s->left.unlab); ABC_FREE(s->left.lab); ABC_FREE(s->theta); ABC_FREE(s->junk); ABC_FREE(s->gamma); ABC_FREE(s->start); ABC_FREE(s->prevnon); free(s->nextnon-1); ABC_FREE(s->clist); ABC_FREE(s->ccount); ABC_FREE(s->count); ABC_FREE(s->bucket); ABC_FREE(s->stuff); ABC_FREE(s->right.clen); ABC_FREE(s->right.cfront); ABC_FREE(s->left.clen); ABC_FREE(s->left.cfront); ABC_FREE(s->indmark); ABC_FREE(s->sinduce); ABC_FREE(s->ninduce); ABC_FREE(s->depAdj); ABC_FREE(s->depEdg); ABC_FREE(s->marks); for (i = 0; i < Abc_NtkPiNum(s->pNtk); i++) { Vec_IntFree( s->iDep[i] ); Vec_IntFree( s->obs[i] ); Vec_PtrFree( s->topOrder[i] ); } for (i = 0; i < Abc_NtkPoNum(s->pNtk); i++) { Vec_IntFree( s->oDep[i] ); Vec_IntFree( s->ctrl[i] ); } for (i = 0; i < Vec_PtrSize(s->randomVectorArray_sim1); i++) Vec_IntFree((Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim1, i)); for (i = 0; i < Vec_PtrSize(s->randomVectorArray_sim2); i++) Vec_IntFree((Vec_Int_t *)Vec_PtrEntry(s->randomVectorArray_sim2, i)); Vec_PtrFree( s->randomVectorArray_sim1 ); Vec_PtrFree( s->randomVectorArray_sim2 ); ABC_FREE(s->randomVectorSplit_sim1); ABC_FREE(s->randomVectorSplit_sim2); Abc_NtkDelete( s->pNtk_permuted ); for (i = 0; i < Vec_PtrSize(s->satCounterExamples); i++) { struct sim_result * cex = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, i); ABC_FREE( cex->inVec ); ABC_FREE( cex->outVec ); ABC_FREE( cex ); } Vec_PtrFree(s->satCounterExamples); ABC_FREE( s->pModel ); ABC_FREE( s->iDep ); ABC_FREE( s->oDep ); ABC_FREE( s->obs ); ABC_FREE( s->ctrl ); ABC_FREE( s->topOrder ); ABC_FREE(s); } struct saucy * saucy_alloc(Abc_Ntk_t * pNtk) { int i; int numouts = Abc_NtkPoNum(pNtk); int numins = Abc_NtkPiNum(pNtk); int n = numins + numouts; struct saucy *s = ABC_ALLOC(struct saucy, 1); if (s == NULL) return NULL; s->ninduce = ints(n); s->sinduce = ints(n); s->indmark = bits(n); s->left.cfront = zeros(n); s->left.clen = ints(n); s->right.cfront = zeros(n); s->right.clen = ints(n); s->stuff = bits(n+1); s->bucket = ints(n+2); s->count = ints(n+1); s->ccount = zeros(n); s->clist = ints(n); s->nextnon = ints(n+1) + 1; s->prevnon = ints(n+1); s->anctar = ints(n); s->start = ints(n); s->gamma = ints(n); s->junk = ints(n); s->theta = ints(n); s->thsize = ints(n); s->left.lab = ints(n); s->left.unlab = ints(n); s->right.lab = ints(n); s->right.unlab = ints(n); s->splitvar = ints(n); s->splitwho = ints(n); s->splitfrom = ints(n); s->splitlev = ints(n+1); s->unsupp = ints(n); s->conncnts = zeros(n); s->diffmark = bits(n); s->diffs = ints(n); s->difflev = ints(n); s->undifflev = ints(n); s->specmin = ints(n); s->thnext = ints(n); s->thprev = ints(n); s->threp = ints(n); s->thfront = ints(n); s->pairs = ints(n); s->unpairs = ints(n); s->diffnons = ints(n); s->undiffnons = ints(n); s->marks = bits(n); s->iDep = ABC_ALLOC( Vec_Int_t*, numins ); s->oDep = ABC_ALLOC( Vec_Int_t*, numouts ); s->obs = ABC_ALLOC( Vec_Int_t*, numins ); s->ctrl = ABC_ALLOC( Vec_Int_t*, numouts ); for(i = 0; i < numins; i++) { s->iDep[i] = Vec_IntAlloc( 1 ); s->obs[i] = Vec_IntAlloc( 1 ); } for(i = 0; i < numouts; i++) { s->oDep[i] = Vec_IntAlloc( 1 ); s->ctrl[i] = Vec_IntAlloc( 1 ); } s->randomVectorArray_sim1 = Vec_PtrAlloc( n ); s->randomVectorSplit_sim1 = zeros( n ); s->randomVectorArray_sim2 = Vec_PtrAlloc( n ); s->randomVectorSplit_sim2= zeros( n ); s->satCounterExamples = Vec_PtrAlloc( 1 ); s->pModel = ints( numins ); if (s->ninduce && s->sinduce && s->left.cfront && s->left.clen && s->right.cfront && s->right.clen && s->stuff && s->bucket && s->count && s->ccount && s->clist && s->nextnon-1 && s->prevnon && s->start && s->gamma && s->theta && s->left.unlab && s->right.lab && s->right.unlab && s->left.lab && s->splitvar && s->splitwho && s->junk && s->splitfrom && s->splitlev && s->thsize && s->unsupp && s->conncnts && s->anctar && s->diffmark && s->diffs && s->indmark && s->thnext && s->thprev && s->threp && s->thfront && s->pairs && s->unpairs && s->diffnons && s->undiffnons && s->difflev && s->undifflev && s->specmin) { return s; } else { saucy_free(s); return NULL; } } static void print_stats(FILE *f, struct saucy_stats stats ) { fprintf(f, "group size = %fe%d\n", stats.grpsize_base, stats.grpsize_exp); fprintf(f, "levels = %d\n", stats.levels); fprintf(f, "nodes = %d\n", stats.nodes); fprintf(f, "generators = %d\n", stats.gens); fprintf(f, "total support = %d\n", stats.support); fprintf(f, "average support = %.2f\n",(double)(stats.support)/(double)(stats.gens)); fprintf(f, "nodes per generator = %.2f\n",(double)(stats.nodes)/(double)(stats.gens)); fprintf(f, "bad nodes = %d\n", stats.bads); } /* From this point up are SAUCY functions*/ ///////////////////////////////////////////////////////////////////////////////////////////////////////// /* From this point down are new functions */ static char * getVertexName(Abc_Ntk_t *pNtk, int v) { Abc_Obj_t * pObj; int numouts = Abc_NtkPoNum(pNtk); if (v < numouts) pObj = (Abc_Obj_t *)Vec_PtrEntry(pNtk->vPos, v); else pObj = (Abc_Obj_t *)Vec_PtrEntry(pNtk->vPis, v - numouts); return Abc_ObjName(pObj); } static Vec_Ptr_t ** findTopologicalOrder( Abc_Ntk_t * pNtk ) { Vec_Ptr_t ** vNodes; Abc_Obj_t * pObj, * pFanout; int i, k; extern void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); /* start the array of nodes */ vNodes = ABC_ALLOC(Vec_Ptr_t *, Abc_NtkPiNum(pNtk)); for(i = 0; i < Abc_NtkPiNum(pNtk); i++) vNodes[i] = Vec_PtrAlloc(50); Abc_NtkForEachCi( pNtk, pObj, i ) { /* set the traversal ID */ Abc_NtkIncrementTravId( pNtk ); Abc_NodeSetTravIdCurrent( pObj ); pObj = Abc_ObjFanout0Ntk(pObj); Abc_ObjForEachFanout( pObj, pFanout, k ) Abc_NtkDfsReverse_rec( pFanout, vNodes[i] ); } return vNodes; } static void getDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep) { Vec_Ptr_t * vSuppFun; int i, j; vSuppFun = Sim_ComputeFunSupp(pNtk, 0); for(i = 0; i < Abc_NtkPoNum(pNtk); i++) { char * seg = (char *)vSuppFun->pArray[i]; for(j = 0; j < Abc_NtkPiNum(pNtk); j+=8) { if(((*seg) & 0x01) == 0x01) Vec_IntPushOrder(oDep[i], j); if(((*seg) & 0x02) == 0x02) Vec_IntPushOrder(oDep[i], j+1); if(((*seg) & 0x04) == 0x04) Vec_IntPushOrder(oDep[i], j+2); if(((*seg) & 0x08) == 0x08) Vec_IntPushOrder(oDep[i], j+3); if(((*seg) & 0x10) == 0x10) Vec_IntPushOrder(oDep[i], j+4); if(((*seg) & 0x20) == 0x20) Vec_IntPushOrder(oDep[i], j+5); if(((*seg) & 0x40) == 0x40) Vec_IntPushOrder(oDep[i], j+6); if(((*seg) & 0x80) == 0x80) Vec_IntPushOrder(oDep[i], j+7); seg++; } } for(i = 0; i < Abc_NtkPoNum(pNtk); i++) for(j = 0; j < Vec_IntSize(oDep[i]); j++) Vec_IntPush(iDep[Vec_IntEntry(oDep[i], j)], i); /*for(i = 0; i < Abc_NtkPoNum(pNtk); i++) { printf("Output %d: ", i); for(j = 0; j < Vec_IntSize(oDep[i]); j++) printf("%d ", Vec_IntEntry(oDep[i], j)); printf("\n"); } printf("\n"); for(i = 0; i < Abc_NtkPiNum(pNtk); i++) { printf("Input %d: ", i); for(j = 0; j < Vec_IntSize(iDep[i]); j++) printf("%d ", Vec_IntEntry(iDep[i], j)); printf("\n"); } printf("\n"); */ } static void getDependenciesDummy(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep) { int i, j; /* let's assume that every output is dependent on every input */ for(i = 0; i < Abc_NtkPoNum(pNtk); i++) for(j = 0; j < Abc_NtkPiNum(pNtk); j++) Vec_IntPush(oDep[i], j); for(i = 0; i < Abc_NtkPiNum(pNtk); i++) for(j = 0; j < Abc_NtkPoNum(pNtk); j++) Vec_IntPush(iDep[i], j); } static struct saucy_graph * buildDepGraph(Abc_Ntk_t *pNtk, Vec_Int_t ** iDep, Vec_Int_t ** oDep) { int i, j, k; struct saucy_graph *g = NULL; int n, e, *adj, *edg; n = Abc_NtkPoNum(pNtk) + Abc_NtkPiNum(pNtk); for (e = 0, i = 0; i < Abc_NtkPoNum(pNtk); i++) e += Vec_IntSize(oDep[i]); g = ABC_ALLOC(struct saucy_graph, 1); adj = zeros(n+1); edg = ints(2*e); g->n = n; g->e = e; g->adj = adj; g->edg = edg; adj[0] = 0; for (i = 0; i < n; i++) { /* first add outputs and then inputs */ if ( i < Abc_NtkPoNum(pNtk)) { adj[i+1] = adj[i] + Vec_IntSize(oDep[i]); for (k = 0, j = adj[i]; j < adj[i+1]; j++, k++) edg[j] = Vec_IntEntry(oDep[i], k) + Abc_NtkPoNum(pNtk); } else { adj[i+1] = adj[i] + Vec_IntSize(iDep[i-Abc_NtkPoNum(pNtk)]); for (k = 0, j = adj[i]; j < adj[i+1]; j++, k++) edg[j] = Vec_IntEntry(iDep[i-Abc_NtkPoNum(pNtk)], k); } } /* print graph for testing */ /*for (i = 0; i < n; i++) { printf("%d: ", i); for (j = adj[i]; j < adj[i+1]; j++) printf("%d ", edg[j]); printf("\n"); }*/ return g; } static Vec_Int_t * assignRandomBitsToCells(Abc_Ntk_t * pNtk, struct coloring *c) { Vec_Int_t * randVec = Vec_IntAlloc( 1 ); int i, bit; for (i = 0; i < Abc_NtkPiNum(pNtk); i += (c->clen[i+Abc_NtkPoNum(pNtk)]+1)) { bit = (int)(SIM_RANDOM_UNSIGNED % 2); Vec_IntPush(randVec, bit); } return randVec; } static int * generateProperInputVector( Abc_Ntk_t * pNtk, struct coloring *c, Vec_Int_t * randomVector ) { int * vPiValues; int i, j, k, bit, input; int numouts = Abc_NtkPoNum(pNtk); int numins = Abc_NtkPiNum(pNtk); int n = numouts + numins; vPiValues = ABC_ALLOC( int, numins); for (i = numouts, k = 0; i < n; i += (c->clen[i]+1), k++) { if (k == Vec_IntSize(randomVector)) break; bit = Vec_IntEntry(randomVector, k); for (j = i; j <= (i + c->clen[i]); j++) { input = c->lab[j] - numouts; vPiValues[input] = bit; } } //if (k != Vec_IntSize(randomVector)) { if (i < n) { ABC_FREE( vPiValues ); return NULL; } return vPiValues; } static int ifInputVectorsAreConsistent( struct saucy * s, int * leftVec, int * rightVec ) { /* This function assumes that left and right partitions are isomorphic */ int i, j; int lab; int left_bit, right_bit; int numouts = Abc_NtkPoNum(s->pNtk); int n = numouts + Abc_NtkPiNum(s->pNtk); for (i = numouts; i < n; i += (s->right.clen[i]+1)) { lab = s->left.lab[i] - numouts; left_bit = leftVec[lab]; for (j = i+1; j <= (i + s->right.clen[i]); j++) { lab = s->left.lab[j] - numouts; if (left_bit != leftVec[lab]) return -1; } lab = s->right.lab[i] - numouts; right_bit = rightVec[lab]; for (j = i+1; j <= (i + s->right.clen[i]); j++) { lab = s->right.lab[j] - numouts; if (right_bit != rightVec[lab]) return 0; } if (left_bit != right_bit) return 0; } return 1; } static int ifOutputVectorsAreConsistent( struct saucy * s, int * leftVec, int * rightVec ) { /* This function assumes that left and right partitions are isomorphic */ int i, j; int count1, count2; for (i = 0; i < Abc_NtkPoNum(s->pNtk); i += (s->right.clen[i]+1)) { count1 = count2 = 0; for (j = i; j <= (i + s->right.clen[i]); j++) { if (leftVec[s->left.lab[j]]) count1++; if (rightVec[s->right.lab[j]]) count2++; } if (count1 != count2) return 0; } return 1; } static struct saucy_graph * buildSim1Graph( Abc_Ntk_t * pNtk, struct coloring *c, Vec_Int_t * randVec, Vec_Int_t ** iDep, Vec_Int_t ** oDep ) { int i, j, k; struct saucy_graph *g; int n, e, *adj, *edg; int * vPiValues, * output; int numOneOutputs = 0; int numouts = Abc_NtkPoNum(pNtk); int numins = Abc_NtkPiNum(pNtk); vPiValues = generateProperInputVector(pNtk, c, randVec); if (vPiValues == NULL) return NULL; output = Abc_NtkVerifySimulatePattern(pNtk, vPiValues); for (i = 0; i < numouts; i++) { if (output[i]) numOneOutputs++; } g = ABC_ALLOC(struct saucy_graph, 1); n = numouts + numins; e = numins * numOneOutputs; adj = ints(n+1); edg = ints(2*e); g->n = n; g->e = e; g->adj = adj; g->edg = edg; adj[0] = 0; for (i = 0; i < numouts; i++) { if (output[i]) { adj[i+1] = adj[i] + Vec_IntSize(oDep[i]); for (j = adj[i], k = 0; j < adj[i+1]; j++, k++) edg[j] = Vec_IntEntry(oDep[i], k) + numouts; } else { adj[i+1] = adj[i]; } } for (i = 0; i < numins; i++) { adj[i+numouts+1] = adj[i+numouts]; for (k = 0, j = adj[i+numouts]; k < Vec_IntSize(iDep[i]); k++) { if (output[Vec_IntEntry(iDep[i], k)]) { edg[j++] = Vec_IntEntry(iDep[i], k); adj[i+numouts+1]++; } } } /* print graph */ /*for (i = 0; i < n; i++) { printf("%d: ", i); for (j = adj[i]; j < adj[i+1]; j++) printf("%d ", edg[j]); printf("\n"); }*/ ABC_FREE( vPiValues ); ABC_FREE( output ); return g; } static struct saucy_graph * buildSim2Graph( Abc_Ntk_t * pNtk, struct coloring *c, Vec_Int_t * randVec, Vec_Int_t ** iDep, Vec_Int_t ** oDep, Vec_Ptr_t ** topOrder, Vec_Int_t ** obs, Vec_Int_t ** ctrl ) { int i, j, k; struct saucy_graph *g = NULL; int n, e = 0, *adj, *edg; int * vPiValues; int * output, * output2; int numouts = Abc_NtkPoNum(pNtk); int numins = Abc_NtkPiNum(pNtk); extern int * Abc_NtkSimulateOneNode( Abc_Ntk_t * , int * , int , Vec_Ptr_t ** ); vPiValues = generateProperInputVector(pNtk, c, randVec); if (vPiValues == NULL) return NULL; output = Abc_NtkVerifySimulatePattern( pNtk, vPiValues ); for (i = 0; i < numins; i++) { if (!c->clen[c->cfront[i+numouts]]) continue; if (vPiValues[i] == 0) vPiValues[i] = 1; else vPiValues[i] = 0; output2 = Abc_NtkSimulateOneNode( pNtk, vPiValues, i, topOrder ); for (j = 0; j < Vec_IntSize(iDep[i]); j++) { if (output[Vec_IntEntry(iDep[i], j)] != output2[Vec_IntEntry(iDep[i], j)]) { Vec_IntPush(obs[i], Vec_IntEntry(iDep[i], j)); Vec_IntPush(ctrl[Vec_IntEntry(iDep[i], j)], i); e++; } } if (vPiValues[i] == 0) vPiValues[i] = 1; else vPiValues[i] = 0; ABC_FREE( output2 ); } /* build the graph */ g = ABC_ALLOC(struct saucy_graph, 1); n = numouts + numins; adj = ints(n+1); edg = ints(2*e); g->n = n; g->e = e; g->adj = adj; g->edg = edg; adj[0] = 0; for (i = 0; i < numouts; i++) { adj[i+1] = adj[i] + Vec_IntSize(ctrl[i]); for (k = 0, j = adj[i]; j < adj[i+1]; j++, k++) edg[j] = Vec_IntEntry(ctrl[i], k) + numouts; } for (i = 0; i < numins; i++) { adj[i+numouts+1] = adj[i+numouts] + Vec_IntSize(obs[i]); for (k = 0, j = adj[i+numouts]; j < adj[i+numouts+1]; j++, k++) edg[j] = Vec_IntEntry(obs[i], k); } /* print graph */ /*for (i = 0; i < n; i++) { printf("%d: ", i); for (j = adj[i]; j < adj[i+1]; j++) printf("%d ", edg[j]); printf("\n"); }*/ ABC_FREE( output ); ABC_FREE( vPiValues ); for (j = 0; j < numins; j++) Vec_IntClear(obs[j]); for (j = 0; j < numouts; j++) Vec_IntClear(ctrl[j]); return g; } static void bumpActivity( struct saucy * s, struct sim_result * cex ) { int i; struct sim_result * cex2; if ( (cex->activity += s->activityInc) > 1e20 ) { /* Rescale: */ for (i = 0; i < Vec_PtrSize(s->satCounterExamples); i++) { cex2 = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, i); cex2->activity *= 1e-20; } s->activityInc *= 1e-20; } } static void reduceDB( struct saucy * s ) { int i, j; double extra_lim = s->activityInc / Vec_PtrSize(s->satCounterExamples); /* Remove any clause below this activity */ struct sim_result * cex; while (Vec_PtrSize(s->satCounterExamples) > (0.7 * MAX_LEARNTS)) { for (i = j = 0; i < Vec_PtrSize(s->satCounterExamples); i++) { cex = (struct sim_result *)Vec_PtrEntry(s->satCounterExamples, i); if (cex->activity < extra_lim) { ABC_FREE(cex->inVec); ABC_FREE(cex->outVec); ABC_FREE(cex); } else if (j < i) { Vec_PtrWriteEntry(s->satCounterExamples, j, cex); j++; } } //printf("Database size reduced from %d to %d\n", Vec_PtrSize(s->satCounterExamples), j); Vec_PtrShrink(s->satCounterExamples, j); extra_lim *= 2; } assert(Vec_PtrSize(s->satCounterExamples) <= (0.7 * MAX_LEARNTS)); } static struct sim_result * analyzeConflict( Abc_Ntk_t * pNtk, int * pModel, int fVerbose ) { Abc_Obj_t * pNode; int i, count = 0; int * pValues; struct sim_result * cex; int numouts = Abc_NtkPoNum(pNtk); int numins = Abc_NtkPiNum(pNtk); cex = ABC_ALLOC(struct sim_result, 1); cex->inVec = ints( numins ); cex->outVec = ints( numouts ); /* get the CO values under this model */ pValues = Abc_NtkVerifySimulatePattern( pNtk, pModel ); Abc_NtkForEachCi( pNtk, pNode, i ) cex->inVec[Abc_ObjId(pNode)-1] = pModel[i]; Abc_NtkForEachCo( pNtk, pNode, i ) { cex->outVec[Abc_ObjId(pNode)-numins-1] = pValues[i]; if (pValues[i]) count++; } cex->outVecOnes = count; cex->activity = 0; if (fVerbose) { Abc_NtkForEachCi( pNtk, pNode, i ) printf(" %s=%d", Abc_ObjName(pNode), pModel[i]); printf("\n"); } ABC_FREE( pValues ); return cex; } static int Abc_NtkCecSat_saucy( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel ) { extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor ); Abc_Ntk_t * pMiter; Abc_Ntk_t * pCnf; int RetValue; int nConfLimit; int nInsLimit; int i; nConfLimit = 10000; nInsLimit = 0; /* get the miter of the two networks */ pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); exit(1); } RetValue = Abc_NtkMiterIsConstant( pMiter ); if ( RetValue == 0 ) { //printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); /* report the error */ pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 ); for (i = 0; i < Abc_NtkPiNum(pNtk1); i++) pModel[i] = pMiter->pModel[i]; ABC_FREE( pMiter->pModel ); Abc_NtkDelete( pMiter ); return 0; } if ( RetValue == 1 ) { Abc_NtkDelete( pMiter ); //printf( "Networks are equivalent after structural hashing.\n" ); return 1; } /* convert the miter into a CNF */ pCnf = Abc_NtkMulti( pMiter, 0, 100, 1, 0, 0, 0 ); Abc_NtkDelete( pMiter ); if ( pCnf == NULL ) { printf( "Renoding for CNF has failed.\n" ); exit(1); } /* solve the CNF using the SAT solver */ RetValue = Abc_NtkMiterSat( pCnf, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, 0, NULL, NULL ); if ( RetValue == -1 ) { printf( "Networks are undecided (SAT solver timed out).\n" ); exit(1); } /*else if ( RetValue == 0 ) printf( "Networks are NOT EQUIVALENT after SAT.\n" ); else printf( "Networks are equivalent after SAT.\n" );*/ if ( pCnf->pModel ) { for (i = 0; i < Abc_NtkPiNum(pNtk1); i++) pModel[i] = pCnf->pModel[i]; } ABC_FREE( pCnf->pModel ); Abc_NtkDelete( pCnf ); return RetValue; } void saucyGateWay( Abc_Ntk_t * pNtkOrig, Abc_Obj_t * pNodePo, FILE * gFile, int fBooleanMatching, int fLookForSwaps, int fFixOutputs, int fFixInputs, int fQuiet, int fPrintTree ) { Abc_Ntk_t * pNtk; struct saucy *s; struct saucy_stats stats; int *colors; int i, clk = clock(); if (pNodePo == NULL) pNtk = Abc_NtkDup( pNtkOrig ); else pNtk = Abc_NtkCreateCone( pNtkOrig, Abc_ObjFanin0(pNodePo), Abc_ObjName(pNodePo), 0 ); if (Abc_NtkPiNum(pNtk) == 0) { Abc_Print( 0, "This output is not dependent on any input\n" ); Abc_NtkDelete( pNtk ); return; } s = saucy_alloc( pNtk ); /******* Getting Dependencies *******/ printf("Build functional dependency graph (dependency stats are below) ... "); getDependencies( pNtk, s->iDep, s->oDep ); printf("\t--------------------\n"); /************************************/ /* Finding toplogical orde */ s->topOrder = findTopologicalOrder( pNtk ); /* Setting graph colors: outputs = 0 and inputs = 1 */ colors = ints(Abc_NtkPoNum(pNtk) + Abc_NtkPiNum(pNtk)); if (fFixOutputs) { for (i = 0; i < Abc_NtkPoNum(pNtk); i++) colors[i] = i; } else { for (i = 0; i < Abc_NtkPoNum(pNtk); i++) colors[i] = 0; } if (fFixInputs) { int c = (fFixOutputs) ? Abc_NtkPoNum(pNtk) : 1; for (i = 0; i < Abc_NtkPiNum(pNtk); i++) colors[i+Abc_NtkPoNum(pNtk)] = c+i; } else { int c = (fFixOutputs) ? Abc_NtkPoNum(pNtk) : 1; for (i = 0; i < Abc_NtkPiNum(pNtk); i++) colors[i+Abc_NtkPoNum(pNtk)] = c; } /* Are we looking for Boolean matching? */ s->fBooleanMatching = fBooleanMatching; if (fBooleanMatching) { NUM_SIM1_ITERATION = 50; NUM_SIM2_ITERATION = 50; } else { NUM_SIM1_ITERATION = 200; NUM_SIM2_ITERATION = 200; } /* Set the print automorphism routine */ if (!fQuiet) s->print_automorphism = print_automorphism_ntk; else s->print_automorphism = print_automorphism_quiet; /* Set the output file for generators */ if (gFile == NULL) s->gFile = stdout; else s->gFile = gFile; /* Set print tree option */ s->fPrintTree = fPrintTree; /* Set input permutations option */ s->fLookForSwaps = fLookForSwaps; saucy_search(pNtk, s, 0, colors, &stats); print_stats(stdout, stats); if (fBooleanMatching) { if (stats.grpsize_base > 1 || stats.grpsize_exp > 0) printf("*** Networks are equivalent ***\n"); else printf("*** Networks are NOT equivalent ***\n"); } saucy_free(s); Abc_NtkDelete(pNtk); if (1) { FILE * hadi = fopen("hadi.txt", "a"); fprintf(hadi, "group size = %fe%d\n", stats.grpsize_base, stats.grpsize_exp); fclose(hadi); } ABC_PRT( "Runtime", clock() - clk ); }ABC_NAMESPACE_IMPL_END