Adding commands 'bm2' and 'saucy3' developed by Hadi Katebi, Igor Markov, and…

Adding commands 'bm2' and 'saucy3' developed by Hadi Katebi, Igor Markov, and Karem Sakallah at U Michigan.

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

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 );
@@ -23096,6 +23100,269 @@ usage:
   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  <file1> <file2>\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 <name>] [-F <file>] [-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 <name> : (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 <file> : 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    []
+
+  Description []
 
   SideEffects []
 

src/base/abci/abcSaucy.c

+/**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 <pdarga@umich.edu>
+ * and Mark Liffiton <liffiton@umich.edu>
+ * and Hadi Katebi <hadik@eecs.umich.edu>
+ * 
+ * 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
+
+

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 \