From 23d36a8d5665d7a586777c9723c4aa803b253fc1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 16 Aug 2017 14:20:52 +0700 Subject: Integrating Satoko into 'bmc' and 'bmc2'. --- src/aig/gia/giaEquiv.c | 2 +- src/aig/saig/saigTempor.c | 2 +- src/base/abci/abc.c | 28 ++++++++--- src/base/abci/abcDar.c | 8 +-- src/base/main/mainMC.c | 4 +- src/proof/abs/absIter.c | 2 +- src/proof/abs/absOldRef.c | 2 +- src/proof/ssw/sswRarity.c | 2 +- src/sat/bmc/bmc.h | 4 +- src/sat/bmc/bmcBmc.c | 68 +++++++++++++++++++------ src/sat/bmc/bmcBmc2.c | 125 +++++++++++++++++++++++++++++++++------------- 11 files changed, 178 insertions(+), 69 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index f41db898..84d9f1b1 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -1970,7 +1970,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f pTemp = Gia_ManToAig( pSrm, 0 ); // Aig_ManPrintStats( pTemp ); Gia_ManStop( pSrm ); - Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVerbose, 0, NULL, 0 ); + Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVerbose, 0, NULL, 0, 0 ); pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL; Aig_ManStop( pTemp ); if ( pCex == NULL ) diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c index d800537d..3ba22bec 100644 --- a/src/aig/saig/saigTempor.c +++ b/src/aig/saig/saigTempor.c @@ -223,7 +223,7 @@ Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nCon // run BMC2 if ( fUseBmc ) { - RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished, 0 ); + RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished, 0, 0 ); if ( RetValue == 0 ) { Vec_IntFreeP( &vTransSigs ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 01132def..a6a77571 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -24368,9 +24368,10 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) int nCofFanLit; int fVerbose; int iFrames; + int fUseSatoko; char * pLogFileName = NULL; - extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int * piFrames ); + extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int * piFrames, int fUseSatoko ); // set defaults nFrames = 20; nSizeMax = 100000; @@ -24381,8 +24382,9 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) fNewAlgo = 1; nCofFanLit = 0; fVerbose = 0; + fUseSatoko = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDLrvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDLrsvh" ) ) != EOF ) { switch ( c ) { @@ -24469,6 +24471,9 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': fNewAlgo ^= 1; break; + case 's': + fUseSatoko ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -24493,7 +24498,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Does not work for combinational networks.\n" ); return 0; } - pAbc->Status = Abc_NtkDarBmc( pNtk, 0, nFrames, nSizeMax, nNodeDelta, 0, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, 0, nCofFanLit, fVerbose, &iFrames ); + pAbc->Status = Abc_NtkDarBmc( pNtk, 0, nFrames, nSizeMax, nNodeDelta, 0, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, 0, nCofFanLit, fVerbose, &iFrames, fUseSatoko ); pAbc->nFrames = iFrames; Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); if ( pLogFileName ) @@ -24501,7 +24506,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: bmc [-FNC num] [-L file] [-rcvh]\n" ); + Abc_Print( -2, "usage: bmc [-FNC num] [-L file] [-rcsvh]\n" ); Abc_Print( -2, "\t performs bounded model checking with static unrolling\n" ); Abc_Print( -2, "\t-F num : the number of time frames [default = %d]\n", nFrames ); Abc_Print( -2, "\t-N num : the max number of nodes in the frames [default = %d]\n", nSizeMax ); @@ -24510,6 +24515,7 @@ usage: Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); Abc_Print( -2, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); // Abc_Print( -2, "\t-a : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" ); + Abc_Print( -2, "\t-s : toggle using Satoko instead of build-in MiniSAT [default = %s]\n", fUseSatoko? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -24542,9 +24548,10 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) int fOrDecomp; int fVerbose; int iFrames; + int fUseSatoko; char * pLogFileName = NULL; - extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int * piFrames ); + extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int * piFrames, int fUseSatoko ); // set defaults nStart = 0; @@ -24558,8 +24565,9 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) fNewAlgo = 0; fOrDecomp = 0; fVerbose = 0; + fUseSatoko = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFNTCGDLruvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFNTCGDLrusvh" ) ) != EOF ) { switch ( c ) { @@ -24658,6 +24666,9 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'u': fOrDecomp ^= 1; break; + case 's': + fUseSatoko ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -24682,7 +24693,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Does not work for combinational networks.\n" ); return 0; } - pAbc->Status = Abc_NtkDarBmc( pNtk, nStart, nFrames, nSizeMax, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fOrDecomp, 0, fVerbose, &iFrames ); + pAbc->Status = Abc_NtkDarBmc( pNtk, nStart, nFrames, nSizeMax, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fOrDecomp, 0, fVerbose, &iFrames, fUseSatoko ); pAbc->nFrames = iFrames; Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); if ( pLogFileName ) @@ -24690,7 +24701,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: bmc2 [-SFTCGD num] [-L file] [-uvh]\n" ); + Abc_Print( -2, "usage: bmc2 [-SFTCGD num] [-L file] [-usvh]\n" ); Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" ); Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", nStart ); Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", nFrames ); @@ -24700,6 +24711,7 @@ usage: Abc_Print( -2, "\t-D num : the delta in the number of nodes [default = %d]\n", nNodeDelta ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); Abc_Print( -2, "\t-u : toggle performing structural OR-decomposition [default = %s]\n", fOrDecomp? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle using Satoko instead of build-in MiniSAT [default = %s]\n", fUseSatoko? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 147f7c2f..996ae6a2 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2258,7 +2258,7 @@ static void sigfunc( int signo ) SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int * piFrames ) +int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int * piFrames, int fUseSatoko ) { Aig_Man_t * pMan; Vec_Int_t * vMap = NULL; @@ -2284,7 +2284,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int if ( fNewAlgo ) // command 'bmc' { int iFrame; - RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit ); + RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit, fUseSatoko ); if ( piFrames ) *piFrames = iFrame; ABC_FREE( pNtk->pModel ); @@ -2309,7 +2309,7 @@ ABC_PRT( "Time", Abc_Clock() - clk ); } else { - RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames, 0 ); + RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames, 0, fUseSatoko ); ABC_FREE( pNtk->pModel ); ABC_FREE( pNtk->pSeqModel ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; @@ -2829,7 +2829,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, i if ( pSecPar->fTryBmc ) { - RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame, 0 ); + RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame, 0, 0 ); if ( RetValue == 0 ) { Abc_Print( 1, "Networks are not equivalent.\n" ); diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c index 43d3ea85..482d8d35 100644 --- a/src/base/main/mainMC.c +++ b/src/base/main/mainMC.c @@ -94,7 +94,7 @@ int main( int argc, char * argv[] ) { // perform BMC if ( pAig->nRegs != 0 ) - RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL, 0 ); + RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL, 0, 0 ); // perform full-blown SEC if ( RetValue != 0 ) @@ -123,7 +123,7 @@ int main( int argc, char * argv[] ) int nSizeMax = 500000; int nBTLimit = 10000000; int fRewrite = 0; - RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth, 0 ); + RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth, 0, 0 ); if ( RetValue != 0 ) RetValue = -1; } diff --git a/src/proof/abs/absIter.c b/src/proof/abs/absIter.c index 7b660359..ff14132d 100644 --- a/src/proof/abs/absIter.c +++ b/src/proof/abs/absIter.c @@ -58,7 +58,7 @@ int Gia_IterTryImprove( Gia_Man_t * p, int nTimeOut, int iFrame0 ) int nBTLimitAll = 0; int fVerbose = 0; int RetValue, iFrame; - RetValue = Saig_BmcPerform( pAig, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, &iFrame, 1 ); + RetValue = Saig_BmcPerform( pAig, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, &iFrame, 1, 0 ); assert( RetValue == 0 || RetValue == -1 ); Aig_ManStop( pAig ); Gia_ManStop( pAbs ); diff --git a/src/proof/abs/absOldRef.c b/src/proof/abs/absOldRef.c index 315ecf89..1674f144 100644 --- a/src/proof/abs/absOldRef.c +++ b/src/proof/abs/absOldRef.c @@ -203,7 +203,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo } else { - Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames, 0 ); + Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames, 0, 0 ); } if ( pAbs->pSeqModel == NULL ) return NULL; diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index a02ea01b..1b7cab23 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -1011,7 +1011,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) if ( fTryBmc ) { Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits ); - Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0 ); + Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0, 0 ); // if ( pNewAig->pSeqModel != NULL ) // Abc_Print( 1, "BMC has found a counter-example in frame %d.\n", iFrameFail ); Aig_ManStop( pNewAig ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index bdb89684..689647e7 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -160,9 +160,9 @@ struct Bmc_ParFf_t_ /*=== bmcBCore.c ==========================================================*/ extern void Bmc_ManBCorePerform( Gia_Man_t * pGia, Bmc_BCorePar_t * pPars ); /*=== bmcBmc.c ==========================================================*/ -extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); +extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit, int fUseSatoko ); /*=== bmcBmc2.c ==========================================================*/ -extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ); +extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent, int fUseSatoko ); /*=== bmcBmc3.c ==========================================================*/ extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ); extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ); diff --git a/src/sat/bmc/bmcBmc.c b/src/sat/bmc/bmcBmc.c index bcad9013..8f7452e5 100644 --- a/src/sat/bmc/bmcBmc.c +++ b/src/sat/bmc/bmcBmc.c @@ -21,6 +21,8 @@ #include "proof/fra/fra.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" +#include "sat/satoko/satoko.h" +#include "sat/satoko/solver.h" #include "bmc.h" ABC_NAMESPACE_IMPL_START @@ -171,6 +173,26 @@ ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START +/**Function************************************************************* + + Synopsis [Returns a counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Sat2_SolverGetModel( satoko_t * p, int * pVars, int nVars ) +{ + int * pModel; + int i; + pModel = ABC_CALLOC( int, nVars+1 ); + for ( i = 0; i < nVars; i++ ) + pModel[i] = solver_read_cex_varvalue(p, pVars[i]); + return pModel; +} /**Function************************************************************* @@ -183,10 +205,11 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ) +int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit, int fUseSatoko ) { extern Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit ); - sat_solver * pSat; + sat_solver * pSat = NULL; + satoko_t * pSat2 = NULL; Cnf_Dat_t * pCnf; Aig_Man_t * pFrames, * pAigTemp; Aig_Obj_t * pObj; @@ -241,12 +264,25 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) ); //if ( s_fInterrupt ) //return -1; - pSat = sat_solver_new(); - sat_solver_setnvars( pSat, pCnf->nVars ); - for ( i = 0; i < pCnf->nClauses; i++ ) + if ( fUseSatoko ) { - if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) - assert( 0 ); + satoko_opts_t opts; + satoko_default_opts(&opts); + opts.conf_limit = nConfLimit; + pSat2 = satoko_create(); + satoko_configure(pSat2, &opts); + satoko_setnvars(pSat2, pCnf->nVars); + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !satoko_add_clause( pSat2, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) + assert( 0 ); + } + else + { + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, pCnf->nVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + assert( 0 ); } if ( fVerbose ) { @@ -254,7 +290,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim ABC_PRT( "Time", Abc_Clock() - clk ); fflush( stdout ); } - status = sat_solver_simplify(pSat); + status = pSat ? sat_solver_simplify(pSat) : 1; if ( status == 0 ) { if ( fVerbose ) @@ -268,8 +304,6 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim abctime clkPart = Abc_Clock(); Aig_ManForEachCo( pFrames, pObj, i ) { -//if ( s_fInterrupt ) -//return -1; Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); if ( fVerbose ) { @@ -277,12 +311,17 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); } clk = Abc_Clock(); - status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( pSat2 ) + status = satoko_solve_assumptions_limit( pSat2, &Lit, 1, nConfLimit ); + else + status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) ) { printf( "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); - printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations ); + printf( "Conf =%8.0f. Imp =%11.0f. ", + (double)(pSat ? pSat->stats.conflicts : solver_conflictnum(pSat2)), + (double)(pSat ? pSat->stats.propagations : satoko_stats(pSat2).n_propagations) ); ABC_PRT( "T", Abc_Clock() - clkPart ); clkPart = Abc_Clock(); fflush( stdout ); @@ -303,7 +342,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim else if ( status == l_True ) { Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames ); - int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); + int * pModel = pSat2 ? Sat2_SolverGetModel(pSat2, vCiIds->pArray, vCiIds->nSize) : Sat_SolverGetModel(pSat, vCiIds->pArray, vCiIds->nSize); pModel[Aig_ManCiNum(pFrames)] = pObj->Id; pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel ); ABC_FREE( pModel ); @@ -323,7 +362,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim } } } - sat_solver_delete( pSat ); + if ( pSat ) sat_solver_delete( pSat ); + if ( pSat2 ) satoko_destroy( pSat2 ); Cnf_DataFree( pCnf ); Aig_ManStop( pFrames ); return RetValue; diff --git a/src/sat/bmc/bmcBmc2.c b/src/sat/bmc/bmcBmc2.c index 47bfc008..5c2df0d7 100644 --- a/src/sat/bmc/bmcBmc2.c +++ b/src/sat/bmc/bmcBmc2.c @@ -20,6 +20,8 @@ #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" +#include "sat/satoko/satoko.h" +#include "sat/satoko/solver.h" #include "proof/ssw/ssw.h" #include "bmc.h" @@ -49,6 +51,7 @@ struct Saig_Bmc_t_ Vec_Ptr_t * vAig2Frm; // mapping of AIG nodees into Frames nodes // SAT solver sat_solver * pSat; // SAT solver + satoko_t * pSat2; // SAT solver int nSatVars; // the number of used SAT variables Vec_Int_t * vObj2Var; // mapping of frames objects in CNF variables int nStitchVars; @@ -277,7 +280,7 @@ void Abs_ManFreeAray( Vec_Ptr_t * p ) SeeAlso [] ***********************************************************************/ -Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose ) +Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fUseSatoko ) { Saig_Bmc_t * p; Aig_Obj_t * pObj; @@ -303,14 +306,27 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); // create SAT solver p->nSatVars = 1; - p->pSat = sat_solver_new(); - p->pSat->nLearntStart = 10000;//p->pPars->nLearnedStart; - p->pSat->nLearntDelta = 5000;//p->pPars->nLearnedDelta; - p->pSat->nLearntRatio = 75;//p->pPars->nLearnedPerce; - p->pSat->nLearntMax = p->pSat->nLearntStart; - sat_solver_setnvars( p->pSat, 2000 ); Lit = toLit( p->nSatVars ); - sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + if ( fUseSatoko ) + { + satoko_opts_t opts; + satoko_default_opts(&opts); + opts.conf_limit = nConfMaxOne; + p->pSat2 = satoko_create(); + satoko_configure(p->pSat2, &opts); + satoko_setnvars(p->pSat2, 2000); + satoko_add_clause( p->pSat2, &Lit, 1 ); + } + else + { + p->pSat = sat_solver_new(); + p->pSat->nLearntStart = 10000;//p->pPars->nLearnedStart; + p->pSat->nLearntDelta = 5000;//p->pPars->nLearnedDelta; + p->pSat->nLearntRatio = 75;//p->pPars->nLearnedPerce; + p->pSat->nLearntMax = p->pSat->nLearntStart; + sat_solver_setnvars( p->pSat, 2000 ); + sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + } Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ ); // other data structures p->vTargets = Vec_PtrAlloc( 1000 ); @@ -336,7 +352,8 @@ void Saig_BmcManStop( Saig_Bmc_t * p ) Aig_ManStop( p->pFrm ); Vec_VecFree( (Vec_Vec_t *)p->vAig2Frm ); Vec_IntFree( p->vObj2Var ); - sat_solver_delete( p->pSat ); + if ( p->pSat ) sat_solver_delete( p->pSat ); + if ( p->pSat2 ) satoko_destroy( p->pSat2 ); Vec_PtrFree( p->vTargets ); Vec_IntFree( p->vVisited ); ABC_FREE( p ); @@ -575,17 +592,42 @@ void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf ) // add clauses connecting existing variables Lits[0] = toLitCond( VarNumOld, 0 ); Lits[1] = toLitCond( VarNumNew, 1 ); - if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) ) - assert( 0 ); + if ( p->pSat2 ) + { + if ( !satoko_add_clause( p->pSat2, Lits, 2 ) ) + assert( 0 ); + } + else + { + if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) ) + assert( 0 ); + } Lits[0] = toLitCond( VarNumOld, 1 ); Lits[1] = toLitCond( VarNumNew, 0 ); - if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) ) - assert( 0 ); + if ( p->pSat2 ) + { + if ( !satoko_add_clause( p->pSat2, Lits, 2 ) ) + assert( 0 ); + } + else + { + if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) ) + assert( 0 ); + } } // add CNF to the SAT solver - for ( i = 0; i < pCnf->nClauses; i++ ) - if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) - break; + if ( p->pSat2 ) + { + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !satoko_add_clause( p->pSat2, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) + break; + } + else + { + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + break; + } if ( i < pCnf->nClauses ) printf( "SAT solver became UNSAT after adding clauses.\n" ); } @@ -648,7 +690,7 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p ) iVarNum = Saig_BmcSatNum( p, pObjFrm ); if ( iVarNum == 0 ) continue; - if ( sat_solver_var_value( p->pSat, iVarNum ) ) + if ( p->pSat2 ? solver_read_cex_varvalue(p->pSat2, iVarNum) : sat_solver_var_value(p->pSat, iVarNum) ) Abc_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i ); } } @@ -678,7 +720,7 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved ) Aig_Obj_t * pObj; int i, k, VarNum, Lit, status, RetValue; assert( Vec_PtrSize(p->vTargets) > 0 ); - if ( p->pSat->qtail != p->pSat->qhead ) + if ( p->pSat && p->pSat->qtail != p->pSat->qhead ) { RetValue = sat_solver_simplify(p->pSat); assert( RetValue != 0 ); @@ -687,27 +729,36 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved ) { if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart ) continue; - if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll ) + if ( p->nConfMaxAll && (p->pSat ? p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) > p->nConfMaxAll ) return l_Undef; VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) ); Lit = toLitCond( VarNum, Aig_IsComplement(pObj) ); - RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->nConfMaxOne, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( p->pSat2 ) + RetValue = satoko_solve_assumptions_limit( p->pSat2, &Lit, 1, p->nConfMaxOne ); + else + RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->nConfMaxOne, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue == l_False ) // unsat { // add final unit clause Lit = lit_neg( Lit ); - status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + if ( p->pSat2 ) + status = satoko_add_clause( p->pSat2, &Lit, 1 ); + else + status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); assert( status ); - // add learned units - for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ ) + if ( p->pSat ) { - Lit = veci_begin(&p->pSat->unit_lits)[k]; - status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); - assert( status ); + // add learned units + for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ ) + { + Lit = veci_begin(&p->pSat->unit_lits)[k]; + status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + assert( status ); + } + veci_resize(&p->pSat->unit_lits, 0); + // propagate units + sat_solver_compress( p->pSat ); } - veci_resize(&p->pSat->unit_lits, 0); - // propagate units - sat_solver_compress( p->pSat ); continue; } if ( RetValue == l_Undef ) // undecided @@ -758,7 +809,7 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p ) SeeAlso [] ***********************************************************************/ -int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ) +int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent, int fUseSatoko ) { Saig_Bmc_t * p; Aig_Man_t * pNew; @@ -782,10 +833,15 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll ); } nFramesMax = nFramesMax ? nFramesMax : ABC_INFINITY; - p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose ); + p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose, fUseSatoko ); // set runtime limit if ( nTimeOut ) - sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); + { + if ( p->pSat2 ) + solver_set_runtime_limit( p->pSat2, nTimeToStop ); + else + sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); + } for ( Iter = 0; ; Iter++ ) { clk2 = Abc_Clock(); @@ -810,7 +866,8 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax if ( fVerbose ) { printf( "%4d : F =%5d. O =%4d. And =%8d. Var =%8d. Conf =%7d. ", - Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts ); + Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, + p->pSat ? (int)p->pSat->stats.conflicts : solver_conflictnum(p->pSat2) ); printf( "%4.0f MB", 4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) ); printf( "%9.2f sec", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); printf( "\n" ); @@ -865,7 +922,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax { if ( p->iFrameLast >= p->nFramesMax ) printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); - else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll ) + else if ( p->nConfMaxAll && (p->pSat ? (int)p->pSat->stats.conflicts : solver_conflictnum(p->pSat2)) > p->nConfMaxAll ) printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); else if ( nTimeOut && Abc_Clock() > nTimeToStop ) printf( "Reached timeout (%d seconds).\n", nTimeOut ); -- cgit v1.2.3