/**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 "ivy.h" #include "satSolver.h" #include "extra.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 // 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; }; 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 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_FraigMarkConeSetActivity( 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_FraigMan_t * p ); static void Ivy_FraigMiterProve( Ivy_FraigMan_t * p ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Performs fraiging of the initial AIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Ivy_Man_t * Ivy_FraigProve( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) { Ivy_FraigMan_t * p; Ivy_Man_t * pManAigNew; int clk; 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 [Performs fraiging of the initial 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; 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 [Performs fraiging of the initial AIG.] 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 ); // 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; Ivy_FraigStop( p ); return pManAigNew; } /**Function************************************************************* Synopsis [Performs fraiging of the initial AIG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams ) { memset( pParams, 0, sizeof(Ivy_FraigParams_t) ); pParams->nSimWords = 32; pParams->SimSatur = 0.005; pParams->fPatScores = 0; pParams->MaxScore = 25; pParams->nBTLimitNode = 100; // conflict limit at a node pParams->nBTLimitMiter = 500000; // conflict limit at an output pParams->nBTLimitGlobal = 0; // conflict limit global pParams->nInsLimitNode = 0; // inspection limit at a node pParams->nInsLimitMiter = 0; // inspection limit at an output pParams->nInsLimitGlobal = 0; // inspection limit global } /**Function************************************************************* Synopsis [Starts the fraiging manager.] 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_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 ); PRT( "time1 ", p->time1 ); } /**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 [Simulates one node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_NodeAssignRandom( 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++ ) pSims->pData[i] = Ivy_ObjRandomSim(); } /**Function************************************************************* Synopsis [Simulates one node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_NodeAssignConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int fConst1 ) { Ivy_FraigSim_t * pSims; int i; pSims = Ivy_ObjSim(pObj); for ( i = 0; i < p->nSimWords; i++ ) pSims->pData[i] = fConst1? ~(unsigned)0 : 0; } /**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 [Simulates AIG manager.] Description [Assumes that the PI simulation info is attached.] 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 [Simulates AIG manager.] Description [Assumes that the PI simulation info is attached.] 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 ); /* for ( i = 0; i < Limit; i++ ) Extra_PrintBinary( stdout, Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) ), 30 ), printf( "\n" ); */ } /**Function************************************************************* Synopsis [Adds new nodes 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 new nodes to the equivalence class.] 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 [Updates the list of classes after base class has split.] 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 [Refines the classes after simulation.] Description [Assumes that simulation info is assigned. Returns the number of classes refined.] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pClass, * pClass2; int clk, RetValue, Counter = 0; 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 [Stops the fraiging manager.] 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 [Copy pattern from the solver into the internal storage.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigSavePattern0( Ivy_FraigMan_t * p ) { memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); } /**Function************************************************************* Synopsis [Copy pattern from the solver into the internal storage.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigSavePattern1( Ivy_FraigMan_t * p ) { memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords ); } /**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 [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) ) ) return 1; return 0; } /**Function************************************************************* Synopsis [Stops the fraiging 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 ); //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 ); //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 ); //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); } while ( (double)nChanges / nClasses > p->pParams->SimSatur ); // Ivy_FraigPrintSimClasses( p ); // check if some outputs already became non-constant if ( Ivy_FraigCheckOutputSims(p) ) printf( "Special case: One of the POs is already non-const zero.\n" ); } /**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 [Stops the fraiging manager.] 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 ( 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 ); //printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); if ( nChanges == 0 ) break; } } /**Function************************************************************* Synopsis [Reports the status of the miter.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigMiterStatus( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj, * pObjNew; int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0; Ivy_ManForEachPo( p->pManAig, pObj, i ) { pObjNew = Ivy_ObjChild0Equiv(pObj); // check if the output is constant 1 if ( pObjNew == p->pManFraig->pConst1 ) { CountNonConst0++; continue; } // check if the output is constant 0 if ( pObjNew == Ivy_Not(p->pManFraig->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" ); } return 1; } /**Function************************************************************* Synopsis [Works on the miter.] Description [Tries to prove each output until encountering a sat output.] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj, * pObjNew; int i, RetValue, clk = clock(); int fVerbose = p->pParams->fVerbose; 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) ); break; } // 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_IsComplement(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) ); 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; int i, k = 0; p->nClassesZero = Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 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 ); pObj->pEquiv = Ivy_FraigAnd( p, pObj ); } 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 ); 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 { 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 [Performs fraiging for one node.] Description [Returns the fraiged node.] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigCleanActivity( Ivy_FraigMan_t * p ) { double * pActivity; int i; pActivity = sat_solver_activity(p->pSat); for ( i = 0; i < p->nSatVars; i++ ) { pActivity[i] = 0.0; sat_solver_order_update( p->pSat, i ); } } /**Function************************************************************* Synopsis [Performs fraiging for one node.] Description [Returns the fraiged node.] SideEffects [] SeeAlso [] ***********************************************************************/ void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p ) { double * pActivity; int i; pActivity = sat_solver_activity(p->pSat); for ( i = 0; i < p->nSatVars; i++ ) printf( "%d %.3f ", i, pActivity[i] ); printf( "\n" ); } /**Function************************************************************* Synopsis [Performs fraiging for one node.] Description [Returns the fraiged node.] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ) { int pLits[4], RetValue, RetValue1, nBTLimit, clk; // 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)sqrt(nBTLimit); } 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 ); // 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, nBTLimit, p->pParams->nInsLimitNode, p->pParams->nBTLimitGlobal, p->pParams->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, nBTLimit, p->pParams->nInsLimitNode, p->pParams->nBTLimitGlobal, p->pParams->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; } // return SAT proof p->nSatProof++; return 1; } /**Function************************************************************* Synopsis [Performs fraiging 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_FraigMarkConeSetActivity( 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, p->pParams->nBTLimitMiter, p->pParams->nInsLimitMiter, p->pParams->nBTLimitGlobal, p->pParams->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; 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 [Collects the supergate.] 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 [Addes clauses to the solver.] 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 [Performs fraiging for one node.] Description [Returns the fraiged node.] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigMarkConeSetActivity_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, double * pActivity, int LevelMax, Vec_Ptr_t * vPiVars ) { Vec_Ptr_t * vFanins; Ivy_Obj_t * pFanin; int i, Counter; assert( !Ivy_IsComplement(pObj) ); if ( Ivy_ObjIsConst1(pObj) ) return 0; assert( Ivy_ObjSatNum(pObj) ); if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) ) return 0; Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj); // add this variable to the decision assert( Ivy_ObjSatNum(pObj) > 0 ); // pActivity[Ivy_ObjSatNum(pObj)] = 3.0 * pow( 0.97, LevelMax - pObj->Level ); // sat_solver_order_unassigned( p->pSat, Ivy_ObjSatNum(pObj) ); // pActivity[Ivy_ObjSatNum(pObj)] += 3.0 * pObj->Level / LevelMax; // sat_solver_order_update( p->pSat, Ivy_ObjSatNum(pObj) ); if ( LevelMax > 150 && (int)pObj->Level > LevelMax - 100 ) sat_solver_act_var_bump_factor( p->pSat, Ivy_ObjSatNum(pObj), 1.0 + 10.0 * (pObj->Level - (LevelMax - 100)) / 100 ); // add the PI to the list if ( Ivy_ObjIsPi(pObj) ) { Vec_PtrPush( vPiVars, pObj ); return 0; } // explore the fanins vFanins = Ivy_ObjFaninVec( pObj ); Counter = 1; Vec_PtrForEachEntry( vFanins, pFanin, i ) Counter += Ivy_FraigMarkConeSetActivity_rec( p, Ivy_Regular(pFanin), pActivity, LevelMax, vPiVars ); return Counter; // Counter = Ivy_FraigMarkConeSetActivity_rec( p, Ivy_ObjFanin0(pObj), pActivity, LevelMax, vPiVars ); // Counter += Ivy_FraigMarkConeSetActivity_rec( p, Ivy_ObjFanin1(pObj), pActivity, LevelMax, vPiVars ); // return Counter; } /**Function************************************************************* Synopsis [Performs fraiging for one node.] Description [Returns the fraiged node.] SideEffects [] SeeAlso [] ***********************************************************************/ int Ivy_FraigMarkConeSetActivity( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ) { int clk, LevelMax, Counter; assert( pOld || pNew ); clk = clock(); Vec_PtrClear( p->vPiVars ); Ivy_ManIncrementTravId( p->pManFraig ); // Ivy_FraigCleanActivity( p ); // sat_solver_order_clean( p->pSat ); //printf( "\n" ); //printf( "Adding\n" ); LevelMax = IVY_MAX( pNew ? pNew->Level : 0, pOld ? pOld->Level : 0 ); Counter = 0; if ( pOld ) Counter += Ivy_FraigMarkConeSetActivity_rec( p, pOld, sat_solver_activity(p->pSat), LevelMax, p->vPiVars ); if ( pNew ) Counter += Ivy_FraigMarkConeSetActivity_rec( p, pNew, sat_solver_activity(p->pSat), LevelMax, p->vPiVars ); //Ivy_FraigPrintActivity( p ); //printf( "\n" ); //printf( "Solving\n" ); // printf( "%d ", Vec_PtrSize(p->vPiVars) ); p->timeTrav += clock() - clk; return 1; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////