diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-27 22:38:01 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-27 22:38:01 -0700 |
commit | 17a0d944b305cbadeb2bbbcdd7ef3c82b50c3c7a (patch) | |
tree | 4b2335e0e9e2cc797e18b86d9cde2d8efa6483b6 /src | |
parent | 613e8b2ad6b24369467179b15c2ab2638f9b8672 (diff) | |
download | abc-17a0d944b305cbadeb2bbbcdd7ef3c82b50c3c7a.tar.gz abc-17a0d944b305cbadeb2bbbcdd7ef3c82b50c3c7a.tar.bz2 abc-17a0d944b305cbadeb2bbbcdd7ef3c82b50c3c7a.zip |
SAT sweeping under constraints.
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abc.c | 5 | ||||
-rw-r--r-- | src/proof/ssc/sscClass.c | 4 | ||||
-rw-r--r-- | src/proof/ssc/sscCore.c | 85 | ||||
-rw-r--r-- | src/proof/ssc/sscInt.h | 2 | ||||
-rw-r--r-- | src/proof/ssc/sscSat.c | 40 | ||||
-rw-r--r-- | src/proof/ssc/sscSim.c | 1 |
6 files changed, 98 insertions, 39 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2f785a22..b15b5b04 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27186,14 +27186,15 @@ int Abc_CommandAbc9CFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9CFraig(): There is no AIG.\n" ); return 1; } - Abc_Print( 0, "Current AIG contains %d constraints.\n", pAbc->pGia->nConstrs ); pTemp = Ssc_PerformSweepingConstr( pAbc->pGia, pPars ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: Abc_Print( -2, "usage: &cfraig [-WC <num>] [-rmdwvh]\n" ); - Abc_Print( -2, "\t performs conditional combinational SAT sweeping\n" ); + Abc_Print( -2, "\t performs combinational SAT sweeping under constraints\n" ); + Abc_Print( -2, "\t which are present in the AIG or set manually using \"constr\"\n" ); + Abc_Print( -2, "\t (constraints are listed as last POs and true when they are 0)\n" ); Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); diff --git a/src/proof/ssc/sscClass.c b/src/proof/ssc/sscClass.c index 308fbada..a9904148 100644 --- a/src/proof/ssc/sscClass.c +++ b/src/proof/ssc/sscClass.c @@ -257,8 +257,8 @@ void Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs ) Vec_IntForEachEntryDouble( vDisPairs, iRepr, iObj, i ) if ( iRepr == Gia_ObjRepr(p, iObj) ) printf( "Pair (%d, %d) are still equivalent.\n", iRepr, iObj ), Result = 0; - if ( Result ) - printf( "Classes are refined correctly.\n" ); +// if ( Result ) +// printf( "Classes are refined correctly.\n" ); } diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c index 1aada663..00491e31 100644 --- a/src/proof/ssc/sscCore.c +++ b/src/proof/ssc/sscCore.c @@ -52,7 +52,6 @@ void Ssc_ManSetDefaultParams( Ssc_Pars_t * p ) p->fVerbose = 0; // verbose stats } - /**Function************************************************************* Synopsis [] @@ -104,7 +103,7 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar return NULL; } sat_solver_bookmark( p->pSat ); - Vec_IntPrint( p->vPivot ); +// Vec_IntPrint( p->vPivot ); Gia_ManSetPhasePattern( p->pAig, p->vPivot ); Gia_ManSetPhasePattern( p->pCare, p->vPivot ); if ( Gia_ManCheckCoPhase(p->pCare) ) @@ -121,6 +120,26 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar Ssc_GiaClassesInit( pAig ); return p; } +void Ssc_ManPrintStats( Ssc_Man_t * p ) +{ + Abc_Print( 1, "Parameters: SimWords = %d. SatConfs = %d. SatVarMax = %d. CallsRec = %d. Verbose = %d.\n", + p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax, p->pPars->nCallsRecycle, p->pPars->fVerbose ); + Abc_Print( 1, "SAT calls : Total = %d. Proof = %d. Cex = %d. Undec = %d.\n", + p->nSatCalls, p->nSatCallsUnsat, p->nSatCallsSat, p->nSatCallsUndec ); + Abc_Print( 1, "SAT solver: Vars = %d. Clauses = %d. Recycles = %d. Sim rounds = %d.\n", + sat_solver_nvars(p->pSat), sat_solver_nclauses(p->pSat), p->nRecycles, p->nSimRounds ); + + p->timeOther = p->timeTotal - p->timeSimInit - p->timeSimSat - p->timeCnfGen - p->timeSatSat - p->timeSatUnsat - p->timeSatUndec; + ABC_PRTP( "Initialization ", p->timeSimInit, p->timeTotal ); + ABC_PRTP( "SAT simulation ", p->timeSimSat, p->timeTotal ); + ABC_PRTP( "CNF generation ", p->timeSimSat, p->timeTotal ); + ABC_PRTP( "SAT solving ", p->timeSat-p->timeCnfGen, p->timeTotal ); + ABC_PRTP( " unsat ", p->timeSatUnsat, p->timeTotal ); + ABC_PRTP( " sat ", p->timeSatSat, p->timeTotal ); + ABC_PRTP( " undecided ", p->timeSatUndec, p->timeTotal ); + ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); + ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); +} /**Function************************************************************* @@ -140,6 +159,7 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t Gia_Obj_t * pObj, * pRepr; clock_t clk, clkTotal = clock(); int i, fCompl, status; +clk = clock(); assert( Gia_ManRegNum(pCare) == 0 ); assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) ); assert( Gia_ManIsNormalized(pAig) ); @@ -151,14 +171,14 @@ Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t if ( p == NULL ) return Gia_ManDup( pAig ); // perform simulation -clk = clock(); if ( Gia_ManAndNum(pCare) == 0 ) // no constraints { for ( i = 0; i < 16; i++ ) { Ssc_GiaRandomPiPattern( pAig, 10, NULL ); Ssc_GiaSimRound( pAig ); - Ssc_GiaClassesRefine( pAig ); + if ( pPars->fVerbose ) + Ssc_GiaClassesRefine( pAig ); Gia_ManEquivPrintClasses( pAig, 0, 0 ); } } @@ -176,63 +196,86 @@ p->timeSimInit += clock() - clk; { if ( pAig->iPatsPi == 64 * pPars->nWords ) { +clk = clock(); Ssc_GiaSimRound( pAig ); Ssc_GiaClassesRefine( pAig ); - Gia_ManEquivPrintClasses( pAig, 0, 0 ); + if ( pPars->fVerbose ) + Gia_ManEquivPrintClasses( pAig, 0, 0 ); Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs ); + Vec_IntClear( p->vDisPairs ); + // prepare next patterns Ssc_GiaResetPiPattern( pAig, pPars->nWords ); Ssc_GiaSavePiPattern( pAig, p->vPivot ); - Vec_IntClear( p->vDisPairs ); +p->timeSimSat += clock() - clk; } if ( Gia_ObjIsAnd(pObj) ) pObj->Value = Gia_ManHashAnd( p->pFraig, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); if ( !Gia_ObjHasRepr(pAig, i) ) continue; pRepr = Gia_ObjReprObj(pAig, i); - if ( pRepr->Value == pObj->Value ) + if ( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase ) ) continue; assert( Abc_Lit2Var(pRepr->Value) != Abc_Lit2Var(pObj->Value) ); fCompl = pRepr->fPhase ^ pObj->fPhase ^ Abc_LitIsCompl(pRepr->Value) ^ Abc_LitIsCompl(pObj->Value); // perform SAT call - clk = clock(); +clk = clock(); p->nSatCalls++; status = Ssc_ManCheckEquivalence( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl ); if ( status == l_False ) { p->nSatCallsUnsat++; - p->timeSatUnsat += clock() - clk; pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase ); } else if ( status == l_True ) { p->nSatCallsSat++; - p->timeSatSat += clock() - clk; Ssc_GiaSavePiPattern( pAig, p->vPattern ); Vec_IntPush( p->vDisPairs, Gia_ObjRepr(p->pAig, i) ); Vec_IntPush( p->vDisPairs, i ); +// printf( "Try %2d and %2d: ", Gia_ObjRepr(p->pAig, i), i ); +// Vec_IntPrint( p->vPattern ); } else if ( status == l_Undef ) - { p->nSatCallsUndec++; - p->timeSatUndec += clock() - clk; - } else assert( 0 ); +p->timeSat += clock() - clk; + } + if ( pAig->iPatsPi > 1 ) + { +clk = clock(); + while ( pAig->iPatsPi < 64 * pPars->nWords ) + Ssc_GiaSavePiPattern( pAig, p->vPivot ); + Ssc_GiaSimRound( pAig ); + Ssc_GiaClassesRefine( pAig ); + if ( pPars->fVerbose ) + Gia_ManEquivPrintClasses( pAig, 0, 0 ); + Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs ); + Vec_IntClear( p->vDisPairs ); +p->timeSimSat += clock() - clk; } +// Gia_ManEquivPrintClasses( pAig, 1, 0 ); - // remember the resulting AIG + // generate the resulting AIG pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 ); if ( pResult == NULL ) { printf( "There is no equivalences.\n" ); + ABC_FREE( pAig->pReprs ); + ABC_FREE( pAig->pNexts ); pResult = Gia_ManDup( pAig ); } + p->timeTotal = clock() - clkTotal; + if ( pPars->fVerbose ) + Ssc_ManPrintStats( p ); Ssc_ManStop( p ); // count the number of representatives if ( pPars->fVerbose ) { - Gia_ManEquivPrintClasses( pAig, 0, 0 ); - Abc_Print( 1, "Reduction in AIG nodes:%8d ->%8d. ", Gia_ManAndNum(pAig), Gia_ManAndNum(pResult) ); +// Gia_ManEquivPrintClasses( pAig, 0, 0 ); + Abc_Print( 1, "Reduction in AIG nodes:%8d ->%8d (%6.2f %%). ", + Gia_ManAndNum(pAig), Gia_ManAndNum(pResult), + 100.0 - 100.0 * Gia_ManAndNum(pResult) / Gia_ManAndNum(pAig) ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); } return pResult; @@ -241,6 +284,8 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars ) { Gia_Man_t * pAig, * pCare, * pResult; int i; + if ( pPars->fVerbose ) + Abc_Print( 0, "SAT sweeping AIG with %d constraints.\n", p->nConstrs ); if ( p->nConstrs == 0 ) { pAig = Gia_ManDup( p ); @@ -257,6 +302,14 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars ) pCare = Gia_ManDupCones( p, Vec_IntArray(vOuts) + Gia_ManPoNum(p) - p->nConstrs, p->nConstrs, 0 ); Vec_IntFree( vOuts ); } + if ( pPars->fVerbose ) + { + printf( "User AIG: " ); + Gia_ManPrintStats( pAig, 0, 0, 0 ); + printf( "Care AIG: " ); + Gia_ManPrintStats( pCare, 0, 0, 0 ); + } + pAig = Gia_ManDupLevelized( pResult = pAig ); Gia_ManStop( pResult ); pResult = Ssc_PerformSweeping( pAig, pCare, pPars ); diff --git a/src/proof/ssc/sscInt.h b/src/proof/ssc/sscInt.h index 7e710c19..f0a556a6 100644 --- a/src/proof/ssc/sscInt.h +++ b/src/proof/ssc/sscInt.h @@ -64,6 +64,7 @@ struct Ssc_Man_t_ Vec_Int_t * vPattern; // counter-example Vec_Int_t * vDisPairs; // disproved pairs // SAT calls statistics + int nSimRounds; // the number of simulation rounds int nRecycles; // the number of times SAT solver was recycled int nCallsSince; // the number of calls since the last recycle int nSatCalls; // the number of SAT calls @@ -74,6 +75,7 @@ struct Ssc_Man_t_ clock_t timeSimInit; // simulation and class computation clock_t timeSimSat; // simulation of the counter-examples clock_t timeCnfGen; // generation of CNF + clock_t timeSat; // total SAT time clock_t timeSatSat; // sat clock_t timeSatUnsat; // unsat clock_t timeSatUndec; // undecided diff --git a/src/proof/ssc/sscSat.c b/src/proof/ssc/sscSat.c index ea9c599f..f6d5e9af 100644 --- a/src/proof/ssc/sscSat.c +++ b/src/proof/ssc/sscSat.c @@ -210,8 +210,9 @@ static void Ssc_ManCnfNodeAddToSolver( Ssc_Man_t * p, int NodeId ) Gia_Obj_t * pNode; int i, k, Id, Lit; clock_t clk; + assert( NodeId > 0 ); // quit if CNF is ready - if ( NodeId == 0 || Ssc_ObjSatVar(p, NodeId) ) + if ( Ssc_ObjSatVar(p, NodeId) ) return; clk = clock(); // start the frontier @@ -345,33 +346,24 @@ Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p ) int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl ) { int pLitsSat[2], RetValue; + clock_t clk; + assert( iRepr < iNode ); // if ( p->nTimeOut ) // sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + clock() ); // create CNF + if ( iRepr ) Ssc_ManCnfNodeAddToSolver( p, iRepr ); Ssc_ManCnfNodeAddToSolver( p, iNode ); sat_solver_compress( p->pSat ); // order the literals pLitsSat[0] = Abc_Var2Lit( Ssc_ObjSatVar(p, iRepr), 0 ); - pLitsSat[1] = Abc_Var2Lit( Ssc_ObjSatVar(p, iNode), 0 ); - if ( pLitsSat[0] < pLitsSat[1] ) - ABC_SWAP( int, pLitsSat[0], pLitsSat[1] ); - - // correct polarity - pLitsSat[1] = Abc_LitNotCond( pLitsSat[1], !fCompl ); // extra complement! - if ( !Abc_LitIsCompl(pLitsSat[1]) ) - { - pLitsSat[0] = Abc_LitNot( pLitsSat[0] ); - pLitsSat[1] = Abc_LitNot( pLitsSat[1] ); - } - assert( pLitsSat[0] > pLitsSat[1] ); - assert( Abc_LitIsCompl(pLitsSat[1]) ); - assert( pLitsSat[1] != 0 ); + pLitsSat[1] = Abc_Var2Lit( Ssc_ObjSatVar(p, iNode), fCompl ^ (int)(iRepr > 0) ); // solve under assumptions - // A = 1; B = 0 OR A = 1; B = 1 + // A = 1; B = 0 + clk = clock(); RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue == l_False ) { @@ -379,22 +371,27 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl ) pLitsSat[1] = Abc_LitNot( pLitsSat[1] ); // compl RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 ); assert( RetValue ); + p->timeSatUnsat += clock() - clk; } else if ( RetValue == l_True ) { Ssc_ManCollectSatPattern( p, p->vPattern ); + p->timeSatSat += clock() - clk; return l_True; } else // if ( RetValue1 == l_Undef ) + { + p->timeSatUndec += clock() - clk; return l_Undef; + } // if the old node was constant 0, we already know the answer - if ( pLitsSat[1] == 0 ) + if ( iRepr == 0 ) return l_False; - assert( pLitsSat[1] > 1 ); // solve under assumptions - // A = 0; B = 1 OR A = 0; B = 0 + // A = 0; B = 1 + clk = clock(); RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue == l_False ) { @@ -402,14 +399,19 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl ) pLitsSat[1] = Abc_LitNot( pLitsSat[1] ); RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 ); assert( RetValue ); + p->timeSatUnsat += clock() - clk; } else if ( RetValue == l_True ) { Ssc_ManCollectSatPattern( p, p->vPattern ); + p->timeSatSat += clock() - clk; return l_True; } else // if ( RetValue1 == l_Undef ) + { + p->timeSatUndec += clock() - clk; return l_Undef; + } return l_False; } diff --git a/src/proof/ssc/sscSim.c b/src/proof/ssc/sscSim.c index 89585ba6..9a2c1033 100644 --- a/src/proof/ssc/sscSim.c +++ b/src/proof/ssc/sscSim.c @@ -212,6 +212,7 @@ void Ssc_GiaSimRound( Gia_Man_t * p ) assert( pSim == Gia_ObjSimObj( p, pObj ) ); pSim0 = pSim - pObj->iDiff0 * nWords; Ssc_SimDup( pSim, pSim0, nWords, Gia_ObjFaninC0(pObj) ); +// Extra_PrintBinary( stdout, pSim, 64 ), printf( "\n" ); pSim += nWords; } } |