From a8d75dcc60da15644efbd20529609a1495df229a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 10 Jul 2007 08:01:00 -0700 Subject: [PATCH] Version abc70710 --- abc.rc | 7 +- src/aig/dar/darCore.c | 4 - src/aig/dar/darMan.c | 4 +- src/aig/dar/module.make | 2 + src/aig/fra/fra.h | 8 +- src/aig/fra/fraAnd.c | 18 +-- src/aig/fra/fraClass.c | 263 ++++++++++++++++++++++++++++------------ src/aig/fra/fraCnf.c | 1 + src/aig/fra/fraMan.c | 46 +++++-- src/aig/fra/fraSim.c | 14 ++- src/aig/ivy/ivyFraig.c | 8 +- src/base/abc/abcUtil.c | 3 +- src/base/abci/abc.c | 99 ++++++++++++++- src/base/abci/abcDar.c | 32 +++++ src/opt/kit/kitGraph.c | 2 + src/opt/lpk/lpkCore.c | 8 +- src/opt/lpk/lpkCut.c | 14 ++- src/opt/lpk/lpkMan.c | 2 +- src/opt/lpk/module.make | 14 +-- 19 files changed, 421 insertions(+), 128 deletions(-) diff --git a/abc.rc b/abc.rc index 57879554a..f1cf78d61 100644 --- a/abc.rc +++ b/abc.rc @@ -160,8 +160,9 @@ alias tst6 "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_ #alias t "r c.blif; st; wc c.cnf" #alias t "r test/dsdmap6.blif; lutpack -vw; cec" -alias t "r i10_if4.blif; lp" -alias t1 "r pj1_if4.blif; lp" -alias t2 "r pj1_if6.blif; lp" +#alias t "r i10_if4.blif; lp" +#alias t1 "r pj1_if4.blif; lp" +#alias t2 "r pj1_if6.blif; lp" +alias t "r pj/pj1.blif; st; dfraig -v" diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index 147cd38f5..235637666 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -64,10 +64,6 @@ int Dar_ManRewrite( Dar_Man_t * p ) continue; if ( i > nNodesOld ) break; - if ( pObj->Id == 654 ) - { - int x = 0; - } // compute cuts for the node clk = clock(); pCutSet = Dar_ObjComputeCuts_rec( p, pObj ); diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c index 25b15e9c4..52df88907 100644 --- a/src/aig/dar/darMan.c +++ b/src/aig/dar/darMan.c @@ -94,7 +94,7 @@ Dar_Man_t * Dar_ManStartFrom( Dar_Man_t * p ) Dar_Obj_t * pObj; int i; // create the new manager - pNew = Dar_ManStart(); + pNew = Dar_ManStart( Dar_ManObjIdMax(p) + 1 ); // create the PIs Dar_ManConst1(p)->pData = Dar_ManConst1(pNew); Dar_ManForEachPi( p, pObj, i ) @@ -119,7 +119,7 @@ Dar_Man_t * Dar_ManDup( Dar_Man_t * p ) Dar_Obj_t * pObj; int i; // create the new manager - pNew = Dar_ManStart(); + pNew = Dar_ManStart( Dar_ManObjIdMax(p) + 1 ); // create the PIs Dar_ManConst1(p)->pData = Dar_ManConst1(pNew); Dar_ManForEachPi( p, pObj, i ) diff --git a/src/aig/dar/module.make b/src/aig/dar/module.make index e258757fa..4bf473d43 100644 --- a/src/aig/dar/module.make +++ b/src/aig/dar/module.make @@ -9,5 +9,7 @@ SRC += src/aig/dar/darBalance.c \ src/aig/dar/darMem.c \ src/aig/dar/darObj.c \ src/aig/dar/darOper.c \ + src/aig/dar/darSeq.c \ src/aig/dar/darTable.c \ + src/aig/dar/darTruth.c \ src/aig/dar/darUtil.c diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 41d8692d6..ee52520a5 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 333ef1b13..86cbbc9e9 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 1f2fc1651..ac6a4f4a0 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,10 +36,53 @@ /// 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.] @@ -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 18a5ceb63..a662ade20 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 cccd1d75c..67921318f 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 e8b881595..7207cfa24 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************************************************************* diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index e9a65881b..a922674df 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -733,7 +733,12 @@ 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) ); +// printf( "%d", Ivy_InfoHasBit(pPat, i) ); + } +// printf( "\n" ); + 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 ); @@ -1742,7 +1747,6 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p ) 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; @@ -2018,6 +2022,8 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld ) if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) ) return pObjNew; assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) ); +// printf( "Node = %d. Repr = %d.\n", pObjOld->Id, Ivy_ObjClassNodeRepr(pObjOld)->Id ); + // 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 diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 3de48f005..bb1ae2edb 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -1490,7 +1490,8 @@ void Abc_NtkTransferCopy( Abc_Ntk_t * pNtk ) static inline int Abc_ObjCrossCutInc( Abc_Obj_t * pObj ) { // pObj->pCopy = (void *)(((int)pObj->pCopy)++); - ((char*)pObj->pCopy)++; + int Value = (int)pObj->pCopy; + pObj->pCopy = (void *)(Value + 1); return (int)pObj->pCopy == Abc_ObjFanoutNum(pObj); } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index cd67205cd..06f4299de 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -112,6 +112,7 @@ static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -267,6 +268,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "New AIG", "iresyn", Abc_CommandIResyn, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "isat", Abc_CommandISat, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "ifraig", Abc_CommandIFraig, 1 ); + Cmd_CommandAdd( pAbc, "New AIG", "dfraig", Abc_CommandDFraig, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "iprove", Abc_CommandIProve, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 ); @@ -333,7 +335,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) { extern void Dar_LibStart(); - Dar_LibStart(); +// Dar_LibStart(); } } @@ -352,7 +354,7 @@ void Abc_End() { { extern void Dar_LibStop(); - Dar_LibStop(); +// Dar_LibStop(); } Abc_NtkFraigStoreClean(); @@ -6077,14 +6079,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // Abc_Ntk4VarTable( pNtk ); // Dar_NtkGenerateArrays( pNtk ); // Dar_ManDeriveCnfTest2(); - +/* if ( !Abc_NtkIsStrash(pNtk) ) { fprintf( pErr, "Network should be strashed. Command has failed.\n" ); return 1; } +*/ // pNtkRes = Abc_NtkDar( pNtk ); - pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" ); +// pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" ); + pNtkRes = NULL; if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -6900,6 +6904,93 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c, fProve, fVerbose, fDoSparse; + int nConfLimit; + + extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nConfLimit = 100; + fDoSparse = 0; + fProve = 0; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Cspvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; + case 's': + fDoSparse ^= 1; + break; + case 'p': + fProve ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 0; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: dfraig [-C num] [-spvh]\n" ); + fprintf( pErr, "\t performs fraiging using a new method\n" ); + fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); + fprintf( pErr, "\t-s : toggle considering sparse functions [default = %s]\n", fDoSparse? "yes": "no" ); + fprintf( pErr, "\t-p : toggle proving the miter outputs [default = %s]\n", fProve? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index c2988cbb6..ba3ac89d1 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -21,6 +21,7 @@ #include "abc.h" #include "dar.h" #include "cnf.h" +#include "fra.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -443,6 +444,37 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose ) +{ + Fra_Par_t Params, * pParams = &Params; + Abc_Ntk_t * pNtkAig; + Dar_Man_t * pMan, * pTemp; + pMan = Abc_NtkToDar( pNtk ); + if ( pMan == NULL ) + return NULL; + Fra_ParamsDefault( pParams ); + pParams->nBTLimitNode = nConfLimit; + pParams->fVerbose = fVerbose; + pParams->fProve = fProve; + pParams->fDoSparse = fDoSparse; + pMan = Fra_Perform( pTemp = pMan, pParams ); + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Dar_ManStop( pTemp ); + Dar_ManStop( pMan ); + return pNtkAig; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/kit/kitGraph.c b/src/opt/kit/kitGraph.c index e2deb4eff..8bc7ca91e 100644 --- a/src/opt/kit/kitGraph.c +++ b/src/opt/kit/kitGraph.c @@ -357,6 +357,8 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 1 ); // tried 1 and found not useful in "renode" if ( RetValue == -1 ) return NULL; + if ( Vec_IntSize(vMemory) > 128 ) + return NULL; // printf( "Isop size = %d.\n", Vec_IntSize(vMemory) ); assert( RetValue == 0 || RetValue == 1 ); // derive factored form diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c index aa0368a99..a1da45b50 100644 --- a/src/opt/lpk/lpkCore.c +++ b/src/opt/lpk/lpkCore.c @@ -229,7 +229,6 @@ p->timeMap += clock() - clk; int Lpk_ResynthesizeNode( Lpk_Man_t * p ) { static int Count = 0; - char * pFileName; Kit_DsdNtk_t * pDsdNtk; Lpk_Cut_t * pCut; unsigned * pTruth; @@ -245,6 +244,8 @@ p->timeCuts += clock() - clk; } p->timeCuts += clock() - clk; +//return 0; + if ( p->pPars->fVeryVerbose ) printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals ); // try the good cuts @@ -289,12 +290,13 @@ p->timeTruth += clock() - clk; if ( p->pPars->fVeryVerbose ) { +// char * pFileName; printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ", i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight ); Kit_DsdPrint( stdout, pDsdNtk ); // Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves ); - pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ ); - printf( "Saved truth table in file \"%s\".\n", pFileName ); +// pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ ); +// printf( "Saved truth table in file \"%s\".\n", pFileName ); } // update the network diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c index 12dae15b4..27a0317ce 100644 --- a/src/opt/lpk/lpkCut.c +++ b/src/opt/lpk/lpkCut.c @@ -474,12 +474,16 @@ if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 ) assert( p->nCuts < LPK_CUTS_MAX ); p->nCuts++; - assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup ); +// assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup ); + /* printf( " Creating cut: " ); Lpk_NodePrintCut( p, pCutNew, 1 ); printf( "\n" ); */ + +// if ( !(pCut->nNodes <= p->nMffc + pCutNew->nNodesDup) ) +// printf( "Assertion in line 477 failed.\n" ); } /**Function************************************************************* @@ -519,9 +523,17 @@ int Lpk_NodeCuts( Lpk_Man_t * p ) pCut = p->pCuts + i; if ( pCut->nLeaves == 0 ) continue; + // try to expand the fanins of this cut for ( k = 0; k < (int)pCut->nLeaves; k++ ) { + + if ( p->pObj->Id == 28 && i == 273 && k == 13 ) + { + Abc_Obj_t * pFanin = Abc_NtkObj(p->pNtk, pCut->pLeaves[k]); + int s = 0; + } + // create a new cut Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] ); // quit if the number of cuts has exceeded the limit diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c index 5dd544508..c11a0a334 100644 --- a/src/opt/lpk/lpkMan.c +++ b/src/opt/lpk/lpkMan.c @@ -50,7 +50,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ) p->pPars = pPars; p->nCutsMax = LPK_CUTS_MAX; p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax ); - p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) ); + p->vTtNodes = Vec_PtrAllocSimInfo( 1024, Abc_TruthWordNum(pPars->nVarsMax) ); p->vCover = Vec_IntAlloc( 1 << 12 ); for ( i = 0; i < 8; i++ ) p->vSets[i] = Vec_IntAlloc(100); diff --git a/src/opt/lpk/module.make b/src/opt/lpk/module.make index 9e7bbc7c5..9a46e0cea 100644 --- a/src/opt/lpk/module.make +++ b/src/opt/lpk/module.make @@ -1,7 +1,7 @@ -SRC += src/aig/lpk/lpkCore.c \ - src/aig/lpk/lpkCut.c \ - src/aig/lpk/lpkMan.c \ - src/aig/lpk/lpkMap.c \ - src/aig/lpk/lpkMulti.c \ - src/aig/lpk/lpkMux.c \ - src/aig/lpk/lpkSets.c +SRC += src/opt/lpk/lpkCore.c \ + src/opt/lpk/lpkCut.c \ + src/opt/lpk/lpkMan.c \ + src/opt/lpk/lpkMap.c \ + src/opt/lpk/lpkMulti.c \ + src/opt/lpk/lpkMux.c \ + src/opt/lpk/lpkSets.c