Version abc61122

1 files changed, 2704 insertions, 0 deletions

diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
new file mode 100644
index 00000000..269ca257
--- /dev/null
+++ b/src/aig/ivy/ivyFraig.c
@@ -0,0 +1,2704 @@
+/**CFile****************************************************************
+
+  FileName    [ivyFraig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Functional reduction of AIGs]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyFraig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "satSolver.h"
+#include "extra.h"
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ivy_FraigMan_t_        Ivy_FraigMan_t;
+typedef struct Ivy_FraigSim_t_        Ivy_FraigSim_t;
+typedef struct Ivy_FraigList_t_       Ivy_FraigList_t;
+
+struct Ivy_FraigList_t_
+{
+    Ivy_Obj_t *         pHead;
+    Ivy_Obj_t *         pTail;
+    int                 nItems;
+};
+
+struct Ivy_FraigSim_t_
+{
+    int                 Type;
+    Ivy_FraigSim_t *    pNext;
+    Ivy_FraigSim_t *    pFanin0;
+    Ivy_FraigSim_t *    pFanin1;
+    unsigned            pData[0];
+};
+
+struct Ivy_FraigMan_t_
+{
+    // general info 
+    Ivy_FraigParams_t * pParams;        // various parameters
+    // temporary backtrack limits because "sint64" cannot be defined in Ivy_FraigParams_t ...
+    sint64              nBTLimitGlobal; // global limit on the number of backtracks
+    sint64              nInsLimitGlobal;// global limit on the number of clause inspects
+    // AIG manager
+    Ivy_Man_t *         pManAig;        // the starting AIG manager
+    Ivy_Man_t *         pManFraig;      // the final AIG manager
+    // simulation information
+    int                 nSimWords;      // the number of words
+    char *              pSimWords;      // the simulation info
+    Ivy_FraigSim_t *    pSimStart;      // the list of simulation info for internal nodes
+    // counter example storage
+    int                 nPatWords;      // the number of words in the counter example
+    unsigned *          pPatWords;      // the counter example
+    int *               pPatScores;     // the scores of each pattern
+    // equivalence classes 
+    Ivy_FraigList_t     lClasses;       // equivalence classes
+    Ivy_FraigList_t     lCand;          // candidatates
+    int                 nPairs;         // the number of pairs of nodes
+    // equivalence checking
+    sat_solver *        pSat;           // SAT solver
+    int                 nSatVars;       // the number of variables currently used
+    Vec_Ptr_t *         vPiVars;        // the PIs of the cone used 
+    // other 
+    ProgressBar *       pProgress;
+    // statistics
+    int                 nSimRounds;
+    int                 nNodesMiter;
+    int                 nClassesZero;
+    int                 nClassesBeg;
+    int                 nClassesEnd;
+    int                 nPairsBeg;
+    int                 nPairsEnd;
+    int                 nSatCalls;
+    int                 nSatCallsSat;
+    int                 nSatCallsUnsat;
+    int                 nSatProof;
+    int                 nSatFails;
+    int                 nSatFailsReal;
+    // runtime
+    int                 timeSim;
+    int                 timeTrav;
+    int                 timeSat;
+    int                 timeSatUnsat;
+    int                 timeSatSat;
+    int                 timeSatFail;
+    int                 timeRef;
+    int                 timeTotal;
+    int                 time1;
+    int                 time2;
+};
+
+typedef struct Prove_ParamsStruct_t_      Prove_Params_t;
+struct Prove_ParamsStruct_t_
+{
+    // general parameters
+    int     fUseFraiging;          // enables fraiging
+    int     fUseRewriting;         // enables rewriting
+    int     fUseBdds;              // enables BDD construction when other methods fail
+    int     fVerbose;              // prints verbose stats
+    // iterations
+    int     nItersMax;             // the number of iterations
+    // mitering 
+    int     nMiteringLimitStart;   // starting mitering limit
+    float   nMiteringLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
+    // rewriting 
+    int     nRewritingLimitStart;  // the number of rewriting iterations
+    float   nRewritingLimitMulti;  // multiplicative coefficient to increase the limit in each iteration
+    // fraiging 
+    int     nFraigingLimitStart;   // starting backtrack(conflict) limit
+    float   nFraigingLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
+    // last-gasp BDD construction
+    int     nBddSizeLimit;         // the number of BDD nodes when construction is aborted
+    int     fBddReorder;           // enables dynamic BDD variable reordering
+    // last-gasp mitering
+    int     nMiteringLimitLast;    // final mitering limit
+    // global SAT solver limits
+    sint64  nTotalBacktrackLimit;  // global limit on the number of backtracks
+    sint64  nTotalInspectLimit;    // global limit on the number of clause inspects
+    // global resources applied
+    sint64  nTotalBacktracksMade;  // the total number of backtracks made
+    sint64  nTotalInspectsMade;    // the total number of inspects made
+};
+
+static inline Ivy_FraigSim_t * Ivy_ObjSim( Ivy_Obj_t * pObj )                            { return (Ivy_FraigSim_t *)pObj->pFanout;  }
+static inline Ivy_Obj_t * Ivy_ObjClassNodeLast( Ivy_Obj_t * pObj )                       { return pObj->pNextFan0;  }
+static inline Ivy_Obj_t * Ivy_ObjClassNodeRepr( Ivy_Obj_t * pObj )                       { return pObj->pNextFan0;  }
+static inline Ivy_Obj_t * Ivy_ObjClassNodeNext( Ivy_Obj_t * pObj )                       { return pObj->pNextFan1;  }
+static inline Ivy_Obj_t * Ivy_ObjNodeHashNext( Ivy_Obj_t * pObj )                        { return pObj->pPrevFan0;  }
+static inline Ivy_Obj_t * Ivy_ObjEquivListNext( Ivy_Obj_t * pObj )                       { return pObj->pPrevFan0;  }
+static inline Ivy_Obj_t * Ivy_ObjEquivListPrev( Ivy_Obj_t * pObj )                       { return pObj->pPrevFan1;  }
+static inline Ivy_Obj_t * Ivy_ObjFraig( Ivy_Obj_t * pObj )                               { return pObj->pEquiv;     }
+static inline int         Ivy_ObjSatNum( Ivy_Obj_t * pObj )                              { return (int)pObj->pNextFan0;         }
+static inline Vec_Ptr_t * Ivy_ObjFaninVec( Ivy_Obj_t * pObj )                            { return (Vec_Ptr_t *)pObj->pNextFan1; }
+
+static inline void        Ivy_ObjSetSim( Ivy_Obj_t * pObj, Ivy_FraigSim_t * pSim )       { pObj->pFanout = (Ivy_Obj_t *)pSim; }
+static inline void        Ivy_ObjSetClassNodeLast( Ivy_Obj_t * pObj, Ivy_Obj_t * pLast ) { pObj->pNextFan0 = pLast; }
+static inline void        Ivy_ObjSetClassNodeRepr( Ivy_Obj_t * pObj, Ivy_Obj_t * pRepr ) { pObj->pNextFan0 = pRepr; }
+static inline void        Ivy_ObjSetClassNodeNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pNextFan1 = pNext; }
+static inline void        Ivy_ObjSetNodeHashNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext )  { pObj->pPrevFan0 = pNext; }
+static inline void        Ivy_ObjSetEquivListNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; }
+static inline void        Ivy_ObjSetEquivListPrev( Ivy_Obj_t * pObj, Ivy_Obj_t * pPrev ) { pObj->pPrevFan1 = pPrev; }
+static inline void        Ivy_ObjSetFraig( Ivy_Obj_t * pObj, Ivy_Obj_t * pNode )         { pObj->pEquiv    = pNode; }
+static inline void        Ivy_ObjSetSatNum( Ivy_Obj_t * pObj, int Num )                  { pObj->pNextFan0 = (Ivy_Obj_t *)Num;     }
+static inline void        Ivy_ObjSetFaninVec( Ivy_Obj_t * pObj, Vec_Ptr_t * vFanins )    { pObj->pNextFan1 = (Ivy_Obj_t *)vFanins; }
+
+static inline unsigned    Ivy_ObjRandomSim()                       { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
+
+// iterate through equivalence classes
+#define Ivy_FraigForEachEquivClass( pList, pEnt )                 \
+    for ( pEnt = pList;                                           \
+          pEnt;                                                   \
+          pEnt = Ivy_ObjEquivListNext(pEnt) )
+#define Ivy_FraigForEachEquivClassSafe( pList, pEnt, pEnt2 )      \
+    for ( pEnt = pList,                                           \
+          pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL;         \
+          pEnt;                                                   \
+          pEnt = pEnt2,                                           \
+          pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL )
+// iterate through nodes in one class
+#define Ivy_FraigForEachClassNode( pClass, pEnt )                 \
+    for ( pEnt = pClass;                                          \
+          pEnt;                                                   \
+          pEnt = Ivy_ObjClassNodeNext(pEnt) )
+// iterate through nodes in the hash table
+#define Ivy_FraigForEachBinNode( pBin, pEnt )                     \
+    for ( pEnt = pBin;                                            \
+          pEnt;                                                   \
+          pEnt = Ivy_ObjNodeHashNext(pEnt) )
+
+static Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+static Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+static Ivy_Man_t *   Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, sint64 nBTLimitGlobal, sint64 nInsLimitGlobal, sint64 * pnSatConfs, sint64 * pnSatInspects );
+static void          Ivy_FraigPrint( Ivy_FraigMan_t * p );
+static void          Ivy_FraigStop( Ivy_FraigMan_t * p );
+static void          Ivy_FraigSimulate( Ivy_FraigMan_t * p );
+static void          Ivy_FraigSweep( Ivy_FraigMan_t * p );
+static Ivy_Obj_t *   Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld );
+static int           Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
+static int           Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj );
+static void          Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
+static int           Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew );
+static void          Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew );
+static int           Ivy_FraigMiterStatus( Ivy_Man_t * pMan );
+static void          Ivy_FraigMiterProve( Ivy_FraigMan_t * p );
+static void          Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose );
+static int *         Ivy_FraigCreateModel( Ivy_FraigMan_t * p );
+
+static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 );
+
+static sint64 s_nBTLimitGlobal = 0;
+static sint64 s_nInsLimitGlobal = 0;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the default solving parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams )
+{
+    memset( pParams, 0, sizeof(Ivy_FraigParams_t) );
+    pParams->nSimWords        =      32;  // the number of words in the simulation info
+    pParams->dSimSatur        =   0.005;  // the ratio of refined classes when saturation is reached
+    pParams->fPatScores       =       0;  // enables simulation pattern scoring
+    pParams->MaxScore         =      25;  // max score after which resimulation is used
+    pParams->fDoSparse        =       1;  // skips sparse functions
+//    pParams->dActConeRatio    =    0.05;  // the ratio of cone to be bumped
+//    pParams->dActConeBumpMax  =     5.0;  // the largest bump of activity
+    pParams->dActConeRatio    =     0.3;  // the ratio of cone to be bumped
+    pParams->dActConeBumpMax  =    10.0;  // the largest bump of activity
+
+    pParams->nBTLimitNode     =     100;  // conflict limit at a node
+    pParams->nBTLimitMiter    =  500000;  // conflict limit at an output
+//    pParams->nBTLimitGlobal   =       0;  // conflict limit global
+//    pParams->nInsLimitGlobal  =       0;  // inspection limit global
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs combinational equivalence checking for the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
+{
+    Prove_Params_t * pParams = pPars;
+    Ivy_FraigParams_t Params, * pIvyParams = &Params; 
+    Ivy_Man_t * pManAig, * pManTemp;
+    int RetValue, nIter, Counter, clk, timeStart = clock();
+    sint64 nSatConfs, nSatInspects;
+
+    // start the network and parameters
+    pManAig = *ppManAig;
+    Ivy_FraigParamsDefault( pIvyParams );
+    pIvyParams->fVerbose = pParams->fVerbose;
+    pIvyParams->fProve = 1;
+
+    if ( pParams->fVerbose )
+    {
+        printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
+            pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
+        printf( "Mitering = %d (%3.1f).  Rewriting = %d (%3.1f).  Fraiging = %d (%3.1f).\n", 
+            pParams->nMiteringLimitStart,  pParams->nMiteringLimitMulti, 
+            pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
+            pParams->nFraigingLimitStart,  pParams->nFraigingLimitMulti );
+        printf( "Mitering last = %d.\n", 
+            pParams->nMiteringLimitLast );
+    }
+
+    // if SAT only, solve without iteration
+    if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
+    {
+        clk = clock();
+        pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
+        pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
+        RetValue = Ivy_FraigMiterStatus( pManAig );
+        Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
+        *ppManAig = pManAig;
+        return RetValue;
+    }
+
+    if ( Ivy_ManNodeNum(pManAig) < 500 )
+    {
+        // run the first mitering
+        clk = clock();
+        pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig);
+        pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
+        RetValue = Ivy_FraigMiterStatus( pManAig );
+        Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
+        if ( RetValue >= 0 )
+        {
+            *ppManAig = pManAig;
+            return RetValue;
+        }
+    }
+
+    // check the current resource limits
+    RetValue = -1;
+    for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
+    {
+        if ( pParams->fVerbose )
+        {
+            printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, 
+                 (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 
+                 (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
+            fflush( stdout );
+        }
+
+        // try rewriting
+        if ( pParams->fUseRewriting )
+        {
+            clk = clock();
+            Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
+            pManAig = Ivy_ManRwsat( pManAig, 0 );  
+            RetValue = Ivy_FraigMiterStatus( pManAig );
+            Ivy_FraigMiterPrint( pManAig, "Rewriting  ", clk, pParams->fVerbose );
+        }
+        if ( RetValue >= 0 )
+            break;
+
+        // try fraiging followed by mitering
+        if ( pParams->fUseFraiging )
+        {
+            clk = clock();
+            pIvyParams->nBTLimitNode  = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter));
+            pIvyParams->nBTLimitMiter = (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig);
+            pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects );  Ivy_ManStop( pManTemp );
+            RetValue = Ivy_FraigMiterStatus( pManAig );
+            Ivy_FraigMiterPrint( pManAig, "Fraiging   ", clk, pParams->fVerbose );
+        }
+        if ( RetValue >= 0 )
+            break;
+
+        // add to the number of backtracks and inspects
+        pParams->nTotalBacktracksMade += nSatConfs;
+        pParams->nTotalInspectsMade   += nSatInspects;
+        // check if global resource limit is reached
+        if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
+             (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
+        {
+            printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
+            *ppManAig = pManAig;
+            return -1;
+        }
+    }    
+
+    if ( RetValue < 0 )
+    {
+        if ( pParams->fVerbose )
+        {
+            printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
+            fflush( stdout );
+        }
+        clk = clock();
+        pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
+        if ( pParams->nTotalBacktrackLimit )
+            s_nBTLimitGlobal  = pParams->nTotalBacktrackLimit - pParams->nTotalBacktracksMade;
+        if ( pParams->nTotalInspectLimit )
+            s_nInsLimitGlobal = pParams->nTotalInspectLimit -   pParams->nTotalInspectsMade;        
+        pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
+        s_nBTLimitGlobal  = 0;
+        s_nInsLimitGlobal = 0;        
+        RetValue = Ivy_FraigMiterStatus( pManAig );
+        Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
+    }
+
+    // assign the model if it was proved by rewriting (const 1 miter)
+    if ( RetValue == 0 && pManAig->pData == NULL )
+    {
+        pManAig->pData = ALLOC( int, Ivy_ManPiNum(pManAig) );
+        memset( pManAig->pData, 0, sizeof(int) * Ivy_ManPiNum(pManAig) );
+    }
+    *ppManAig = pManAig;
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, sint64 nBTLimitGlobal, sint64 nInsLimitGlobal, sint64 * pnSatConfs, sint64 * pnSatInspects )
+{ 
+    Ivy_FraigMan_t * p;
+    Ivy_Man_t * pManAigNew;
+    int clk;
+    if ( Ivy_ManNodeNum(pManAig) == 0 )
+        return Ivy_ManDup(pManAig);
+clk = clock();
+    assert( Ivy_ManLatchNum(pManAig) == 0 );
+    p = Ivy_FraigStart( pManAig, pParams );
+    // set global limits
+    p->nBTLimitGlobal  = nBTLimitGlobal;
+    p->nInsLimitGlobal = nInsLimitGlobal; 
+    
+    Ivy_FraigSimulate( p );
+    Ivy_FraigSweep( p );
+    pManAigNew = p->pManFraig;
+p->timeTotal = clock() - clk;
+    if ( pnSatConfs )
+        *pnSatConfs = p->pSat? p->pSat->stats.conflicts : 0;
+    if ( pnSatInspects )
+        *pnSatInspects = p->pSat? p->pSat->stats.inspects : 0;
+    Ivy_FraigStop( p );
+    return pManAigNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+    Ivy_FraigMan_t * p;
+    Ivy_Man_t * pManAigNew;
+    int clk;
+    if ( Ivy_ManNodeNum(pManAig) == 0 )
+        return Ivy_ManDup(pManAig);
+clk = clock();
+    assert( Ivy_ManLatchNum(pManAig) == 0 );
+    p = Ivy_FraigStart( pManAig, pParams );
+    Ivy_FraigSimulate( p );
+    Ivy_FraigSweep( p );
+    pManAigNew = p->pManFraig;
+p->timeTotal = clock() - clk;
+    Ivy_FraigStop( p );
+    return pManAigNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Applies brute-force SAT to the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+    Ivy_FraigMan_t * p;
+    Ivy_Man_t * pManAigNew;
+    Ivy_Obj_t * pObj;
+    int i, clk;
+clk = clock();
+    assert( Ivy_ManLatchNum(pManAig) == 0 );
+    p = Ivy_FraigStartSimple( pManAig, pParams );
+    // set global limits
+    p->nBTLimitGlobal  = s_nBTLimitGlobal;
+    p->nInsLimitGlobal = s_nInsLimitGlobal; 
+    // duplicate internal nodes
+    Ivy_ManForEachNode( p->pManAig, pObj, i )
+        pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+    // try to prove each output of the miter
+    Ivy_FraigMiterProve( p );
+    // add the POs
+    Ivy_ManForEachPo( p->pManAig, pObj, i )
+        Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
+    // clean the new manager
+    Ivy_ManForEachObj( p->pManFraig, pObj, i )
+    {
+        if ( Ivy_ObjFaninVec(pObj) )
+            Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
+        pObj->pNextFan0 = pObj->pNextFan1 = NULL;
+    }
+    // remove dangling nodes 
+    Ivy_ManCleanup( p->pManFraig );
+    pManAigNew = p->pManFraig;
+p->timeTotal = clock() - clk;
+
+//printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) );
+//PRT( "Time", p->timeTotal );
+    Ivy_FraigStop( p );
+    return pManAigNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the fraiging manager without simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+    Ivy_FraigMan_t * p;
+    // allocat the fraiging manager
+    p = ALLOC( Ivy_FraigMan_t, 1 );
+    memset( p, 0, sizeof(Ivy_FraigMan_t) );
+    p->pParams   = pParams;
+    p->pManAig   = pManAig;
+    p->pManFraig = Ivy_ManStartFrom( pManAig );
+    p->vPiVars   = Vec_PtrAlloc( 100 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+    Ivy_FraigMan_t * p;
+    Ivy_FraigSim_t * pSims;
+    Ivy_Obj_t * pObj;
+    int i, k, EntrySize;
+    // clean the fanout representation
+    Ivy_ManForEachObj( pManAig, pObj, i )
+//        pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
+        assert( !pObj->pEquiv && !pObj->pFanout );
+    // allocat the fraiging manager
+    p = ALLOC( Ivy_FraigMan_t, 1 );
+    memset( p, 0, sizeof(Ivy_FraigMan_t) );
+    p->pParams   = pParams;
+    p->pManAig   = pManAig;
+    p->pManFraig = Ivy_ManStartFrom( pManAig );
+    // allocate simulation info
+    p->nSimWords    = pParams->nSimWords;
+//    p->pSimWords    = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nSimWords ); 
+    EntrySize    = sizeof(Ivy_FraigSim_t) + sizeof(unsigned) * p->nSimWords;
+    p->pSimWords = (char *)malloc( Ivy_ManObjNum(pManAig) * EntrySize ); 
+    memset( p->pSimWords, 0, EntrySize );
+    k = 0;
+    Ivy_ManForEachObj( pManAig, pObj, i )
+    {
+        pSims = (Ivy_FraigSim_t *)(p->pSimWords + EntrySize * k++);
+        pSims->pNext = NULL;
+        if ( Ivy_ObjIsNode(pObj) )
+        {
+            if ( p->pSimStart == NULL )
+                p->pSimStart = pSims;
+            else
+                ((Ivy_FraigSim_t *)(p->pSimWords + EntrySize * (k-2)))->pNext = pSims;
+            pSims->pFanin0 = Ivy_ObjSim( Ivy_ObjFanin0(pObj) );
+            pSims->pFanin1 = Ivy_ObjSim( Ivy_ObjFanin1(pObj) );
+            pSims->Type = (Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) << 2) | (Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)) << 1) | pObj->fPhase;
+        }
+        else
+        {
+            pSims->pFanin0 = NULL;
+            pSims->pFanin1 = NULL;
+            pSims->Type = 0;
+        }
+        Ivy_ObjSetSim( pObj, pSims );
+    }
+    assert( k == Ivy_ManObjNum(pManAig) );
+    // allocate storage for sim pattern
+    p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
+    p->pPatWords = ALLOC( unsigned, p->nPatWords ); 
+    p->pPatScores = ALLOC( int, 32 * p->nSimWords ); 
+    p->vPiVars   = Vec_PtrAlloc( 100 );
+    // set random number generator
+    srand( 0xABCABC );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigStop( Ivy_FraigMan_t * p )
+{
+    if ( p->pParams->fVerbose )
+        Ivy_FraigPrint( p );
+    if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
+    if ( p->pSat ) sat_solver_delete( p->pSat );
+    FREE( p->pPatScores );
+    FREE( p->pPatWords );
+    FREE( p->pSimWords );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats for the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigPrint( Ivy_FraigMan_t * p )
+{
+    double nMemory;
+    nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nSimWords*sizeof(unsigned)/(1<<20);
+    printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb.  ", p->nSimWords, p->nSimRounds, nMemory );
+    printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
+    printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pParams->nBTLimitNode, p->pParams->nBTLimitMiter );
+    printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
+        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
+    printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", 
+        Ivy_ManNodeNum(p->pManFraig), p->nNodesMiter, Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
+    if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
+    PRT( "AIG simulation  ", p->timeSim  );
+    PRT( "AIG traversal   ", p->timeTrav  );
+    PRT( "SAT solving     ", p->timeSat   );
+    PRT( "    Unsat       ", p->timeSatUnsat );
+    PRT( "    Sat         ", p->timeSatSat   );
+    PRT( "    Fail        ", p->timeSatFail  );
+    PRT( "Class refining  ", p->timeRef   );
+    PRT( "TOTAL RUNTIME   ", p->timeTotal );
+    if ( p->time1 ) { PRT( "time1           ", p->time1 ); }
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns random patterns to the PI node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeAssignRandom( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+    Ivy_FraigSim_t * pSims;
+    int i;
+    assert( Ivy_ObjIsPi(pObj) );
+    pSims = Ivy_ObjSim(pObj);
+    for ( i = 0; i < p->nSimWords; i++ )
+        pSims->pData[i] = Ivy_ObjRandomSim();
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns constant patterns to the PI node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeAssignConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int fConst1 )
+{
+    Ivy_FraigSim_t * pSims;
+    int i;
+    assert( Ivy_ObjIsPi(pObj) );
+    pSims = Ivy_ObjSim(pObj);
+    for ( i = 0; i < p->nSimWords; i++ )
+        pSims->pData[i] = fConst1? ~(unsigned)0 : 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assings random simulation info for the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigAssignRandom( Ivy_FraigMan_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    Ivy_ManForEachPi( p->pManAig, pObj, i )
+        Ivy_NodeAssignRandom( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assings distance-1 simulation info for the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigAssignDist1( Ivy_FraigMan_t * p, unsigned * pPat )
+{
+    Ivy_Obj_t * pObj;
+    int i, Limit;
+    Ivy_ManForEachPi( p->pManAig, pObj, i )
+        Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) );
+    Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
+    for ( i = 0; i < Limit; i++ )
+        Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeHasZeroSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+    Ivy_FraigSim_t * pSims;
+    int i;
+    pSims = Ivy_ObjSim(pObj);
+    for ( i = 0; i < p->nSimWords; i++ )
+        if ( pSims->pData[i] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if simulation infos are equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeCompareSims( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
+{
+    Ivy_FraigSim_t * pSims0, * pSims1;
+    int i;
+    pSims0 = Ivy_ObjSim(pObj0);
+    pSims1 = Ivy_ObjSim(pObj1);
+    for ( i = 0; i < p->nSimWords; i++ )
+        if ( pSims0->pData[i] != pSims1->pData[i] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeSimulateSim( Ivy_FraigMan_t * p, Ivy_FraigSim_t * pSims )
+{
+    unsigned * pData, * pData0, * pData1;
+    int i;
+    pData  = pSims->pData;
+    pData0 = pSims->pFanin0->pData;
+    pData1 = pSims->pFanin1->pData;
+    switch( pSims->Type )
+    {
+    case 0:
+        for ( i = 0; i < p->nSimWords; i++ )
+            pData[i] = (pData0[i] & pData1[i]);
+        break;
+    case 1:
+        for ( i = 0; i < p->nSimWords; i++ )
+            pData[i] = ~(pData0[i] & pData1[i]);
+        break;
+    case 2:
+        for ( i = 0; i < p->nSimWords; i++ )
+            pData[i] = (pData0[i] & ~pData1[i]);
+        break;
+    case 3:
+        for ( i = 0; i < p->nSimWords; i++ )
+            pData[i] = (~pData0[i] | pData1[i]);
+        break;
+    case 4:
+        for ( i = 0; i < p->nSimWords; i++ )
+            pData[i] = (~pData0[i] & pData1[i]);
+        break;
+    case 5:
+        for ( i = 0; i < p->nSimWords; i++ )
+            pData[i] = (pData0[i] | ~pData1[i]);
+        break;
+    case 6:
+        for ( i = 0; i < p->nSimWords; i++ )
+            pData[i] = ~(pData0[i] | pData1[i]);
+        break;
+    case 7:
+        for ( i = 0; i < p->nSimWords; i++ )
+            pData[i] = (pData0[i] | pData1[i]);
+        break;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeSimulate( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+    Ivy_FraigSim_t * pSims, * pSims0, * pSims1;
+    int fCompl, fCompl0, fCompl1, i;
+    assert( !Ivy_IsComplement(pObj) );
+    // get hold of the simulation information
+    pSims  = Ivy_ObjSim(pObj);
+    pSims0 = Ivy_ObjSim(Ivy_ObjFanin0(pObj));
+    pSims1 = Ivy_ObjSim(Ivy_ObjFanin1(pObj));
+    // get complemented attributes of the children using their random info
+    fCompl  = pObj->fPhase;
+    fCompl0 = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj));
+    fCompl1 = Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj));
+    // simulate
+    if ( fCompl0 && fCompl1 )
+    {
+        if ( fCompl )
+            for ( i = 0; i < p->nSimWords; i++ )
+                pSims->pData[i] = (pSims0->pData[i] | pSims1->pData[i]);
+        else
+            for ( i = 0; i < p->nSimWords; i++ )
+                pSims->pData[i] = ~(pSims0->pData[i] | pSims1->pData[i]);
+    }
+    else if ( fCompl0 && !fCompl1 )
+    {
+        if ( fCompl )
+            for ( i = 0; i < p->nSimWords; i++ )
+                pSims->pData[i] = (pSims0->pData[i] | ~pSims1->pData[i]);
+        else
+            for ( i = 0; i < p->nSimWords; i++ )
+                pSims->pData[i] = (~pSims0->pData[i] & pSims1->pData[i]);
+    }
+    else if ( !fCompl0 && fCompl1 )
+    {
+        if ( fCompl )
+            for ( i = 0; i < p->nSimWords; i++ )
+                pSims->pData[i] = (~pSims0->pData[i] | pSims1->pData[i]);
+        else
+            for ( i = 0; i < p->nSimWords; i++ )
+                pSims->pData[i] = (pSims0->pData[i] & ~pSims1->pData[i]);
+    }
+    else // if ( !fCompl0 && !fCompl1 )
+    {
+        if ( fCompl )
+            for ( i = 0; i < p->nSimWords; i++ )
+                pSims->pData[i] = ~(pSims0->pData[i] & pSims1->pData[i]);
+        else
+            for ( i = 0; i < p->nSimWords; i++ )
+                pSims->pData[i] = (pSims0->pData[i] & pSims1->pData[i]);
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash value using simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ivy_NodeHash( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+    static int s_FPrimes[128] = { 
+        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
+        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
+        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
+        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
+        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
+        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
+        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
+        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
+        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
+        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
+        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
+        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
+        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+    };
+    Ivy_FraigSim_t * pSims;
+    unsigned uHash;
+    int i;
+    assert( p->nSimWords <= 128 );
+    uHash = 0;
+    pSims  = Ivy_ObjSim(pObj);
+    for ( i = 0; i < p->nSimWords; i++ )
+        uHash ^= pSims->pData[i] * s_FPrimes[i];
+    return uHash;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates AIG manager.]
+
+  Description [Assumes that the PI simulation info is attached.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSimulateOne( Ivy_FraigMan_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i, clk;
+clk = clock();
+    Ivy_ManForEachNode( p->pManAig, pObj, i )
+    {
+        Ivy_NodeSimulate( p, pObj );
+/*
+        if ( Ivy_ObjFraig(pObj) == NULL )
+            printf( "%3d --- -- %d  :  ", pObj->Id, pObj->fPhase );
+        else
+            printf( "%3d %3d %2d %d  :  ", pObj->Id, Ivy_Regular(Ivy_ObjFraig(pObj))->Id, Ivy_ObjSatNum(Ivy_Regular(Ivy_ObjFraig(pObj))), pObj->fPhase );
+        Extra_PrintBinary( stdout, Ivy_ObjSim(pObj), 30 );
+        printf( "\n" );
+*/
+    }
+p->timeSim += clock() - clk;
+p->nSimRounds++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates AIG manager.]
+
+  Description [Assumes that the PI simulation info is attached.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSimulateOneSim( Ivy_FraigMan_t * p )
+{
+    Ivy_FraigSim_t * pSims;
+    int clk;
+clk = clock();
+    for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext )
+        Ivy_NodeSimulateSim( p, pSims );
+p->timeSim += clock() - clk;
+p->nSimRounds++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one node to the equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeAddToClass( Ivy_Obj_t * pClass, Ivy_Obj_t * pObj )
+{
+    if ( Ivy_ObjClassNodeNext(pClass) == NULL )
+        Ivy_ObjSetClassNodeNext( pClass, pObj );
+    else
+        Ivy_ObjSetClassNodeNext( Ivy_ObjClassNodeLast(pClass), pObj );
+    Ivy_ObjSetClassNodeLast( pClass, pObj );
+    Ivy_ObjSetClassNodeRepr( pObj, pClass );
+    Ivy_ObjSetClassNodeNext( pObj, NULL );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds equivalence class to the list of classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigAddClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass )
+{
+    if ( pList->pHead == NULL )
+    {
+        pList->pHead = pClass;
+        pList->pTail = pClass;
+        Ivy_ObjSetEquivListPrev( pClass, NULL );
+        Ivy_ObjSetEquivListNext( pClass, NULL ); 
+    }
+    else
+    {
+        Ivy_ObjSetEquivListNext( pList->pTail, pClass ); 
+        Ivy_ObjSetEquivListPrev( pClass, pList->pTail );
+        Ivy_ObjSetEquivListNext( pClass, NULL ); 
+        pList->pTail = pClass;
+    }
+    pList->nItems++;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Updates the list of classes after base class has split.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigInsertClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pBase, Ivy_Obj_t * pClass )
+{
+    Ivy_ObjSetEquivListPrev( pClass, pBase );
+    Ivy_ObjSetEquivListNext( pClass, Ivy_ObjEquivListNext(pBase) ); 
+    if ( Ivy_ObjEquivListNext(pBase) )
+        Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pBase), pClass );
+    Ivy_ObjSetEquivListNext( pBase, pClass ); 
+    if ( pList->pTail == pBase )
+        pList->pTail = pClass;
+    pList->nItems++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes equivalence class from the list of classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigRemoveClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass )
+{
+    if ( pList->pHead == pClass )
+        pList->pHead = Ivy_ObjEquivListNext(pClass);
+    if ( pList->pTail == pClass )
+        pList->pTail = Ivy_ObjEquivListPrev(pClass);
+    if ( Ivy_ObjEquivListPrev(pClass) )
+        Ivy_ObjSetEquivListNext( Ivy_ObjEquivListPrev(pClass), Ivy_ObjEquivListNext(pClass) ); 
+    if ( Ivy_ObjEquivListNext(pClass) )
+        Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pClass), Ivy_ObjEquivListPrev(pClass) );
+    Ivy_ObjSetEquivListNext( pClass, NULL ); 
+    Ivy_ObjSetEquivListPrev( pClass, NULL );
+    pClass->fMarkA = 0;
+    pList->nItems--;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of pairs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigCountPairsClasses( Ivy_FraigMan_t * p )
+{
+    Ivy_Obj_t * pClass, * pNode;
+    int nPairs = 0, nNodes;
+    return nPairs;
+
+    Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
+    {
+        nNodes = 0;
+        Ivy_FraigForEachClassNode( pClass, pNode )
+            nNodes++;
+        nPairs += nNodes * (nNodes - 1) / 2;
+    }
+    return nPairs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates initial simulation classes.]
+
+  Description [Assumes that simulation info is assigned.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p )
+{
+    Ivy_Obj_t ** pTable;
+    Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry;
+    int i, nTableSize;
+    unsigned Hash;
+    pConst1 = Ivy_ManConst1(p->pManAig);
+    // allocate the table
+    nTableSize = Ivy_ManObjNum(p->pManAig) / 2 + 13;
+    pTable = ALLOC( Ivy_Obj_t *, nTableSize ); 
+    memset( pTable, 0, sizeof(Ivy_Obj_t *) * nTableSize );
+    // collect nodes into the table
+    Ivy_ManForEachObj( p->pManAig, pObj, i )
+    {
+        if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
+            continue;
+        Hash = Ivy_NodeHash( p, pObj );
+        if ( Hash == 0 && Ivy_NodeHasZeroSim( p, pObj ) )
+        {
+            Ivy_NodeAddToClass( pConst1, pObj );
+            continue;
+        }
+        // add the node to the table
+        pBin = pTable[Hash % nTableSize];
+        Ivy_FraigForEachBinNode( pBin, pEntry )
+            if ( Ivy_NodeCompareSims( p, pEntry, pObj ) )
+            {
+                Ivy_NodeAddToClass( pEntry, pObj );
+                break;
+            }
+        // check if the entry was added
+        if ( pEntry )
+            continue;
+        Ivy_ObjSetNodeHashNext( pObj, pBin );
+        pTable[Hash % nTableSize] = pObj;
+    }
+    // collect non-trivial classes
+    assert( p->lClasses.pHead == NULL );
+    Ivy_ManForEachObj( p->pManAig, pObj, i )
+    {
+        if ( !Ivy_ObjIsConst1(pObj) && !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
+            continue;
+        Ivy_ObjSetNodeHashNext( pObj, NULL );
+        if ( Ivy_ObjClassNodeRepr(pObj) == NULL )
+        {
+            assert( Ivy_ObjClassNodeNext(pObj) == NULL );
+            continue;
+        }
+        // recognize the head of the class
+        if ( Ivy_ObjClassNodeNext( Ivy_ObjClassNodeRepr(pObj) ) != NULL )
+            continue;
+        // clean the class representative and add it to the list
+        Ivy_ObjSetClassNodeRepr( pObj, NULL );
+        Ivy_FraigAddClass( &p->lClasses, pObj );
+    }
+    // free the table
+    free( pTable );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively refines the class after simulation.]
+
+  Description [Returns 1 if the class has changed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigRefineClass_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass )
+{
+    Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode;
+    int RetValue = 0;
+    // check if there is refinement
+    pListOld = pClass;
+    Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew )
+    {
+        if ( !Ivy_NodeCompareSims(p, pClass, pClassNew) )
+        {
+            if ( p->pParams->fPatScores )
+                Ivy_FraigAddToPatScores( p, pClass, pClassNew );
+            break;
+        }
+        pListOld = pClassNew;
+    }
+    if ( pClassNew == NULL )
+        return 0;
+    // set representative of the new class
+    Ivy_ObjSetClassNodeRepr( pClassNew, NULL );
+    // start the new list
+    pListNew = pClassNew;
+    // go through the remaining nodes and sort them into two groups:
+    // (1) matches of the old node; (2) non-matches of the old node
+    Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClassNew), pNode )
+        if ( Ivy_NodeCompareSims( p, pClass, pNode ) )
+        {
+            Ivy_ObjSetClassNodeNext( pListOld, pNode );
+            pListOld = pNode;
+        }
+        else
+        {
+            Ivy_ObjSetClassNodeNext( pListNew, pNode );
+            Ivy_ObjSetClassNodeRepr( pNode, pClassNew );
+            pListNew = pNode;
+        }
+    // finish both lists
+    Ivy_ObjSetClassNodeNext( pListNew, NULL );
+    Ivy_ObjSetClassNodeNext( pListOld, NULL );
+    // update the list of classes
+    Ivy_FraigInsertClass( &p->lClasses, pClass, pClassNew );
+    // if the old class is trivial, remove it
+    if ( Ivy_ObjClassNodeNext(pClass) == NULL )
+        Ivy_FraigRemoveClass( &p->lClasses, pClass );
+    // if the new class is trivial, remove it; otherwise, try to refine it
+    if ( Ivy_ObjClassNodeNext(pClassNew) == NULL )
+        Ivy_FraigRemoveClass( &p->lClasses, pClassNew );
+    else
+        RetValue = Ivy_FraigRefineClass_rec( p, pClassNew );
+    return RetValue + 1;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Creates the counter-example from the successful pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigCheckOutputSimsSavePattern( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{ 
+    Ivy_FraigSim_t * pSims;
+    int i, k, BestPat, * pModel;
+    // find the word of the pattern
+    pSims = Ivy_ObjSim(pObj);
+    for ( i = 0; i < p->nSimWords; i++ )
+        if ( pSims->pData[i] )
+            break;
+    assert( i < p->nSimWords );
+    // find the bit of the pattern
+    for ( k = 0; k < 32; k++ )
+        if ( pSims->pData[i] & (1 << k) )
+            break;
+    assert( k < 32 );
+    // determine the best pattern
+    BestPat = i * 32 + k;
+    // fill in the counter-example data
+    pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+    Ivy_ManForEachPi( p->pManAig, pObj, i )
+        pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat);
+    // set the model
+    assert( p->pManFraig->pData == NULL );
+    p->pManFraig->pData = pModel;
+    return;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the one of the output is already non-constant 0.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    Ivy_ManForEachPo( p->pManAig, pObj, i )
+        if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) )
+        {
+            // create the counter-example from this pattern
+            Ivy_FraigCheckOutputSimsSavePattern( p, Ivy_ObjFanin0(pObj) );
+            return 1;
+        }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines the classes after simulation.]
+
+  Description [Assumes that simulation info is assigned. Returns the
+  number of classes refined.]
+               
+  SideEffects [Large equivalence class of constant 0 may cause problems.]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p )
+{
+    Ivy_Obj_t * pClass, * pClass2;
+    int clk, RetValue, Counter = 0;
+    // check if some outputs already became non-constant
+    // this is a special case when computation can be stopped!!!
+    if ( p->pParams->fProve )
+        Ivy_FraigCheckOutputSims( p );
+    if ( p->pManFraig->pData )
+        return 0;
+    // refine the classed
+clk = clock();
+    Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 )
+    {
+        if ( pClass->fMarkA )
+            continue;
+        RetValue = Ivy_FraigRefineClass_rec( p, pClass );
+        Counter += ( RetValue > 0 );
+//if ( Ivy_ObjIsConst1(pClass) )
+//printf( "%d ", RetValue );
+//if ( Ivy_ObjIsConst1(pClass) )
+//    p->time1 += clock() - clk;
+    }
+p->timeRef += clock() - clk;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print the class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigPrintClass( Ivy_Obj_t * pClass )
+{
+    Ivy_Obj_t * pObj;
+    printf( "Class {" );
+    Ivy_FraigForEachClassNode( pClass, pObj )
+        printf( " %d(%d)%c", pObj->Id, pObj->Level, pObj->fPhase? '+' : '-' );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of elements in the class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigCountClassNodes( Ivy_Obj_t * pClass )
+{
+    Ivy_Obj_t * pObj;
+    int Counter = 0;
+    Ivy_FraigForEachClassNode( pClass, pObj )
+        Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints simulation classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigPrintSimClasses( Ivy_FraigMan_t * p )
+{
+    Ivy_Obj_t * pClass;
+    Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
+    {
+//        Ivy_FraigPrintClass( pClass );
+        printf( "%d ", Ivy_FraigCountClassNodes( pClass ) );
+    }
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generated const 0 pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSavePattern0( Ivy_FraigMan_t * p )
+{
+    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [[Generated const 1 pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSavePattern1( Ivy_FraigMan_t * p )
+{
+    memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generates the counter-example satisfying the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p )
+{
+    int * pModel;
+    Ivy_Obj_t * pObj;
+    int i;
+    pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+    Ivy_ManForEachPi( p->pManFraig, pObj, i )
+        pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True );
+    return pModel;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSavePattern( Ivy_FraigMan_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+    Ivy_ManForEachPi( p->pManFraig, pObj, i )
+//    Vec_PtrForEachEntry( p->vPiVars, pObj, i )
+        if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
+            Ivy_InfoSetBit( p->pPatWords, i );
+//            Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSavePattern2( Ivy_FraigMan_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+//    Ivy_ManForEachPi( p->pManFraig, pObj, i )
+    Vec_PtrForEachEntry( p->vPiVars, pObj, i )
+        if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
+//            Ivy_InfoSetBit( p->pPatWords, i );
+            Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSavePattern3( Ivy_FraigMan_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    for ( i = 0; i < p->nPatWords; i++ )
+        p->pPatWords[i] = Ivy_ObjRandomSim();
+    Vec_PtrForEachEntry( p->vPiVars, pObj, i )
+        if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) )
+            Ivy_InfoXorBit( p->pPatWords, pObj->Id - 1 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs simulation of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSimulate( Ivy_FraigMan_t * p )
+{
+    int nChanges, nClasses;
+    // start the classes
+    Ivy_FraigAssignRandom( p );
+    Ivy_FraigSimulateOne( p );
+    Ivy_FraigCreateClasses( p );
+//printf( "Starting classes = %5d.   Pairs = %6d.\n", p->lClasses.nItems, Ivy_FraigCountPairsClasses(p) );
+    // refine classes by walking 0/1 patterns
+    Ivy_FraigSavePattern0( p );
+    Ivy_FraigAssignDist1( p, p->pPatWords );
+    Ivy_FraigSimulateOne( p );
+    nChanges = Ivy_FraigRefineClasses( p );
+    if ( p->pManFraig->pData )
+        return;
+//printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
+    Ivy_FraigSavePattern1( p );
+    Ivy_FraigAssignDist1( p, p->pPatWords );
+    Ivy_FraigSimulateOne( p );
+    nChanges = Ivy_FraigRefineClasses( p );
+    if ( p->pManFraig->pData )
+        return;
+//printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
+    // refine classes by random simulation
+    do {
+        Ivy_FraigAssignRandom( p );
+        Ivy_FraigSimulateOne( p );
+        nClasses = p->lClasses.nItems;
+        nChanges = Ivy_FraigRefineClasses( p );
+        if ( p->pManFraig->pData )
+            return;
+//printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
+    } while ( (double)nChanges / nClasses > p->pParams->dSimSatur );
+//    Ivy_FraigPrintSimClasses( p );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans pattern scores.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigCleanPatScores( Ivy_FraigMan_t * p )
+{
+    int i, nLimit = p->nSimWords * 32;
+    for ( i = 0; i < nLimit; i++ )
+        p->pPatScores[i] = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds to pattern scores.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew )
+{
+    Ivy_FraigSim_t * pSims0, * pSims1;
+    unsigned uDiff;
+    int i, w;
+    // get hold of the simulation information
+    pSims0 = Ivy_ObjSim(pClass);
+    pSims1 = Ivy_ObjSim(pClassNew);
+    // iterate through the differences and record the score
+    for ( w = 0; w < p->nSimWords; w++ )
+    {
+        uDiff = pSims0->pData[w] ^ pSims1->pData[w];
+        if ( uDiff == 0 )
+            continue;
+        for ( i = 0; i < 32; i++ )
+            if ( uDiff & ( 1 << i ) )
+                p->pPatScores[w*32+i]++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Selects the best pattern.]
+
+  Description [Returns 1 if such pattern is found.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigSelectBestPat( Ivy_FraigMan_t * p )
+{
+    Ivy_FraigSim_t * pSims;
+    Ivy_Obj_t * pObj;
+    int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1;
+    for ( i = 1; i < nLimit; i++ )
+    {
+        if ( MaxScore < p->pPatScores[i] )
+        {
+            MaxScore = p->pPatScores[i];
+            BestPat = i;
+        }
+    }
+    if ( MaxScore == 0 )
+        return 0;
+//    if ( MaxScore > p->pParams->MaxScore )
+//    printf( "Max score is %3d.  ", MaxScore );
+    // copy the best pattern into the selected pattern
+    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+    Ivy_ManForEachPi( p->pManAig, pObj, i )
+    {
+        pSims = Ivy_ObjSim(pObj);
+        if ( Ivy_InfoHasBit(pSims->pData, BestPat) )
+            Ivy_InfoSetBit(p->pPatWords, i);
+    }
+    return MaxScore;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates fraiging manager after finding a counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
+{
+    int nChanges;
+    Ivy_FraigAssignDist1( p, p->pPatWords );
+    Ivy_FraigSimulateOne( p );
+    if ( p->pParams->fPatScores )
+        Ivy_FraigCleanPatScores( p );
+    nChanges = Ivy_FraigRefineClasses( p );
+    if ( p->pManFraig->pData )
+        return;
+    if ( nChanges < 1 )
+        printf( "Error: A counter-example did not refine classes!\n" );
+    assert( nChanges >= 1 );
+//printf( "Refined classes! = %5d.   Changes = %4d.\n", p->lClasses.nItems, nChanges );
+
+    if ( !p->pParams->fPatScores )
+        return;
+
+    // perform additional simulation using dist1 patterns derived from successful patterns
+    while ( Ivy_FraigSelectBestPat(p) > p->pParams->MaxScore )
+    {
+        Ivy_FraigAssignDist1( p, p->pPatWords );
+        Ivy_FraigSimulateOne( p );
+        Ivy_FraigCleanPatScores( p );
+        nChanges = Ivy_FraigRefineClasses( p );
+        if ( p->pManFraig->pData )
+            return;
+//printf( "Refined class!!! = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
+        if ( nChanges == 0 )
+            break;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the status of the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose )
+{
+    if ( !fVerbose )
+        return;
+    printf( "Nodes = %7d.  Levels = %4d.  ", Ivy_ManNodeNum(pNtk), Ivy_ManLevels(pNtk) );
+    PRT( pString, clock() - clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reports the status of the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigMiterStatus( Ivy_Man_t * pMan )
+{
+    Ivy_Obj_t * pObj, * pObjNew;
+    int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
+    if ( pMan->pData )
+        return 0;
+    Ivy_ManForEachPo( pMan, pObj, i )
+    {
+        pObjNew = Ivy_ObjChild0(pObj);
+        // check if the output is constant 1
+        if ( pObjNew == pMan->pConst1 )
+        {
+            CountNonConst0++;
+            continue;
+        }
+        // check if the output is constant 0
+        if ( pObjNew == Ivy_Not(pMan->pConst1) )
+        {
+            CountConst0++;
+            continue;
+        }
+        // check if the output can be constant 0
+        if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
+        {
+            CountNonConst0++;
+            continue;
+        }
+        CountUndecided++;
+    }
+/*
+    if ( p->pParams->fVerbose )
+    {
+        printf( "Miter has %d outputs. ", Ivy_ManPoNum(p->pManAig) );
+        printf( "Const0 = %d.  ", CountConst0 );
+        printf( "NonConst0 = %d.  ", CountNonConst0 );
+        printf( "Undecided = %d.  ", CountUndecided );
+        printf( "\n" );
+    }
+*/
+    if ( CountNonConst0 )
+        return 0;
+    if ( CountUndecided )
+        return -1;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Tries to prove each output of the miter until encountering a sat output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
+{
+    Ivy_Obj_t * pObj, * pObjNew;
+    int i, RetValue, clk = clock();
+    int fVerbose = 0;
+    Ivy_ManForEachPo( p->pManAig, pObj, i )
+    {
+        if ( i && fVerbose )
+        {
+            PRT( "Time", clock() -clk );
+        }
+        pObjNew = Ivy_ObjChild0Equiv(pObj);
+        // check if the output is constant 1
+        if ( pObjNew == p->pManFraig->pConst1 )
+        {
+            if ( fVerbose )
+                printf( "Output %2d (out of %2d) is constant 1.  ", i, Ivy_ManPoNum(p->pManAig) );
+            break;
+        }
+        // check if the output is constant 0
+        if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) )
+        {
+            if ( fVerbose )
+                printf( "Output %2d (out of %2d) is already constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
+            continue;
+        }
+        // check if the output can be constant 0
+        if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
+        {
+            if ( fVerbose )
+                printf( "Output %2d (out of %2d) cannot be constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
+            // assing constant 0 model
+            p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+            memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
+            break;
+        }
+/*
+        // check the representative of this node
+        pRepr = Ivy_ObjClassNodeRepr(Ivy_ObjFanin0(pObj));
+        if ( Ivy_Regular(pRepr) != p->pManAig->pConst1 )
+            printf( "Representative is not constant 1.\n" );
+        else
+            printf( "Representative is constant 1.\n" );
+*/
+        // try to prove the output constant 0
+        RetValue = Ivy_FraigNodeIsConst( p, Ivy_Regular(pObjNew) );
+        if ( RetValue == 1 )  // proved equivalent
+        {
+            if ( fVerbose )
+                printf( "Output %2d (out of %2d) was proved constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
+            // set the constant miter
+            Ivy_ObjFanin0(pObj)->pEquiv = Ivy_NotCond( p->pManFraig->pConst1, !Ivy_ObjFaninC0(pObj) );
+            continue;
+        }
+        if ( RetValue == -1 ) // failed
+        {
+            if ( fVerbose )
+                printf( "Output %2d (out of %2d) has timed out at %d backtracks.  ", i, Ivy_ManPoNum(p->pManAig), p->pParams->nBTLimitMiter );
+            continue;
+        }
+        // proved satisfiable
+        if ( fVerbose )
+            printf( "Output %2d (out of %2d) was proved NOT a constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
+        // create the model
+        p->pManFraig->pData = Ivy_FraigCreateModel(p);
+        break;
+    }
+    if ( fVerbose )
+    {
+        PRT( "Time", clock() -clk );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSweep( Ivy_FraigMan_t * p )
+{
+    Ivy_Obj_t * pObj;//, * pTemp;
+    int i, k = 0;
+p->nClassesZero = p->lClasses.pHead? (Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0) : 0;
+p->nClassesBeg  = p->lClasses.nItems;
+    // duplicate internal nodes
+    p->pProgress = Extra_ProgressBarStart( stdout, Ivy_ManNodeNum(p->pManAig) );
+    Ivy_ManForEachNode( p->pManAig, pObj, i )
+    {
+        Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
+        // default to simple strashing if simulation detected a counter-example for a PO
+        if ( p->pManFraig->pData )
+            pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+        else
+            pObj->pEquiv = Ivy_FraigAnd( p, pObj );
+        assert( pObj->pEquiv != NULL );
+//        pTemp = Ivy_Regular(pObj->pEquiv);
+//        assert( Ivy_Regular(pObj->pEquiv)->Type );
+    }
+    Extra_ProgressBarStop( p->pProgress );
+p->nClassesEnd = p->lClasses.nItems;
+    // try to prove the outputs of the miter
+    p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig);
+//    Ivy_FraigMiterStatus( p->pManFraig );
+    if ( p->pParams->fProve && p->pManFraig->pData == NULL )
+        Ivy_FraigMiterProve( p );
+    // add the POs
+    Ivy_ManForEachPo( p->pManAig, pObj, i )
+        Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
+    // clean the old manager
+    Ivy_ManForEachObj( p->pManAig, pObj, i )
+        pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
+    // clean the new manager
+    Ivy_ManForEachObj( p->pManFraig, pObj, i )
+    {
+        if ( Ivy_ObjFaninVec(pObj) )
+            Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
+        pObj->pNextFan0 = pObj->pNextFan1 = NULL;
+    }
+    // remove dangling nodes 
+    Ivy_ManCleanup( p->pManFraig );
+    // clean up the class marks
+    Ivy_FraigForEachEquivClass( p->lClasses.pHead, pObj )
+        pObj->fMarkA = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for one node.]
+
+  Description [Returns the fraiged node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
+{ 
+    Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew;
+    int RetValue;
+    // get the fraiged fanins
+    pFanin0New = Ivy_ObjChild0Equiv(pObjOld);
+    pFanin1New = Ivy_ObjChild1Equiv(pObjOld);
+    // get the candidate fraig node
+    pObjNew = Ivy_And( p->pManFraig, pFanin0New, pFanin1New );
+    // get representative of this class
+    if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node
+         (!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node
+    {
+//        if ( Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1 )
+//        {
+//            int x = 0;
+//        }
+        assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
+        assert( pObjNew != Ivy_Regular(pFanin0New) );
+        assert( pObjNew != Ivy_Regular(pFanin1New) );
+        return pObjNew;
+    }
+    // get the fraiged representative
+    pObjReprNew = Ivy_ObjFraig(Ivy_ObjClassNodeRepr(pObjOld));
+    // if the fraiged nodes are the same return
+    if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) )
+        return pObjNew;
+    assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) );
+    // they are different (the counter-example is in p->pPatWords)
+    RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew) );
+    if ( RetValue == 1 )  // proved equivalent
+    {
+        // mark the class as proved
+        if ( Ivy_ObjClassNodeNext(pObjOld) == NULL )
+            Ivy_ObjClassNodeRepr(pObjOld)->fMarkA = 1;
+        return Ivy_NotCond( pObjReprNew, pObjOld->fPhase ^ Ivy_ObjClassNodeRepr(pObjOld)->fPhase );
+    }
+    if ( RetValue == -1 ) // failed
+        return pObjNew;
+    // simulate the counter-example and return the new node
+    Ivy_FraigResimulate( p );
+    return pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints variable activity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p )
+{
+    int i;
+    for ( i = 0; i < p->nSatVars; i++ )
+        printf( "%d %.3f  ", i, p->pSat->activity[i] );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Runs equivalence test for the two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
+{
+    int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
+
+    // make sure the nodes are not complemented
+    assert( !Ivy_IsComplement(pNew) );
+    assert( !Ivy_IsComplement(pOld) );
+    assert( pNew != pOld );
+
+    // if at least one of the nodes is a failed node, perform adjustments:
+    // if the backtrack limit is small, simply skip this node
+    // if the backtrack limit is > 10, take the quare root of the limit
+    nBTLimit = p->pParams->nBTLimitNode;
+    if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
+    {
+        p->nSatFails++;
+        // fail immediately
+//        return -1;
+        if ( nBTLimit <= 10 )
+            return -1;
+        nBTLimit = (int)pow(nBTLimit, 0.7);
+    }
+    p->nSatCalls++;
+
+    // make sure the solver is allocated and has enough variables
+    if ( p->pSat == NULL )
+    {
+        p->pSat = sat_solver_new();
+        p->nSatVars = 1;
+        sat_solver_setnvars( p->pSat, 1000 );
+    }
+
+    // if the nodes do not have SAT variables, allocate them
+    Ivy_FraigNodeAddToSolver( p, pOld, pNew );
+
+    // prepare variable activity
+    Ivy_FraigSetActivityFactors( p, pOld, pNew ); 
+
+    // solve under assumptions
+    // A = 1; B = 0     OR     A = 1; B = 1 
+clk = clock();
+    pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 );
+    pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
+//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
+        (sint64)nBTLimit, (sint64)0, 
+        p->nBTLimitGlobal, p->nInsLimitGlobal );
+p->timeSat += clock() - clk;
+    if ( RetValue1 == l_False )
+    {
+p->timeSatUnsat += clock() - clk;
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+        // continue solving the other implication
+        p->nSatCallsUnsat++;
+    }
+    else if ( RetValue1 == l_True )
+    {
+p->timeSatSat += clock() - clk;
+        Ivy_FraigSavePattern( p );
+        p->nSatCallsSat++;
+        return 0;
+    }
+    else // if ( RetValue1 == l_Undef )
+    {
+p->timeSatFail += clock() - clk;
+        // mark the node as the failed node
+        if ( pOld != p->pManFraig->pConst1 ) 
+            pOld->fFailTfo = 1;
+        pNew->fFailTfo = 1;
+        p->nSatFailsReal++;
+        return -1;
+    }
+
+    // if the old node was constant 0, we already know the answer
+    if ( pOld == p->pManFraig->pConst1 )
+    {
+        p->nSatProof++;
+        return 1;
+    }
+
+    // solve under assumptions
+    // A = 0; B = 1     OR     A = 0; B = 0 
+clk = clock();
+    pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 );
+    pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
+        (sint64)nBTLimit, (sint64)0, 
+        p->nBTLimitGlobal, p->nInsLimitGlobal );
+p->timeSat += clock() - clk;
+    if ( RetValue1 == l_False )
+    {
+p->timeSatUnsat += clock() - clk;
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+        p->nSatCallsUnsat++;
+    }
+    else if ( RetValue1 == l_True )
+    {
+p->timeSatSat += clock() - clk;
+        Ivy_FraigSavePattern( p );
+        p->nSatCallsSat++;
+        return 0;
+    }
+    else // if ( RetValue1 == l_Undef )
+    {
+p->timeSatFail += clock() - clk;
+        // mark the node as the failed node
+        pOld->fFailTfo = 1;
+        pNew->fFailTfo = 1;
+        p->nSatFailsReal++;
+        return -1;
+    }
+/*
+    // check BDD proof
+    {
+        int RetVal;
+        PRT( "Sat", clock() - clk2 );
+        clk2 = clock();
+        RetVal = Ivy_FraigNodesAreEquivBdd( pOld, pNew );
+//        printf( "%d ", RetVal );
+        assert( RetVal );
+        PRT( "Bdd", clock() - clk2 );
+        printf( "\n" );
+    }
+*/
+    // return SAT proof
+    p->nSatProof++;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Runs equivalence test for one node.]
+
+  Description [Returns the fraiged node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
+{
+    int pLits[2], RetValue1, RetValue, clk;
+
+    // make sure the nodes are not complemented
+    assert( !Ivy_IsComplement(pNew) );
+    assert( pNew != p->pManFraig->pConst1 );
+    p->nSatCalls++;
+
+    // make sure the solver is allocated and has enough variables
+    if ( p->pSat == NULL )
+    {
+        p->pSat = sat_solver_new();
+        p->nSatVars = 1;
+        sat_solver_setnvars( p->pSat, 1000 );
+    }
+
+    // if the nodes do not have SAT variables, allocate them
+    Ivy_FraigNodeAddToSolver( p, NULL, pNew );
+
+    // prepare variable activity
+    Ivy_FraigSetActivityFactors( p, NULL, pNew ); 
+
+    // solve under assumptions
+clk = clock();
+    pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase );
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 
+        (sint64)p->pParams->nBTLimitMiter, (sint64)0, 
+        p->nBTLimitGlobal, p->nInsLimitGlobal );
+p->timeSat += clock() - clk;
+    if ( RetValue1 == l_False )
+    {
+p->timeSatUnsat += clock() - clk;
+        pLits[0] = lit_neg( pLits[0] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+        assert( RetValue );
+        // continue solving the other implication
+        p->nSatCallsUnsat++;
+    }
+    else if ( RetValue1 == l_True )
+    {
+p->timeSatSat += clock() - clk;
+        if ( p->pPatWords )
+            Ivy_FraigSavePattern( p );
+        p->nSatCallsSat++;
+        return 0;
+    }
+    else // if ( RetValue1 == l_Undef )
+    {
+p->timeSatFail += clock() - clk;
+        // mark the node as the failed node
+        pNew->fFailTfo = 1;
+        p->nSatFailsReal++;
+        return -1;
+    }
+
+    // return SAT proof
+    p->nSatProof++;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigAddClausesMux( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode )
+{
+    Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE;
+    int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
+
+    assert( !Ivy_IsComplement( pNode ) );
+    assert( Ivy_ObjIsMuxType( pNode ) );
+    // get nodes (I = if, T = then, E = else)
+    pNodeI = Ivy_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+    // get the variable numbers
+    VarF = Ivy_ObjSatNum(pNode);
+    VarI = Ivy_ObjSatNum(pNodeI);
+    VarT = Ivy_ObjSatNum(Ivy_Regular(pNodeT));
+    VarE = Ivy_ObjSatNum(Ivy_Regular(pNodeE));
+    // get the complementation flags
+    fCompT = Ivy_IsComplement(pNodeT);
+    fCompE = Ivy_IsComplement(pNodeE);
+
+    // f = ITE(i, t, e)
+
+    // i' + t' + f
+    // i' + t  + f'
+    // i  + e' + f
+    // i  + e  + f'
+
+    // create four clauses
+    pLits[0] = toLitCond(VarI, 1);
+    pLits[1] = toLitCond(VarT, 1^fCompT);
+    pLits[2] = toLitCond(VarF, 0);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 1);
+    pLits[1] = toLitCond(VarT, 0^fCompT);
+    pLits[2] = toLitCond(VarF, 1);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 0);
+    pLits[1] = toLitCond(VarE, 1^fCompE);
+    pLits[2] = toLitCond(VarF, 0);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 0);
+    pLits[1] = toLitCond(VarE, 0^fCompE);
+    pLits[2] = toLitCond(VarF, 1);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+
+    // two additional clauses
+    // t' & e' -> f'
+    // t  & e  -> f 
+
+    // t  + e   + f'
+    // t' + e'  + f 
+
+    if ( VarT == VarE )
+    {
+//        assert( fCompT == !fCompE );
+        return;
+    }
+
+    pLits[0] = toLitCond(VarT, 0^fCompT);
+    pLits[1] = toLitCond(VarE, 0^fCompE);
+    pLits[2] = toLitCond(VarF, 1);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarT, 1^fCompT);
+    pLits[1] = toLitCond(VarE, 1^fCompE);
+    pLits[2] = toLitCond(VarF, 0);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigAddClausesSuper( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t * vSuper )
+{
+    Ivy_Obj_t * pFanin;
+    int * pLits, nLits, RetValue, i;
+    assert( !Ivy_IsComplement(pNode) );
+    assert( Ivy_ObjIsNode( pNode ) );
+    // create storage for literals
+    nLits = Vec_PtrSize(vSuper) + 1;
+    pLits = ALLOC( int, nLits );
+    // suppose AND-gate is A & B = C
+    // add !A => !C   or   A + !C
+    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    {
+        pLits[0] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), Ivy_IsComplement(pFanin));
+        pLits[1] = toLitCond(Ivy_ObjSatNum(pNode), 1);
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+    }
+    // add A & B => C   or   !A + !B + C
+    Vec_PtrForEachEntry( vSuper, pFanin, i )
+        pLits[i] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), !Ivy_IsComplement(pFanin));
+    pLits[nLits-1] = toLitCond(Ivy_ObjSatNum(pNode), 0);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
+    assert( RetValue );
+    free( pLits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigCollectSuper_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
+{
+    // if the new node is complemented or a PI, another gate begins
+    if ( Ivy_IsComplement(pObj) || Ivy_ObjIsPi(pObj) || (!fFirst && Ivy_ObjRefs(pObj) > 1) || 
+         (fUseMuxes && Ivy_ObjIsMuxType(pObj)) )
+    {
+        Vec_PtrPushUnique( vSuper, pObj );
+        return;
+    }
+    // go through the branches
+    Ivy_FraigCollectSuper_rec( Ivy_ObjChild0(pObj), vSuper, 0, fUseMuxes );
+    Ivy_FraigCollectSuper_rec( Ivy_ObjChild1(pObj), vSuper, 0, fUseMuxes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ivy_FraigCollectSuper( Ivy_Obj_t * pObj, int fUseMuxes )
+{
+    Vec_Ptr_t * vSuper;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( !Ivy_ObjIsPi(pObj) );
+    vSuper = Vec_PtrAlloc( 4 );
+    Ivy_FraigCollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
+    return vSuper;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the solver clause database.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigObjAddToFrontier( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+{
+    assert( !Ivy_IsComplement(pObj) );
+    if ( Ivy_ObjSatNum(pObj) )
+        return;
+    assert( Ivy_ObjSatNum(pObj) == 0 );
+    assert( Ivy_ObjFaninVec(pObj) == NULL );
+    if ( Ivy_ObjIsConst1(pObj) )
+        return;
+//printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
+    Ivy_ObjSetSatNum( pObj, p->nSatVars++ );
+    if ( Ivy_ObjIsNode(pObj) )
+        Vec_PtrPush( vFrontier, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the solver clause database.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
+{ 
+    Vec_Ptr_t * vFrontier, * vFanins;
+    Ivy_Obj_t * pNode, * pFanin;
+    int i, k, fUseMuxes = 1;
+    assert( pOld || pNew );
+    // quit if CNF is ready
+    if ( (!pOld || Ivy_ObjFaninVec(pOld)) && (!pNew || Ivy_ObjFaninVec(pNew)) )
+        return;
+    // start the frontier
+    vFrontier = Vec_PtrAlloc( 100 );
+    if ( pOld ) Ivy_FraigObjAddToFrontier( p, pOld, vFrontier );
+    if ( pNew ) Ivy_FraigObjAddToFrontier( p, pNew, vFrontier );
+    // explore nodes in the frontier
+    Vec_PtrForEachEntry( vFrontier, pNode, i )
+    {
+        // create the supergate
+        assert( Ivy_ObjSatNum(pNode) );
+        assert( Ivy_ObjFaninVec(pNode) == NULL );
+        if ( fUseMuxes && Ivy_ObjIsMuxType(pNode) )
+        {
+            vFanins = Vec_PtrAlloc( 4 );
+            Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin1(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin1(pNode) ) );
+            Vec_PtrForEachEntry( vFanins, pFanin, k )
+                Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
+            Ivy_FraigAddClausesMux( p, pNode );
+        }
+        else
+        {
+            vFanins = Ivy_FraigCollectSuper( pNode, fUseMuxes );
+            Vec_PtrForEachEntry( vFanins, pFanin, k )
+                Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
+            Ivy_FraigAddClausesSuper( p, pNode, vFanins );
+        }
+        assert( Vec_PtrSize(vFanins) > 1 );
+        Ivy_ObjSetFaninVec( pNode, vFanins );
+    }
+    Vec_PtrFree( vFrontier );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets variable activities in the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigSetActivityFactors_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int LevelMin, int LevelMax )
+{
+    Vec_Ptr_t * vFanins;
+    Ivy_Obj_t * pFanin;
+    int i, Counter = 0;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjSatNum(pObj) );
+    // skip visited variables
+    if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) )
+        return 0;
+    Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj);
+    // add the PI to the list
+    if ( pObj->Level <= (unsigned)LevelMin || Ivy_ObjIsPi(pObj) )
+        return 0;
+    // set the factor of this variable
+    // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pParams->dActConeBumpMax / ThisBump
+    p->pSat->factors[Ivy_ObjSatNum(pObj)] = p->pParams->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
+    veci_push(&p->pSat->act_vars, Ivy_ObjSatNum(pObj));
+    // explore the fanins
+    vFanins = Ivy_ObjFaninVec( pObj );
+    Vec_PtrForEachEntry( vFanins, pFanin, i )
+        Counter += Ivy_FraigSetActivityFactors_rec( p, Ivy_Regular(pFanin), LevelMin, LevelMax );
+    return 1 + Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets variable activities in the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
+{
+    int clk, LevelMin, LevelMax;
+    assert( pOld || pNew );
+clk = clock(); 
+    // reset the active variables
+    veci_resize(&p->pSat->act_vars, 0);
+    // prepare for traversal
+    Ivy_ManIncrementTravId( p->pManFraig );
+    // determine the min and max level to visit
+    assert( p->pParams->dActConeRatio > 0 && p->pParams->dActConeRatio < 1 );
+    LevelMax = IVY_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
+    LevelMin = (int)(LevelMax * (1.0 - p->pParams->dActConeRatio));
+    // traverse
+    if ( pOld && !Ivy_ObjIsConst1(pOld) )
+        Ivy_FraigSetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
+    if ( pNew && !Ivy_ObjIsConst1(pNew) )
+        Ivy_FraigSetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
+//Ivy_FraigPrintActivity( p );
+p->timeTrav += clock() - clk;
+    return 1;
+}
+
+
+
+#include "cuddInt.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Checks equivalence using BDDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Ivy_FraigNodesAreEquivBdd_int( DdManager * dd, DdNode * bFunc, Vec_Ptr_t * vFront, int Level )
+{
+    DdNode ** pFuncs;
+    DdNode * bFuncNew;
+    Vec_Ptr_t * vTemp;
+    Ivy_Obj_t * pObj, * pFanin;
+    int i, NewSize;
+    // create new frontier
+    vTemp = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( vFront, pObj, i )
+    {
+        if ( (int)pObj->Level != Level )
+        {
+            pObj->fMarkB = 1;
+            pObj->TravId = Vec_PtrSize(vTemp);
+            Vec_PtrPush( vTemp, pObj );
+            continue;
+        }
+
+        pFanin = Ivy_ObjFanin0(pObj);
+        if ( pFanin->fMarkB == 0 )
+        {
+            pFanin->fMarkB = 1;
+            pFanin->TravId = Vec_PtrSize(vTemp);
+            Vec_PtrPush( vTemp, pFanin );
+        }
+
+        pFanin = Ivy_ObjFanin1(pObj);
+        if ( pFanin->fMarkB == 0 )
+        {
+            pFanin->fMarkB = 1;
+            pFanin->TravId = Vec_PtrSize(vTemp);
+            Vec_PtrPush( vTemp, pFanin );
+        }
+    }
+    // collect the permutation
+    NewSize = IVY_MAX(dd->size, Vec_PtrSize(vTemp));
+    pFuncs = ALLOC( DdNode *, NewSize );
+    Vec_PtrForEachEntry( vFront, pObj, i )
+    {
+        if ( (int)pObj->Level != Level )
+            pFuncs[i] = Cudd_bddIthVar( dd, pObj->TravId );
+        else
+            pFuncs[i] = Cudd_bddAnd( dd, 
+                Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ),
+                Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ) );
+        Cudd_Ref( pFuncs[i] );
+    }
+    // add the remaining vars
+    assert( NewSize == dd->size );
+    for ( i = Vec_PtrSize(vFront); i < dd->size; i++ )
+    {
+        pFuncs[i] = Cudd_bddIthVar( dd, i );
+        Cudd_Ref( pFuncs[i] );
+    }
+
+    // create new
+    bFuncNew = Cudd_bddVectorCompose( dd, bFunc, pFuncs ); Cudd_Ref( bFuncNew );
+    // clean trav Id
+    Vec_PtrForEachEntry( vTemp, pObj, i )
+    {
+        pObj->fMarkB = 0;
+        pObj->TravId = 0;
+    }
+    // deref
+    for ( i = 0; i < dd->size; i++ )
+        Cudd_RecursiveDeref( dd, pFuncs[i] );
+    free( pFuncs );
+
+    free( vFront->pArray );
+    *vFront = *vTemp;
+
+    vTemp->nCap = vTemp->nSize = 0;
+    vTemp->pArray = NULL;
+    Vec_PtrFree( vTemp );
+
+    Cudd_Deref( bFuncNew );
+    return bFuncNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks equivalence using BDDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 )
+{
+    static DdManager * dd = NULL;
+    DdNode * bFunc, * bTemp;
+    Vec_Ptr_t * vFront;
+    Ivy_Obj_t * pObj;
+    int i, RetValue, Iter, Level;
+    // start the manager
+    if ( dd == NULL )
+        dd = Cudd_Init( 50, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    // create front
+    vFront = Vec_PtrAlloc( 100 );
+    Vec_PtrPush( vFront, pObj1 );
+    Vec_PtrPush( vFront, pObj2 );
+    // get the function
+    bFunc = Cudd_bddXor( dd, Cudd_bddIthVar(dd,0), Cudd_bddIthVar(dd,1) );  Cudd_Ref( bFunc );
+    bFunc = Cudd_NotCond( bFunc, pObj1->fPhase != pObj2->fPhase );
+    // try running BDDs
+    for ( Iter = 0; ; Iter++ )
+    {
+        // find max level
+        Level = 0;
+        Vec_PtrForEachEntry( vFront, pObj, i )
+            if ( Level < (int)pObj->Level )
+                Level = (int)pObj->Level;
+        if ( Level == 0 )
+            break;            
+        bFunc = Ivy_FraigNodesAreEquivBdd_int( dd, bTemp = bFunc, vFront, Level ); Cudd_Ref( bFunc );
+        Cudd_RecursiveDeref( dd, bTemp );
+        if ( bFunc == Cudd_ReadLogicZero(dd) ) // proved
+            {printf( "%d", Iter ); break;}
+        if ( Cudd_DagSize(bFunc) > 1000 )
+            {printf( "b" ); break;}
+        if ( dd->size > 120 )
+            {printf( "s" ); break;}
+        if ( Iter > 50 )
+            {printf( "i" ); break;}
+    }
+    if ( bFunc == Cudd_ReadLogicZero(dd) ) // unsat
+        RetValue = 1;
+    else if ( Level == 0 ) // sat
+        RetValue = 0;
+    else 
+        RetValue = -1; // spaceout/timeout
+    Cudd_RecursiveDeref( dd, bFunc );
+    Vec_PtrFree( vFront );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+