From 28467823812f63a40f9a322b1fefc7decce4b766 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 22 Aug 2007 08:01:00 -0700 Subject: Version abc70822 --- src/aig/fra/fra.h | 6 +- src/aig/fra/fraClass.c | 172 ++++++++++++++++++++++++++++++++++++++++++++++--- src/aig/fra/fraCore.c | 104 ++++++++++++++++++++---------- src/aig/fra/fraImp.c | 16 +++-- src/aig/fra/fraInd.c | 55 +++++++++------- src/aig/fra/fraMan.c | 1 + src/aig/fra/fraPart.c | 86 +++++++++++++++++++++++++ src/aig/fra/fraSec.c | 5 +- src/aig/fra/fraSim.c | 13 +++- 9 files changed, 380 insertions(+), 78 deletions(-) (limited to 'src/aig/fra') diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index c8617d84..217d1fba 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -73,6 +73,7 @@ struct Fra_Par_t_ int nBTLimitMiter; // conflict limit at an output int nFramesP; // the number of timeframes to in the prefix int nFramesK; // the number of timeframes to unroll + int nMaxImps; // the maximum number of implications to consider int fRewrite; // use rewriting for constraint reduction int fLatchCorr; // computes latch correspondence only int fUseImps; // use implications @@ -133,6 +134,7 @@ struct Fra_Man_t_ // counter example storage int nPatWords; // the number of words in the counter example unsigned * pPatWords; // the counter example + Vec_Int_t * vCex; // satisfiability solving sat_solver * pSat; // SAT solver int nSatVars; // the number of variables currently used @@ -226,6 +228,8 @@ extern int Fra_ClassesCountPairs( Fra_Cla_t * p ); extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 ); extern void Fra_ClassesLatchCorr( Fra_Man_t * p ); extern void Fra_ClassesPostprocess( Fra_Cla_t * p ); +extern void Fra_ClassesSelectRepr( Fra_Cla_t * p ); +extern Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ); /*=== fraCnf.c ========================================================*/ extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); /*=== fraCore.c ========================================================*/ @@ -240,7 +244,7 @@ extern int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps extern int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps ); extern void Fra_ImpCompactArray( Vec_Int_t * vImps ); /*=== fraInd.c ========================================================*/ -extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ); +extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index a9d727da..d6db125b 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -114,9 +114,18 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ) int i; Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 ); memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) ); + if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 ) + { + Aig_ManForEachObj( p->pAig, pObj, i ) + { + if ( p->pAig->pReprs[i] != NULL ) + printf( "Classes are not cleared!\n" ); + assert( p->pAig->pReprs[i] == NULL ); + } + } if ( vFailed ) - Vec_PtrForEachEntry( vFailed, pObj, i ) - p->pAig->pReprs[pObj->Id] = NULL; + Vec_PtrForEachEntry( vFailed, pObj, i ) + p->pAig->pReprs[pObj->Id] = NULL; } /**Function************************************************************* @@ -206,7 +215,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass ) assert( Fra_ClassObjRepr(pTemp) == pClass[0] ); printf( "{ " ); for ( i = 0; pTemp = pClass[i]; i++ ) - printf( "%d ", pTemp->Id, Fra_ClassObjRepr(pTemp)? Fra_ClassObjRepr(pTemp)->Id : -1 ); + printf( "%d(%d) ", pTemp->Id, pTemp->Level ); printf( "}\n" ); } @@ -227,8 +236,11 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ) Aig_Obj_t * pObj; int i; - printf( "Const = %5d. Class = %5d. Lit = %5d.\n", + printf( "Const = %5d. Class = %5d. Lit = %5d. ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) ); + if ( p->vImps && Vec_IntSize(p->vImps) > 0 ) + printf( "Imp = %5d. ", Vec_IntSize(p->vImps) ); + printf( "\n" ); if ( fVeryVerbose ) { @@ -283,10 +295,10 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr ) { if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) continue; + // skip the node with more that the given number of levels +// if ( pObj->Level > 3 ) +// continue; } -//printf( "%3d : ", pObj->Id ); -//Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 ); -//printf( "\n" ); // hash the node by its simulation info iEntry = p->pFuncNodeHash( pObj, nTableSize ); // check if the node belongs to the class of constant 1 @@ -494,7 +506,6 @@ int Fra_ClassesRefine( Fra_Cla_t * p ) vTemp = p->vClassesTemp; p->vClassesTemp = p->vClasses; p->vClasses = vTemp; - p->fRefinement = (nRefis > 0); return nRefis; } @@ -531,7 +542,6 @@ int Fra_ClassesRefine1( Fra_Cla_t * p ) Vec_PtrShrink( p->vClasses1, k ); if ( Vec_PtrSize(p->vClassNew) == 0 ) return 0; - p->fRefinement = 1; /* printf( "Refined const-1 class: {" ); Vec_PtrForEachEntry( p->vClassNew, pObj, i ) @@ -675,6 +685,95 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) free( pWeights ); } +/**Function************************************************************* + + Synopsis [Postprocesses the classes by selecting representative lowest in top order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ClassesSelectRepr( Fra_Cla_t * p ) +{ + Aig_Obj_t ** pClass, * pNodeMin; + int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur; + // reassign representatives in each class + Vec_PtrForEachEntry( p->vClasses, pClass, i ) + { + // collect support sizes and find the min-support node + pNodeMin = NULL; + nSuppSizeMin = AIG_INFINITY; + for ( c = 0; pClass[c]; c++ ) + { + nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] ); +// nSuppSizeCur = 1; + if ( nSuppSizeMin > nSuppSizeCur || + (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) ) + { + nSuppSizeMin = nSuppSizeCur; + pNodeMin = pClass[c]; + cMinSupp = c; + } + } + // skip the case when the repr did not change + if ( cMinSupp == 0 ) + continue; + // make the new node the representative of the class + pClass[cMinSupp] = pClass[0]; + pClass[0] = pNodeMin; + // set the representative + for ( c = 0; pClass[c]; c++ ) + Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL ); + } +} + + + +static inline Aig_Obj_t * Fra_ObjEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return ppEquivs[pObj->Id]; } +static inline void Fra_ObjSetEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ppEquivs[pObj->Id] = pNode; } + +static inline Aig_Obj_t * Fra_ObjChild0Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)); } +static inline Aig_Obj_t * Fra_ObjChild1Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)); } + +/**Function************************************************************* + + Synopsis [Add the node and its constraints to the new AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, Aig_Obj_t ** ppEquivs ) +{ + Aig_Obj_t * pObjNew, * pObjRepr, * pObjReprNew, * pMiter;//, * pObjNew2; + // skip nodes without representative + if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL ) + return; + assert( pObjRepr->Id < pObj->Id ); + // get the new node + pObjNew = Fra_ObjEqu( ppEquivs, pObj ); + // get the new node of the representative + pObjReprNew = Fra_ObjEqu( ppEquivs, pObjRepr ); + // if this is the same node, no need to add constraints + if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) ) + return; + // these are different nodes - perform speculative reduction +// pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase ); + // set the new node +// Fra_ObjSetEqu( ppEquivs, pObj, pObjNew2 ); + // add the constraint + pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) ); + pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) ); + pMiter = Aig_Not( pMiter ); + Aig_ObjCreatePo( pManFraig, pMiter ); +} + /**Function************************************************************* Synopsis [Derives AIG for the partitioned problem.] @@ -688,7 +787,60 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) ***********************************************************************/ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ) { - + Aig_Man_t * pManFraig; + Aig_Obj_t * pObj, * pObjNew; + Aig_Obj_t ** pLatches, ** ppEquivs; + int i, k, f, nFramesAll = nFramesK + 1; + assert( Aig_ManRegNum(p->pAig) > 0 ); + assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); + assert( nFramesK > 0 ); + // start the fraig package + pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * nFramesAll ); + // allocate place for the node mapping + ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p->pAig) + 1 ); + Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) ); + // create latches for the first frame + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) ); + // add timeframes + pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) ); + for ( f = 0; f < nFramesAll; f++ ) + { + // create PIs for this frame + Aig_ManForEachPiSeq( p->pAig, pObj, i ) + Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) ); + // set the constraints on the latch outputs + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs ); + // add internal nodes of this frame + Aig_ManForEachNode( p->pAig, pObj, i ) + { + pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) ); + Fra_ObjSetEqu( ppEquivs, pObj, pObjNew ); + Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs ); + } + if ( f == nFramesAll - 1 ) + break; + if ( f == nFramesAll - 2 ) + pManFraig->nAsserts = Aig_ManPoNum(pManFraig); + // save the latch input values + k = 0; + Aig_ManForEachLiSeq( p->pAig, pObj, i ) + pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj ); + // insert them to the latch output values + k = 0; + Aig_ManForEachLoSeq( p->pAig, pObj, i ) + Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] ); + } + free( pLatches ); + free( ppEquivs ); + // mark the asserts + assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 ); +printf( "Assert miters = %6d. Output miters = %6d.\n", + pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts ); + // remove dangling nodes + Aig_ManCleanup( pManFraig ); + return pManFraig; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 3c76af03..9adbb7a9 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -24,6 +24,23 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/* + Speculating reduction in the sequential case leads to an interesting + situation when a counter-ex may not refine any classes. This happens + for non-constant equivalence classes. In such cases the representative + of the class (proved by simulation to be non-constant) may be reduced + to a constant during the speculative reduction. The fraig-representative + of this representative node is a constant node, even though this is a + non-constant class. Experiments have shown that this situation happens + very often at the beginning of the refinement iteration when there are + many spurious candidate equivalence classes (especially if heavy-duty + simulatation of BMC was node used at the beginning). As a result, the + SAT solver run may return a counter-ex that distinguishes the given + representative node from the constant-1 node but this counter-ex + does not distinguish the nodes in the non-costant class... This is why + there is no check of refinment after a counter-ex in the sequential case. +*/ + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -115,6 +132,54 @@ static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_ pNode->pData = p; } +/**Function************************************************************* + + Synopsis [Verifies the generated counter-ex.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex ) +{ + Aig_Obj_t * pObj, ** ppClass; + int i, c; + assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) ); + // make sure the input pattern is not used + Aig_ManForEachObj( p->pManAig, pObj, i ) + assert( !pObj->fMarkB ); + // simulate the cex through the AIG + Aig_ManConst1(p->pManAig)->fMarkB = 1; + Aig_ManForEachPi( p->pManAig, pObj, i ) + pObj->fMarkB = Vec_IntEntry(vCex, i); + Aig_ManForEachNode( p->pManAig, pObj, i ) + pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & + (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); + Aig_ManForEachPo( p->pManAig, pObj, i ) + pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); + // check if the classes hold + Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i ) + { + if ( pObj->fPhase != pObj->fMarkB ) + printf( "The node %d is not constant under cex!\n", pObj->Id ); + } + Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i ) + { + for ( c = 1; ppClass[c]; c++ ) + if ( (ppClass[0]->fPhase ^ ppClass[c]->fPhase) != (ppClass[0]->fMarkB ^ ppClass[c]->fMarkB) ) + printf( "The nodes %d and %d are not equal under cex!\n", ppClass[0]->Id, ppClass[c]->Id ); +// for ( c = 0; ppClass[c]; c++ ) +// if ( Fra_ObjFraig(ppClass[c],p->pPars->nFramesK) == Aig_ManConst1(p->pManFraig) ) +// printf( "A member of non-constant class has a constant repr!\n" ); + } + // clean the simulation pattern + Aig_ManForEachObj( p->pManAig, pObj, i ) + pObj->fMarkB = 0; +} + /**Function************************************************************* Synopsis [Performs fraiging for one node.] @@ -173,47 +238,20 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) ); return; } -//printf( "Disproved %d and %d.\n", pObj->Id, pObjRepr->Id ); // disprove the nodes + p->pCla->fRefinement = 1; // if we do not include the node into those disproved, we may end up // merging this node with another representative, for which proof has timed out if ( p->vTimeouts ) Vec_PtrPush( p->vTimeouts, pObj ); + // verify that the counter-example satisfies all the constraints +// if ( p->vCex ) +// Fra_FraigVerifyCounterEx( p, p->vCex ); // simulate the counter-example and return the Fraig node Fra_SmlResimulate( p ); -/* -printf( "%d -> %d.\n", pObj->Id, pObjRepr->Id ); -Fra_ClassesPrint( p->pCla, 1 ); -printf( "%3d : ", 19 ); -Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 19), 32 * p->pSml->nWordsTotal ); -printf( "\n" ); -printf( "%3d : ", 27 ); -Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 27), 32 * p->pSml->nWordsTotal ); -printf( "\n" ); -printf( "%3d : ", 30 ); -Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 30), 32 * p->pSml->nWordsTotal ); -printf( "\n" ); -printf( "\n\n" ); -*/ - if ( Fra_ClassObjRepr(pObj) == pObjRepr ) - { -/* -//Fra_ClassesPrint( p->pCla, 1 ); -//printf( "\n\n" ); -printf( "%3d : ", pObj->Id ); -Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObj->Id), 32 * p->pSml->nWordsTotal ); -printf( "\n" ); -printf( "%3d : ", pObjRepr->Id ); -Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObjRepr->Id), 32 * p->pSml->nWordsTotal ); -printf( "\n" ); -*/ - if ( Aig_ObjIsPi(pObj) ) - printf( "primary input\n" ); - else - printf( "NOT primary input\n" ); + if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr ) printf( "Fra_FraigNode(): Error in class refinement!\n" ); - } - assert( Fra_ClassObjRepr(pObj) != pObjRepr ); + assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr ); } /**Function************************************************************* diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c index 25b34e03..8af11b78 100644 --- a/src/aig/fra/fraImp.c +++ b/src/aig/fra/fraImp.c @@ -205,7 +205,7 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit ) +Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit, int * pCostRange ) { Vec_Int_t * vImpsNew; int * pCostCount, nImpCount, Imp, i, c; @@ -239,6 +239,8 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, break; } free( pCostCount ); + if ( pCostRange ) + *pCostRange = c; return vImpsNew; } @@ -290,7 +292,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in int * pImpCosts, * pNodesI, * pNodesK; int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0; int CostMin = AIG_INFINITY, CostMax = 0; - int i, k, Imp, clk = clock(); + int i, k, Imp, CostRange, clk = clock(); assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit ); // normalize both managers pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords ); @@ -350,9 +352,10 @@ finish: Fra_SmlStop( pSeq ); // select implications with the highest cost + CostRange = CostMin; if ( Vec_IntSize(vImps) > nImpUseLimit ) { - vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit ); + vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange ); Vec_IntFree( vTemp ); } @@ -365,8 +368,8 @@ finish: (int (*)(const void *, const void *)) Sml_CompareMaxId ); if ( p->pPars->fVerbose ) { -printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d. Cost = [%d - %d] ", - nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostMax ); +printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d. Cost = [%d < %d < %d] ", + nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostRange, CostMax ); PRT( "Time", clock() - clk ); } return vImps; @@ -381,7 +384,7 @@ PRT( "Time", clock() - clk ); Synopsis [Add implication clauses to the SAT solver.] - Description [] + Description [Note that implications should be checked in the first frame!] SideEffects [] @@ -540,7 +543,6 @@ int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps ) { Vec_IntWriteEntry( vImps, i, 0 ); RetValue = 1; - p->pCla->fRefinement = 1; } } return RetValue; diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index d754f3ae..6d8305c0 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -50,11 +50,9 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p ) pTemp = Aig_ManDup( p->pManFraig, 0 ); // pTemp = Dar_ManRwsat( pTemp, 1, 0 ); pTemp = Dar_ManRewriteDefault( pTemp ); - // printf( "Before = %6d. After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) ); //Aig_ManDumpBlif( p->pManFraig, "1.blif" ); //Aig_ManDumpBlif( pTemp, "2.blif" ); - // Fra_FramesWriteCone( pTemp ); // Aig_ManStop( pTemp ); // transfer PI/register pointers @@ -128,8 +126,7 @@ static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * p Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) { Aig_Man_t * pManFraig; - Aig_Obj_t * pObj, * pObjNew; - Aig_Obj_t ** pLatches; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; int i, k, f; assert( p->pManFraig == NULL ); assert( Aig_ManRegNum(p->pManAig) > 0 ); @@ -149,7 +146,6 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) ); // add timeframes - pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pManAig) ); for ( f = 0; f < p->nFramesAll - 1; f++ ) { // set the constraints on the latch outputs @@ -162,23 +158,15 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) Fra_ObjSetFraig( pObj, f, pObjNew ); Fra_FramesConstrainNode( pManFraig, pObj, f ); } - // save the latch input values - k = 0; - Aig_ManForEachLiSeq( p->pManAig, pObj, i ) - pLatches[k++] = Fra_ObjChild0Fra(pObj,f); - assert( k == Aig_ManRegNum(p->pManAig) ); - // insert them to the latch output values - k = 0; - Aig_ManForEachLoSeq( p->pManAig, pObj, i ) - Fra_ObjSetFraig( pObj, f+1, pLatches[k++] ); - assert( k == Aig_ManRegNum(p->pManAig) ); + // transfer latch input to the latch outputs + Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k ) + Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) ); } - free( pLatches ); // mark the asserts pManFraig->nAsserts = Aig_ManPoNum(pManFraig); - // add the POs for the latch inputs - Aig_ManForEachLiSeq( p->pManAig, pObj, i ) - Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) ); + // add the POs for the latch outputs of the last frame + Aig_ManForEachLoSeq( p->pManAig, pObj, i ) + Aig_ObjCreatePo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) ); // remove dangling nodes Aig_ManCleanup( pManFraig ); @@ -198,7 +186,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ) +Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter ) { int fUseSimpleCnf = 0; int fUseOldSimulation = 0; @@ -229,6 +217,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, Fra_ParamsDefaultSeq( pPars ); pPars->nFramesP = nFramesP; pPars->nFramesK = nFramesK; + pPars->nMaxImps = nMaxImps; pPars->fVerbose = fVerbose; pPars->fRewrite = fRewrite; pPars->fLatchCorr = fLatchCorr; @@ -249,9 +238,16 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, } else { + // bug: r iscas/blif/s5378.blif ; st; ssw -v // bug: r iscas/blif/s1238.blif ; st; ssw -v // refine the classes with more simulation rounds - p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 2 ); //pPars->nFramesK + 1, 6 ); // 32, 2 ); +if ( fVerbose ) +printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 ); + p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 ); +if ( fVerbose ) +{ +PRT( "Time", clock() - clk ); +} Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr ); // Fra_ClassesPostprocess( p->pCla ); // allocate new simulation manager for simulating counter-examples @@ -259,19 +255,26 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords ); } - // perform BMC - Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK + 1 ); + // perform BMC (for the min number of frames) + Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK ); //Fra_ClassesPrint( p->pCla, 1 ); +// p->vCex = Vec_IntAlloc( 1000 ); // select the most expressive implications if ( pPars->fUseImps ) - p->pCla->vImps = Fra_ImpDerive( p, 5000000, 5000, pPars->fLatchCorr ); + p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr ); p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 ); p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); p->nNodesBeg = Aig_ManNodeNum(pManAig); p->nRegsBeg = Aig_ManRegNum(pManAig); + // dump AIG of the timeframes +// pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK ); +// Aig_ManDumpBlif( pManAigNew, "frame_aig.blif" ); +// Fra_ManPartitionTest2( pManAigNew ); +// Aig_ManStop( pManAigNew ); + // iterate the inductive case p->pCla->fRefinement = 1; for ( nIter = 0; p->pCla->fRefinement; nIter++ ) @@ -341,7 +344,11 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, // cleanup Fra_ManClean( p ); +// if ( nIter == 3 ) +// break; } +// Fra_ClassesPrint( p->pCla, 1 ); +// Fra_ClassesSelectRepr( p->pCla ); // move the classes into representatives and reduce AIG clk2 = clock(); Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index 2b8e0a68..0116bbc4 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -248,6 +248,7 @@ void Fra_ManStop( Fra_Man_t * p ) if ( p->pSat ) sat_solver_delete( p->pSat ); if ( p->pCla ) Fra_ClassesStop( p->pCla ); if ( p->pSml ) Fra_SmlStop( p->pSml ); + if ( p->vCex ) Vec_IntFree( p->vCex ); FREE( p->pMemFraig ); FREE( p->pMemFanins ); FREE( p->pMemSatNums ); diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c index d3fdbcfd..6e593694 100644 --- a/src/aig/fra/fraPart.c +++ b/src/aig/fra/fraPart.c @@ -170,6 +170,92 @@ PRT( "Scanning", clock() - clk ); +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_ManPartitionTest2( Aig_Man_t * p ) +{ + Vec_Vec_t * vSupps, * vSuppsIn; + Vec_Int_t * vSup, * vSup2, * vSup3; + Aig_Obj_t * pObj; + int Entry, Entry2, Entry3, Counter; + int i, k, m, n, clk; + char * pSupp; + + // compute supports +clk = clock(); + vSupps = Aig_ManSupports( p ); +PRT( "Supports", clock() - clk ); + // remove last entry + Aig_ManForEachPo( p, pObj, i ) + { + vSup = Vec_VecEntry( vSupps, i ); + Vec_IntPop( vSup ); + // remember support +// pObj->pNext = (Aig_Obj_t *)vSup; + } + + // create reverse supports +clk = clock(); + vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + { + if ( i == p->nAsserts ) + break; + vSup = Vec_VecEntry( vSupps, i ); + Vec_IntForEachEntry( vSup, Entry, k ) + Vec_VecPush( vSuppsIn, Entry, (void *)i ); + } +PRT( "Inverse ", clock() - clk ); + + // create affective supports +clk = clock(); + pSupp = ALLOC( char, Aig_ManPiNum(p) ); + Aig_ManForEachPo( p, pObj, i ) + { + if ( i % 50 != 0 ) + continue; + vSup = Vec_VecEntry( vSupps, i ); + memset( pSupp, 0, sizeof(char) * Aig_ManPiNum(p) ); + // go through each input of this output + Vec_IntForEachEntry( vSup, Entry, k ) + { + pSupp[Entry] = 1; + vSup2 = Vec_VecEntry( vSuppsIn, Entry ); + // go though each assert of this input + Vec_IntForEachEntry( vSup2, Entry2, m ) + { + vSup3 = Vec_VecEntry( vSupps, Entry2 ); + // go through each input of this assert + Vec_IntForEachEntry( vSup3, Entry3, n ) + { + pSupp[Entry3] = 1; + } + } + } + // count the entries + Counter = 0; + for ( m = 0; m < Aig_ManPiNum(p); m++ ) + Counter += pSupp[m]; + printf( "%d(%d) ", Vec_IntSize(vSup), Counter ); + } + printf( "\n" ); +PRT( "Extension ", clock() - clk ); + + free( pSupp ); + Vec_VecFree( vSupps ); + Vec_VecFree( vSuppsIn ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 2a0d06b5..8b9258cb 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -43,11 +43,12 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose { Aig_Man_t * pNew; int nFrames, RetValue, nIter, clk, clkTotal = clock(); + int fLatchCorr = 0; if ( nFramesFix ) { nFrames = nFramesFix; // perform seq sweeping for one frame number - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter ); } else { @@ -55,7 +56,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose for ( nFrames = 1; ; nFrames++ ) { clk = clock(); - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter ); + pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter ); RetValue = Fra_FraigMiterStatus( pNew ); if ( fVerbose ) { diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index b31fcb7f..3463ee0d 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -199,6 +199,17 @@ void Fra_SmlSavePattern( Fra_Man_t * p ) Aig_ManForEachPi( p->pManFraig, pObj, i ) if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True ) Aig_InfoSetBit( p->pPatWords, i ); +/* + if ( p->vCex ) + { + Vec_IntClear( p->vCex ); + for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ ) + Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) ); + for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ ) + Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) ); + } +*/ + /* printf( "Pattern: " ); Aig_ManForEachPi( p->pManFraig, pObj, i ) @@ -601,7 +612,7 @@ clk = clock(); if ( p->pCla->vImps ) nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps ); p->timeRef += clock() - clk; - if ( nChanges < 1 ) + if ( !p->pPars->nFramesK && nChanges < 1 ) printf( "Error: A counter-example did not refine classes!\n" ); // assert( nChanges >= 1 ); //printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges ); -- cgit v1.2.3