summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaEquiv.c2
-rw-r--r--src/aig/saig/saigTempor.c2
-rw-r--r--src/base/abci/abc.c28
-rw-r--r--src/base/abci/abcDar.c8
-rw-r--r--src/base/main/mainMC.c4
-rw-r--r--src/proof/abs/absIter.c2
-rw-r--r--src/proof/abs/absOldRef.c2
-rw-r--r--src/proof/ssw/sswRarity.c2
-rw-r--r--src/sat/bmc/bmc.h4
-rw-r--r--src/sat/bmc/bmcBmc.c68
-rw-r--r--src/sat/bmc/bmcBmc2.c125
11 files changed, 178 insertions, 69 deletions
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 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-14 16:32:02 +0000