diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-10 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-10 08:01:00 -0700 |
commit | a8d75dcc60da15644efbd20529609a1495df229a (patch) | |
tree | 2ff1676ca093b5fc6c4684d59212fc24e030ffb1 /src/aig/fra | |
parent | 39bc4842e9a3e0c443df5e585bfdece76320870a (diff) | |
download | abc-a8d75dcc60da15644efbd20529609a1495df229a.tar.gz abc-a8d75dcc60da15644efbd20529609a1495df229a.tar.bz2 abc-a8d75dcc60da15644efbd20529609a1495df229a.zip |
Version abc70710
Diffstat (limited to 'src/aig/fra')
-rw-r--r-- | src/aig/fra/fra.h | 8 | ||||
-rw-r--r-- | src/aig/fra/fraAnd.c | 18 | ||||
-rw-r--r-- | src/aig/fra/fraClass.c | 263 | ||||
-rw-r--r-- | src/aig/fra/fraCnf.c | 1 | ||||
-rw-r--r-- | src/aig/fra/fraMan.c | 46 | ||||
-rw-r--r-- | src/aig/fra/fraSim.c | 14 |
6 files changed, 249 insertions, 101 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 41d8692d..ee52520a 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -142,14 +142,14 @@ static inline Dar_Obj_t * Fra_ObjRepr( Dar_Obj_t * pObj ) 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 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 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 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; } + //////////////////////////////////////////////////////////////////////// /// ITERATORS /// //////////////////////////////////////////////////////////////////////// @@ -161,6 +161,7 @@ static inline void Fra_ObjSetSatNum( Dar_Obj_t * pObj, int Num ) /*=== fraAnd.c ========================================================*/ extern void Fra_Sweep( Fra_Man_t * p ); /*=== fraClass.c ========================================================*/ +extern void Fra_PrintClasses( Fra_Man_t * p ); extern void Fra_CreateClasses( Fra_Man_t * p ); extern int Fra_RefineClasses( Fra_Man_t * p ); extern int Fra_RefineClasses1( Fra_Man_t * p ); @@ -171,6 +172,7 @@ extern Dar_Man_t * Fra_Perform( Dar_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 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 ========================================================*/ diff --git a/src/aig/fra/fraAnd.c b/src/aig/fra/fraAnd.c index 333ef1b1..86cbbc9e 100644 --- a/src/aig/fra/fraAnd.c +++ b/src/aig/fra/fraAnd.c @@ -51,14 +51,15 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld ) pFanin1Fraig = Fra_ObjChild1Fra(pObjOld); // get the fraiged node pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig ); + Dar_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 { assert( Dar_Regular(pFanin0Fraig) != Dar_Regular(pFanin1Fraig) ); - assert( pObjFraig != Dar_Regular(pFanin0Fraig) ); - assert( pObjFraig != Dar_Regular(pFanin1Fraig) ); + assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin0Fraig) ); + assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin1Fraig) ); return pObjFraig; } // get the fraiged representative @@ -67,11 +68,13 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld ) if ( Dar_Regular(pObjFraig) == Dar_Regular(pObjOldReprFraig) ) return pObjFraig; assert( Dar_Regular(pObjFraig) != Dar_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) ); if ( RetValue == 1 ) // proved equivalent { - pObjOld->fMarkA = 1; +// pObjOld->fMarkA = 1; return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase ); } if ( RetValue == -1 ) // failed @@ -79,11 +82,12 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld ) if ( !p->pPars->fSpeculate ) return pObjFraig; // substitute the node - pObjOld->fMarkB = 1; +// pObjOld->fMarkB = 1; return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase ); } // simulate the counter-example and return the Fraig node Fra_Resimulate( p ); + assert( Fra_ObjRepr(pObjOld) != pObjOldRepr ); return pObjFraig; } @@ -103,7 +107,7 @@ void Fra_Sweep( Fra_Man_t * p ) Dar_Obj_t * pObj, * pObjNew; int i, k = 0; p->nClassesZero = Vec_PtrSize(p->vClasses1); -p->nClassesBeg = Vec_PtrSize(p->vClasses); +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 ) @@ -114,11 +118,11 @@ p->nClassesBeg = Vec_PtrSize(p->vClasses); pObjNew = Dar_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) ); else pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented - assert( Fra_ObjFraig(pObj) != NULL ); Fra_ObjSetFraig( pObj, pObjNew ); + assert( Fra_ObjFraig(pObj) != NULL ); } // Extra_ProgressBarStop( p->pProgress ); -p->nClassesEnd = Vec_PtrSize(p->vClasses); +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); // Fra_MiterStatus( p->pManFraig ); diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 1f2fc165..ac6a4f4a 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -25,6 +25,7 @@ to the array of pointers to the nodes in each class. The first node of the class is its representative node. The representative has the smallest topological order among the class nodes. + The nodes inside each class are ordered according to their topological order. The classes are ordered according to the topological order of their representatives. The array of pointers to the class nodes is terminated with a NULL pointer. To enable dynamic addition of new classes (during class refinement), @@ -35,12 +36,55 @@ /// 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; } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* + Synopsis [Prints simulation classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_PrintClass( Dar_Obj_t ** pClass ) +{ + Dar_Obj_t * pTemp; + int i; + printf( "{ " ); + for ( i = 0; pTemp = pClass[i]; i++ ) + printf( "%d ", pTemp->Id ); + printf( "}\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints simulation classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fra_CountClass( Dar_Obj_t ** pClass ) +{ + Dar_Obj_t * pTemp; + int i; + for ( i = 0; pTemp = pClass[i]; i++ ); + return i; +} + +/**Function************************************************************* + Synopsis [Count the number of pairs.] Description [] @@ -56,22 +100,40 @@ int Fra_CountPairsClasses( Fra_Man_t * p ) int i, nNodes, nPairs = 0; Vec_PtrForEachEntry( p->vClasses, pClass, i ) { - for ( nNodes = 0; pClass[nNodes]; nNodes++ ) - { - if ( nNodes > DAR_INFINITY ) - { - printf( "Error in equivalence classes.\n" ); - break; - } - } - nPairs += (nNodes - 1) * (nNodes - 2) / 2; + nNodes = Fra_CountClass( pClass ); + assert( nNodes > 1 ); + nPairs += nNodes * (nNodes - 1) / 2; } return nPairs; } /**Function************************************************************* - Synopsis [Computes hash value using simulation info.] + Synopsis [Prints simulation classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_PrintClasses( Fra_Man_t * p ) +{ + Dar_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 ) + { +// printf( "%3d (%3d) : ", Fra_CountClass(pClass) ); +// Fra_PrintClass( pClass ); + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Computes hash value of the node using its simulation info.] Description [] @@ -102,7 +164,7 @@ unsigned Fra_NodeHash( Fra_Man_t * p, Dar_Obj_t * pObj ) int i; assert( p->nSimWords <= 128 ); uHash = 0; - pSims = Fra_ObjSim(pObj); + pSims = Fra_ObjSim(pObj); for ( i = 0; i < p->nSimWords; i++ ) uHash ^= pSims[i] * s_FPrimes[i]; return uHash; @@ -110,7 +172,7 @@ unsigned Fra_NodeHash( Fra_Man_t * p, Dar_Obj_t * pObj ) /**Function******************************************************************** - Synopsis [Returns the next prime >= p.] + Synopsis [Returns the next prime >= p.] Description [Copied from CUDD, for stand-aloneness.] @@ -158,18 +220,21 @@ unsigned int Cudd_PrimeFra( unsigned int p ) ***********************************************************************/ void Fra_CreateClasses( Fra_Man_t * p ) { - Dar_Obj_t ** pTable; - Dar_Obj_t * pObj; - int i, k, k2, nTableSize, nEntries, iEntry; - // allocate the table - nTableSize = Cudd_PrimeFra( Dar_ManNodeNum(p->pManAig) ); - pTable = ALLOC( Dar_Obj_t *, nTableSize ); - memset( pTable, 0, sizeof(Dar_Obj_t *) * nTableSize ); - // collect nodes into the table + Dar_Obj_t ** ppTable, ** ppNexts; + Dar_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 ); + + // add all the nodes to the hash table Vec_PtrClear( p->vClasses1 ); Dar_ManForEachObj( p->pManAig, pObj, i ) { - if ( !Dar_ObjIsPi(pObj) && !Dar_ObjIsNode(pObj) ) + if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) ) continue; // hash the node by its simulation info iEntry = Fra_NodeHash( p, pObj ) % nTableSize; @@ -177,52 +242,80 @@ 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) ); continue; } - // add the node to the table - pObj->pData = pTable[iEntry]; - pTable[iEntry] = pObj; + // add the node to the class + if ( ppTable[iEntry] == NULL ) + { + ppTable[iEntry] = pObj; + Fra_ObjSetNext( ppNexts, pObj, pObj ); + } + else + { + Fra_ObjSetNext( ppNexts, pObj, Fra_ObjNext(ppNexts,ppTable[iEntry]) ); + Fra_ObjSetNext( ppNexts, ppTable[iEntry], pObj ); + } } + // count the total number of nodes in the non-trivial classes + // mark the representative nodes of each equivalence class nEntries = 0; for ( i = 0; i < nTableSize; i++ ) - if ( pTable[i] && pTable[i]->pData ) + if ( ppTable[i] && ppTable[i] != Fra_ObjNext(ppNexts, ppTable[i]) ) { - k = 0; - for ( pObj = pTable[i]; pObj; pObj = pObj->pData ) - k++; - nEntries += 2*k; + for ( pTemp = Fra_ObjNext(ppNexts, ppTable[i]), k = 1; + pTemp != ppTable[i]; + pTemp = Fra_ObjNext(ppNexts, pTemp), k++ ); + assert( k > 1 ); + nEntries += k; + // mark the node + assert( ppTable[i]->fMarkA == 0 ); + ppTable[i]->fMarkA = 1; } + // allocate room for classes - p->pMemClasses = ALLOC( Dar_Obj_t *, nEntries + 2*Vec_PtrSize(p->vClasses1) ); - p->pMemClassesFree = p->pMemClasses + nEntries; - // copy the entries into storage + p->pMemClasses = ALLOC( Dar_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; - for ( i = 0; i < nTableSize; i++ ) - if ( pTable[i] && pTable[i]->pData ) + Dar_ManForEachObj( p->pManAig, pObj, i ) + { + if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) ) + continue; + // skip the nodes that are not representatives of non-trivial classes + if ( pObj->fMarkA == 0 ) + continue; + pObj->fMarkA = 0; + // add the class of nodes + Vec_PtrPush( p->vClasses, p->pMemClasses + 2*nEntries ); + // count the number of entries in this class + for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; + pTemp != pObj; + pTemp = Fra_ObjNext(ppNexts, pTemp), k++ ); + nNodes = k; + assert( nNodes > 1 ); + // add the nodes to the class in the topological order + p->pMemClasses[2*nEntries] = pObj; + for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; + pTemp != pObj; + pTemp = Fra_ObjNext(ppNexts, pTemp), k++ ) { - k = 0; - for ( pObj = pTable[i]; pObj; pObj = pObj->pData ) - k++; - // write entries in the topological order - k2 = k; - for ( pObj = pTable[i]; pObj; pObj = pObj->pData ) - { - k2--; - p->pMemClasses[nEntries+k2] = pObj; - p->pMemClasses[nEntries+k+k2] = NULL; - } - assert( k2 == 0 ); - Vec_PtrPush( p->vClasses, p->pMemClasses + nEntries ); - nEntries += 2*k; + p->pMemClasses[2*nEntries+nNodes-k] = pTemp; + Fra_ObjSetRepr( pTemp, pObj ); } - free( pTable ); + // add as many empty entries +// memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Dar_Obj_t *) * nNodes ); + p->pMemClasses[2*nEntries + nNodes] = NULL; + // increment the number of entries + nEntries += k; + } + free( ppTable ); + free( ppNexts ); // now it is time to refine the classes Fra_RefineClasses( p ); - // set the pointer to the manager - Dar_ManForEachObj( p->pManAig, pObj, i ) - pObj->pData = p->pManAig; } /**Function************************************************************* @@ -236,40 +329,42 @@ void Fra_CreateClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** pClass ) +Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass ) { - Dar_Obj_t * pObj; + Dar_Obj_t * pObj, ** ppThis; int i; - assert( pClass[1] != NULL ); + assert( ppClass[0] != NULL && ppClass[1] != NULL ); // check if the class is going to be refined - for ( pObj = pClass[1]; pObj; pObj++ ) - if ( !Fra_NodeCompareSims(p, pClass[0], pObj) ) + for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ ) + if ( !Fra_NodeCompareSims(p, ppClass[0], pObj) ) break; if ( pObj == NULL ) return NULL; // split the class Vec_PtrClear( p->vClassOld ); Vec_PtrClear( p->vClassNew ); - Vec_PtrPush( p->vClassOld, pClass[0] ); - for ( pObj = pClass[1]; pObj; pObj++ ) - if ( Fra_NodeCompareSims(p, pClass[0], pObj) ) + Vec_PtrPush( p->vClassOld, ppClass[0] ); + for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ ) + if ( Fra_NodeCompareSims(p, ppClass[0], pObj) ) Vec_PtrPush( p->vClassOld, pObj ); else Vec_PtrPush( p->vClassNew, pObj ); // put the nodes back into the class memory Vec_PtrForEachEntry( p->vClassOld, pObj, i ) { - pClass[i] = pObj; - pClass[Vec_PtrSize(p->vClassOld)+i] = NULL; + ppClass[i] = pObj; + ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL; + Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL ); } - pClass += 2*Vec_PtrSize(p->vClassOld); + ppClass += 2*Vec_PtrSize(p->vClassOld); // put the new nodes into the class memory Vec_PtrForEachEntry( p->vClassNew, pObj, i ) { - pClass[i] = pObj; - pClass[Vec_PtrSize(p->vClassNew)+i] = NULL; + ppClass[i] = pObj; + ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL; + Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL ); } - return pClass; + return ppClass; } /**Function************************************************************* @@ -295,7 +390,10 @@ int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses ) Vec_PtrPop( vClasses ); // if the new class is trivial, stop if ( pClass2[1] == NULL ) + { + nRefis++; break; + } // othewise, add the class and continue Vec_PtrPush( vClasses, pClass2 ); pClass = pClass2; @@ -319,7 +417,7 @@ int Fra_RefineClasses( Fra_Man_t * p ) { Vec_Ptr_t * vTemp; Dar_Obj_t ** pClass; - int clk, i, nRefis = 0; + int clk, i, nRefis; // check if some outputs already became non-constant // this is a special case when computation can be stopped!!! if ( p->pPars->fProve ) @@ -328,12 +426,13 @@ int Fra_RefineClasses( Fra_Man_t * p ) return 0; // refine the classes clk = clock(); + nRefis = 0; Vec_PtrClear( p->vClassesTemp ); Vec_PtrForEachEntry( p->vClasses, pClass, i ) { // add the class to the new array Vec_PtrPush( p->vClassesTemp, pClass ); - // refine the class interatively + // refine the class iteratively nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp ); } // exchange the class representation @@ -357,11 +456,17 @@ p->timeRef += clock() - clk; ***********************************************************************/ int Fra_RefineClasses1( Fra_Man_t * p ) { - Dar_Obj_t * pObj, ** pClass; - int i, k; + Dar_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) ); // collect all the nodes to be refined - Vec_PtrClear( p->vClassNew ); k = 0; + Vec_PtrClear( p->vClassNew ); Vec_PtrForEachEntry( p->vClasses1, pObj, i ) { if ( Fra_NodeHasZeroSim( p, pObj ) ) @@ -373,18 +478,24 @@ int Fra_RefineClasses1( Fra_Man_t * p ) if ( Vec_PtrSize(p->vClassNew) == 0 ) return 0; if ( Vec_PtrSize(p->vClassNew) == 1 ) + { + Fra_ObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL ); return 1; + } // create a new class composed of these nodes - pClass = p->pMemClassesFree; + ppClass = p->pMemClassesFree; p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew); Vec_PtrForEachEntry( p->vClassNew, pObj, i ) { - pClass[i] = pObj; - pClass[Vec_PtrSize(p->vClassNew)+i] = NULL; + ppClass[i] = pObj; + ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL; + Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL ); } - Vec_PtrPush( p->vClasses, pClass ); + Vec_PtrPush( p->vClasses, ppClass ); // iteratively refine this class - return 1 + Fra_RefineClassLastIter( p, p->vClasses ); + nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses ); +p->timeRef += clock() - clk; + return nRefis; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c index 18a5ceb6..a662ade2 100644 --- a/src/aig/fra/fraCnf.c +++ b/src/aig/fra/fraCnf.c @@ -209,6 +209,7 @@ Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes ) ***********************************************************************/ void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontier ) { + Fra_Man_t * pTemp = pObj->pData; assert( !Dar_IsComplement(pObj) ); if ( Fra_ObjSatNum(pObj) ) return; diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index cccd1d75..67921318 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -69,8 +69,6 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars ) { Fra_Man_t * p; - Dar_Obj_t * pObj; - int i; // allocate the fraiging manager p = ALLOC( Fra_Man_t, 1 ); memset( p, 0, sizeof(Fra_Man_t) ); @@ -82,13 +80,17 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars ) p->nSimWords = pPars->nSimWords; p->pSimWords = ALLOC( unsigned, (Dar_ManObjIdMax(pManAig) + 1) * p->nSimWords ); // clean simulation info of the constant node - memset( p->pSimWords, 0, p->nSimWords * sizeof(unsigned) ); + memset( p->pSimWords, 0, sizeof(unsigned) * ((Dar_ManPiNum(pManAig) + 1) * p->nSimWords) ); // allocate storage for sim pattern p->nPatWords = Dar_BitWordNum( Dar_ManPiNum(pManAig) ); p->pPatWords = ALLOC( unsigned, p->nPatWords ); p->pPatScores = ALLOC( int, 32 * p->nSimWords ); p->vPiVars = Vec_PtrAlloc( 100 ); p->vClasses = Vec_PtrAlloc( 100 ); + p->vClasses1 = Vec_PtrAlloc( 100 ); + p->vClassOld = Vec_PtrAlloc( 100 ); + 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 ); @@ -98,17 +100,41 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars ) p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc ); memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) ); p->pMemSatNums = ALLOC( int, p->nSizeAlloc ); - memset( p->pMemSatNums, 0xff, p->nSizeAlloc * sizeof(int) ); + memset( p->pMemSatNums, 0, p->nSizeAlloc * sizeof(int) ); + // set random number generator + srand( 0xABCABC ); + // make sure the satisfying assignment is node assigned + assert( p->pManFraig->pData == NULL ); + // connect AIG managers to the FRAIG manager + Fra_ManPrepare( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [Prepares managers by transfering pointers to the objects.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ManPrepare( Fra_Man_t * p ) +{ + Dar_Obj_t * pObj; + int i; + // set the pointers to the manager + Dar_ManForEachObj( p->pManFraig, pObj, i ) + pObj->pData = p; + // set the pointer to the manager + Dar_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) ); - // set the pointers to the manager - Dar_ManForEachObj( p->pManFraig, pObj, i ) - pObj->pData = p->pManFraig; - // set random number generator - srand( 0xABCABC ); - return p; } /**Function************************************************************* diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index e8b88159..7207cfa2 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -105,7 +105,11 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat ) Dar_Obj_t * pObj; int i, Limit; Dar_ManForEachPi( p->pManAig, pObj, i ) + { Fra_NodeAssignConst( p, pObj, Dar_InfoHasBit(pPat, i) ); +// printf( "%d", Dar_InfoHasBit(pPat, i) ); + } +// printf( "\n" ); Limit = DAR_MIN( Dar_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 ); for ( i = 0; i < Limit; i++ ) Dar_InfoXorBit( Fra_ObjSim( Dar_ManPi(p->pManAig,i) ), i+1 ); @@ -441,7 +445,7 @@ void Fra_Resimulate( Fra_Man_t * 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 ); +//printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges ); if ( !p->pPars->fPatScores ) return; @@ -487,7 +491,7 @@ void Fra_Simulate( Fra_Man_t * p ) Fra_SimulateOne( p ); nChanges = Fra_RefineClasses( p ); nChanges += Fra_RefineClasses1( p ); - if ( p->pManFraig ) + if ( p->pManFraig->pData ) return; //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) ); Fra_SavePattern1( p ); @@ -495,7 +499,7 @@ void Fra_Simulate( Fra_Man_t * p ) Fra_SimulateOne( p ); nChanges = Fra_RefineClasses( p ); nChanges += Fra_RefineClasses1( p ); - if ( p->pManFraig ) + if ( p->pManFraig->pData ) return; //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) ); // refine classes by random simulation @@ -505,11 +509,11 @@ void Fra_Simulate( Fra_Man_t * p ) nClasses = Vec_PtrSize(p->vClasses); nChanges = Fra_RefineClasses( p ); nChanges += Fra_RefineClasses1( p ); - if ( p->pManFraig ) + if ( p->pManFraig->pData ) return; //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) ); } while ( (double)nChanges / nClasses > p->pPars->dSimSatur ); -// Fra_PrintSimClasses( p ); +// Fra_PrintClasses( p ); } /**Function************************************************************* |