luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver.

This commit is contained in:
Alan Mishchenko 2016-05-19 22:33:40 -07:00
parent 2d0a8fb4cb
commit 2ded89cca5
6 changed files with 13 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/base/abci/abc.c
View File

@ -23269,7 +23269,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdruvzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdurvzh" ) ) != EOF )
{
switch ( c )
{
@ -23435,6 +23435,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'u':
fOrDecomp ^= 1;
break;
case 'r':
pPars->fNoRestarts ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -23501,7 +23504,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axduvzh]\n" );
Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axdurvzh]\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", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
@ -23521,6 +23524,7 @@ usage:
Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dropping (replacing by 0) SAT outputs [default = %s]\n", pPars->fDropSatOuts? "yes": "no" );
Abc_Print( -2, "\t-u : toggle performing structural OR-decomposition [default = %s]\n", fOrDecomp? "yes": "not" );
Abc_Print( -2, "\t-r : toggle disabling periodic restarts [default = %s]\n", pPars->fNoRestarts? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");

6
src/base/wlc/wlcReadSmt.c
View File

@ -738,7 +738,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode )
if ( Smt_EntryIsName(iRoot0) )
{
char * pName, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0));
int fSigned = 0, iObj;
int iObj;
if ( pStr0[0] == 'l' && pStr0[1] == 'e' && pStr0[2] == 't' && pStr0[3] == '\0' )
{
// let ((s35550 (bvor s48 s35549)))
@ -809,8 +809,8 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode )
int iRoot3 = Vec_IntEntry( vRoots, 3 );
char * pStr2 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot2));
char * pStr3 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot3));
int Num1 = atoi( pStr1 );
int Num2 = atoi( pStr2 );
int Num1 = atoi( pStr2 );
int Num2 = atoi( pStr3 );
assert( Num1 >= Num2 );
fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT);
Range = (Num1 - Num2 + 1) + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) );

1
src/sat/bmc/bmc.h
View File

@ -60,6 +60,7 @@ struct Saig_ParBmc_t_
int fDropSatOuts; // replace sat outputs by constant 0
int nFfToAddMax; // max number of flops to add during CBA
int fSkipRand; // skip random decisions
int fNoRestarts; // disables periodic restarts
int nLearnedStart; // starting learned clause limit
int nLearnedDelta; // delta of learned clause limit
int nLearnedPerce; // ratio of learned clause limit

1
src/sat/bmc/bmcBmc3.c
View File

@ -1415,6 +1415,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
p->pSat->nLearntMax = p->pSat->nLearntStart;
p->pSat->fNoRestarts = p->pPars->fNoRestarts;
if ( pPars->fSolveAll && p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
if ( pPars->fVerbose )

2
src/sat/bsat/satSolver.c
View File

@ -1660,7 +1660,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
int next;
// Reached bound on number of conflicts:
if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){
if ( (!s->fNoRestarts && nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){
s->progress_estimate = sat_solver_progress(s);
sat_solver_canceluntil(s,s->root_level);
veci_delete(&learnt_clause);

1
src/sat/bsat/satSolver.h
View File

@ -179,6 +179,7 @@ struct sat_solver_t
int fSkipSimplify; // set to one to skip simplification of the clause database
int fNotUseRandom; // do not allow random decisions with a fixed probability
int fNoRestarts; // disables periodic restarts
int * pGlobalVars; // for experiments with global vars during interpolation
// clause store