From 60bb6dbf69efb5b1cb7253eff9e2a836bc21d5d0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Jul 2013 18:06:09 -0700 Subject: Adding commands 'bm2' and 'saucy3' developed by Hadi Katebi, Igor Markov, and Karem Sakallah at U Michigan. --- abclib.dsp | 4 + src/base/abci/abc.c | 267 ++++ src/base/abci/abcSaucy.c | 3346 +++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/module.make | 1 + 4 files changed, 3618 insertions(+) create mode 100644 src/base/abci/abcSaucy.c diff --git a/abclib.dsp b/abclib.dsp index a3228d4c..aac22ee4 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -439,6 +439,10 @@ SOURCE=.\src\base\abci\abcSat.c # End Source File # Begin Source File +SOURCE=.\src\base\abci\abcSaucy.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abci\abcScorr.c # End Source File # Begin Source File diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7012e7ba..b17acfea 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -299,6 +299,8 @@ static int Abc_CommandConstr ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandUnfold ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFold ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBm ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBm2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSaucy ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestCex ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPdr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -850,6 +852,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "unfold", Abc_CommandUnfold, 1 ); Cmd_CommandAdd( pAbc, "Verification", "fold", Abc_CommandFold, 1 ); Cmd_CommandAdd( pAbc, "Verification", "bm", Abc_CommandBm, 1 ); + Cmd_CommandAdd( pAbc, "Verification", "bm2", Abc_CommandBm2, 1 ); + Cmd_CommandAdd( pAbc, "Verification", "saucy3", Abc_CommandSaucy, 1 ); Cmd_CommandAdd( pAbc, "Verification", "testcex", Abc_CommandTestCex, 0 ); Cmd_CommandAdd( pAbc, "Verification", "pdr", Abc_CommandPdr, 0 ); Cmd_CommandAdd( pAbc, "Verification", "reconcile", Abc_CommandReconcile, 1 ); @@ -23091,6 +23095,269 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandBm2( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t *pNtk, *pNtk1, *pNtk2; + int fDelete1, fDelete2; + Abc_Obj_t * pObj; + char ** pArgvNew; + int c, nArgcNew, i; + + extern void saucyGateWay( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodePo, FILE * gFile, int fBooleanMatching, + int fLookForSwaps, int fFixOutputs, int fFixInputs, int fQuiet, int fPrintTree); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + Abc_Print( -2, "Unknown switch.\n"); + goto usage; + } + } + + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew , &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) + return 1; + + if( (unsigned)Abc_NtkPiNum(pNtk1) != (unsigned)Abc_NtkPiNum(pNtk2) || + (unsigned)Abc_NtkPoNum(pNtk1) != (unsigned)Abc_NtkPoNum(pNtk2) ) + { + Abc_Print( -2, "Mismatch in the number of inputs or outputs\n"); + Abc_Print( -2, "*** Networks are NOT equivalent ***\n"); + if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); + if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); + return 1; + } + + Abc_NtkPermute(pNtk2, 1, 1, 0 ); + Abc_NtkShortNames(pNtk2); + + Abc_NtkForEachCi( pNtk1, pObj, i ) { + char * newName = Abc_ObjNamePrefix( pObj, "N1:" ); + Nm_ManDeleteIdName( pNtk1->pManName, pObj->Id); + Abc_ObjAssignName( pObj, newName, NULL ); + } + Abc_NtkForEachCo( pNtk1, pObj, i ) { + char * newName = Abc_ObjNamePrefix( pObj, "N1:" ); + Nm_ManDeleteIdName( pNtk1->pManName, pObj->Id); + Abc_ObjAssignName( pObj, newName, NULL ); + } + + Abc_NtkForEachCi( pNtk2, pObj, i ) { + char * newName = Abc_ObjNamePrefix( pObj, "N2:" ); + Nm_ManDeleteIdName( pNtk2->pManName, pObj->Id); + Abc_ObjAssignName( pObj, newName, NULL ); + } + Abc_NtkForEachCo( pNtk2, pObj, i ) { + char * newName = Abc_ObjNamePrefix( pObj, "N2:" ); + Nm_ManDeleteIdName( pNtk2->pManName, pObj->Id); + Abc_ObjAssignName( pObj, newName, NULL ); + } + + Abc_NtkAppend( pNtk1, pNtk2, 1 ); + saucyGateWay( pNtk1, NULL, NULL, 1, 0, 0, 0, 0, 0); + + if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); + if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); + return 0; + +usage: + Abc_Print( -2, "usage: bm2 \n" ); + Abc_Print( -2, "\t performs Boolean matching (PP-equivalence)\n" ); + Abc_Print( -2, "\t for equivalent circuits, permutation that maps one circuit\n" ); + Abc_Print( -2, "\t to another is printed to standard output (PIs and POs of the\n" ); + Abc_Print( -2, "\t first network have prefix \"N1:\", while PIs and POs of the\n" ); + Abc_Print( -2, "\t second network have prefix \"N2:\")\n" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\tfile1 : the file with the first network\n"); + Abc_Print( -2, "\tfile2 : the file with the second network\n"); + + Abc_Print( -2, "\t \n" ); + Abc_Print( -2, "\t This command was contributed by Hadi Katebi from U Michigan.\n" ); + Abc_Print( -2, "\t The paper describing the method: H. Katebi, K. Sakallah and\n"); + Abc_Print( -2, "\t I. L. Markov.\n" ); + Abc_Print( -2, "\t \"Generalized Boolean Symmetries Through Nested Partition\n"); + Abc_Print( -2, "\t Refinement\". Proc. ICCAD 2013. \n" ); + //Abc_Print( -2, "\t http://www.eecs.umich.edu/~imarkov/pubs/conf/date10-match.pdf\n" ); + Abc_Print( -2, "\t \n" ); + + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandSaucy( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t *pNtk; + char * outputName = NULL; + FILE * gFile = NULL; + int fOutputsOneAtTime = 0; + int fFixOutputs = 0; + int fFixInputs = 0; + int fLookForSwaps = 0; + int fQuiet = 0; + int fPrintTree = 0; + int c; + + extern void saucyGateWay( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodePo, FILE * gFile, int fBooleanMatching, + int fLookForSwaps, int fFixOutputs, int fFixInputs, int fQuiet, int fPrintTree); + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "OFiosqvh" ) ) != EOF ) + { + switch ( c ) + { + case 'O': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-O\" should be followed by an output name or the keyword all.\n" ); + goto usage; + } + outputName = argv[globalUtilOptind]; + if ( !strcmp(argv[globalUtilOptind], "all") ) + fOutputsOneAtTime ^= 1; + globalUtilOptind++; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" ); + goto usage; + } + if ( (gFile = fopen( argv[globalUtilOptind], "w" )) == NULL ) + { + Abc_Print( -1, "Cannot create output file \"%s\". ", argv[globalUtilOptind] ); + return 1; + } + globalUtilOptind++; + break; + case 'i': + fFixOutputs ^= 1; + break; + case 'o': + fFixInputs ^= 1; + break; + case 's': + fLookForSwaps ^= 1; + break; + case 'q': + fQuiet ^= 1; + break; + case 'v': + fPrintTree ^= 1; + break; + case 'h': + goto usage; + default: + Abc_Print( -2, "Unknown switch.\n"); + goto usage; + } + } + + pNtk = Abc_FrameReadNtk(pAbc); + + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -1, "This command works only for AIGs (run \"strash\").\n" ); + return 1; + } + + pNtk = Abc_NtkDup( pNtk ); + Abc_NtkOrderObjsByName( pNtk, 1 ); + + if (fOutputsOneAtTime) { + int i; + Abc_Obj_t * pNodePo; + FILE * hadi = fopen("hadi.txt", "w"); + Abc_NtkForEachPo( pNtk, pNodePo, i ) { + printf("Ouput %s\n\n", Abc_ObjName(pNodePo)); + saucyGateWay( pNtk, pNodePo, gFile, 0, fLookForSwaps, fFixOutputs, fFixInputs, fQuiet, fPrintTree ); + printf("----------------------------------------\n"); + } + fclose(hadi); + } else if (outputName != NULL) { + int i; + Abc_Obj_t * pNodePo; + Abc_NtkForEachPo( pNtk, pNodePo, i ) { + if (!strcmp(Abc_ObjName(pNodePo), outputName)) { + saucyGateWay( pNtk, pNodePo, gFile, 0, fLookForSwaps, fFixOutputs, fFixInputs, fQuiet, fPrintTree ); + Abc_NtkDelete( pNtk ); + return 0; + } + } + Abc_Print( -1, "Output not found\n" ); + return 1; + } else + saucyGateWay( pNtk, NULL, gFile, 0, fLookForSwaps, fFixOutputs, fFixInputs, fQuiet, fPrintTree ); + + if (gFile != NULL) fclose(gFile); + Abc_NtkDelete( pNtk ); + return 0; + +usage: + Abc_Print( -2, "usage: saucy3 [-O ] [-F ] [-iosqvh]\n\n" ); + Abc_Print( -2, "\t computes functional symmetries of the netowrk\n" ); + Abc_Print( -2, "\t prints symmetry generators to the standard output\n" ); + Abc_Print( -2, "\t-O : (optional) compute symmetries only for output given by name\n"); + Abc_Print( -2, "\t only inputs in the output cone are permuted\n"); + Abc_Print( -2, "\t (special case) name=all, compute symmetries for each\n" ); + Abc_Print( -2, "\t output, but only one output at a time\n" ); + Abc_Print( -2, "\t [default = compute symmetries by permuting all I/Os]\n" ); + Abc_Print( -2, "\t-F : print symmetry generators to file [default = stdout]\n"); + Abc_Print( -2, "\t-i : permute just the inputs (fix the outputs) [default = no]\n"); + Abc_Print( -2, "\t-o : permute just the outputs (fix the inputs) [default = no]\n"); + Abc_Print( -2, "\t-s : only look for swaps of inputs [default = no]\n"); + Abc_Print( -2, "\t-q : quiet (do not print symmetry generators) [default = no]\n"); + Abc_Print( -2, "\t-v : verbose (print the search tree) [default = no]\n"); + Abc_Print( -2, "\t-h : print the command usage\n"); + + Abc_Print( -2, "\t \n" ); + Abc_Print( -2, "\t This command was contributed by Hadi Katebi from U Michigan." ); + Abc_Print( -2, "\t The paper describing the method: H. Katebi, K. Sakallah and\n"); + Abc_Print( -2, "\t I. L. Markov.\n" ); + Abc_Print( -2, "\t \"Generalized Boolean Symmetries Through Nested Partition\n"); + Abc_Print( -2, "\t Refinement\". Proc. ICCAD 2013. \n" ); + //Abc_Print( -2, "\t http://www.eecs.umich.edu/~imarkov/pubs/conf/date10-match.pdf\n" ); + Abc_Print( -2, "\t Saucy webpage: http://vlsicad.eecs.umich.edu/BK/SAUCY/\n" ); + + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcSaucy.c b/src/base/abci/abcSaucy.c new file mode 100644 index 00000000..b67dbcbb --- /dev/null +++ b/src/base/abci/abcSaucy.c @@ -0,0 +1,3346 @@ +/**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 + +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); +int Abc_NtkCecSat_saucy(Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel); +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); + + +/* + * 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 +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 = 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 = Vec_PtrEntry(s->satCounterExamples, i); + + for (j = 0; j < Vec_PtrSize(s->satCounterExamples); j++) { + if (flag[j]) continue; + + cex2 = 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_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_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_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_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 = Vec_PtrEntry(s->pNtk->vPos, i); + pObjPerm = Vec_PtrEntry(s->pNtk_permuted->vPos, s->gamma[i]); + } + else { + pObj = Vec_PtrEntry(s->pNtk->vPis, i - numouts); + pObjPerm = 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 = Vec_PtrEntry(s->pNtk->vPos, s->gamma[i]); + pObjPerm = Vec_PtrEntry(s->pNtk_permuted->vPos, i); + } + else { + pObj = Vec_PtrEntry(s->pNtk->vPis, s->gamma[i] - numouts); + pObjPerm = 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_PtrEntry(s->randomVectorArray_sim1, i)); + for (i = 0; i < Vec_PtrSize(s->randomVectorArray_sim2); i++) + Vec_IntFree(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 = 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 = Vec_PtrEntry(pNtk->vPos, v); + else + pObj = 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 = 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 = 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 + + diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 5554ea93..8d97c6cf 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -58,6 +58,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcRpo.c \ src/base/abci/abcRr.c \ src/base/abci/abcSat.c \ + src/base/abci/abcSaucy.c \ src/base/abci/abcScorr.c \ src/base/abci/abcSense.c \ src/base/abci/abcSpeedup.c \ -- cgit v1.2.3