diff options
-rw-r--r-- | src/base/abci/abc.c | 8 | ||||
-rw-r--r-- | src/proof/cec/cec.h | 1 | ||||
-rw-r--r-- | src/proof/cec/cecCore.c | 5 | ||||
-rw-r--r-- | src/proof/cec/cecInt.h | 2 | ||||
-rw-r--r-- | src/proof/cec/cecPat.c | 28 | ||||
-rw-r--r-- | src/proof/cec/cecSolve.c | 69 |
6 files changed, 100 insertions, 13 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dff328eb..6ca352cd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28931,7 +28931,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Cec_ManFraSetDefaultParams( pPars ); pPars->fSatSweeping = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdcwvh" ) ) != EOF ) { switch ( c ) { @@ -29010,6 +29010,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': pPars->fDualOut ^= 1; break; + case 'c': + pPars->fRunCSat ^= 1; + break; case 'w': pPars->fVeryVerbose ^= 1; break; @@ -29030,7 +29033,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdwvh]\n" ); + Abc_Print( -2, "usage: &fraig [-WRILDC <num>] [-rmdcwvh]\n" ); Abc_Print( -2, "\t performs combinational SAT sweeping\n" ); Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds ); @@ -29041,6 +29044,7 @@ usage: Abc_Print( -2, "\t-r : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" ); Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); Abc_Print( -2, "\t-d : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle using circuit-based solver [default = %s]\n", pPars->fRunCSat? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index 65d2e24e..2e69f7a4 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -107,6 +107,7 @@ struct Cec_ParFra_t_ int fDualOut; // miter with separate outputs int fColorDiff; // miter with separate outputs int fSatSweeping; // enable SAT sweeping + int fRunCSat; // enable another solver int fVeryVerbose; // verbose stats int fVerbose; // verbose stats int iOutFail; // the failed output diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index c77b8fa1..71335e85 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -426,7 +426,10 @@ p->timeSim += Abc_Clock() - clk; break; } clk = Abc_Clock(); - Cec_ManSatSolve( pPat, pSrm, pParsSat ); + if ( pPars->fRunCSat ) + Cec_ManSatSolveCSat( pPat, pSrm, pParsSat ); + else + Cec_ManSatSolve( pPat, pSrm, pParsSat ); p->timeSat += Abc_Clock() - clk; if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) ) { diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h index dd6dc618..ef1dd983 100644 --- a/src/proof/cec/cecInt.h +++ b/src/proof/cec/cecInt.h @@ -190,6 +190,7 @@ extern Cec_ManFra_t * Cec_ManFraStart( Gia_Man_t * pAig, Cec_ParFra_t * p extern void Cec_ManFraStop( Cec_ManFra_t * p ); /*=== cecPat.c ============================================================*/ extern void Cec_ManPatSavePattern( Cec_ManPat_t * pPat, Cec_ManSat_t * p, Gia_Obj_t * pObj ); +extern void Cec_ManPatSavePatternCSat( Cec_ManPat_t * pMan, Vec_Int_t * vPat ); extern Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nWords ); extern Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit ); /*=== cecSeq.c ============================================================*/ @@ -201,6 +202,7 @@ extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig ); /*=== cecSolve.c ============================================================*/ extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj ); extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ); +extern void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ); extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats ); extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus ); extern int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj ); diff --git a/src/proof/cec/cecPat.c b/src/proof/cec/cecPat.c index c175eaa7..91a0c941 100644 --- a/src/proof/cec/cecPat.c +++ b/src/proof/cec/cecPat.c @@ -360,20 +360,21 @@ void Cec_ManPatSavePattern( Cec_ManPat_t * pMan, Cec_ManSat_t * p, Gia_Obj_t * { Vec_Int_t * vPat; int nPatLits; - abctime clk, clkTotal = Abc_Clock(); + abctime clkTotal = Abc_Clock(); +// abctime clk; assert( Gia_ObjIsCo(pObj) ); pMan->nPats++; pMan->nPatsAll++; // compute values in the cone of influence -clk = Abc_Clock(); +//clk = Abc_Clock(); Gia_ManIncrementTravId( p->pAig ); nPatLits = Cec_ManPatComputePattern_rec( p, p->pAig, Gia_ObjFanin0(pObj) ); assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 1 ); pMan->nPatLits += nPatLits; pMan->nPatLitsAll += nPatLits; -pMan->timeFind += Abc_Clock() - clk; +//pMan->timeFind += Abc_Clock() - clk; // compute sensitizing path -clk = Abc_Clock(); +//clk = Abc_Clock(); Vec_IntClear( pMan->vPattern1 ); Gia_ManIncrementTravId( p->pAig ); Cec_ManPatComputePattern1_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern1 ); @@ -385,19 +386,26 @@ clk = Abc_Clock(); vPat = Vec_IntSize(pMan->vPattern1) < Vec_IntSize(pMan->vPattern2) ? pMan->vPattern1 : pMan->vPattern2; pMan->nPatLitsMin += Vec_IntSize(vPat); pMan->nPatLitsMinAll += Vec_IntSize(vPat); -pMan->timeShrink += Abc_Clock() - clk; +//pMan->timeShrink += Abc_Clock() - clk; // verify pattern using ternary simulation -clk = Abc_Clock(); - Cec_ManPatVerifyPattern( p->pAig, pObj, vPat ); -pMan->timeVerify += Abc_Clock() - clk; +//clk = Abc_Clock(); +// Cec_ManPatVerifyPattern( p->pAig, pObj, vPat ); +//pMan->timeVerify += Abc_Clock() - clk; // sort pattern -clk = Abc_Clock(); +//clk = Abc_Clock(); Vec_IntSort( vPat, 0 ); -pMan->timeSort += Abc_Clock() - clk; +//pMan->timeSort += Abc_Clock() - clk; // save pattern Cec_ManPatStore( pMan, vPat ); pMan->timeTotal += Abc_Clock() - clkTotal; } +void Cec_ManPatSavePatternCSat( Cec_ManPat_t * pMan, Vec_Int_t * vPat ) +{ + // sort pattern + Vec_IntSort( vPat, 0 ); + // save pattern + Cec_ManPatStore( pMan, vPat ); +} /**Function************************************************************* diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c index c799d17d..e3db0b93 100644 --- a/src/proof/cec/cecSolve.c +++ b/src/proof/cec/cecSolve.c @@ -735,6 +735,75 @@ clk2 = Abc_Clock(); Cec_ManSatStop( p ); } +/**Function************************************************************* + + Synopsis [Performs one round of solving for the POs of the AIG.] + + Description [Labels the nodes that have been proved (pObj->fMark1) + and returns the set of satisfying assignments.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSatSolveExractPattern( Vec_Int_t * vCexStore, int iStart, Vec_Int_t * vPat ) +{ + int k, nSize; + Vec_IntClear( vPat ); + // skip the output number + iStart++; + // get the number of items + nSize = Vec_IntEntry( vCexStore, iStart++ ); + if ( nSize <= 0 ) + return iStart; + // extract pattern + for ( k = 0; k < nSize; k++ ) + Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) ); + return iStart; +} +void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ) +{ + Vec_Str_t * vStatus; + Vec_Int_t * vPat = Vec_IntAlloc( 1000 ); + Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 ); + Gia_Obj_t * pObj; + int i, status, iStart = 0; + assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) ); + // reset the manager + if ( pPat ) + { + pPat->iStart = Vec_StrSize(pPat->vStorage); + pPat->nPats = 0; + pPat->nPatLits = 0; + pPat->nPatLitsMin = 0; + } + Gia_ManForEachCo( pAig, pObj, i ) + { + status = (int)Vec_StrEntry(vStatus, i); + pObj->fMark0 = (status == 0); + pObj->fMark1 = (status == 1); + if ( Vec_IntSize(vCexStore) > 0 && status != 1 ) + iStart = Cec_ManSatSolveExractPattern( vCexStore, iStart, vPat ); + if ( status != 0 ) + continue; + // save the pattern + if ( pPat && Vec_IntSize(vPat) > 0 ) + { + abctime clk3 = Abc_Clock(); + Cec_ManPatSavePatternCSat( pPat, vPat ); + pPat->timeTotalSave += Abc_Clock() - clk3; + } + // quit if one of them is solved + if ( pPars->fCheckMiter ) + break; + } + assert( iStart == Vec_IntSize(vCexStore) ); + Vec_IntFree( vPat ); + Vec_StrFree( vStatus ); + Vec_IntFree( vCexStore ); +} + /**Function************************************************************* |