diff options
Diffstat (limited to 'src/aig/fra')
| -rw-r--r-- | src/aig/fra/fra.h | 49 | ||||
| -rw-r--r-- | src/aig/fra/fraAnd.c | 52 | ||||
| -rw-r--r-- | src/aig/fra/fraClass.c | 56 | ||||
| -rw-r--r-- | src/aig/fra/fraCnf.c | 72 | ||||
| -rw-r--r-- | src/aig/fra/fraCore.c | 10 | ||||
| -rw-r--r-- | src/aig/fra/fraMan.c | 38 | ||||
| -rw-r--r-- | src/aig/fra/fraSat.c | 36 | ||||
| -rw-r--r-- | src/aig/fra/fraSim.c | 96 |
8 files changed, 205 insertions, 204 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 29195d19..7f2df105 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -36,6 +36,7 @@ extern "C" { #include <time.h> #include "vec.h" +#include "aig.h" #include "dar.h" #include "satSolver.h" @@ -73,8 +74,8 @@ struct Fra_Man_t_ // high-level data Fra_Par_t * pPars; // parameters governing fraiging // AIG managers - Dar_Man_t * pManAig; // the starting AIG manager - Dar_Man_t * pManFraig; // the final AIG manager + Aig_Man_t * pManAig; // the starting AIG manager + Aig_Man_t * pManFraig; // the final AIG manager // simulation info unsigned * pSimWords; // memory for simulation information int nSimWords; // the number of simulation words @@ -86,8 +87,8 @@ struct Fra_Man_t_ Vec_Ptr_t * vClasses; // equivalence classes Vec_Ptr_t * vClasses1; // equivalence class of Const1 node Vec_Ptr_t * vClassesTemp; // temporary storage for new classes - Dar_Obj_t ** pMemClasses; // memory allocated for equivalence classes - Dar_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used + Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes + Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used Vec_Ptr_t * vClassOld; // old equivalence class after splitting Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting int nPairs; // the number of pairs of nodes @@ -98,8 +99,8 @@ struct Fra_Man_t_ sint64 nBTLimitGlobal; // resource limit sint64 nInsLimitGlobal; // resource limit // various data members - Dar_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes - Dar_Obj_t ** pMemRepr; // memory allocated for points to the node representatives + Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes + Aig_Obj_t ** pMemRepr; // memory allocated for points to the node representatives Vec_Ptr_t ** pMemFanins; // the arrays of fanins int * pMemSatNums; // the array of SAT numbers int nSizeAlloc; // allocated size of the arrays @@ -135,21 +136,21 @@ struct Fra_Man_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -static inline unsigned * Fra_ObjSim( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; } +static inline unsigned * Fra_ObjSim( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; } static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); } -static inline Dar_Obj_t * Fra_ObjFraig( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]; } -static inline Dar_Obj_t * Fra_ObjRepr( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]; } -static inline Vec_Ptr_t * Fra_ObjFaninVec( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; } -static inline int Fra_ObjSatNum( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; } +static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]; } +static inline Aig_Obj_t * Fra_ObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]; } +static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; } +static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; } -static inline void Fra_ObjSetFraig( Dar_Obj_t * pObj, Dar_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id] = pNode; } -static inline void Fra_ObjSetRepr( Dar_Obj_t * pObj, Dar_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id] = pNode; } -static inline void Fra_ObjSetFaninVec( Dar_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; } -static inline void Fra_ObjSetSatNum( Dar_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; } +static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id] = pNode; } +static inline void Fra_ObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id] = pNode; } +static inline void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; } +static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; } -static inline Dar_Obj_t * Fra_ObjChild0Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL; } -static inline Dar_Obj_t * Fra_ObjChild1Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL; } +static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; } //////////////////////////////////////////////////////////////////////// /// ITERATORS /// @@ -167,21 +168,21 @@ extern void Fra_CreateClasses( Fra_Man_t * p ); extern int Fra_RefineClasses( Fra_Man_t * p ); extern int Fra_RefineClasses1( Fra_Man_t * p ); /*=== fraCnf.c ========================================================*/ -extern void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew ); +extern void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); /*=== fraCore.c ========================================================*/ -extern Dar_Man_t * Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pParams ); +extern Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pParams ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); -extern Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pParams ); +extern Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams ); extern void Fra_ManPrepare( Fra_Man_t * p ); extern void Fra_ManStop( Fra_Man_t * p ); extern void Fra_ManPrint( Fra_Man_t * p ); /*=== fraSat.c ========================================================*/ -extern int Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew ); -extern int Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew ); +extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); +extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); /*=== fraSim.c ========================================================*/ -extern int Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj ); -extern int Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 ); +extern int Fra_NodeHasZeroSim( Fra_Man_t * p, Aig_Obj_t * pObj ); +extern int Fra_NodeCompareSims( Fra_Man_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); extern void Fra_SavePattern( Fra_Man_t * p ); extern void Fra_Simulate( Fra_Man_t * p ); extern void Fra_Resimulate( Fra_Man_t * p ); diff --git a/src/aig/fra/fraAnd.c b/src/aig/fra/fraAnd.c index a360ce9b..36b4ccc3 100644 --- a/src/aig/fra/fraAnd.c +++ b/src/aig/fra/fraAnd.c @@ -40,48 +40,48 @@ SeeAlso [] ***********************************************************************/ -Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld ) +Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld ) { - Dar_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig; + Aig_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig; int RetValue; - assert( !Dar_IsComplement(pObjOld) ); - assert( Dar_ObjIsNode(pObjOld) ); + assert( !Aig_IsComplement(pObjOld) ); + assert( Aig_ObjIsNode(pObjOld) ); // get the fraiged fanins pFanin0Fraig = Fra_ObjChild0Fra(pObjOld); pFanin1Fraig = Fra_ObjChild1Fra(pObjOld); // get the fraiged node - pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig ); - if ( Dar_ObjIsConst1(Dar_Regular(pObjFraig)) ) + pObjFraig = Aig_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig ); + if ( Aig_ObjIsConst1(Aig_Regular(pObjFraig)) ) return pObjFraig; - Dar_Regular(pObjFraig)->pData = p; + Aig_Regular(pObjFraig)->pData = p; // get representative of this class pObjOldRepr = Fra_ObjRepr(pObjOld); if ( pObjOldRepr == NULL || // this is a unique node - (!p->pPars->fDoSparse && pObjOldRepr == Dar_ManConst1(p->pManAig)) ) // this is a sparse node + (!p->pPars->fDoSparse && pObjOldRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node { - assert( Dar_Regular(pFanin0Fraig) != Dar_Regular(pFanin1Fraig) ); - assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin0Fraig) ); - assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin1Fraig) ); + assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) ); + assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) ); + assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin1Fraig) ); return pObjFraig; } // get the fraiged representative pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr); // if the fraiged nodes are the same, return - if ( Dar_Regular(pObjFraig) == Dar_Regular(pObjOldReprFraig) ) + if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjOldReprFraig) ) return pObjFraig; - assert( Dar_Regular(pObjFraig) != Dar_ManConst1(p->pManFraig) ); + assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) ); // printf( "Node = %d. Repr = %d.\n", pObjOld->Id, pObjOldRepr->Id ); // if they are proved different, the c-ex will be in p->pPatWords - RetValue = Fra_NodesAreEquiv( p, Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) ); + RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) ); if ( RetValue == 1 ) // proved equivalent { // pObjOld->fMarkA = 1; - return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase ); + return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase ); } if ( RetValue == -1 ) // failed { - Dar_Obj_t * ppNodes[2] = { Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) }; + Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) }; Vec_Ptr_t * vNodes; if ( !p->pPars->fSpeculate ) @@ -90,11 +90,11 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld ) // pObjOld->fMarkB = 1; p->nSpeculs++; - vNodes = Dar_ManDfsNodes( p->pManFraig, ppNodes, 2 ); + vNodes = Aig_ManDfsNodes( p->pManFraig, ppNodes, 2 ); printf( "%d ", Vec_PtrSize(vNodes) ); Vec_PtrFree( vNodes ); - return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase ); + return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase ); } // printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id ); // simulate the counter-example and return the Fraig node @@ -118,18 +118,18 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld ) ***********************************************************************/ void Fra_Sweep( Fra_Man_t * p ) { - Dar_Obj_t * pObj, * pObjNew; + Aig_Obj_t * pObj, * pObjNew; int i, k = 0; p->nClassesZero = Vec_PtrSize(p->vClasses1); p->nClassesBeg = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0); // duplicate internal nodes -// p->pProgress = Extra_ProgressBarStart( stdout, Dar_ManNodeNum(p->pManAig) ); - Dar_ManForEachNode( p->pManAig, pObj, i ) +// p->pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p->pManAig) ); + Aig_ManForEachNode( p->pManAig, pObj, i ) { // Extra_ProgressBarUpdate( p->pProgress, k++, NULL ); // default to simple strashing if simulation detected a counter-example for a PO if ( p->pManFraig->pData ) - pObjNew = Dar_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) ); + pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) ); else pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented Fra_ObjSetFraig( pObj, pObjNew ); @@ -138,15 +138,15 @@ p->nClassesBeg = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0 // Extra_ProgressBarStop( p->pProgress ); p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0); // try to prove the outputs of the miter - p->nNodesMiter = Dar_ManNodeNum(p->pManFraig); + p->nNodesMiter = Aig_ManNodeNum(p->pManFraig); // Fra_MiterStatus( p->pManFraig ); // if ( p->pPars->fProve && p->pManFraig->pData == NULL ) // Fra_MiterProve( p ); // add the POs - Dar_ManForEachPo( p->pManAig, pObj, i ) - Dar_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) ); + Aig_ManForEachPo( p->pManAig, pObj, i ) + Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) ); // remove dangling nodes - Dar_ManCleanup( p->pManFraig ); + Aig_ManCleanup( p->pManFraig ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 33421423..3de54453 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -36,8 +36,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static inline Dar_Obj_t * Fra_ObjNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pObj ) { return ppNexts[pObj->Id]; } -static inline void Fra_ObjSetNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pObj, Dar_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; } +static inline Aig_Obj_t * Fra_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj ) { return ppNexts[pObj->Id]; } +static inline void Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -54,9 +54,9 @@ static inline void Fra_ObjSetNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pOb SeeAlso [] ***********************************************************************/ -void Fra_PrintClass( Dar_Obj_t ** pClass ) +void Fra_PrintClass( Aig_Obj_t ** pClass ) { - Dar_Obj_t * pTemp; + Aig_Obj_t * pTemp; int i; printf( "{ " ); for ( i = 0; pTemp = pClass[i]; i++ ) @@ -75,9 +75,9 @@ void Fra_PrintClass( Dar_Obj_t ** pClass ) SeeAlso [] ***********************************************************************/ -int Fra_CountClass( Dar_Obj_t ** pClass ) +int Fra_CountClass( Aig_Obj_t ** pClass ) { - Dar_Obj_t * pTemp; + Aig_Obj_t * pTemp; int i; for ( i = 0; pTemp = pClass[i]; i++ ); return i; @@ -96,7 +96,7 @@ int Fra_CountClass( Dar_Obj_t ** pClass ) ***********************************************************************/ int Fra_CountPairsClasses( Fra_Man_t * p ) { - Dar_Obj_t ** pClass; + Aig_Obj_t ** pClass; int i, nNodes, nPairs = 0; Vec_PtrForEachEntry( p->vClasses, pClass, i ) { @@ -120,7 +120,7 @@ int Fra_CountPairsClasses( Fra_Man_t * p ) ***********************************************************************/ void Fra_PrintClasses( Fra_Man_t * p ) { - Dar_Obj_t ** pClass; + Aig_Obj_t ** pClass; int i; printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_CountPairsClasses(p) ); Vec_PtrForEachEntry( p->vClasses, pClass, i ) @@ -142,7 +142,7 @@ void Fra_PrintClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -unsigned Fra_NodeHash( Fra_Man_t * p, Dar_Obj_t * pObj ) +unsigned Fra_NodeHash( Fra_Man_t * p, Aig_Obj_t * pObj ) { static int s_FPrimes[128] = { 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, @@ -220,21 +220,21 @@ unsigned int Cudd_PrimeFra( unsigned int p ) ***********************************************************************/ void Fra_CreateClasses( Fra_Man_t * p ) { - Dar_Obj_t ** ppTable, ** ppNexts; - Dar_Obj_t * pObj, * pTemp; + Aig_Obj_t ** ppTable, ** ppNexts; + Aig_Obj_t * pObj, * pTemp; int i, k, nTableSize, nEntries, nNodes, iEntry; // allocate the hash table hashing simulation info into nodes - nTableSize = Cudd_PrimeFra( Dar_ManObjIdMax(p->pManAig) + 1 ); - ppTable = ALLOC( Dar_Obj_t *, nTableSize ); - ppNexts = ALLOC( Dar_Obj_t *, nTableSize ); - memset( ppTable, 0, sizeof(Dar_Obj_t *) * nTableSize ); + nTableSize = Cudd_PrimeFra( Aig_ManObjIdMax(p->pManAig) + 1 ); + ppTable = ALLOC( Aig_Obj_t *, nTableSize ); + ppNexts = ALLOC( Aig_Obj_t *, nTableSize ); + memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize ); // add all the nodes to the hash table Vec_PtrClear( p->vClasses1 ); - Dar_ManForEachObj( p->pManAig, pObj, i ) + Aig_ManForEachObj( p->pManAig, pObj, i ) { - if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) continue; // hash the node by its simulation info iEntry = Fra_NodeHash( p, pObj ) % nTableSize; @@ -242,7 +242,7 @@ void Fra_CreateClasses( Fra_Man_t * p ) if ( iEntry == 0 && Fra_NodeHasZeroSim( p, pObj ) ) { Vec_PtrPush( p->vClasses1, pObj ); - Fra_ObjSetRepr( pObj, Dar_ManConst1(p->pManAig) ); + Fra_ObjSetRepr( pObj, Aig_ManConst1(p->pManAig) ); continue; } // add the node to the class @@ -275,15 +275,15 @@ void Fra_CreateClasses( Fra_Man_t * p ) } // allocate room for classes - p->pMemClasses = ALLOC( Dar_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) ); + p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) ); p->pMemClassesFree = p->pMemClasses + 2*nEntries; // copy the entries into storage in the topological order Vec_PtrClear( p->vClasses ); nEntries = 0; - Dar_ManForEachObj( p->pManAig, pObj, i ) + Aig_ManForEachObj( p->pManAig, pObj, i ) { - if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) continue; // skip the nodes that are not representatives of non-trivial classes if ( pObj->fMarkA == 0 ) @@ -307,7 +307,7 @@ void Fra_CreateClasses( Fra_Man_t * p ) Fra_ObjSetRepr( pTemp, pObj ); } // add as many empty entries -// memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Dar_Obj_t *) * nNodes ); +// memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Aig_Obj_t *) * nNodes ); p->pMemClasses[2*nEntries + nNodes] = NULL; // increment the number of entries nEntries += k; @@ -329,9 +329,9 @@ void Fra_CreateClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass ) +Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass ) { - Dar_Obj_t * pObj, ** ppThis; + Aig_Obj_t * pObj, ** ppThis; int i; assert( ppClass[0] != NULL && ppClass[1] != NULL ); @@ -390,7 +390,7 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass ) ***********************************************************************/ int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses ) { - Dar_Obj_t ** pClass, ** pClass2; + Aig_Obj_t ** pClass, ** pClass2; int nRefis; pClass = Vec_PtrEntryLast( vClasses ); for ( nRefis = 0; pClass2 = Fra_RefineClassOne( p, pClass ); nRefis++ ) @@ -426,7 +426,7 @@ int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses ) int Fra_RefineClasses( Fra_Man_t * p ) { Vec_Ptr_t * vTemp; - Dar_Obj_t ** pClass; + Aig_Obj_t ** pClass; int clk, i, nRefis; // check if some outputs already became non-constant // this is a special case when computation can be stopped!!! @@ -466,14 +466,14 @@ p->timeRef += clock() - clk; ***********************************************************************/ int Fra_RefineClasses1( Fra_Man_t * p ) { - Dar_Obj_t * pObj, ** ppClass; + Aig_Obj_t * pObj, ** ppClass; int i, k, nRefis, clk; // check if there is anything to refine if ( Vec_PtrSize(p->vClasses1) == 0 ) return 0; clk = clock(); // make sure constant 1 class contains only non-constant nodes - assert( Vec_PtrEntry(p->vClasses1,0) != Dar_ManConst1(p->pManAig) ); + assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pManAig) ); // collect all the nodes to be refined k = 0; Vec_PtrClear( p->vClassNew ); diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c index a662ade2..7df55d93 100644 --- a/src/aig/fra/fraCnf.c +++ b/src/aig/fra/fraCnf.c @@ -40,23 +40,23 @@ SeeAlso [] ***********************************************************************/ -void Fra_AddClausesMux( Fra_Man_t * p, Dar_Obj_t * pNode ) +void Fra_AddClausesMux( Fra_Man_t * p, Aig_Obj_t * pNode ) { - Dar_Obj_t * pNodeI, * pNodeT, * pNodeE; + Aig_Obj_t * pNodeI, * pNodeT, * pNodeE; int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; - assert( !Dar_IsComplement( pNode ) ); - assert( Dar_ObjIsMuxType( pNode ) ); + assert( !Aig_IsComplement( pNode ) ); + assert( Aig_ObjIsMuxType( pNode ) ); // get nodes (I = if, T = then, E = else) - pNodeI = Dar_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); + pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); // get the variable numbers VarF = Fra_ObjSatNum(pNode); VarI = Fra_ObjSatNum(pNodeI); - VarT = Fra_ObjSatNum(Dar_Regular(pNodeT)); - VarE = Fra_ObjSatNum(Dar_Regular(pNodeE)); + VarT = Fra_ObjSatNum(Aig_Regular(pNodeT)); + VarE = Fra_ObjSatNum(Aig_Regular(pNodeE)); // get the complementation flags - fCompT = Dar_IsComplement(pNodeT); - fCompE = Dar_IsComplement(pNodeE); + fCompT = Aig_IsComplement(pNodeT); + fCompE = Aig_IsComplement(pNodeE); // f = ITE(i, t, e) @@ -123,12 +123,12 @@ void Fra_AddClausesMux( Fra_Man_t * p, Dar_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper ) +void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) { - Dar_Obj_t * pFanin; + Aig_Obj_t * pFanin; int * pLits, nLits, RetValue, i; - assert( !Dar_IsComplement(pNode) ); - assert( Dar_ObjIsNode( pNode ) ); + assert( !Aig_IsComplement(pNode) ); + assert( Aig_ObjIsNode( pNode ) ); // create storage for literals nLits = Vec_PtrSize(vSuper) + 1; pLits = ALLOC( int, nLits ); @@ -136,14 +136,14 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper ) // add !A => !C or A + !C Vec_PtrForEachEntry( vSuper, pFanin, i ) { - pLits[0] = toLitCond(Fra_ObjSatNum(Dar_Regular(pFanin)), Dar_IsComplement(pFanin)); + pLits[0] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), Aig_IsComplement(pFanin)); pLits[1] = toLitCond(Fra_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(Fra_ObjSatNum(Dar_Regular(pFanin)), !Dar_IsComplement(pFanin)); + pLits[i] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), !Aig_IsComplement(pFanin)); pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); assert( RetValue ); @@ -161,18 +161,18 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper ) SeeAlso [] ***********************************************************************/ -void Fra_CollectSuper_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) +void Fra_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) { // if the new node is complemented or a PI, another gate begins - if ( Dar_IsComplement(pObj) || Dar_ObjIsPi(pObj) || (!fFirst && Dar_ObjRefs(pObj) > 1) || - (fUseMuxes && Dar_ObjIsMuxType(pObj)) ) + if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || + (fUseMuxes && Aig_ObjIsMuxType(pObj)) ) { Vec_PtrPushUnique( vSuper, pObj ); return; } // go through the branches - Fra_CollectSuper_rec( Dar_ObjChild0(pObj), vSuper, 0, fUseMuxes ); - Fra_CollectSuper_rec( Dar_ObjChild1(pObj), vSuper, 0, fUseMuxes ); + Fra_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes ); + Fra_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes ); } /**Function************************************************************* @@ -186,11 +186,11 @@ void Fra_CollectSuper_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes ) +Vec_Ptr_t * Fra_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes ) { Vec_Ptr_t * vSuper; - assert( !Dar_IsComplement(pObj) ); - assert( !Dar_ObjIsPi(pObj) ); + assert( !Aig_IsComplement(pObj) ); + assert( !Aig_ObjIsPi(pObj) ); vSuper = Vec_PtrAlloc( 4 ); Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); return vSuper; @@ -207,19 +207,19 @@ Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes ) SeeAlso [] ***********************************************************************/ -void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontier ) +void Fra_ObjAddToFrontier( Fra_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier ) { Fra_Man_t * pTemp = pObj->pData; - assert( !Dar_IsComplement(pObj) ); + assert( !Aig_IsComplement(pObj) ); if ( Fra_ObjSatNum(pObj) ) return; assert( Fra_ObjSatNum(pObj) == 0 ); assert( Fra_ObjFaninVec(pObj) == NULL ); - if ( Dar_ObjIsConst1(pObj) ) + if ( Aig_ObjIsConst1(pObj) ) return; //printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars ); Fra_ObjSetSatNum( pObj, p->nSatVars++ ); - if ( Dar_ObjIsNode(pObj) ) + if ( Aig_ObjIsNode(pObj) ) Vec_PtrPush( vFrontier, pObj ); } @@ -234,10 +234,10 @@ void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontie SeeAlso [] ***********************************************************************/ -void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew ) +void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { Vec_Ptr_t * vFrontier, * vFanins; - Dar_Obj_t * pNode, * pFanin; + Aig_Obj_t * pNode, * pFanin; int i, k, fUseMuxes = 1; assert( pOld || pNew ); // quit if CNF is ready @@ -253,22 +253,22 @@ void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew ) // create the supergate assert( Fra_ObjSatNum(pNode) ); assert( Fra_ObjFaninVec(pNode) == NULL ); - if ( fUseMuxes && Dar_ObjIsMuxType(pNode) ) + if ( fUseMuxes && Aig_ObjIsMuxType(pNode) ) { vFanins = Vec_PtrAlloc( 4 ); - Vec_PtrPushUnique( vFanins, Dar_ObjFanin0( Dar_ObjFanin0(pNode) ) ); - Vec_PtrPushUnique( vFanins, Dar_ObjFanin0( Dar_ObjFanin1(pNode) ) ); - Vec_PtrPushUnique( vFanins, Dar_ObjFanin1( Dar_ObjFanin0(pNode) ) ); - Vec_PtrPushUnique( vFanins, Dar_ObjFanin1( Dar_ObjFanin1(pNode) ) ); + Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) ); + Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) ); Vec_PtrForEachEntry( vFanins, pFanin, k ) - Fra_ObjAddToFrontier( p, Dar_Regular(pFanin), vFrontier ); + Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); Fra_AddClausesMux( p, pNode ); } else { vFanins = Fra_CollectSuper( pNode, fUseMuxes ); Vec_PtrForEachEntry( vFanins, pFanin, k ) - Fra_ObjAddToFrontier( p, Dar_Regular(pFanin), vFrontier ); + Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier ); Fra_AddClausesSuper( p, pNode, vFanins ); } assert( Vec_PtrSize(vFanins) > 1 ); diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 7fdd1b83..5338d662 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -39,15 +39,15 @@ SeeAlso [] ***********************************************************************/ -Dar_Man_t * Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pPars ) +Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars ) { Fra_Man_t * p; - Dar_Man_t * pManAigNew; + Aig_Man_t * pManAigNew; int clk; - if ( Dar_ManNodeNum(pManAig) == 0 ) - return Dar_ManDup(pManAig); + if ( Aig_ManNodeNum(pManAig) == 0 ) + return Aig_ManDup(pManAig); clk = clock(); - assert( Dar_ManLatchNum(pManAig) == 0 ); + assert( Aig_ManLatchNum(pManAig) == 0 ); p = Fra_ManStart( pManAig, pPars ); Fra_Simulate( p ); Fra_Sweep( p ); diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index 19ed6c03..78246a8c 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -66,7 +66,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars ) +Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) { Fra_Man_t * p; // allocate the fraiging manager @@ -74,15 +74,15 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars ) memset( p, 0, sizeof(Fra_Man_t) ); p->pPars = pPars; p->pManAig = pManAig; - p->pManFraig = Dar_ManStartFrom( pManAig ); - assert( Dar_ManPiNum(p->pManAig) == Dar_ManPiNum(p->pManFraig) ); + p->pManFraig = Aig_ManStartFrom( pManAig ); + assert( Aig_ManPiNum(p->pManAig) == Aig_ManPiNum(p->pManFraig) ); // allocate simulation info p->nSimWords = pPars->nSimWords; - p->pSimWords = ALLOC( unsigned, (Dar_ManObjIdMax(pManAig) + 1) * p->nSimWords ); + p->pSimWords = ALLOC( unsigned, (Aig_ManObjIdMax(pManAig) + 1) * p->nSimWords ); // clean simulation info of the constant node - memset( p->pSimWords, 0, sizeof(unsigned) * ((Dar_ManPiNum(pManAig) + 1) * p->nSimWords) ); + memset( p->pSimWords, 0, sizeof(unsigned) * ((Aig_ManPiNum(pManAig) + 1) * p->nSimWords) ); // allocate storage for sim pattern - p->nPatWords = Dar_BitWordNum( Dar_ManPiNum(pManAig) ); + p->nPatWords = Aig_BitWordNum( Aig_ManPiNum(pManAig) ); p->pPatWords = ALLOC( unsigned, p->nPatWords ); p->pPatScores = ALLOC( int, 32 * p->nSimWords ); p->vPiVars = Vec_PtrAlloc( 100 ); @@ -92,11 +92,11 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars ) p->vClassNew = Vec_PtrAlloc( 100 ); p->vClassesTemp = Vec_PtrAlloc( 100 ); // allocate other members - p->nSizeAlloc = Dar_ManObjIdMax(pManAig) + 1; - p->pMemFraig = ALLOC( Dar_Obj_t *, p->nSizeAlloc ); - memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Dar_Obj_t *) ); - p->pMemRepr = ALLOC( Dar_Obj_t *, p->nSizeAlloc ); - memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Dar_Obj_t *) ); + p->nSizeAlloc = Aig_ManObjIdMax(pManAig) + 1; + p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc ); + memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) ); + p->pMemRepr = ALLOC( Aig_Obj_t *, p->nSizeAlloc ); + memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) ); p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc ); memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) ); p->pMemSatNums = ALLOC( int, p->nSizeAlloc ); @@ -123,18 +123,18 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars ) ***********************************************************************/ void Fra_ManPrepare( Fra_Man_t * p ) { - Dar_Obj_t * pObj; + Aig_Obj_t * pObj; int i; // set the pointers to the manager - Dar_ManForEachObj( p->pManFraig, pObj, i ) + Aig_ManForEachObj( p->pManFraig, pObj, i ) pObj->pData = p; // set the pointer to the manager - Dar_ManForEachObj( p->pManAig, pObj, i ) + Aig_ManForEachObj( p->pManAig, pObj, i ) pObj->pData = p; // set the pointers to the available fraig nodes - Fra_ObjSetFraig( Dar_ManConst1(p->pManAig), Dar_ManConst1(p->pManFraig) ); - Dar_ManForEachPi( p->pManAig, pObj, i ) - Fra_ObjSetFraig( pObj, Dar_ManPi(p->pManFraig, i) ); + Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), Aig_ManConst1(p->pManFraig) ); + Aig_ManForEachPi( p->pManAig, pObj, i ) + Fra_ObjSetFraig( pObj, Aig_ManPi(p->pManFraig, i) ); } /**Function************************************************************* @@ -187,14 +187,14 @@ void Fra_ManStop( Fra_Man_t * p ) ***********************************************************************/ void Fra_ManPrint( Fra_Man_t * p ) { - double nMemory = 1.0*Dar_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20); + double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(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->pPars->nBTLimitNode, p->pPars->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", - Dar_ManNodeNum(p->pManFraig), p->nNodesMiter, Dar_ManNodeNum(p->pManAig), 0, 0, p->nSatVars ); + Aig_ManNodeNum(p->pManFraig), p->nNodesMiter, Aig_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 ); diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c index 1c72c807..66b1ba5a 100644 --- a/src/aig/fra/fraSat.c +++ b/src/aig/fra/fraSat.c @@ -24,7 +24,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew ); +static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -41,13 +41,13 @@ static int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * SeeAlso [] ***********************************************************************/ -int Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew ) +int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock(); // make sure the nodes are not complemented - assert( !Dar_IsComplement(pNew) ); - assert( !Dar_IsComplement(pOld) ); + assert( !Aig_IsComplement(pNew) ); + assert( !Aig_IsComplement(pOld) ); assert( pNew != pOld ); // if at least one of the nodes is a failed node, perform adjustments: @@ -189,12 +189,12 @@ p->timeSatFail += clock() - clk; SeeAlso [] ***********************************************************************/ -int Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew ) +int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ) { int pLits[2], RetValue1, RetValue, clk; // make sure the nodes are not complemented - assert( !Dar_IsComplement(pNew) ); + assert( !Aig_IsComplement(pNew) ); assert( pNew != p->pManFraig->pConst1 ); p->nSatCalls++; @@ -261,19 +261,19 @@ p->timeSatFail += clock() - clk; SeeAlso [] ***********************************************************************/ -int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, int LevelMax ) +int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, int LevelMax ) { Vec_Ptr_t * vFanins; - Dar_Obj_t * pFanin; + Aig_Obj_t * pFanin; int i, Counter = 0; - assert( !Dar_IsComplement(pObj) ); + assert( !Aig_IsComplement(pObj) ); assert( Fra_ObjSatNum(pObj) ); // skip visited variables - if ( Dar_ObjIsTravIdCurrent(p->pManFraig, pObj) ) + if ( Aig_ObjIsTravIdCurrent(p->pManFraig, pObj) ) return 0; - Dar_ObjSetTravIdCurrent(p->pManFraig, pObj); + Aig_ObjSetTravIdCurrent(p->pManFraig, pObj); // add the PI to the list - if ( pObj->Level <= (unsigned)LevelMin || Dar_ObjIsPi(pObj) ) + if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsPi(pObj) ) return 0; // set the factor of this variable // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump @@ -282,7 +282,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, i // explore the fanins vFanins = Fra_ObjFaninVec( pObj ); Vec_PtrForEachEntry( vFanins, pFanin, i ) - Counter += Fra_SetActivityFactors_rec( p, Dar_Regular(pFanin), LevelMin, LevelMax ); + Counter += Fra_SetActivityFactors_rec( p, Aig_Regular(pFanin), LevelMin, LevelMax ); return 1 + Counter; } @@ -297,7 +297,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, i SeeAlso [] ***********************************************************************/ -int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew ) +int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { int clk, LevelMin, LevelMax; assert( pOld || pNew ); @@ -305,15 +305,15 @@ clk = clock(); // reset the active variables veci_resize(&p->pSat->act_vars, 0); // prepare for traversal - Dar_ManIncrementTravId( p->pManFraig ); + Aig_ManIncrementTravId( p->pManFraig ); // determine the min and max level to visit assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 ); - LevelMax = DAR_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) ); + LevelMax = AIG_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) ); LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio)); // traverse - if ( pOld && !Dar_ObjIsConst1(pOld) ) + if ( pOld && !Aig_ObjIsConst1(pOld) ) Fra_SetActivityFactors_rec( p, pOld, LevelMin, LevelMax ); - if ( pNew && !Dar_ObjIsConst1(pNew) ) + if ( pNew && !Aig_ObjIsConst1(pNew) ) Fra_SetActivityFactors_rec( p, pNew, LevelMin, LevelMax ); //Fra_PrintActivity( p ); p->timeTrav += clock() - clk; diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 7207cfa2..beaa79fd 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -39,11 +39,11 @@ SeeAlso [] ***********************************************************************/ -void Fra_NodeAssignRandom( Fra_Man_t * p, Dar_Obj_t * pObj ) +void Fra_NodeAssignRandom( Fra_Man_t * p, Aig_Obj_t * pObj ) { unsigned * pSims; int i; - assert( Dar_ObjIsPi(pObj) ); + assert( Aig_ObjIsPi(pObj) ); pSims = Fra_ObjSim(pObj); for ( i = 0; i < p->nSimWords; i++ ) pSims[i] = Fra_ObjRandomSim(); @@ -60,11 +60,11 @@ void Fra_NodeAssignRandom( Fra_Man_t * p, Dar_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Fra_NodeAssignConst( Fra_Man_t * p, Dar_Obj_t * pObj, int fConst1 ) +void Fra_NodeAssignConst( Fra_Man_t * p, Aig_Obj_t * pObj, int fConst1 ) { unsigned * pSims; int i; - assert( Dar_ObjIsPi(pObj) ); + assert( Aig_ObjIsPi(pObj) ); pSims = Fra_ObjSim(pObj); for ( i = 0; i < p->nSimWords; i++ ) pSims[i] = fConst1? ~(unsigned)0 : 0; @@ -83,9 +83,9 @@ void Fra_NodeAssignConst( Fra_Man_t * p, Dar_Obj_t * pObj, int fConst1 ) ***********************************************************************/ void Fra_AssignRandom( Fra_Man_t * p ) { - Dar_Obj_t * pObj; + Aig_Obj_t * pObj; int i; - Dar_ManForEachPi( p->pManAig, pObj, i ) + Aig_ManForEachPi( p->pManAig, pObj, i ) Fra_NodeAssignRandom( p, pObj ); } @@ -102,17 +102,17 @@ void Fra_AssignRandom( Fra_Man_t * p ) ***********************************************************************/ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat ) { - Dar_Obj_t * pObj; + Aig_Obj_t * pObj; int i, Limit; - Dar_ManForEachPi( p->pManAig, pObj, i ) + Aig_ManForEachPi( p->pManAig, pObj, i ) { - Fra_NodeAssignConst( p, pObj, Dar_InfoHasBit(pPat, i) ); -// printf( "%d", Dar_InfoHasBit(pPat, i) ); + Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, i) ); +// printf( "%d", Aig_InfoHasBit(pPat, i) ); } // printf( "\n" ); - Limit = DAR_MIN( Dar_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 ); + Limit = AIG_MIN( Aig_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 ); for ( i = 0; i < Limit; i++ ) - Dar_InfoXorBit( Fra_ObjSim( Dar_ManPi(p->pManAig,i) ), i+1 ); + Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 ); } /**Function************************************************************* @@ -126,7 +126,7 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat ) SeeAlso [] ***********************************************************************/ -int Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj ) +int Fra_NodeHasZeroSim( Fra_Man_t * p, Aig_Obj_t * pObj ) { unsigned * pSims; int i; @@ -148,7 +148,7 @@ int Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Fra_NodeComplementSim( Fra_Man_t * p, Dar_Obj_t * pObj ) +void Fra_NodeComplementSim( Fra_Man_t * p, Aig_Obj_t * pObj ) { unsigned * pSims; int i; @@ -168,7 +168,7 @@ void Fra_NodeComplementSim( Fra_Man_t * p, Dar_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -int Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 ) +int Fra_NodeCompareSims( Fra_Man_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) { unsigned * pSims0, * pSims1; int i; @@ -192,20 +192,20 @@ int Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 ) SeeAlso [] ***********************************************************************/ -void Fra_NodeSimulate( Fra_Man_t * p, Dar_Obj_t * pObj ) +void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj ) { unsigned * pSims, * pSims0, * pSims1; int fCompl, fCompl0, fCompl1, i; - assert( !Dar_IsComplement(pObj) ); - assert( Dar_ObjIsNode(pObj) ); + assert( !Aig_IsComplement(pObj) ); + assert( Aig_ObjIsNode(pObj) ); // get hold of the simulation information pSims = Fra_ObjSim(pObj); - pSims0 = Fra_ObjSim(Dar_ObjFanin0(pObj)); - pSims1 = Fra_ObjSim(Dar_ObjFanin1(pObj)); + pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)); + pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)); // get complemented attributes of the children using their random info fCompl = pObj->fPhase; - fCompl0 = Dar_ObjFaninPhase(Dar_ObjChild0(pObj)); - fCompl1 = Dar_ObjFaninPhase(Dar_ObjChild1(pObj)); + fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj)); + fCompl1 = Aig_ObjFaninPhase(Aig_ObjChild1(pObj)); // simulate if ( fCompl0 && fCompl1 ) { @@ -290,13 +290,13 @@ void Fra_SavePattern1( Fra_Man_t * p ) ***********************************************************************/ void Fra_SavePattern( Fra_Man_t * p ) { - Dar_Obj_t * pObj; + Aig_Obj_t * pObj; int i; memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); - Dar_ManForEachPi( p->pManFraig, pObj, i ) + Aig_ManForEachPi( p->pManFraig, pObj, i ) // Vec_PtrForEachEntry( p->vPiVars, pObj, i ) if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True ) - Dar_InfoSetBit( p->pPatWords, i ); + Aig_InfoSetBit( p->pPatWords, i ); // Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 ); } @@ -329,7 +329,7 @@ void Fra_CleanPatScores( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Fra_AddToPatScores( Fra_Man_t * p, Dar_Obj_t * pClass, Dar_Obj_t * pClassNew ) +void Fra_AddToPatScores( Fra_Man_t * p, Aig_Obj_t * pClass, Aig_Obj_t * pClassNew ) { unsigned * pSims0, * pSims1; unsigned uDiff; @@ -363,7 +363,7 @@ void Fra_AddToPatScores( Fra_Man_t * p, Dar_Obj_t * pClass, Dar_Obj_t * pClassNe int Fra_SelectBestPat( Fra_Man_t * p ) { unsigned * pSims; - Dar_Obj_t * pObj; + Aig_Obj_t * pObj; int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1; for ( i = 1; i < nLimit; i++ ) { @@ -379,11 +379,11 @@ int Fra_SelectBestPat( Fra_Man_t * p ) // printf( "Max score is %3d. ", MaxScore ); // copy the best pattern into the selected pattern memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); - Dar_ManForEachPi( p->pManAig, pObj, i ) + Aig_ManForEachPi( p->pManAig, pObj, i ) { pSims = Fra_ObjSim(pObj); - if ( Dar_InfoHasBit(pSims, BestPat) ) - Dar_InfoSetBit(p->pPatWords, i); + if ( Aig_InfoHasBit(pSims, BestPat) ) + Aig_InfoSetBit(p->pPatWords, i); } return MaxScore; } @@ -401,17 +401,17 @@ int Fra_SelectBestPat( Fra_Man_t * p ) ***********************************************************************/ void Fra_SimulateOne( Fra_Man_t * p ) { - Dar_Obj_t * pObj; + Aig_Obj_t * pObj; int i, clk; clk = clock(); - Dar_ManForEachNode( p->pManAig, pObj, i ) + Aig_ManForEachNode( p->pManAig, pObj, i ) { Fra_NodeSimulate( p, pObj ); /* - if ( Dar_ObjFraig(pObj) == NULL ) + if ( Aig_ObjFraig(pObj) == NULL ) printf( "%3d --- -- %d : ", pObj->Id, pObj->fPhase ); else - printf( "%3d %3d %2d %d : ", pObj->Id, Dar_Regular(Dar_ObjFraig(pObj))->Id, Dar_ObjSatNum(Dar_Regular(Dar_ObjFraig(pObj))), pObj->fPhase ); + printf( "%3d %3d %2d %d : ", pObj->Id, Aig_Regular(Aig_ObjFraig(pObj))->Id, Aig_ObjSatNum(Aig_Regular(Aig_ObjFraig(pObj))), pObj->fPhase ); Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 30 ); printf( "\n" ); */ @@ -527,7 +527,7 @@ void Fra_Simulate( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Dar_Obj_t * pObj ) +void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj ) { unsigned * pSims; int i, k, BestPat, * pModel; @@ -545,10 +545,10 @@ void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Dar_Obj_t * pObj ) // determine the best pattern BestPat = i * 32 + k; // fill in the counter-example data - pModel = ALLOC( int, Dar_ManPiNum(p->pManFraig) ); - Dar_ManForEachPi( p->pManAig, pObj, i ) + pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig) ); + Aig_ManForEachPi( p->pManAig, pObj, i ) { - pModel[i] = Dar_InfoHasBit(Fra_ObjSim(pObj), BestPat); + pModel[i] = Aig_InfoHasBit(Fra_ObjSim(pObj), BestPat); // printf( "%d", pModel[i] ); } // printf( "\n" ); @@ -571,26 +571,26 @@ void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Dar_Obj_t * pObj ) ***********************************************************************/ int Fra_CheckOutputSims( Fra_Man_t * p ) { - Dar_Obj_t * pObj; + Aig_Obj_t * pObj; int i; // make sure the reference simulation pattern does not detect the bug - pObj = Dar_ManPo( p->pManAig, 0 ); - assert( Dar_ObjFanin0(pObj)->fPhase == (unsigned)Dar_ObjFaninC0(pObj) ); // Dar_ObjFaninPhase(Dar_ObjChild0(pObj)) == 0 - Dar_ManForEachPo( p->pManAig, pObj, i ) + pObj = Aig_ManPo( p->pManAig, 0 ); + assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); // Aig_ObjFaninPhase(Aig_ObjChild0(pObj)) == 0 + Aig_ManForEachPo( p->pManAig, pObj, i ) { // complement simulation info -// if ( Dar_ObjFanin0(pObj)->fPhase ^ Dar_ObjFaninC0(pObj) ) // Dar_ObjFaninPhase(Dar_ObjChild0(pObj)) -// Fra_NodeComplementSim( p, Dar_ObjFanin0(pObj) ); +// if ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) ) // Aig_ObjFaninPhase(Aig_ObjChild0(pObj)) +// Fra_NodeComplementSim( p, Aig_ObjFanin0(pObj) ); // check - if ( !Fra_NodeHasZeroSim( p, Dar_ObjFanin0(pObj) ) ) + if ( !Fra_NodeHasZeroSim( p, Aig_ObjFanin0(pObj) ) ) { // create the counter-example from this pattern - Fra_CheckOutputSimsSavePattern( p, Dar_ObjFanin0(pObj) ); + Fra_CheckOutputSimsSavePattern( p, Aig_ObjFanin0(pObj) ); return 1; } // complement simulation info -// if ( Dar_ObjFanin0(pObj)->fPhase ^ Dar_ObjFaninC0(pObj) ) -// Fra_NodeComplementSim( p, Dar_ObjFanin0(pObj) ); +// if ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) ) +// Fra_NodeComplementSim( p, Aig_ObjFanin0(pObj) ); } return 0; } |