diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/dch/dchMan.c | 9 | ||||
-rw-r--r-- | src/aig/dch/dchSimSat.c | 7 | ||||
-rw-r--r-- | src/aig/fra/fraClass.c | 2 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 6 | ||||
-rw-r--r-- | src/aig/ivy/ivyFraig.c | 7 | ||||
-rw-r--r-- | src/aig/ssw/sswAig.c | 38 | ||||
-rw-r--r-- | src/aig/ssw/sswClass.c | 59 | ||||
-rw-r--r-- | src/aig/ssw/sswCore.c | 23 | ||||
-rw-r--r-- | src/aig/ssw/sswInt.h | 4 | ||||
-rw-r--r-- | src/aig/ssw/sswMan.c | 31 | ||||
-rw-r--r-- | src/aig/ssw/sswSat.c | 80 | ||||
-rw-r--r-- | src/aig/ssw/sswSimSat.c | 66 | ||||
-rw-r--r-- | src/aig/ssw/sswSweep.c | 88 |
13 files changed, 303 insertions, 117 deletions
diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c index 6c005fbf..a5faa2a6 100644 --- a/src/aig/dch/dchMan.c +++ b/src/aig/dch/dchMan.c @@ -170,16 +170,21 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p ) sat_solver_setnvars( p->pSat, 1000 ); // var 0 is not used // var 1 is reserved for const1 node - add the clause - Lit = toLit( 1 ); + p->nSatVars = 1; +// p->nSatVars = 0; + Lit = toLit( p->nSatVars ); if ( p->pPars->fPolarFlip ) Lit = lit_neg( Lit ); sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); - p->nSatVars = 2; + Dch_ObjSetSatNum( p, Aig_ManConst1(p->pAigFraig), p->nSatVars++ ); + p->nRecycles++; p->nCallsSince = 0; } + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c index 1fefa6eb..7a6865bd 100644 --- a/src/aig/dch/dchSimSat.c +++ b/src/aig/dch/dchSimSat.c @@ -108,8 +108,11 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj ) Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj); if ( Aig_ObjIsPi(pObj) ) { - Aig_Obj_t * pObjFraig = Dch_ObjFraig( pObj ); - int nVarNum = Dch_ObjSatNum( p, pObjFraig ); + Aig_Obj_t * pObjFraig; + int nVarNum; + pObjFraig = Dch_ObjFraig( pObj ); + assert( !Aig_IsComplement(pObjFraig) ); + nVarNum = Dch_ObjSatNum( p, pObjFraig ); // get the value from the SAT solver // (account for the fact that some vars may be minimized away) pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum ); diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 498ea758..442cf80e 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -296,7 +296,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs ) if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) continue; // skip the node with more that the given number of levels - if ( nMaxLevs && (int)pObj->Level >= nMaxLevs ) + if ( nMaxLevs && (int)pObj->Level > nMaxLevs ) continue; } // hash the node by its simulation info diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 668c20cb..76c7abad 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -505,6 +505,7 @@ PRT( "Time", clock() - clk ); int nLitsOld = Fra_ClassesCountLits(p->pCla); int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0; int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0; + int clk3 = clock(); if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop ) { @@ -571,7 +572,7 @@ p->timeTrav += clock() - clk2; // report the intermediate results if ( pPars->fVerbose ) { - printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. ", + printf( "%3d : Const = %6d. Cl = %6d. L = %6d. LR = %6d. ", nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts ); if ( p->pCla->vImps ) @@ -579,7 +580,8 @@ p->timeTrav += clock() - clk2; if ( p->pPars->fUse1Hot ) printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) ); printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) ); - printf( "\n" ); + PRT( "T", clock() - clk3 ); +// printf( "\n" ); } // perform sweeping diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index c306c394..25f7a3ef 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -2226,7 +2226,7 @@ p->timeSatFail += clock() - clk; int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew ) { int pLits[2], RetValue1, clk; -// int RetValue; + int RetValue; // make sure the nodes are not complemented assert( !Ivy_IsComplement(pNew) ); @@ -2261,8 +2261,8 @@ p->timeSat += clock() - clk; { p->timeSatUnsat += clock() - clk; pLits[0] = lit_neg( pLits[0] ); -// RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); -// assert( RetValue ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); + assert( RetValue ); // continue solving the other implication p->nSatCallsUnsat++; } @@ -2533,6 +2533,7 @@ void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * Ivy_ObjSetFaninVec( pNode, vFanins ); } Vec_PtrFree( vFrontier ); + sat_solver_simplify( p->pSat ); } /**Function************************************************************* diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c index 47f15e55..9304edc7 100644 --- a/src/aig/ssw/sswAig.c +++ b/src/aig/ssw/sswAig.c @@ -44,7 +44,8 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, { Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew; // skip nodes without representative - if ( (pObjRepr = Aig_ObjRepr(pAig, pObj)) == NULL ) + pObjRepr = Aig_ObjRepr(pAig, pObj); + if ( pObjRepr == NULL ) return; p->nConstrTotal++; assert( pObjRepr->Id < pObj->Id ); @@ -53,16 +54,26 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, // get the new node of the representative pObjReprNew = Ssw_ObjFraig( p, pObjRepr, iFrame ); // if this is the same node, no need to add constraints - if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) ) - return; + if ( pObj->fPhase == pObjRepr->fPhase ) + { + assert( pObjNew != Aig_Not(pObjReprNew) ); + if ( pObjNew == pObjReprNew ) + return; + } + else + { + assert( pObjNew != pObjReprNew ); + if ( pObjNew == Aig_Not(pObjReprNew) ) + return; + } p->nConstrReduced++; // these are different nodes - perform speculative reduction pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase ); // set the new node Ssw_ObjSetFraig( p, pObj, iFrame, pObjNew2 ); // add the constraint - Aig_ObjCreatePo( pFrames, Aig_Regular(pObjNew) ); - Aig_ObjCreatePo( pFrames, Aig_Regular(pObjReprNew) ); + Aig_ObjCreatePo( pFrames, pObjNew2 ); + Aig_ObjCreatePo( pFrames, pObjNew ); } /**Function************************************************************* @@ -80,7 +91,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) { Aig_Man_t * pFrames; Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; - int i, k, f; + int i, f; assert( p->pFrames == NULL ); assert( Aig_ManRegNum(p->pAig) > 0 ); assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); @@ -90,18 +101,14 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) // create latches for the first frame Saig_ManForEachLo( p->pAig, pObj, i ) Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(pFrames) ); - // create PI nodes for the frames - for ( f = 0; f < p->pPars->nFramesK; f++ ) - Aig_ManForEachPiSeq( p->pAig, pObj, i ) - Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) ); - // map constant nodes - for ( f = 0; f < p->pPars->nFramesK; f++ ) - Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) ); - // add timeframes p->nConstrTotal = p->nConstrReduced = 0; for ( f = 0; f < p->pPars->nFramesK; f++ ) { + // map constants and PIs + Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) ); + Aig_ManForEachPiSeq( p->pAig, pObj, i ) + Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) ); // set the constraints on the latch outputs Aig_ManForEachLoSeq( p->pAig, pObj, i ) Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f ); @@ -113,7 +120,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f ); } // transfer latch input to the latch outputs - Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, k ) + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) ); } // add the POs for the latch outputs of the last frame @@ -124,6 +131,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) Aig_ManCleanup( pFrames ); // make sure the satisfying assignment is node assigned assert( pFrames->pData == NULL ); +//Aig_ManShow( pFrames, 0, NULL ); return pFrames; } diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index bf4883e3..c84a5d3d 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -425,15 +425,15 @@ void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs ) { if ( fLatchCorr ) { - if ( !Aig_ObjIsPi(pObj) ) + if ( !Saig_ObjIsPi(p->pAig, pObj) ) continue; } else { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsPi(p->pAig, pObj) ) continue; // skip the node with more that the given number of levels - if ( nMaxLevs && (int)pObj->Level >= nMaxLevs ) + if ( nMaxLevs && (int)pObj->Level > nMaxLevs ) continue; } // check if the node belongs to the class of constant 1 @@ -556,7 +556,7 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax p = Ssw_ClassesStart( pAig ); // go through the nodes p->nCands1 = 0; - Aig_ManForEachObj( p->pAig, pObj, i ) + Aig_ManForEachObj( pAig, pObj, i ) { if ( fLatchCorr ) { @@ -568,10 +568,10 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsLo(pAig, pObj) ) continue; // skip the node with more that the given number of levels - if ( nMaxLevs && (int)pObj->Level >= nMaxLevs ) + if ( nMaxLevs && (int)pObj->Level > nMaxLevs ) continue; } - Ssw_ObjSetConst1Cand( p->pAig, pObj ); + Ssw_ObjSetConst1Cand( pAig, pObj ); p->nCands1++; } // allocate room for classes @@ -708,6 +708,53 @@ int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs return 1; } +/**Function************************************************************* + + Synopsis [Refine the group of constant 1 nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive ) +{ + Aig_Obj_t * pObj, * pReprNew, ** ppClassNew; + int i; + // collect the nodes to be refined + Vec_PtrClear( p->vClassNew ); + for ( i = 0; i < Vec_PtrSize(p->pAig->vObjs); i++ ) + if ( p->pAig->pReprs[i] == Aig_ManConst1(p->pAig) ) + { + pObj = Aig_ManObj( p->pAig, i ); + if ( !p->pFuncNodeIsConst( p->pManData, pObj ) ) + Vec_PtrPush( p->vClassNew, pObj ); + } + // check if there is a new class + if ( Vec_PtrSize(p->vClassNew) == 0 ) + return 0; + p->nCands1 -= Vec_PtrSize(p->vClassNew); + pReprNew = Vec_PtrEntry( p->vClassNew, 0 ); + Aig_ObjSetRepr( p->pAig, pReprNew, NULL ); + if ( Vec_PtrSize(p->vClassNew) == 1 ) + return 1; + // create a new class composed of these nodes + ppClassNew = p->pMemClassesFree; + p->pMemClassesFree += Vec_PtrSize(p->vClassNew); + Vec_PtrForEachEntry( p->vClassNew, pObj, i ) + { + ppClassNew[i] = pObj; + Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL ); + } + Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) ); + // refine them recursively + if ( fRecursive ) + return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 ); + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 1e314b78..6c19ab70 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -48,7 +48,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) p->nConstrs = 0; // treat the last nConstrs POs as seq constraints p->nBTLimit = 1000; // conflict limit at a node p->fPolarFlip = 0; // uses polarity adjustment - p->fLatchCorr = 0; // performs register correspondence + p->fLatchCorr = 1; // performs register correspondence p->fVerbose = 1; // verbose stats p->nIters = 0; // the number of iterations performed } @@ -66,6 +66,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) ***********************************************************************/ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) { + Aig_Man_t * pAigNew; Ssw_Man_t * p; int RetValue, nIter, clk, clkTotal = clock(); // reset random numbers @@ -75,27 +76,33 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) // compute candidate equivalence classes p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); // refine classes using BMC - Ssw_ClassesPrint( p->ppClasses, 0 ); + if ( pPars->fVerbose ) + Ssw_ClassesPrint( p->ppClasses, 0 ); Ssw_ManSweepBmc( p ); - Ssw_ClassesPrint( p->ppClasses, 0 ); + Ssw_ManCleanup( p ); + if ( pPars->fVerbose ) + Ssw_ClassesPrint( p->ppClasses, 0 ); // refine classes using induction for ( nIter = 0; ; nIter++ ) { clk = clock(); - RetValue = Ssw_ManSweep(p); + RetValue = Ssw_ManSweep( p ); if ( pPars->fVerbose ) { - printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. NR = %6d. ", + printf( "%3d : Const = %6d. Cl = %6d. L = %6d. LR = %6d. NR = %6d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), - p->nConstrTotal, p->nConstrReduced, p->nFrameNodes ); + p->nConstrTotal, p->nConstrReduced, Aig_ManNodeNum(p->pFrames) ); PRT( "T", clock() - clk ); } + Ssw_ManCleanup( p ); if ( !RetValue ) break; - } + } p->timeTotal = clock() - clkTotal; Ssw_ManStop( p ); - return Aig_ManDupRepr( pAig, 0 ); + pAigNew = Aig_ManDupRepr( pAig, 0 ); + Aig_ManSeqCleanup( pAigNew ); + return pAigNew; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 0e54af32..21621c0d 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -55,7 +55,6 @@ struct Ssw_Man_t_ Aig_Man_t * pAig; // user-given AIG Aig_Man_t * pFrames; // final AIG Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes - int nFrameNodes; // the number of nodes in the timeframes // equivalence classes Ssw_Cla_t * ppClasses; // equivalence classes of nodes // Aig_Obj_t ** pReprsProved; // equivalences proved @@ -70,6 +69,7 @@ struct Ssw_Man_t_ // constraints int nConstrTotal; // the number of total constraints int nConstrReduced; // the number of reduced constraints + int nStragers; // SAT calls statistics int nSatCalls; // the number of SAT calls int nSatProof; // the number of proofs @@ -136,6 +136,7 @@ extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, extern int Ssw_ClassesRefine( Ssw_Cla_t * p ); extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive ); extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive ); +extern int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive ); /*=== sswCnf.c ===================================================*/ extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ); /*=== sswMan.c ===================================================*/ @@ -148,6 +149,7 @@ extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); /*=== sswSimSat.c ===================================================*/ extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f ); +extern void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f ); /*=== sswSweep.c ===================================================*/ extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p ); diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index 86144ebb..0b935daa 100644 --- a/src/aig/ssw/sswMan.c +++ b/src/aig/ssw/sswMan.c @@ -42,22 +42,25 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) { Ssw_Man_t * p; + // prepare the sequential AIG + assert( Saig_ManRegNum(pAig) > 0 ); + Aig_ManFanoutStart( pAig ); + Aig_ManSetPioNumbers( pAig ); // create interpolation manager p = ALLOC( Ssw_Man_t, 1 ); memset( p, 0, sizeof(Ssw_Man_t) ); p->pPars = pPars; p->pAig = pAig; p->nFrames = pPars->nFramesK + 1; - Aig_ManFanoutStart( pAig ); + p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); // SAT solving p->nSatVars = 1; - p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) ); + p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * p->nFrames ); p->vFanins = Vec_PtrAlloc( 100 ); p->vSimRoots = Vec_PtrAlloc( 1000 ); p->vSimClasses = Vec_PtrAlloc( 1000 ); // equivalences proved // p->pReprsProved = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); - p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); return p; } @@ -97,21 +100,19 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) { printf( "Parameters: Frames = %d. Conf limit = %d. Constrs = %d.\n", p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs ); - printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d.\n", - Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig) ); - printf( "SAT solver: Vars = %d.\n", p->nSatVars ); - printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", + printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. SAT vars = %d.\n", + Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), p->nSatVars ); + printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d. Equivs = %d. Str = %d.\n", p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal, - p->nSatCallsSat, p->nSatFailsReal ); - printf( "Equivs : All = %6d.\n", Ssw_ManCountEquivs(p) ); + p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p), p->nStragers ); printf( "Runtime statistics:\n" ); p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeSimSat-p->timeSat; PRTP( "BMC ", p->timeBmc, p->timeTotal ); PRTP( "Spec reduce", p->timeReduce, p->timeTotal ); PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal ); PRTP( "SAT solving", p->timeSat, p->timeTotal ); - PRTP( " sat ", p->timeSatSat, p->timeTotal ); PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); + PRTP( " sat ", p->timeSatSat, p->timeTotal ); PRTP( " undecided", p->timeSatUndec, p->timeTotal ); PRTP( "Other ", p->timeOther, p->timeTotal ); PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); @@ -135,14 +136,15 @@ void Ssw_ManCleanup( Ssw_Man_t * p ) { Aig_ManStop( p->pFrames ); p->pFrames = NULL; + memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames ); } if ( p->pSat ) { sat_solver_delete( p->pSat ); p->pSat = NULL; - p->nSatVars = 0; +// p->nSatVars = 0; + memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * p->nFrames ); } - memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames ); p->nConstrTotal = 0; p->nConstrReduced = 0; } @@ -192,11 +194,12 @@ void Ssw_ManStartSolver( Ssw_Man_t * p ) sat_solver_setnvars( p->pSat, 10000 ); // var 0 is not used // var 1 is reserved for const1 node - add the clause - Lit = toLit( 1 ); + p->nSatVars = 1; + Lit = toLit( p->nSatVars ); if ( p->pPars->fPolarFlip ) Lit = lit_neg( Lit ); sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); - p->nSatVars = 2; + Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c index 06abd2c9..90752baa 100644 --- a/src/aig/ssw/sswSat.c +++ b/src/aig/ssw/sswSat.c @@ -32,7 +32,7 @@ Synopsis [Runs equivalence test for the two nodes.] - Description [] + Description [Both nodes should be regular and different from each other.] SideEffects [] @@ -42,13 +42,13 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { int nBTLimit = p->pPars->nBTLimit; - int pLits[2], RetValue, RetValue1, status, clk; + int pLits[2], RetValue, RetValue1, clk;//, status; p->nSatCalls++; // sanity checks - assert( !Aig_IsComplement(pNew) ); assert( !Aig_IsComplement(pOld) ); - assert( pNew != pOld ); + assert( !Aig_IsComplement(pNew) ); + assert( pOld != pNew ); if ( p->pSat == NULL ) Ssw_ManStartSolver( p ); @@ -57,14 +57,6 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) Ssw_CnfNodeAddToSolver( p, pOld ); Ssw_CnfNodeAddToSolver( p, pNew ); - // propagate unit clauses - if ( p->pSat->qtail != p->pSat->qhead ) - { - status = sat_solver_simplify(p->pSat); - assert( status != 0 ); - assert( p->pSat->qtail == p->pSat->qhead ); - } - // solve under assumptions // A = 1; B = 0 OR A = 1; B = 1 pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 ); @@ -75,6 +67,10 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); } //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); + + RetValue = sat_solver_simplify(p->pSat); + assert( RetValue != 0 ); + clk = clock(); RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); @@ -117,6 +113,10 @@ p->timeSatUndec += clock() - clk; if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); } + + RetValue = sat_solver_simplify(p->pSat); + assert( RetValue != 0 ); + clk = clock(); RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); @@ -160,23 +160,45 @@ p->timeSatUndec += clock() - clk; ***********************************************************************/ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { - int pLits[2], RetValue; + int pLits[2], RetValue, fComplNew; + Aig_Obj_t * pTemp; // sanity checks - assert( !Aig_IsComplement(pNew) ); - assert( !Aig_IsComplement(pOld) ); - assert( pNew != pOld ); + assert( Aig_Regular(pOld) != Aig_Regular(pNew) ); + // move constant to the old node + if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) ) + { + assert( Aig_Regular(pOld) != Aig_ManConst1(p->pFrames) ); + pTemp = pOld; + pOld = pNew; + pNew = pTemp; + } + + // move complement to the new node + if ( Aig_IsComplement(pOld) ) + { + pOld = Aig_Regular(pOld); + pNew = Aig_Not(pNew); + } + + // start the solver if ( p->pSat == NULL ) Ssw_ManStartSolver( p ); // if the nodes do not have SAT variables, allocate them Ssw_CnfNodeAddToSolver( p, pOld ); - Ssw_CnfNodeAddToSolver( p, pNew ); + Ssw_CnfNodeAddToSolver( p, Aig_Regular(pNew) ); + + // transform the new node + fComplNew = Aig_IsComplement( pNew ); + pNew = Aig_Regular( pNew ); + // consider the constant 1 case if ( pOld == Aig_ManConst1(p->pFrames) ) { - pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), !pNew->fPhase ); + // add constaint A = 1 ----> A + pLits[0] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew ); if ( p->pPars->fPolarFlip ) { if ( pNew->fPhase ) pLits[0] = lit_neg( pLits[0] ); @@ -186,10 +208,11 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) } else { - // solve under assumptions - // A = 1; B = 0 OR A = 1; B = 1 + // add constaint A = B ----> (A v !B)(!A v B) + + // (A v !B) pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 ); - pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase ); + pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), !fComplNew ); if ( p->pPars->fPolarFlip ) { if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); @@ -200,10 +223,9 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); assert( RetValue ); - // solve under assumptions - // A = 0; B = 1 OR A = 0; B = 0 + // (!A v B) pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 ); - pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase ); + pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew); if ( p->pPars->fPolarFlip ) { if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); @@ -214,16 +236,6 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); assert( RetValue ); } -/* - // propagate unit clauses - if ( p->pSat->qtail != p->pSat->qhead ) - { - int status; - status = sat_solver_simplify(p->pSat); - assert( status != 0 ); - assert( p->pSat->qtail == p->pSat->qhead ); - } -*/ return 1; } diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c index 5986c27a..868a016b 100644 --- a/src/aig/ssw/sswSimSat.c +++ b/src/aig/ssw/sswSimSat.c @@ -92,6 +92,32 @@ void Ssw_ManCollectTfoCands( Ssw_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 /**Function************************************************************* + Synopsis [Retrives value of the PI in the original AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) +{ + Aig_Obj_t * pObjFraig; + int nVarNum, Value; + assert( Aig_ObjIsPi(pObj) ); + pObjFraig = Ssw_ObjFraig( p, pObj, f ); + nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) ); + Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum )); + if ( p->pPars->fPolarFlip ) + { + if ( Aig_Regular(pObjFraig)->fPhase ) Value ^= 1; + } + return Value; +} + +/**Function************************************************************* + Synopsis [Resimulates the cone of influence of the solved nodes.] Description [] @@ -108,11 +134,7 @@ void Ssw_ManResimulateSolved_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) Aig_ObjSetTravIdCurrent(p->pAig, pObj); if ( Aig_ObjIsPi(pObj) ) { - Aig_Obj_t * pObjFraig = Ssw_ObjFraig( p, pObj, f ); - int nVarNum = Ssw_ObjSatNum( p, pObjFraig ); - // get the value from the SAT solver - // (account for the fact that some vars may be minimized away) - pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum ); + pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f ); return; } Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj), f ); @@ -194,6 +216,40 @@ void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, i p->timeSimSat += clock() - clk; } +/**Function************************************************************* + + Synopsis [Handle the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ) +{ + Aig_Obj_t * pObj; + int i, RetValue1, RetValue2, clk = clock(); + // set the PI simulation information + Aig_ManConst1(p->pAig)->fMarkB = 1; + Aig_ManForEachPi( p->pAig, pObj, i ) + pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f ); + // simulate internal nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) + & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); + // check equivalence classes + RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 ); + RetValue2 = Ssw_ClassesRefine( p->ppClasses ); + // make sure refinement happened + if ( Aig_ObjIsConst1(pRepr) ) + assert( RetValue1 ); + else + assert( RetValue2 ); +p->timeSimSat += clock() - clk; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c index 18796b20..0630de56 100644 --- a/src/aig/ssw/sswSweep.c +++ b/src/aig/ssw/sswSweep.c @@ -50,12 +50,33 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) return; // get the fraiged node pObjFraig = Ssw_ObjFraig( p, pObj, f ); - if ( pObjFraig == NULL ) - return; + assert( pObjFraig != NULL ); // get the fraiged representative pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f ); - if ( pObjReprFraig == NULL ) + assert( pObjReprFraig != NULL ); + // check if constant 0 pattern distinquishes these nodes + if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) ) + { + Aig_Obj_t * pObj; + int i; + if ( p->pSat->model.cap < p->pSat->size ) + { + veci_resize(&p->pSat->model, 0); + for ( i = 0; i < p->pSat->size; i++ ) + veci_push( &p->pSat->model, (int)l_False ); + } + // set the values of SAT vars to be equal to the phase of the nodes + Aig_ManForEachObj( p->pFrames, pObj, i ) + if ( Ssw_ObjSatNum( p, pObj ) ) + { + int iVar = Ssw_ObjSatNum( p, pObj ); + assert( iVar < p->pSat->size ); + p->pSat->model.ptr[iVar] = (int)(p->pPars->fPolarFlip? 0 : (pObj->fPhase? l_True : l_False)); + p->pSat->model.size = p->pSat->size; + } + p->nStragers++; return; + } // if the fraiged nodes are the same, return if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) { @@ -63,10 +84,15 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) // p->pReprsProved[ pObj->Id ] = pObjRepr; return; } - assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) ); - RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); +// assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) ); + if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) ) + RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); + else + RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) ); + if ( RetValue == -1 ) // timed out { + assert( 0 ); Ssw_ClassesRemoveNode( p->ppClasses, pObj ); p->fRefined = 1; return; @@ -80,7 +106,8 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) return; } // disproved the equivalence - Ssw_ManResimulateCex( p, pObj, pObjRepr, f ); +// Ssw_ManResimulateCex( p, pObj, pObjRepr, f ); + Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f ); assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); p->fRefined = 1; } @@ -110,7 +137,8 @@ clk = clock(); // sweep internal nodes p->fRefined = 0; - pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); + if ( p->pPars->fVerbose ) + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); for ( f = 0; f < p->pPars->nFramesK; f++ ) { // map constants and PIs @@ -120,17 +148,18 @@ clk = clock(); // sweep internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) { - Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL ); + if ( p->pPars->fVerbose ) + Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL ); pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFraig( p, pObj, f, pObjNew ); Ssw_ManSweepNode( p, pObj, f ); } } - Bar_ProgressStop( pProgress ); + if ( p->pPars->fVerbose ) + Bar_ProgressStop( pProgress ); // cleanup - Ssw_ClassesCheck( p->ppClasses ); - Ssw_ManCleanup( p ); +// Ssw_ClassesCheck( p->ppClasses ); p->timeBmc += clock() - clk; return p->fRefined; } @@ -150,21 +179,21 @@ int Ssw_ManSweep( Ssw_Man_t * p ) { Bar_Progress_t * pProgress = NULL; Aig_Obj_t * pObj, * pObj2, * pObjNew; - int nConstrPairs, clk, i, f = p->pPars->nFramesK; + int nConstrPairs, clk, i, f; // perform speculative reduction clk = clock(); // create timeframes p->pFrames = Ssw_FramesWithClasses( p ); - p->nFrameNodes = Aig_ManNodeNum( p->pFrames ); // add constraints + Ssw_ManStartSolver( p ); nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig); assert( (nConstrPairs & 1) == 0 ); for ( i = 0; i < nConstrPairs; i += 2 ) { pObj = Aig_ManPo( p->pFrames, i ); pObj2 = Aig_ManPo( p->pFrames, i+1 ); - Ssw_NodesAreConstrained( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) ); + Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) ); } // build logic cones for register inputs for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) @@ -175,25 +204,36 @@ clk = clock(); sat_solver_simplify( p->pSat ); p->timeReduce += clock() - clk; - // map constants and PIs + // map constants and PIs of the last frame + f = p->pPars->nFramesK; Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); + // make sure LOs are assigned + Saig_ManForEachLo( p->pAig, pObj, i ) + assert( Ssw_ObjFraig( p, pObj, f ) != NULL ); // sweep internal nodes p->fRefined = 0; - pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) ); - Aig_ManForEachNode( p->pAig, pObj, i ) + if ( p->pPars->fVerbose ) + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) ); + Aig_ManForEachObj( p->pAig, pObj, i ) { - Bar_ProgressUpdate( pProgress, i, NULL ); - pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); - Ssw_ObjSetFraig( p, pObj, f, pObjNew ); - Ssw_ManSweepNode( p, pObj, f ); + if ( p->pPars->fVerbose ) + Bar_ProgressUpdate( pProgress, i, NULL ); + if ( Saig_ObjIsLo(p->pAig, pObj) ) + Ssw_ManSweepNode( p, pObj, f ); + else if ( Aig_ObjIsNode(pObj) ) + { + pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); + Ssw_ObjSetFraig( p, pObj, f, pObjNew ); + Ssw_ManSweepNode( p, pObj, f ); + } } - Bar_ProgressStop( pProgress ); + if ( p->pPars->fVerbose ) + Bar_ProgressStop( pProgress ); // cleanup - Ssw_ClassesCheck( p->ppClasses ); - Ssw_ManCleanup( p ); +// Ssw_ClassesCheck( p->ppClasses ); return p->fRefined; } |