abc70930: src/aig/ivy/ivyFraig.c Source File

00001 
00021 #include "satSolver.h"
00022 #include "extra.h"
00023 #include "ivy.h"
00024 
00028 
00029 typedef struct Ivy_FraigMan_t_        Ivy_FraigMan_t;
00030 typedef struct Ivy_FraigSim_t_        Ivy_FraigSim_t;
00031 typedef struct Ivy_FraigList_t_       Ivy_FraigList_t;
00032 
00033 struct Ivy_FraigList_t_
00034 {
00035     Ivy_Obj_t *         pHead;
00036     Ivy_Obj_t *         pTail;
00037     int                 nItems;
00038 };
00039 
00040 struct Ivy_FraigSim_t_
00041 {
00042     int                 Type;
00043     Ivy_FraigSim_t *    pNext;
00044     Ivy_FraigSim_t *    pFanin0;
00045     Ivy_FraigSim_t *    pFanin1;
00046     unsigned            pData[0];
00047 };
00048 
00049 struct Ivy_FraigMan_t_
00050 {
00051     // general info 
00052     Ivy_FraigParams_t * pParams;        // various parameters
00053     // temporary backtrack limits because "sint64" cannot be defined in Ivy_FraigParams_t ...
00054     sint64              nBTLimitGlobal; // global limit on the number of backtracks
00055     sint64              nInsLimitGlobal;// global limit on the number of clause inspects
00056     // AIG manager
00057     Ivy_Man_t *         pManAig;        // the starting AIG manager
00058     Ivy_Man_t *         pManFraig;      // the final AIG manager
00059     // simulation information
00060     int                 nSimWords;      // the number of words
00061     char *              pSimWords;      // the simulation info
00062     Ivy_FraigSim_t *    pSimStart;      // the list of simulation info for internal nodes
00063     // counter example storage
00064     int                 nPatWords;      // the number of words in the counter example
00065     unsigned *          pPatWords;      // the counter example
00066     int *               pPatScores;     // the scores of each pattern
00067     // equivalence classes 
00068     Ivy_FraigList_t     lClasses;       // equivalence classes
00069     Ivy_FraigList_t     lCand;          // candidatates
00070     int                 nPairs;         // the number of pairs of nodes
00071     // equivalence checking
00072     sat_solver *        pSat;           // SAT solver
00073     int                 nSatVars;       // the number of variables currently used
00074     Vec_Ptr_t *         vPiVars;        // the PIs of the cone used 
00075     // other 
00076     ProgressBar *       pProgress;
00077     // statistics
00078     int                 nSimRounds;
00079     int                 nNodesMiter;
00080     int                 nClassesZero;
00081     int                 nClassesBeg;
00082     int                 nClassesEnd;
00083     int                 nPairsBeg;
00084     int                 nPairsEnd;
00085     int                 nSatCalls;
00086     int                 nSatCallsSat;
00087     int                 nSatCallsUnsat;
00088     int                 nSatProof;
00089     int                 nSatFails;
00090     int                 nSatFailsReal;
00091     // runtime
00092     int                 timeSim;
00093     int                 timeTrav;
00094     int                 timeSat;
00095     int                 timeSatUnsat;
00096     int                 timeSatSat;
00097     int                 timeSatFail;
00098     int                 timeRef;
00099     int                 timeTotal;
00100     int                 time1;
00101     int                 time2;
00102 };
00103 
00104 typedef struct Prove_ParamsStruct_t_      Prove_Params_t;
00105 struct Prove_ParamsStruct_t_
00106 {
00107     // general parameters
00108     int     fUseFraiging;          // enables fraiging
00109     int     fUseRewriting;         // enables rewriting
00110     int     fUseBdds;              // enables BDD construction when other methods fail
00111     int     fVerbose;              // prints verbose stats
00112     // iterations
00113     int     nItersMax;             // the number of iterations
00114     // mitering 
00115     int     nMiteringLimitStart;   // starting mitering limit
00116     float   nMiteringLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
00117     // rewriting 
00118     int     nRewritingLimitStart;  // the number of rewriting iterations
00119     float   nRewritingLimitMulti;  // multiplicative coefficient to increase the limit in each iteration
00120     // fraiging 
00121     int     nFraigingLimitStart;   // starting backtrack(conflict) limit
00122     float   nFraigingLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
00123     // last-gasp BDD construction
00124     int     nBddSizeLimit;         // the number of BDD nodes when construction is aborted
00125     int     fBddReorder;           // enables dynamic BDD variable reordering
00126     // last-gasp mitering
00127     int     nMiteringLimitLast;    // final mitering limit
00128     // global SAT solver limits
00129     sint64  nTotalBacktrackLimit;  // global limit on the number of backtracks
00130     sint64  nTotalInspectLimit;    // global limit on the number of clause inspects
00131     // global resources applied
00132     sint64  nTotalBacktracksMade;  // the total number of backtracks made
00133     sint64  nTotalInspectsMade;    // the total number of inspects made
00134 };
00135 
00136 static inline Ivy_FraigSim_t * Ivy_ObjSim( Ivy_Obj_t * pObj )                            { return (Ivy_FraigSim_t *)pObj->pFanout;  }
00137 static inline Ivy_Obj_t * Ivy_ObjClassNodeLast( Ivy_Obj_t * pObj )                       { return pObj->pNextFan0;  }
00138 static inline Ivy_Obj_t * Ivy_ObjClassNodeRepr( Ivy_Obj_t * pObj )                       { return pObj->pNextFan0;  }
00139 static inline Ivy_Obj_t * Ivy_ObjClassNodeNext( Ivy_Obj_t * pObj )                       { return pObj->pNextFan1;  }
00140 static inline Ivy_Obj_t * Ivy_ObjNodeHashNext( Ivy_Obj_t * pObj )                        { return pObj->pPrevFan0;  }
00141 static inline Ivy_Obj_t * Ivy_ObjEquivListNext( Ivy_Obj_t * pObj )                       { return pObj->pPrevFan0;  }
00142 static inline Ivy_Obj_t * Ivy_ObjEquivListPrev( Ivy_Obj_t * pObj )                       { return pObj->pPrevFan1;  }
00143 static inline Ivy_Obj_t * Ivy_ObjFraig( Ivy_Obj_t * pObj )                               { return pObj->pEquiv;     }
00144 static inline int         Ivy_ObjSatNum( Ivy_Obj_t * pObj )                              { return (int)pObj->pNextFan0;         }
00145 static inline Vec_Ptr_t * Ivy_ObjFaninVec( Ivy_Obj_t * pObj )                            { return (Vec_Ptr_t *)pObj->pNextFan1; }
00146 
00147 static inline void        Ivy_ObjSetSim( Ivy_Obj_t * pObj, Ivy_FraigSim_t * pSim )       { pObj->pFanout = (Ivy_Obj_t *)pSim; }
00148 static inline void        Ivy_ObjSetClassNodeLast( Ivy_Obj_t * pObj, Ivy_Obj_t * pLast ) { pObj->pNextFan0 = pLast; }
00149 static inline void        Ivy_ObjSetClassNodeRepr( Ivy_Obj_t * pObj, Ivy_Obj_t * pRepr ) { pObj->pNextFan0 = pRepr; }
00150 static inline void        Ivy_ObjSetClassNodeNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pNextFan1 = pNext; }
00151 static inline void        Ivy_ObjSetNodeHashNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext )  { pObj->pPrevFan0 = pNext; }
00152 static inline void        Ivy_ObjSetEquivListNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; }
00153 static inline void        Ivy_ObjSetEquivListPrev( Ivy_Obj_t * pObj, Ivy_Obj_t * pPrev ) { pObj->pPrevFan1 = pPrev; }
00154 static inline void        Ivy_ObjSetFraig( Ivy_Obj_t * pObj, Ivy_Obj_t * pNode )         { pObj->pEquiv    = pNode; }
00155 static inline void        Ivy_ObjSetSatNum( Ivy_Obj_t * pObj, int Num )                  { pObj->pNextFan0 = (Ivy_Obj_t *)Num;     }
00156 static inline void        Ivy_ObjSetFaninVec( Ivy_Obj_t * pObj, Vec_Ptr_t * vFanins )    { pObj->pNextFan1 = (Ivy_Obj_t *)vFanins; }
00157 
00158 static inline unsigned    Ivy_ObjRandomSim()                       { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
00159 
00160 // iterate through equivalence classes
00161 #define Ivy_FraigForEachEquivClass( pList, pEnt )                 \
00162     for ( pEnt = pList;                                           \
00163           pEnt;                                                   \
00164           pEnt = Ivy_ObjEquivListNext(pEnt) )
00165 #define Ivy_FraigForEachEquivClassSafe( pList, pEnt, pEnt2 )      \
00166     for ( pEnt = pList,                                           \
00167           pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL;         \
00168           pEnt;                                                   \
00169           pEnt = pEnt2,                                           \
00170           pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL )
00171 // iterate through nodes in one class
00172 #define Ivy_FraigForEachClassNode( pClass, pEnt )                 \
00173     for ( pEnt = pClass;                                          \
00174           pEnt;                                                   \
00175           pEnt = Ivy_ObjClassNodeNext(pEnt) )
00176 // iterate through nodes in the hash table
00177 #define Ivy_FraigForEachBinNode( pBin, pEnt )                     \
00178     for ( pEnt = pBin;                                            \
00179           pEnt;                                                   \
00180           pEnt = Ivy_ObjNodeHashNext(pEnt) )
00181 
00182 static Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
00183 static Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
00184 static Ivy_Man_t *   Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, sint64 nBTLimitGlobal, sint64 nInsLimitGlobal, sint64 * pnSatConfs, sint64 * pnSatInspects );
00185 static void          Ivy_FraigPrint( Ivy_FraigMan_t * p );
00186 static void          Ivy_FraigStop( Ivy_FraigMan_t * p );
00187 static void          Ivy_FraigSimulate( Ivy_FraigMan_t * p );
00188 static void          Ivy_FraigSweep( Ivy_FraigMan_t * p );
00189 static Ivy_Obj_t *   Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld );
00190 static int           Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
00191 static int           Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj );
00192 static void          Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
00193 static int           Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew );
00194 static void          Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew );
00195 static int           Ivy_FraigMiterStatus( Ivy_Man_t * pMan );
00196 static void          Ivy_FraigMiterProve( Ivy_FraigMan_t * p );
00197 static void          Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose );
00198 static int *         Ivy_FraigCreateModel( Ivy_FraigMan_t * p );
00199 
00200 static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 );
00201 
00202 static sint64 s_nBTLimitGlobal = 0;
00203 static sint64 s_nInsLimitGlobal = 0;
00204 
00208 
00220 void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams )
00221 {
00222     memset( pParams, 0, sizeof(Ivy_FraigParams_t) );
00223     pParams->nSimWords        =      32;  // the number of words in the simulation info
00224     pParams->dSimSatur        =   0.005;  // the ratio of refined classes when saturation is reached
00225     pParams->fPatScores       =       0;  // enables simulation pattern scoring
00226     pParams->MaxScore         =      25;  // max score after which resimulation is used
00227     pParams->fDoSparse        =       1;  // skips sparse functions
00228 //    pParams->dActConeRatio    =    0.05;  // the ratio of cone to be bumped
00229 //    pParams->dActConeBumpMax  =     5.0;  // the largest bump of activity
00230     pParams->dActConeRatio    =     0.3;  // the ratio of cone to be bumped
00231     pParams->dActConeBumpMax  =    10.0;  // the largest bump of activity
00232 
00233     pParams->nBTLimitNode     =     100;  // conflict limit at a node
00234     pParams->nBTLimitMiter    =  500000;  // conflict limit at an output
00235 //    pParams->nBTLimitGlobal   =       0;  // conflict limit global
00236 //    pParams->nInsLimitGlobal  =       0;  // inspection limit global
00237 }
00238 
00250 int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
00251 {
00252     Prove_Params_t * pParams = pPars;
00253     Ivy_FraigParams_t Params, * pIvyParams = &Params; 
00254     Ivy_Man_t * pManAig, * pManTemp;
00255     int RetValue, nIter, clk, timeStart = clock();//, Counter;
00256     sint64 nSatConfs, nSatInspects;
00257 
00258     // start the network and parameters
00259     pManAig = *ppManAig;
00260     Ivy_FraigParamsDefault( pIvyParams );
00261     pIvyParams->fVerbose = pParams->fVerbose;
00262     pIvyParams->fProve = 1;
00263 
00264     if ( pParams->fVerbose )
00265     {
00266         printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
00267             pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
00268         printf( "Mitering = %d (%3.1f).  Rewriting = %d (%3.1f).  Fraiging = %d (%3.1f).\n", 
00269             pParams->nMiteringLimitStart,  pParams->nMiteringLimitMulti, 
00270             pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
00271             pParams->nFraigingLimitStart,  pParams->nFraigingLimitMulti );
00272         printf( "Mitering last = %d.\n", 
00273             pParams->nMiteringLimitLast );
00274     }
00275 
00276     // if SAT only, solve without iteration
00277     if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
00278     {
00279         clk = clock();
00280         pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
00281         pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
00282         RetValue = Ivy_FraigMiterStatus( pManAig );
00283         Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
00284         *ppManAig = pManAig;
00285         return RetValue;
00286     }
00287 
00288     if ( Ivy_ManNodeNum(pManAig) < 500 )
00289     {
00290         // run the first mitering
00291         clk = clock();
00292         pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig);
00293         pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
00294         RetValue = Ivy_FraigMiterStatus( pManAig );
00295         Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
00296         if ( RetValue >= 0 )
00297         {
00298             *ppManAig = pManAig;
00299             return RetValue;
00300         }
00301     }
00302 
00303     // check the current resource limits
00304     RetValue = -1;
00305     for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
00306     {
00307         if ( pParams->fVerbose )
00308         {
00309             printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, 
00310                  (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 
00311                  (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
00312             fflush( stdout );
00313         }
00314 
00315         // try rewriting
00316         if ( pParams->fUseRewriting )
00317         { // bug in Ivy_NodeFindCutsAll() when leaves are identical!
00318 /*
00319             clk = clock();
00320             Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
00321             pManAig = Ivy_ManRwsat( pManAig, 0 );  
00322             RetValue = Ivy_FraigMiterStatus( pManAig );
00323             Ivy_FraigMiterPrint( pManAig, "Rewriting  ", clk, pParams->fVerbose );
00324 */
00325         }
00326         if ( RetValue >= 0 )
00327             break;
00328 
00329         // try fraiging followed by mitering
00330         if ( pParams->fUseFraiging )
00331         {
00332             clk = clock();
00333             pIvyParams->nBTLimitNode  = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter));
00334             pIvyParams->nBTLimitMiter = (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig);
00335             pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects );  Ivy_ManStop( pManTemp );
00336             RetValue = Ivy_FraigMiterStatus( pManAig );
00337             Ivy_FraigMiterPrint( pManAig, "Fraiging   ", clk, pParams->fVerbose );
00338         }
00339         if ( RetValue >= 0 )
00340             break;
00341 
00342         // add to the number of backtracks and inspects
00343         pParams->nTotalBacktracksMade += nSatConfs;
00344         pParams->nTotalInspectsMade   += nSatInspects;
00345         // check if global resource limit is reached
00346         if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
00347              (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
00348         {
00349             printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
00350             *ppManAig = pManAig;
00351             return -1;
00352         }
00353     }    
00354 
00355     if ( RetValue < 0 )
00356     {
00357         if ( pParams->fVerbose )
00358         {
00359             printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
00360             fflush( stdout );
00361         }
00362         clk = clock();
00363         pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
00364         if ( pParams->nTotalBacktrackLimit )
00365             s_nBTLimitGlobal  = pParams->nTotalBacktrackLimit - pParams->nTotalBacktracksMade;
00366         if ( pParams->nTotalInspectLimit )
00367             s_nInsLimitGlobal = pParams->nTotalInspectLimit -   pParams->nTotalInspectsMade;        
00368         pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
00369         s_nBTLimitGlobal  = 0;
00370         s_nInsLimitGlobal = 0;        
00371         RetValue = Ivy_FraigMiterStatus( pManAig );
00372         Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
00373         // make sure that the sover never returns "undecided" when infinite resource limits are set
00374         if( RetValue == -1 && pParams->nTotalInspectLimit == 0 &&
00375             pParams->nTotalBacktrackLimit == 0 )
00376         {
00377             extern void Prove_ParamsPrint( Prove_Params_t * pParams );
00378             Prove_ParamsPrint( pParams );
00379             printf("ERROR: ABC has returned \"undecided\" in spite of no limits...\n");
00380             exit(1);
00381         }
00382     }
00383 
00384     // assign the model if it was proved by rewriting (const 1 miter)
00385     if ( RetValue == 0 && pManAig->pData == NULL )
00386     {
00387         pManAig->pData = ALLOC( int, Ivy_ManPiNum(pManAig) );
00388         memset( pManAig->pData, 0, sizeof(int) * Ivy_ManPiNum(pManAig) );
00389     }
00390     *ppManAig = pManAig;
00391     return RetValue;
00392 }
00393 
00405 Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, sint64 nBTLimitGlobal, sint64 nInsLimitGlobal, sint64 * pnSatConfs, sint64 * pnSatInspects )
00406 { 
00407     Ivy_FraigMan_t * p;
00408     Ivy_Man_t * pManAigNew;
00409     int clk;
00410     if ( Ivy_ManNodeNum(pManAig) == 0 )
00411         return Ivy_ManDup(pManAig);
00412 clk = clock();
00413     assert( Ivy_ManLatchNum(pManAig) == 0 );
00414     p = Ivy_FraigStart( pManAig, pParams );
00415     // set global limits
00416     p->nBTLimitGlobal  = nBTLimitGlobal;
00417     p->nInsLimitGlobal = nInsLimitGlobal; 
00418     
00419     Ivy_FraigSimulate( p );
00420     Ivy_FraigSweep( p );
00421     pManAigNew = p->pManFraig;
00422 p->timeTotal = clock() - clk;
00423     if ( pnSatConfs )
00424         *pnSatConfs = p->pSat? p->pSat->stats.conflicts : 0;
00425     if ( pnSatInspects )
00426         *pnSatInspects = p->pSat? p->pSat->stats.inspects : 0;
00427     Ivy_FraigStop( p );
00428     return pManAigNew;
00429 }
00430 
00442 Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
00443 {
00444     Ivy_FraigMan_t * p;
00445     Ivy_Man_t * pManAigNew;
00446     int clk;
00447     if ( Ivy_ManNodeNum(pManAig) == 0 )
00448         return Ivy_ManDup(pManAig);
00449 clk = clock();
00450     assert( Ivy_ManLatchNum(pManAig) == 0 );
00451     p = Ivy_FraigStart( pManAig, pParams );
00452     Ivy_FraigSimulate( p );
00453     Ivy_FraigSweep( p );
00454     pManAigNew = p->pManFraig;
00455 p->timeTotal = clock() - clk;
00456     Ivy_FraigStop( p );
00457     return pManAigNew;
00458 }
00459 
00471 Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
00472 {
00473     Ivy_FraigMan_t * p;
00474     Ivy_Man_t * pManAigNew;
00475     Ivy_Obj_t * pObj;
00476     int i, clk;
00477 clk = clock();
00478     assert( Ivy_ManLatchNum(pManAig) == 0 );
00479     p = Ivy_FraigStartSimple( pManAig, pParams );
00480     // set global limits
00481     p->nBTLimitGlobal  = s_nBTLimitGlobal;
00482     p->nInsLimitGlobal = s_nInsLimitGlobal; 
00483     // duplicate internal nodes
00484     Ivy_ManForEachNode( p->pManAig, pObj, i )
00485         pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
00486     // try to prove each output of the miter
00487     Ivy_FraigMiterProve( p );
00488     // add the POs
00489     Ivy_ManForEachPo( p->pManAig, pObj, i )
00490         Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
00491     // clean the new manager
00492     Ivy_ManForEachObj( p->pManFraig, pObj, i )
00493     {
00494         if ( Ivy_ObjFaninVec(pObj) )
00495             Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
00496         pObj->pNextFan0 = pObj->pNextFan1 = NULL;
00497     }
00498     // remove dangling nodes 
00499     Ivy_ManCleanup( p->pManFraig );
00500     pManAigNew = p->pManFraig;
00501 p->timeTotal = clock() - clk;
00502 
00503 //printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) );
00504 //PRT( "Time", p->timeTotal );
00505     Ivy_FraigStop( p );
00506     return pManAigNew;
00507 }
00508 
00520 Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
00521 {
00522     Ivy_FraigMan_t * p;
00523     // allocat the fraiging manager
00524     p = ALLOC( Ivy_FraigMan_t, 1 );
00525     memset( p, 0, sizeof(Ivy_FraigMan_t) );
00526     p->pParams   = pParams;
00527     p->pManAig   = pManAig;
00528     p->pManFraig = Ivy_ManStartFrom( pManAig );
00529     p->vPiVars   = Vec_PtrAlloc( 100 );
00530     return p;
00531 }
00532 
00544 Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
00545 {
00546     Ivy_FraigMan_t * p;
00547     Ivy_FraigSim_t * pSims;
00548     Ivy_Obj_t * pObj;
00549     int i, k, EntrySize;
00550     // clean the fanout representation
00551     Ivy_ManForEachObj( pManAig, pObj, i )
00552 //        pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
00553         assert( !pObj->pEquiv && !pObj->pFanout );
00554     // allocat the fraiging manager
00555     p = ALLOC( Ivy_FraigMan_t, 1 );
00556     memset( p, 0, sizeof(Ivy_FraigMan_t) );
00557     p->pParams   = pParams;
00558     p->pManAig   = pManAig;
00559     p->pManFraig = Ivy_ManStartFrom( pManAig );
00560     // allocate simulation info
00561     p->nSimWords    = pParams->nSimWords;
00562 //    p->pSimWords    = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nSimWords ); 
00563     EntrySize    = sizeof(Ivy_FraigSim_t) + sizeof(unsigned) * p->nSimWords;
00564     p->pSimWords = (char *)malloc( Ivy_ManObjNum(pManAig) * EntrySize ); 
00565     memset( p->pSimWords, 0, EntrySize );
00566     k = 0;
00567     Ivy_ManForEachObj( pManAig, pObj, i )
00568     {
00569         pSims = (Ivy_FraigSim_t *)(p->pSimWords + EntrySize * k++);
00570         pSims->pNext = NULL;
00571         if ( Ivy_ObjIsNode(pObj) )
00572         {
00573             if ( p->pSimStart == NULL )
00574                 p->pSimStart = pSims;
00575             else
00576                 ((Ivy_FraigSim_t *)(p->pSimWords + EntrySize * (k-2)))->pNext = pSims;
00577             pSims->pFanin0 = Ivy_ObjSim( Ivy_ObjFanin0(pObj) );
00578             pSims->pFanin1 = Ivy_ObjSim( Ivy_ObjFanin1(pObj) );
00579             pSims->Type = (Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) << 2) | (Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)) << 1) | pObj->fPhase;
00580         }
00581         else
00582         {
00583             pSims->pFanin0 = NULL;
00584             pSims->pFanin1 = NULL;
00585             pSims->Type = 0;
00586         }
00587         Ivy_ObjSetSim( pObj, pSims );
00588     }
00589     assert( k == Ivy_ManObjNum(pManAig) );
00590     // allocate storage for sim pattern
00591     p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
00592     p->pPatWords = ALLOC( unsigned, p->nPatWords ); 
00593     p->pPatScores = ALLOC( int, 32 * p->nSimWords ); 
00594     p->vPiVars   = Vec_PtrAlloc( 100 );
00595     // set random number generator
00596     srand( 0xABCABC );
00597     return p;
00598 }
00599 
00611 void Ivy_FraigStop( Ivy_FraigMan_t * p )
00612 {
00613     if ( p->pParams->fVerbose )
00614         Ivy_FraigPrint( p );
00615     if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
00616     if ( p->pSat ) sat_solver_delete( p->pSat );
00617     FREE( p->pPatScores );
00618     FREE( p->pPatWords );
00619     FREE( p->pSimWords );
00620     free( p );
00621 }
00622 
00634 void Ivy_FraigPrint( Ivy_FraigMan_t * p )
00635 {
00636     double nMemory;
00637     nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nSimWords*sizeof(unsigned)/(1<<20);
00638     printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb.  ", p->nSimWords, p->nSimRounds, nMemory );
00639     printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
00640     printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pParams->nBTLimitNode, p->pParams->nBTLimitMiter );
00641     printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
00642         p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
00643     printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", 
00644         Ivy_ManNodeNum(p->pManFraig), p->nNodesMiter, Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
00645     if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
00646     PRT( "AIG simulation  ", p->timeSim  );
00647     PRT( "AIG traversal   ", p->timeTrav  );
00648     PRT( "SAT solving     ", p->timeSat   );
00649     PRT( "    Unsat       ", p->timeSatUnsat );
00650     PRT( "    Sat         ", p->timeSatSat   );
00651     PRT( "    Fail        ", p->timeSatFail  );
00652     PRT( "Class refining  ", p->timeRef   );
00653     PRT( "TOTAL RUNTIME   ", p->timeTotal );
00654     if ( p->time1 ) { PRT( "time1           ", p->time1 ); }
00655 }
00656 
00657 
00658 
00670 void Ivy_NodeAssignRandom( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
00671 {
00672     Ivy_FraigSim_t * pSims;
00673     int i;
00674     assert( Ivy_ObjIsPi(pObj) );
00675     pSims = Ivy_ObjSim(pObj);
00676     for ( i = 0; i < p->nSimWords; i++ )
00677         pSims->pData[i] = Ivy_ObjRandomSim();
00678 }
00679 
00691 void Ivy_NodeAssignConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int fConst1 )
00692 {
00693     Ivy_FraigSim_t * pSims;
00694     int i;
00695     assert( Ivy_ObjIsPi(pObj) );
00696     pSims = Ivy_ObjSim(pObj);
00697     for ( i = 0; i < p->nSimWords; i++ )
00698         pSims->pData[i] = fConst1? ~(unsigned)0 : 0;
00699 }
00700 
00712 void Ivy_FraigAssignRandom( Ivy_FraigMan_t * p )
00713 {
00714     Ivy_Obj_t * pObj;
00715     int i;
00716     Ivy_ManForEachPi( p->pManAig, pObj, i )
00717         Ivy_NodeAssignRandom( p, pObj );
00718 }
00719 
00731 void Ivy_FraigAssignDist1( Ivy_FraigMan_t * p, unsigned * pPat )
00732 {
00733     Ivy_Obj_t * pObj;
00734     int i, Limit;
00735     Ivy_ManForEachPi( p->pManAig, pObj, i )
00736     {
00737         Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) );
00738 //        printf( "%d", Ivy_InfoHasBit(pPat, i) );
00739     }
00740 //    printf( "\n" );
00741 
00742     Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
00743     for ( i = 0; i < Limit; i++ )
00744         Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 );
00745 }
00746 
00758 int Ivy_NodeHasZeroSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
00759 {
00760     Ivy_FraigSim_t * pSims;
00761     int i;
00762     pSims = Ivy_ObjSim(pObj);
00763     for ( i = 0; i < p->nSimWords; i++ )
00764         if ( pSims->pData[i] )
00765             return 0;
00766     return 1;
00767 }
00768 
00780 void Ivy_NodeComplementSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
00781 {
00782     Ivy_FraigSim_t * pSims;
00783     int i;
00784     pSims = Ivy_ObjSim(pObj);
00785     for ( i = 0; i < p->nSimWords; i++ )
00786         pSims->pData[i] = ~pSims->pData[i];
00787 }
00788 
00800 int Ivy_NodeCompareSims( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
00801 {
00802     Ivy_FraigSim_t * pSims0, * pSims1;
00803     int i;
00804     pSims0 = Ivy_ObjSim(pObj0);
00805     pSims1 = Ivy_ObjSim(pObj1);
00806     for ( i = 0; i < p->nSimWords; i++ )
00807         if ( pSims0->pData[i] != pSims1->pData[i] )
00808             return 0;
00809     return 1;
00810 }
00811 
00823 void Ivy_NodeSimulateSim( Ivy_FraigMan_t * p, Ivy_FraigSim_t * pSims )
00824 {
00825     unsigned * pData, * pData0, * pData1;
00826     int i;
00827     pData  = pSims->pData;
00828     pData0 = pSims->pFanin0->pData;
00829     pData1 = pSims->pFanin1->pData;
00830     switch( pSims->Type )
00831     {
00832     case 0:
00833         for ( i = 0; i < p->nSimWords; i++ )
00834             pData[i] = (pData0[i] & pData1[i]);
00835         break;
00836     case 1:
00837         for ( i = 0; i < p->nSimWords; i++ )
00838             pData[i] = ~(pData0[i] & pData1[i]);
00839         break;
00840     case 2:
00841         for ( i = 0; i < p->nSimWords; i++ )
00842             pData[i] = (pData0[i] & ~pData1[i]);
00843         break;
00844     case 3:
00845         for ( i = 0; i < p->nSimWords; i++ )
00846             pData[i] = (~pData0[i] | pData1[i]);
00847         break;
00848     case 4:
00849         for ( i = 0; i < p->nSimWords; i++ )
00850             pData[i] = (~pData0[i] & pData1[i]);
00851         break;
00852     case 5:
00853         for ( i = 0; i < p->nSimWords; i++ )
00854             pData[i] = (pData0[i] | ~pData1[i]);
00855         break;
00856     case 6:
00857         for ( i = 0; i < p->nSimWords; i++ )
00858             pData[i] = ~(pData0[i] | pData1[i]);
00859         break;
00860     case 7:
00861         for ( i = 0; i < p->nSimWords; i++ )
00862             pData[i] = (pData0[i] | pData1[i]);
00863         break;
00864     }
00865 }
00866 
00878 void Ivy_NodeSimulate( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
00879 {
00880     Ivy_FraigSim_t * pSims, * pSims0, * pSims1;
00881     int fCompl, fCompl0, fCompl1, i;
00882     assert( !Ivy_IsComplement(pObj) );
00883     // get hold of the simulation information
00884     pSims  = Ivy_ObjSim(pObj);
00885     pSims0 = Ivy_ObjSim(Ivy_ObjFanin0(pObj));
00886     pSims1 = Ivy_ObjSim(Ivy_ObjFanin1(pObj));
00887     // get complemented attributes of the children using their random info
00888     fCompl  = pObj->fPhase;
00889     fCompl0 = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj));
00890     fCompl1 = Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj));
00891     // simulate
00892     if ( fCompl0 && fCompl1 )
00893     {
00894         if ( fCompl )
00895             for ( i = 0; i < p->nSimWords; i++ )
00896                 pSims->pData[i] = (pSims0->pData[i] | pSims1->pData[i]);
00897         else
00898             for ( i = 0; i < p->nSimWords; i++ )
00899                 pSims->pData[i] = ~(pSims0->pData[i] | pSims1->pData[i]);
00900     }
00901     else if ( fCompl0 && !fCompl1 )
00902     {
00903         if ( fCompl )
00904             for ( i = 0; i < p->nSimWords; i++ )
00905                 pSims->pData[i] = (pSims0->pData[i] | ~pSims1->pData[i]);
00906         else
00907             for ( i = 0; i < p->nSimWords; i++ )
00908                 pSims->pData[i] = (~pSims0->pData[i] & pSims1->pData[i]);
00909     }
00910     else if ( !fCompl0 && fCompl1 )
00911     {
00912         if ( fCompl )
00913             for ( i = 0; i < p->nSimWords; i++ )
00914                 pSims->pData[i] = (~pSims0->pData[i] | pSims1->pData[i]);
00915         else
00916             for ( i = 0; i < p->nSimWords; i++ )
00917                 pSims->pData[i] = (pSims0->pData[i] & ~pSims1->pData[i]);
00918     }
00919     else // if ( !fCompl0 && !fCompl1 )
00920     {
00921         if ( fCompl )
00922             for ( i = 0; i < p->nSimWords; i++ )
00923                 pSims->pData[i] = ~(pSims0->pData[i] & pSims1->pData[i]);
00924         else
00925             for ( i = 0; i < p->nSimWords; i++ )
00926                 pSims->pData[i] = (pSims0->pData[i] & pSims1->pData[i]);
00927     }
00928 }
00929 
00941 unsigned Ivy_NodeHash( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
00942 {
00943     static int s_FPrimes[128] = { 
00944         1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
00945         1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
00946         2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
00947         2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
00948         3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
00949         3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
00950         4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
00951         4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
00952         5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
00953         6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
00954         6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
00955         7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
00956         8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
00957     };
00958     Ivy_FraigSim_t * pSims;
00959     unsigned uHash;
00960     int i;
00961     assert( p->nSimWords <= 128 );
00962     uHash = 0;
00963     pSims  = Ivy_ObjSim(pObj);
00964     for ( i = 0; i < p->nSimWords; i++ )
00965         uHash ^= pSims->pData[i] * s_FPrimes[i];
00966     return uHash;
00967 }
00968 
00980 void Ivy_FraigSimulateOne( Ivy_FraigMan_t * p )
00981 {
00982     Ivy_Obj_t * pObj;
00983     int i, clk;
00984 clk = clock();
00985     Ivy_ManForEachNode( p->pManAig, pObj, i )
00986     {
00987         Ivy_NodeSimulate( p, pObj );
00988 /*
00989         if ( Ivy_ObjFraig(pObj) == NULL )
00990             printf( "%3d --- -- %d  :  ", pObj->Id, pObj->fPhase );
00991         else
00992             printf( "%3d %3d %2d %d  :  ", pObj->Id, Ivy_Regular(Ivy_ObjFraig(pObj))->Id, Ivy_ObjSatNum(Ivy_Regular(Ivy_ObjFraig(pObj))), pObj->fPhase );
00993         Extra_PrintBinary( stdout, Ivy_ObjSim(pObj), 30 );
00994         printf( "\n" );
00995 */
00996     }
00997 p->timeSim += clock() - clk;
00998 p->nSimRounds++;
00999 }
01000 
01012 void Ivy_FraigSimulateOneSim( Ivy_FraigMan_t * p )
01013 {
01014     Ivy_FraigSim_t * pSims;
01015     int clk;
01016 clk = clock();
01017     for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext )
01018         Ivy_NodeSimulateSim( p, pSims );
01019 p->timeSim += clock() - clk;
01020 p->nSimRounds++;
01021 }
01022 
01034 void Ivy_NodeAddToClass( Ivy_Obj_t * pClass, Ivy_Obj_t * pObj )
01035 {
01036     if ( Ivy_ObjClassNodeNext(pClass) == NULL )
01037         Ivy_ObjSetClassNodeNext( pClass, pObj );
01038     else
01039         Ivy_ObjSetClassNodeNext( Ivy_ObjClassNodeLast(pClass), pObj );
01040     Ivy_ObjSetClassNodeLast( pClass, pObj );
01041     Ivy_ObjSetClassNodeRepr( pObj, pClass );
01042     Ivy_ObjSetClassNodeNext( pObj, NULL );
01043 }
01044 
01056 void Ivy_FraigAddClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass )
01057 {
01058     if ( pList->pHead == NULL )
01059     {
01060         pList->pHead = pClass;
01061         pList->pTail = pClass;
01062         Ivy_ObjSetEquivListPrev( pClass, NULL );
01063         Ivy_ObjSetEquivListNext( pClass, NULL ); 
01064     }
01065     else
01066     {
01067         Ivy_ObjSetEquivListNext( pList->pTail, pClass ); 
01068         Ivy_ObjSetEquivListPrev( pClass, pList->pTail );
01069         Ivy_ObjSetEquivListNext( pClass, NULL ); 
01070         pList->pTail = pClass;
01071     }
01072     pList->nItems++;
01073 }
01074  
01086 void Ivy_FraigInsertClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pBase, Ivy_Obj_t * pClass )
01087 {
01088     Ivy_ObjSetEquivListPrev( pClass, pBase );
01089     Ivy_ObjSetEquivListNext( pClass, Ivy_ObjEquivListNext(pBase) ); 
01090     if ( Ivy_ObjEquivListNext(pBase) )
01091         Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pBase), pClass );
01092     Ivy_ObjSetEquivListNext( pBase, pClass ); 
01093     if ( pList->pTail == pBase )
01094         pList->pTail = pClass;
01095     pList->nItems++;
01096 }
01097 
01109 void Ivy_FraigRemoveClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass )
01110 {
01111     if ( pList->pHead == pClass )
01112         pList->pHead = Ivy_ObjEquivListNext(pClass);
01113     if ( pList->pTail == pClass )
01114         pList->pTail = Ivy_ObjEquivListPrev(pClass);
01115     if ( Ivy_ObjEquivListPrev(pClass) )
01116         Ivy_ObjSetEquivListNext( Ivy_ObjEquivListPrev(pClass), Ivy_ObjEquivListNext(pClass) ); 
01117     if ( Ivy_ObjEquivListNext(pClass) )
01118         Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pClass), Ivy_ObjEquivListPrev(pClass) );
01119     Ivy_ObjSetEquivListNext( pClass, NULL ); 
01120     Ivy_ObjSetEquivListPrev( pClass, NULL );
01121     pClass->fMarkA = 0;
01122     pList->nItems--;
01123 }
01124 
01136 int Ivy_FraigCountPairsClasses( Ivy_FraigMan_t * p )
01137 {
01138     Ivy_Obj_t * pClass, * pNode;
01139     int nPairs = 0, nNodes;
01140     return nPairs;
01141 
01142     Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
01143     {
01144         nNodes = 0;
01145         Ivy_FraigForEachClassNode( pClass, pNode )
01146             nNodes++;
01147         nPairs += nNodes * (nNodes - 1) / 2;
01148     }
01149     return nPairs;
01150 }
01151 
01163 void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p )
01164 {
01165     Ivy_Obj_t ** pTable;
01166     Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry;
01167     int i, nTableSize;
01168     unsigned Hash;
01169     pConst1 = Ivy_ManConst1(p->pManAig);
01170     // allocate the table
01171     nTableSize = Ivy_ManObjNum(p->pManAig) / 2 + 13;
01172     pTable = ALLOC( Ivy_Obj_t *, nTableSize ); 
01173     memset( pTable, 0, sizeof(Ivy_Obj_t *) * nTableSize );
01174     // collect nodes into the table
01175     Ivy_ManForEachObj( p->pManAig, pObj, i )
01176     {
01177         if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
01178             continue;
01179         Hash = Ivy_NodeHash( p, pObj );
01180         if ( Hash == 0 && Ivy_NodeHasZeroSim( p, pObj ) )
01181         {
01182             Ivy_NodeAddToClass( pConst1, pObj );
01183             continue;
01184         }
01185         // add the node to the table
01186         pBin = pTable[Hash % nTableSize];
01187         Ivy_FraigForEachBinNode( pBin, pEntry )
01188             if ( Ivy_NodeCompareSims( p, pEntry, pObj ) )
01189             {
01190                 Ivy_NodeAddToClass( pEntry, pObj );
01191                 break;
01192             }
01193         // check if the entry was added
01194         if ( pEntry )
01195             continue;
01196         Ivy_ObjSetNodeHashNext( pObj, pBin );
01197         pTable[Hash % nTableSize] = pObj;
01198     }
01199     // collect non-trivial classes
01200     assert( p->lClasses.pHead == NULL );
01201     Ivy_ManForEachObj( p->pManAig, pObj, i )
01202     {
01203         if ( !Ivy_ObjIsConst1(pObj) && !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
01204             continue;
01205         Ivy_ObjSetNodeHashNext( pObj, NULL );
01206         if ( Ivy_ObjClassNodeRepr(pObj) == NULL )
01207         {
01208             assert( Ivy_ObjClassNodeNext(pObj) == NULL );
01209             continue;
01210         }
01211         // recognize the head of the class
01212         if ( Ivy_ObjClassNodeNext( Ivy_ObjClassNodeRepr(pObj) ) != NULL )
01213             continue;
01214         // clean the class representative and add it to the list
01215         Ivy_ObjSetClassNodeRepr( pObj, NULL );
01216         Ivy_FraigAddClass( &p->lClasses, pObj );
01217     }
01218     // free the table
01219     free( pTable );
01220 }
01221 
01233 int Ivy_FraigRefineClass_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass )
01234 {
01235     Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode;
01236     int RetValue = 0;
01237     // check if there is refinement
01238     pListOld = pClass;
01239     Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew )
01240     {
01241         if ( !Ivy_NodeCompareSims(p, pClass, pClassNew) )
01242         {
01243             if ( p->pParams->fPatScores )
01244                 Ivy_FraigAddToPatScores( p, pClass, pClassNew );
01245             break;
01246         }
01247         pListOld = pClassNew;
01248     }
01249     if ( pClassNew == NULL )
01250         return 0;
01251     // set representative of the new class
01252     Ivy_ObjSetClassNodeRepr( pClassNew, NULL );
01253     // start the new list
01254     pListNew = pClassNew;
01255     // go through the remaining nodes and sort them into two groups:
01256     // (1) matches of the old node; (2) non-matches of the old node
01257     Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClassNew), pNode )
01258         if ( Ivy_NodeCompareSims( p, pClass, pNode ) )
01259         {
01260             Ivy_ObjSetClassNodeNext( pListOld, pNode );
01261             pListOld = pNode;
01262         }
01263         else
01264         {
01265             Ivy_ObjSetClassNodeNext( pListNew, pNode );
01266             Ivy_ObjSetClassNodeRepr( pNode, pClassNew );
01267             pListNew = pNode;
01268         }
01269     // finish both lists
01270     Ivy_ObjSetClassNodeNext( pListNew, NULL );
01271     Ivy_ObjSetClassNodeNext( pListOld, NULL );
01272     // update the list of classes
01273     Ivy_FraigInsertClass( &p->lClasses, pClass, pClassNew );
01274     // if the old class is trivial, remove it
01275     if ( Ivy_ObjClassNodeNext(pClass) == NULL )
01276         Ivy_FraigRemoveClass( &p->lClasses, pClass );
01277     // if the new class is trivial, remove it; otherwise, try to refine it
01278     if ( Ivy_ObjClassNodeNext(pClassNew) == NULL )
01279         Ivy_FraigRemoveClass( &p->lClasses, pClassNew );
01280     else
01281         RetValue = Ivy_FraigRefineClass_rec( p, pClassNew );
01282     return RetValue + 1;
01283 }
01284  
01296 void Ivy_FraigCheckOutputSimsSavePattern( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
01297 { 
01298     Ivy_FraigSim_t * pSims;
01299     int i, k, BestPat, * pModel;
01300     // find the word of the pattern
01301     pSims = Ivy_ObjSim(pObj);
01302     for ( i = 0; i < p->nSimWords; i++ )
01303         if ( pSims->pData[i] )
01304             break;
01305     assert( i < p->nSimWords );
01306     // find the bit of the pattern
01307     for ( k = 0; k < 32; k++ )
01308         if ( pSims->pData[i] & (1 << k) )
01309             break;
01310     assert( k < 32 );
01311     // determine the best pattern
01312     BestPat = i * 32 + k;
01313     // fill in the counter-example data
01314     pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
01315     Ivy_ManForEachPi( p->pManAig, pObj, i )
01316     {
01317         pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat);
01318 //        printf( "%d", pModel[i] );
01319     }
01320 //    printf( "\n" );
01321     // set the model
01322     assert( p->pManFraig->pData == NULL );
01323     p->pManFraig->pData = pModel;
01324     return;
01325 }
01326 
01338 int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
01339 {
01340     Ivy_Obj_t * pObj;
01341     int i;
01342     // make sure the reference simulation pattern does not detect the bug
01343     pObj = Ivy_ManPo( p->pManAig, 0 );
01344     assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0
01345     Ivy_ManForEachPo( p->pManAig, pObj, i )
01346     {
01347         // complement simulation info
01348 //        if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj))
01349 //            Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
01350         // check 
01351         if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) )
01352         {
01353             // create the counter-example from this pattern
01354             Ivy_FraigCheckOutputSimsSavePattern( p, Ivy_ObjFanin0(pObj) );
01355             return 1;
01356         }
01357         // complement simulation info
01358 //        if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) )
01359 //            Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
01360     }
01361     return 0;
01362 }
01363 
01376 int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p )
01377 {
01378     Ivy_Obj_t * pClass, * pClass2;
01379     int clk, RetValue, Counter = 0;
01380     // check if some outputs already became non-constant
01381     // this is a special case when computation can be stopped!!!
01382     if ( p->pParams->fProve )
01383         Ivy_FraigCheckOutputSims( p );
01384     if ( p->pManFraig->pData )
01385         return 0;
01386     // refine the classed
01387 clk = clock();
01388     Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 )
01389     {
01390         if ( pClass->fMarkA )
01391             continue;
01392         RetValue = Ivy_FraigRefineClass_rec( p, pClass );
01393         Counter += ( RetValue > 0 );
01394 //if ( Ivy_ObjIsConst1(pClass) )
01395 //printf( "%d ", RetValue );
01396 //if ( Ivy_ObjIsConst1(pClass) )
01397 //    p->time1 += clock() - clk;
01398     }
01399 p->timeRef += clock() - clk;
01400     return Counter;
01401 }
01402 
01414 void Ivy_FraigPrintClass( Ivy_Obj_t * pClass )
01415 {
01416     Ivy_Obj_t * pObj;
01417     printf( "Class {" );
01418     Ivy_FraigForEachClassNode( pClass, pObj )
01419         printf( " %d(%d)%c", pObj->Id, pObj->Level, pObj->fPhase? '+' : '-' );
01420     printf( " }\n" );
01421 }
01422 
01434 int Ivy_FraigCountClassNodes( Ivy_Obj_t * pClass )
01435 {
01436     Ivy_Obj_t * pObj;
01437     int Counter = 0;
01438     Ivy_FraigForEachClassNode( pClass, pObj )
01439         Counter++;
01440     return Counter;
01441 }
01442 
01454 void Ivy_FraigPrintSimClasses( Ivy_FraigMan_t * p )
01455 {
01456     Ivy_Obj_t * pClass;
01457     Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
01458     {
01459 //        Ivy_FraigPrintClass( pClass );
01460         printf( "%d ", Ivy_FraigCountClassNodes( pClass ) );
01461     }
01462 //    printf( "\n" );
01463 }
01464 
01476 void Ivy_FraigSavePattern0( Ivy_FraigMan_t * p )
01477 {
01478     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
01479 }
01480 
01492 void Ivy_FraigSavePattern1( Ivy_FraigMan_t * p )
01493 {
01494     memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
01495 }
01496 
01508 int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p )
01509 {
01510     int * pModel;
01511     Ivy_Obj_t * pObj;
01512     int i;
01513     pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
01514     Ivy_ManForEachPi( p->pManFraig, pObj, i )
01515         pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True );
01516     return pModel;
01517 }
01518 
01530 void Ivy_FraigSavePattern( Ivy_FraigMan_t * p )
01531 {
01532     Ivy_Obj_t * pObj;
01533     int i;
01534     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
01535     Ivy_ManForEachPi( p->pManFraig, pObj, i )
01536 //    Vec_PtrForEachEntry( p->vPiVars, pObj, i )
01537         if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
01538             Ivy_InfoSetBit( p->pPatWords, i );
01539 //            Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
01540 }
01541 
01553 void Ivy_FraigSavePattern2( Ivy_FraigMan_t * p )
01554 {
01555     Ivy_Obj_t * pObj;
01556     int i;
01557     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
01558 //    Ivy_ManForEachPi( p->pManFraig, pObj, i )
01559     Vec_PtrForEachEntry( p->vPiVars, pObj, i )
01560         if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
01561 //            Ivy_InfoSetBit( p->pPatWords, i );
01562             Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
01563 }
01564 
01576 void Ivy_FraigSavePattern3( Ivy_FraigMan_t * p )
01577 {
01578     Ivy_Obj_t * pObj;
01579     int i;
01580     for ( i = 0; i < p->nPatWords; i++ )
01581         p->pPatWords[i] = Ivy_ObjRandomSim();
01582     Vec_PtrForEachEntry( p->vPiVars, pObj, i )
01583         if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) )
01584             Ivy_InfoXorBit( p->pPatWords, pObj->Id - 1 );
01585 }
01586 
01587 
01599 void Ivy_FraigSimulate( Ivy_FraigMan_t * p )
01600 {
01601     int nChanges, nClasses;
01602     // start the classes
01603     Ivy_FraigAssignRandom( p );
01604     Ivy_FraigSimulateOne( p );
01605     Ivy_FraigCreateClasses( p );
01606 //printf( "Starting classes = %5d.   Pairs = %6d.\n", p->lClasses.nItems, Ivy_FraigCountPairsClasses(p) );
01607     // refine classes by walking 0/1 patterns
01608     Ivy_FraigSavePattern0( p );
01609     Ivy_FraigAssignDist1( p, p->pPatWords );
01610     Ivy_FraigSimulateOne( p );
01611     nChanges = Ivy_FraigRefineClasses( p );
01612     if ( p->pManFraig->pData )
01613         return;
01614 //printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
01615     Ivy_FraigSavePattern1( p );
01616     Ivy_FraigAssignDist1( p, p->pPatWords );
01617     Ivy_FraigSimulateOne( p );
01618     nChanges = Ivy_FraigRefineClasses( p );
01619     if ( p->pManFraig->pData )
01620         return;
01621 //printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
01622     // refine classes by random simulation
01623     do {
01624         Ivy_FraigAssignRandom( p );
01625         Ivy_FraigSimulateOne( p );
01626         nClasses = p->lClasses.nItems;
01627         nChanges = Ivy_FraigRefineClasses( p );
01628         if ( p->pManFraig->pData )
01629             return;
01630 //printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
01631     } while ( (double)nChanges / nClasses > p->pParams->dSimSatur );
01632 //    Ivy_FraigPrintSimClasses( p );
01633 }
01634 
01635 
01636 
01648 void Ivy_FraigCleanPatScores( Ivy_FraigMan_t * p )
01649 {
01650     int i, nLimit = p->nSimWords * 32;
01651     for ( i = 0; i < nLimit; i++ )
01652         p->pPatScores[i] = 0;
01653 }
01654 
01666 void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew )
01667 {
01668     Ivy_FraigSim_t * pSims0, * pSims1;
01669     unsigned uDiff;
01670     int i, w;
01671     // get hold of the simulation information
01672     pSims0 = Ivy_ObjSim(pClass);
01673     pSims1 = Ivy_ObjSim(pClassNew);
01674     // iterate through the differences and record the score
01675     for ( w = 0; w < p->nSimWords; w++ )
01676     {
01677         uDiff = pSims0->pData[w] ^ pSims1->pData[w];
01678         if ( uDiff == 0 )
01679             continue;
01680         for ( i = 0; i < 32; i++ )
01681             if ( uDiff & ( 1 << i ) )
01682                 p->pPatScores[w*32+i]++;
01683     }
01684 }
01685 
01697 int Ivy_FraigSelectBestPat( Ivy_FraigMan_t * p )
01698 {
01699     Ivy_FraigSim_t * pSims;
01700     Ivy_Obj_t * pObj;
01701     int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1;
01702     for ( i = 1; i < nLimit; i++ )
01703     {
01704         if ( MaxScore < p->pPatScores[i] )
01705         {
01706             MaxScore = p->pPatScores[i];
01707             BestPat = i;
01708         }
01709     }
01710     if ( MaxScore == 0 )
01711         return 0;
01712 //    if ( MaxScore > p->pParams->MaxScore )
01713 //    printf( "Max score is %3d.  ", MaxScore );
01714     // copy the best pattern into the selected pattern
01715     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
01716     Ivy_ManForEachPi( p->pManAig, pObj, i )
01717     {
01718         pSims = Ivy_ObjSim(pObj);
01719         if ( Ivy_InfoHasBit(pSims->pData, BestPat) )
01720             Ivy_InfoSetBit(p->pPatWords, i);
01721     }
01722     return MaxScore;
01723 }
01724 
01736 void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
01737 {
01738     int nChanges;
01739     Ivy_FraigAssignDist1( p, p->pPatWords );
01740     Ivy_FraigSimulateOne( p );
01741     if ( p->pParams->fPatScores )
01742         Ivy_FraigCleanPatScores( p );
01743     nChanges = Ivy_FraigRefineClasses( p );
01744     if ( p->pManFraig->pData )
01745         return;
01746     if ( nChanges < 1 )
01747         printf( "Error: A counter-example did not refine classes!\n" );
01748     assert( nChanges >= 1 );
01749 //printf( "Refined classes! = %5d.   Changes = %4d.\n", p->lClasses.nItems, nChanges );
01750     if ( !p->pParams->fPatScores )
01751         return;
01752 
01753     // perform additional simulation using dist1 patterns derived from successful patterns
01754     while ( Ivy_FraigSelectBestPat(p) > p->pParams->MaxScore )
01755     {
01756         Ivy_FraigAssignDist1( p, p->pPatWords );
01757         Ivy_FraigSimulateOne( p );
01758         Ivy_FraigCleanPatScores( p );
01759         nChanges = Ivy_FraigRefineClasses( p );
01760         if ( p->pManFraig->pData )
01761             return;
01762 //printf( "Refined class!!! = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
01763         if ( nChanges == 0 )
01764             break;
01765     }
01766 }
01767 
01768 
01780 void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose )
01781 {
01782     if ( !fVerbose )
01783         return;
01784     printf( "Nodes = %7d.  Levels = %4d.  ", Ivy_ManNodeNum(pNtk), Ivy_ManLevels(pNtk) );
01785     PRT( pString, clock() - clk );
01786 }
01787 
01799 int Ivy_FraigMiterStatus( Ivy_Man_t * pMan )
01800 {
01801     Ivy_Obj_t * pObj, * pObjNew;
01802     int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
01803     if ( pMan->pData )
01804         return 0;
01805     Ivy_ManForEachPo( pMan, pObj, i )
01806     {
01807         pObjNew = Ivy_ObjChild0(pObj);
01808         // check if the output is constant 1
01809         if ( pObjNew == pMan->pConst1 )
01810         {
01811             CountNonConst0++;
01812             continue;
01813         }
01814         // check if the output is constant 0
01815         if ( pObjNew == Ivy_Not(pMan->pConst1) )
01816         {
01817             CountConst0++;
01818             continue;
01819         }
01820         // check if the output can be constant 0
01821         if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
01822         {
01823             CountNonConst0++;
01824             continue;
01825         }
01826         CountUndecided++;
01827     }
01828 /*
01829     if ( p->pParams->fVerbose )
01830     {
01831         printf( "Miter has %d outputs. ", Ivy_ManPoNum(p->pManAig) );
01832         printf( "Const0 = %d.  ", CountConst0 );
01833         printf( "NonConst0 = %d.  ", CountNonConst0 );
01834         printf( "Undecided = %d.  ", CountUndecided );
01835         printf( "\n" );
01836     }
01837 */
01838     if ( CountNonConst0 )
01839         return 0;
01840     if ( CountUndecided )
01841         return -1;
01842     return 1;
01843 }
01844 
01856 void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
01857 {
01858     Ivy_Obj_t * pObj, * pObjNew;
01859     int i, RetValue, clk = clock();
01860     int fVerbose = 0;
01861     Ivy_ManForEachPo( p->pManAig, pObj, i )
01862     {
01863         if ( i && fVerbose )
01864         {
01865             PRT( "Time", clock() -clk );
01866         }
01867         pObjNew = Ivy_ObjChild0Equiv(pObj);
01868         // check if the output is constant 1
01869         if ( pObjNew == p->pManFraig->pConst1 )
01870         {
01871             if ( fVerbose )
01872                 printf( "Output %2d (out of %2d) is constant 1.  ", i, Ivy_ManPoNum(p->pManAig) );
01873             // assing constant 0 model
01874             p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
01875             memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
01876             break;
01877         }
01878         // check if the output is constant 0
01879         if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) )
01880         {
01881             if ( fVerbose )
01882                 printf( "Output %2d (out of %2d) is already constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
01883             continue;
01884         }
01885         // check if the output can be constant 0
01886         if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
01887         {
01888             if ( fVerbose )
01889                 printf( "Output %2d (out of %2d) cannot be constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
01890             // assing constant 0 model
01891             p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
01892             memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
01893             break;
01894         }
01895 /*
01896         // check the representative of this node
01897         pRepr = Ivy_ObjClassNodeRepr(Ivy_ObjFanin0(pObj));
01898         if ( Ivy_Regular(pRepr) != p->pManAig->pConst1 )
01899             printf( "Representative is not constant 1.\n" );
01900         else
01901             printf( "Representative is constant 1.\n" );
01902 */
01903         // try to prove the output constant 0
01904         RetValue = Ivy_FraigNodeIsConst( p, Ivy_Regular(pObjNew) );
01905         if ( RetValue == 1 )  // proved equivalent
01906         {
01907             if ( fVerbose )
01908                 printf( "Output %2d (out of %2d) was proved constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
01909             // set the constant miter
01910             Ivy_ObjFanin0(pObj)->pEquiv = Ivy_NotCond( p->pManFraig->pConst1, !Ivy_ObjFaninC0(pObj) );
01911             continue;
01912         }
01913         if ( RetValue == -1 ) // failed
01914         {
01915             if ( fVerbose )
01916                 printf( "Output %2d (out of %2d) has timed out at %d backtracks.  ", i, Ivy_ManPoNum(p->pManAig), p->pParams->nBTLimitMiter );
01917             continue;
01918         }
01919         // proved satisfiable
01920         if ( fVerbose )
01921             printf( "Output %2d (out of %2d) was proved NOT a constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
01922         // create the model
01923         p->pManFraig->pData = Ivy_FraigCreateModel(p);
01924         break;
01925     }
01926     if ( fVerbose )
01927     {
01928         PRT( "Time", clock() -clk );
01929     }
01930 }
01931 
01943 void Ivy_FraigSweep( Ivy_FraigMan_t * p )
01944 {
01945     Ivy_Obj_t * pObj;//, * pTemp;
01946     int i, k = 0;
01947 p->nClassesZero = p->lClasses.pHead? (Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0) : 0;
01948 p->nClassesBeg  = p->lClasses.nItems;
01949     // duplicate internal nodes
01950     p->pProgress = Extra_ProgressBarStart( stdout, Ivy_ManNodeNum(p->pManAig) );
01951     Ivy_ManForEachNode( p->pManAig, pObj, i )
01952     {
01953         Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
01954         // default to simple strashing if simulation detected a counter-example for a PO
01955         if ( p->pManFraig->pData )
01956             pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
01957         else
01958             pObj->pEquiv = Ivy_FraigAnd( p, pObj );
01959         assert( pObj->pEquiv != NULL );
01960 //        pTemp = Ivy_Regular(pObj->pEquiv);
01961 //        assert( Ivy_Regular(pObj->pEquiv)->Type );
01962     }
01963     Extra_ProgressBarStop( p->pProgress );
01964 p->nClassesEnd = p->lClasses.nItems;
01965     // try to prove the outputs of the miter
01966     p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig);
01967 //    Ivy_FraigMiterStatus( p->pManFraig );
01968     if ( p->pParams->fProve && p->pManFraig->pData == NULL )
01969         Ivy_FraigMiterProve( p );
01970     // add the POs
01971     Ivy_ManForEachPo( p->pManAig, pObj, i )
01972         Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
01973     // clean the old manager
01974     Ivy_ManForEachObj( p->pManAig, pObj, i )
01975         pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
01976     // clean the new manager
01977     Ivy_ManForEachObj( p->pManFraig, pObj, i )
01978     {
01979         if ( Ivy_ObjFaninVec(pObj) )
01980             Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
01981         pObj->pNextFan0 = pObj->pNextFan1 = NULL;
01982     }
01983     // remove dangling nodes 
01984     Ivy_ManCleanup( p->pManFraig );
01985     // clean up the class marks
01986     Ivy_FraigForEachEquivClass( p->lClasses.pHead, pObj )
01987         pObj->fMarkA = 0;
01988 }
01989 
02001 Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
02002 { 
02003     Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew;
02004     int RetValue;
02005     // get the fraiged fanins
02006     pFanin0New = Ivy_ObjChild0Equiv(pObjOld);
02007     pFanin1New = Ivy_ObjChild1Equiv(pObjOld);
02008     // get the candidate fraig node
02009     pObjNew = Ivy_And( p->pManFraig, pFanin0New, pFanin1New );
02010     // get representative of this class
02011     if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node
02012          (!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node
02013     {
02014         assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
02015         assert( pObjNew != Ivy_Regular(pFanin0New) );
02016         assert( pObjNew != Ivy_Regular(pFanin1New) );
02017         return pObjNew;
02018     }
02019     // get the fraiged representative
02020     pObjReprNew = Ivy_ObjFraig(Ivy_ObjClassNodeRepr(pObjOld));
02021     // if the fraiged nodes are the same return
02022     if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) )
02023         return pObjNew;
02024     assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) );
02025 //    printf( "Node = %d. Repr = %d.\n", pObjOld->Id, Ivy_ObjClassNodeRepr(pObjOld)->Id );
02026 
02027     // they are different (the counter-example is in p->pPatWords)
02028     RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew) );
02029     if ( RetValue == 1 )  // proved equivalent
02030     {
02031         // mark the class as proved
02032         if ( Ivy_ObjClassNodeNext(pObjOld) == NULL )
02033             Ivy_ObjClassNodeRepr(pObjOld)->fMarkA = 1;
02034         return Ivy_NotCond( pObjReprNew, pObjOld->fPhase ^ Ivy_ObjClassNodeRepr(pObjOld)->fPhase );
02035     }
02036     if ( RetValue == -1 ) // failed
02037         return pObjNew;
02038     // simulate the counter-example and return the new node
02039     Ivy_FraigResimulate( p );
02040     return pObjNew;
02041 }
02042 
02054 void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p )
02055 {
02056     int i;
02057     for ( i = 0; i < p->nSatVars; i++ )
02058         printf( "%d %.3f  ", i, p->pSat->activity[i] );
02059     printf( "\n" );
02060 }
02061 
02073 int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
02074 {
02075     int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
02076 
02077     // make sure the nodes are not complemented
02078     assert( !Ivy_IsComplement(pNew) );
02079     assert( !Ivy_IsComplement(pOld) );
02080     assert( pNew != pOld );
02081 
02082     // if at least one of the nodes is a failed node, perform adjustments:
02083     // if the backtrack limit is small, simply skip this node
02084     // if the backtrack limit is > 10, take the quare root of the limit
02085     nBTLimit = p->pParams->nBTLimitNode;
02086     if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
02087     {
02088         p->nSatFails++;
02089         // fail immediately
02090 //        return -1;
02091         if ( nBTLimit <= 10 )
02092             return -1;
02093         nBTLimit = (int)pow(nBTLimit, 0.7);
02094     }
02095     p->nSatCalls++;
02096 
02097     // make sure the solver is allocated and has enough variables
02098     if ( p->pSat == NULL )
02099     {
02100         p->pSat = sat_solver_new();
02101         p->nSatVars = 1;
02102         sat_solver_setnvars( p->pSat, 1000 );
02103         // var 0 is reserved for const1 node - add the clause
02104 //        pLits[0] = toLit( 0 );
02105 //        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
02106     }
02107 
02108     // if the nodes do not have SAT variables, allocate them
02109     Ivy_FraigNodeAddToSolver( p, pOld, pNew );
02110 
02111     // prepare variable activity
02112     Ivy_FraigSetActivityFactors( p, pOld, pNew ); 
02113 
02114     // solve under assumptions
02115     // A = 1; B = 0     OR     A = 1; B = 1 
02116 clk = clock();
02117     pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 );
02118     pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
02119 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
02120     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
02121         (sint64)nBTLimit, (sint64)0, 
02122         p->nBTLimitGlobal, p->nInsLimitGlobal );
02123 p->timeSat += clock() - clk;
02124     if ( RetValue1 == l_False )
02125     {
02126 p->timeSatUnsat += clock() - clk;
02127         pLits[0] = lit_neg( pLits[0] );
02128         pLits[1] = lit_neg( pLits[1] );
02129         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
02130         assert( RetValue );
02131         // continue solving the other implication
02132         p->nSatCallsUnsat++;
02133     }
02134     else if ( RetValue1 == l_True )
02135     {
02136 p->timeSatSat += clock() - clk;
02137         Ivy_FraigSavePattern( p );
02138         p->nSatCallsSat++;
02139         return 0;
02140     }
02141     else // if ( RetValue1 == l_Undef )
02142     {
02143 p->timeSatFail += clock() - clk;
02144         // mark the node as the failed node
02145         if ( pOld != p->pManFraig->pConst1 ) 
02146             pOld->fFailTfo = 1;
02147         pNew->fFailTfo = 1;
02148         p->nSatFailsReal++;
02149         return -1;
02150     }
02151 
02152     // if the old node was constant 0, we already know the answer
02153     if ( pOld == p->pManFraig->pConst1 )
02154     {
02155         p->nSatProof++;
02156         return 1;
02157     }
02158 
02159     // solve under assumptions
02160     // A = 0; B = 1     OR     A = 0; B = 0 
02161 clk = clock();
02162     pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 );
02163     pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
02164     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
02165         (sint64)nBTLimit, (sint64)0, 
02166         p->nBTLimitGlobal, p->nInsLimitGlobal );
02167 p->timeSat += clock() - clk;
02168     if ( RetValue1 == l_False )
02169     {
02170 p->timeSatUnsat += clock() - clk;
02171         pLits[0] = lit_neg( pLits[0] );
02172         pLits[1] = lit_neg( pLits[1] );
02173         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
02174         assert( RetValue );
02175         p->nSatCallsUnsat++;
02176     }
02177     else if ( RetValue1 == l_True )
02178     {
02179 p->timeSatSat += clock() - clk;
02180         Ivy_FraigSavePattern( p );
02181         p->nSatCallsSat++;
02182         return 0;
02183     }
02184     else // if ( RetValue1 == l_Undef )
02185     {
02186 p->timeSatFail += clock() - clk;
02187         // mark the node as the failed node
02188         pOld->fFailTfo = 1;
02189         pNew->fFailTfo = 1;
02190         p->nSatFailsReal++;
02191         return -1;
02192     }
02193 /*
02194     // check BDD proof
02195     {
02196         int RetVal;
02197         PRT( "Sat", clock() - clk2 );
02198         clk2 = clock();
02199         RetVal = Ivy_FraigNodesAreEquivBdd( pOld, pNew );
02200 //        printf( "%d ", RetVal );
02201         assert( RetVal );
02202         PRT( "Bdd", clock() - clk2 );
02203         printf( "\n" );
02204     }
02205 */
02206     // return SAT proof
02207     p->nSatProof++;
02208     return 1;
02209 }
02210 
02222 int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
02223 {
02224     int pLits[2], RetValue1, RetValue, clk;
02225 
02226     // make sure the nodes are not complemented
02227     assert( !Ivy_IsComplement(pNew) );
02228     assert( pNew != p->pManFraig->pConst1 );
02229     p->nSatCalls++;
02230 
02231     // make sure the solver is allocated and has enough variables
02232     if ( p->pSat == NULL )
02233     {
02234         p->pSat = sat_solver_new();
02235         p->nSatVars = 1;
02236         sat_solver_setnvars( p->pSat, 1000 );
02237         // var 0 is reserved for const1 node - add the clause
02238 //        pLits[0] = toLit( 0 );
02239 //        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
02240     }
02241 
02242     // if the nodes do not have SAT variables, allocate them
02243     Ivy_FraigNodeAddToSolver( p, NULL, pNew );
02244 
02245     // prepare variable activity
02246     Ivy_FraigSetActivityFactors( p, NULL, pNew ); 
02247 
02248     // solve under assumptions
02249 clk = clock();
02250     pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase );
02251     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 
02252         (sint64)p->pParams->nBTLimitMiter, (sint64)0, 
02253         p->nBTLimitGlobal, p->nInsLimitGlobal );
02254 p->timeSat += clock() - clk;
02255     if ( RetValue1 == l_False )
02256     {
02257 p->timeSatUnsat += clock() - clk;
02258         pLits[0] = lit_neg( pLits[0] );
02259         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
02260         assert( RetValue );
02261         // continue solving the other implication
02262         p->nSatCallsUnsat++;
02263     }
02264     else if ( RetValue1 == l_True )
02265     {
02266 p->timeSatSat += clock() - clk;
02267         if ( p->pPatWords )
02268             Ivy_FraigSavePattern( p );
02269         p->nSatCallsSat++;
02270         return 0;
02271     }
02272     else // if ( RetValue1 == l_Undef )
02273     {
02274 p->timeSatFail += clock() - clk;
02275         // mark the node as the failed node
02276         pNew->fFailTfo = 1;
02277         p->nSatFailsReal++;
02278         return -1;
02279     }
02280 
02281     // return SAT proof
02282     p->nSatProof++;
02283     return 1;
02284 }
02285 
02297 void Ivy_FraigAddClausesMux( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode )
02298 {
02299     Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE;
02300     int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
02301 
02302     assert( !Ivy_IsComplement( pNode ) );
02303     assert( Ivy_ObjIsMuxType( pNode ) );
02304     // get nodes (I = if, T = then, E = else)
02305     pNodeI = Ivy_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
02306     // get the variable numbers
02307     VarF = Ivy_ObjSatNum(pNode);
02308     VarI = Ivy_ObjSatNum(pNodeI);
02309     VarT = Ivy_ObjSatNum(Ivy_Regular(pNodeT));
02310     VarE = Ivy_ObjSatNum(Ivy_Regular(pNodeE));
02311     // get the complementation flags
02312     fCompT = Ivy_IsComplement(pNodeT);
02313     fCompE = Ivy_IsComplement(pNodeE);
02314 
02315     // f = ITE(i, t, e)
02316 
02317     // i' + t' + f
02318     // i' + t  + f'
02319     // i  + e' + f
02320     // i  + e  + f'
02321 
02322     // create four clauses
02323     pLits[0] = toLitCond(VarI, 1);
02324     pLits[1] = toLitCond(VarT, 1^fCompT);
02325     pLits[2] = toLitCond(VarF, 0);
02326     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
02327     assert( RetValue );
02328     pLits[0] = toLitCond(VarI, 1);
02329     pLits[1] = toLitCond(VarT, 0^fCompT);
02330     pLits[2] = toLitCond(VarF, 1);
02331     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
02332     assert( RetValue );
02333     pLits[0] = toLitCond(VarI, 0);
02334     pLits[1] = toLitCond(VarE, 1^fCompE);
02335     pLits[2] = toLitCond(VarF, 0);
02336     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
02337     assert( RetValue );
02338     pLits[0] = toLitCond(VarI, 0);
02339     pLits[1] = toLitCond(VarE, 0^fCompE);
02340     pLits[2] = toLitCond(VarF, 1);
02341     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
02342     assert( RetValue );
02343 
02344     // two additional clauses
02345     // t' & e' -> f'
02346     // t  & e  -> f 
02347 
02348     // t  + e   + f'
02349     // t' + e'  + f 
02350 
02351     if ( VarT == VarE )
02352     {
02353 //        assert( fCompT == !fCompE );
02354         return;
02355     }
02356 
02357     pLits[0] = toLitCond(VarT, 0^fCompT);
02358     pLits[1] = toLitCond(VarE, 0^fCompE);
02359     pLits[2] = toLitCond(VarF, 1);
02360     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
02361     assert( RetValue );
02362     pLits[0] = toLitCond(VarT, 1^fCompT);
02363     pLits[1] = toLitCond(VarE, 1^fCompE);
02364     pLits[2] = toLitCond(VarF, 0);
02365     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
02366     assert( RetValue );
02367 }
02368 
02380 void Ivy_FraigAddClausesSuper( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t * vSuper )
02381 {
02382     Ivy_Obj_t * pFanin;
02383     int * pLits, nLits, RetValue, i;
02384     assert( !Ivy_IsComplement(pNode) );
02385     assert( Ivy_ObjIsNode( pNode ) );
02386     // create storage for literals
02387     nLits = Vec_PtrSize(vSuper) + 1;
02388     pLits = ALLOC( int, nLits );
02389     // suppose AND-gate is A & B = C
02390     // add !A => !C   or   A + !C
02391     Vec_PtrForEachEntry( vSuper, pFanin, i )
02392     {
02393         pLits[0] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), Ivy_IsComplement(pFanin));
02394         pLits[1] = toLitCond(Ivy_ObjSatNum(pNode), 1);
02395         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
02396         assert( RetValue );
02397     }
02398     // add A & B => C   or   !A + !B + C
02399     Vec_PtrForEachEntry( vSuper, pFanin, i )
02400         pLits[i] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), !Ivy_IsComplement(pFanin));
02401     pLits[nLits-1] = toLitCond(Ivy_ObjSatNum(pNode), 0);
02402     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
02403     assert( RetValue );
02404     free( pLits );
02405 }
02406 
02418 void Ivy_FraigCollectSuper_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
02419 {
02420     // if the new node is complemented or a PI, another gate begins
02421     if ( Ivy_IsComplement(pObj) || Ivy_ObjIsPi(pObj) || (!fFirst && Ivy_ObjRefs(pObj) > 1) || 
02422          (fUseMuxes && Ivy_ObjIsMuxType(pObj)) )
02423     {
02424         Vec_PtrPushUnique( vSuper, pObj );
02425         return;
02426     }
02427     // go through the branches
02428     Ivy_FraigCollectSuper_rec( Ivy_ObjChild0(pObj), vSuper, 0, fUseMuxes );
02429     Ivy_FraigCollectSuper_rec( Ivy_ObjChild1(pObj), vSuper, 0, fUseMuxes );
02430 }
02431 
02443 Vec_Ptr_t * Ivy_FraigCollectSuper( Ivy_Obj_t * pObj, int fUseMuxes )
02444 {
02445     Vec_Ptr_t * vSuper;
02446     assert( !Ivy_IsComplement(pObj) );
02447     assert( !Ivy_ObjIsPi(pObj) );
02448     vSuper = Vec_PtrAlloc( 4 );
02449     Ivy_FraigCollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
02450     return vSuper;
02451 }
02452 
02464 void Ivy_FraigObjAddToFrontier( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vFrontier )
02465 {
02466     assert( !Ivy_IsComplement(pObj) );
02467     if ( Ivy_ObjSatNum(pObj) )
02468         return;
02469     assert( Ivy_ObjSatNum(pObj) == 0 );
02470     assert( Ivy_ObjFaninVec(pObj) == NULL );
02471     if ( Ivy_ObjIsConst1(pObj) )
02472         return;
02473 //printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
02474     Ivy_ObjSetSatNum( pObj, p->nSatVars++ );
02475     if ( Ivy_ObjIsNode(pObj) )
02476         Vec_PtrPush( vFrontier, pObj );
02477 }
02478 
02490 void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
02491 { 
02492     Vec_Ptr_t * vFrontier, * vFanins;
02493     Ivy_Obj_t * pNode, * pFanin;
02494     int i, k, fUseMuxes = 1;
02495     assert( pOld || pNew );
02496     // quit if CNF is ready
02497     if ( (!pOld || Ivy_ObjFaninVec(pOld)) && (!pNew || Ivy_ObjFaninVec(pNew)) )
02498         return;
02499     // start the frontier
02500     vFrontier = Vec_PtrAlloc( 100 );
02501     if ( pOld ) Ivy_FraigObjAddToFrontier( p, pOld, vFrontier );
02502     if ( pNew ) Ivy_FraigObjAddToFrontier( p, pNew, vFrontier );
02503     // explore nodes in the frontier
02504     Vec_PtrForEachEntry( vFrontier, pNode, i )
02505     {
02506         // create the supergate
02507         assert( Ivy_ObjSatNum(pNode) );
02508         assert( Ivy_ObjFaninVec(pNode) == NULL );
02509         if ( fUseMuxes && Ivy_ObjIsMuxType(pNode) )
02510         {
02511             vFanins = Vec_PtrAlloc( 4 );
02512             Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin0(pNode) ) );
02513             Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin1(pNode) ) );
02514             Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin0(pNode) ) );
02515             Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin1(pNode) ) );
02516             Vec_PtrForEachEntry( vFanins, pFanin, k )
02517                 Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
02518             Ivy_FraigAddClausesMux( p, pNode );
02519         }
02520         else
02521         {
02522             vFanins = Ivy_FraigCollectSuper( pNode, fUseMuxes );
02523             Vec_PtrForEachEntry( vFanins, pFanin, k )
02524                 Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
02525             Ivy_FraigAddClausesSuper( p, pNode, vFanins );
02526         }
02527         assert( Vec_PtrSize(vFanins) > 1 );
02528         Ivy_ObjSetFaninVec( pNode, vFanins );
02529     }
02530     Vec_PtrFree( vFrontier );
02531 }
02532 
02544 int Ivy_FraigSetActivityFactors_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int LevelMin, int LevelMax )
02545 {
02546     Vec_Ptr_t * vFanins;
02547     Ivy_Obj_t * pFanin;
02548     int i, Counter = 0;
02549     assert( !Ivy_IsComplement(pObj) );
02550     assert( Ivy_ObjSatNum(pObj) );
02551     // skip visited variables
02552     if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) )
02553         return 0;
02554     Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj);
02555     // add the PI to the list
02556     if ( pObj->Level <= (unsigned)LevelMin || Ivy_ObjIsPi(pObj) )
02557         return 0;
02558     // set the factor of this variable
02559     // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pParams->dActConeBumpMax / ThisBump
02560     p->pSat->factors[Ivy_ObjSatNum(pObj)] = p->pParams->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
02561     veci_push(&p->pSat->act_vars, Ivy_ObjSatNum(pObj));
02562     // explore the fanins
02563     vFanins = Ivy_ObjFaninVec( pObj );
02564     Vec_PtrForEachEntry( vFanins, pFanin, i )
02565         Counter += Ivy_FraigSetActivityFactors_rec( p, Ivy_Regular(pFanin), LevelMin, LevelMax );
02566     return 1 + Counter;
02567 }
02568 
02580 int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
02581 {
02582     int clk, LevelMin, LevelMax;
02583     assert( pOld || pNew );
02584 clk = clock(); 
02585     // reset the active variables
02586     veci_resize(&p->pSat->act_vars, 0);
02587     // prepare for traversal
02588     Ivy_ManIncrementTravId( p->pManFraig );
02589     // determine the min and max level to visit
02590     assert( p->pParams->dActConeRatio > 0 && p->pParams->dActConeRatio < 1 );
02591     LevelMax = IVY_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
02592     LevelMin = (int)(LevelMax * (1.0 - p->pParams->dActConeRatio));
02593     // traverse
02594     if ( pOld && !Ivy_ObjIsConst1(pOld) )
02595         Ivy_FraigSetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
02596     if ( pNew && !Ivy_ObjIsConst1(pNew) )
02597         Ivy_FraigSetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
02598 //Ivy_FraigPrintActivity( p );
02599 p->timeTrav += clock() - clk;
02600     return 1;
02601 }
02602 
02603 
02604 
02605 #include "cuddInt.h"
02606 
02618 DdNode * Ivy_FraigNodesAreEquivBdd_int( DdManager * dd, DdNode * bFunc, Vec_Ptr_t * vFront, int Level )
02619 {
02620     DdNode ** pFuncs;
02621     DdNode * bFuncNew;
02622     Vec_Ptr_t * vTemp;
02623     Ivy_Obj_t * pObj, * pFanin;
02624     int i, NewSize;
02625     // create new frontier
02626     vTemp = Vec_PtrAlloc( 100 );
02627     Vec_PtrForEachEntry( vFront, pObj, i )
02628     {
02629         if ( (int)pObj->Level != Level )
02630         {
02631             pObj->fMarkB = 1;
02632             pObj->TravId = Vec_PtrSize(vTemp);
02633             Vec_PtrPush( vTemp, pObj );
02634             continue;
02635         }
02636 
02637         pFanin = Ivy_ObjFanin0(pObj);
02638         if ( pFanin->fMarkB == 0 )
02639         {
02640             pFanin->fMarkB = 1;
02641             pFanin->TravId = Vec_PtrSize(vTemp);
02642             Vec_PtrPush( vTemp, pFanin );
02643         }
02644 
02645         pFanin = Ivy_ObjFanin1(pObj);
02646         if ( pFanin->fMarkB == 0 )
02647         {
02648             pFanin->fMarkB = 1;
02649             pFanin->TravId = Vec_PtrSize(vTemp);
02650             Vec_PtrPush( vTemp, pFanin );
02651         }
02652     }
02653     // collect the permutation
02654     NewSize = IVY_MAX(dd->size, Vec_PtrSize(vTemp));
02655     pFuncs = ALLOC( DdNode *, NewSize );
02656     Vec_PtrForEachEntry( vFront, pObj, i )
02657     {
02658         if ( (int)pObj->Level != Level )
02659             pFuncs[i] = Cudd_bddIthVar( dd, pObj->TravId );
02660         else
02661             pFuncs[i] = Cudd_bddAnd( dd, 
02662                 Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ),
02663                 Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ) );
02664         Cudd_Ref( pFuncs[i] );
02665     }
02666     // add the remaining vars
02667     assert( NewSize == dd->size );
02668     for ( i = Vec_PtrSize(vFront); i < dd->size; i++ )
02669     {
02670         pFuncs[i] = Cudd_bddIthVar( dd, i );
02671         Cudd_Ref( pFuncs[i] );
02672     }
02673 
02674     // create new
02675     bFuncNew = Cudd_bddVectorCompose( dd, bFunc, pFuncs ); Cudd_Ref( bFuncNew );
02676     // clean trav Id
02677     Vec_PtrForEachEntry( vTemp, pObj, i )
02678     {
02679         pObj->fMarkB = 0;
02680         pObj->TravId = 0;
02681     }
02682     // deref
02683     for ( i = 0; i < dd->size; i++ )
02684         Cudd_RecursiveDeref( dd, pFuncs[i] );
02685     free( pFuncs );
02686 
02687     free( vFront->pArray );
02688     *vFront = *vTemp;
02689 
02690     vTemp->nCap = vTemp->nSize = 0;
02691     vTemp->pArray = NULL;
02692     Vec_PtrFree( vTemp );
02693 
02694     Cudd_Deref( bFuncNew );
02695     return bFuncNew;
02696 }
02697 
02709 int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 )
02710 {
02711     static DdManager * dd = NULL;
02712     DdNode * bFunc, * bTemp;
02713     Vec_Ptr_t * vFront;
02714     Ivy_Obj_t * pObj;
02715     int i, RetValue, Iter, Level;
02716     // start the manager
02717     if ( dd == NULL )
02718         dd = Cudd_Init( 50, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
02719     // create front
02720     vFront = Vec_PtrAlloc( 100 );
02721     Vec_PtrPush( vFront, pObj1 );
02722     Vec_PtrPush( vFront, pObj2 );
02723     // get the function
02724     bFunc = Cudd_bddXor( dd, Cudd_bddIthVar(dd,0), Cudd_bddIthVar(dd,1) );  Cudd_Ref( bFunc );
02725     bFunc = Cudd_NotCond( bFunc, pObj1->fPhase != pObj2->fPhase );
02726     // try running BDDs
02727     for ( Iter = 0; ; Iter++ )
02728     {
02729         // find max level
02730         Level = 0;
02731         Vec_PtrForEachEntry( vFront, pObj, i )
02732             if ( Level < (int)pObj->Level )
02733                 Level = (int)pObj->Level;
02734         if ( Level == 0 )
02735             break;            
02736         bFunc = Ivy_FraigNodesAreEquivBdd_int( dd, bTemp = bFunc, vFront, Level ); Cudd_Ref( bFunc );
02737         Cudd_RecursiveDeref( dd, bTemp );
02738         if ( bFunc == Cudd_ReadLogicZero(dd) ) // proved
02739             {printf( "%d", Iter ); break;}
02740         if ( Cudd_DagSize(bFunc) > 1000 )
02741             {printf( "b" ); break;}
02742         if ( dd->size > 120 )
02743             {printf( "s" ); break;}
02744         if ( Iter > 50 )
02745             {printf( "i" ); break;}
02746     }
02747     if ( bFunc == Cudd_ReadLogicZero(dd) ) // unsat
02748         RetValue = 1;
02749     else if ( Level == 0 ) // sat
02750         RetValue = 0;
02751     else 
02752         RetValue = -1; // spaceout/timeout
02753     Cudd_RecursiveDeref( dd, bFunc );
02754     Vec_PtrFree( vFront );
02755     return RetValue;
02756 }
02757 
02761 
02762