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

Trying to enable CNF simplification in &bmcs -g.

This commit is contained in:
Alan Mishchenko 2017-09-07 19:16:13 -07:00
parent 68b59b8a1e
commit ba0d855fd4
6 changed files with 74 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -40017,6 +40017,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fUseSynth = 0; // use synthesis pPars->fUseSynth = 0; // use synthesis
pPars->fUseOldCnf = 0; // use old CNF construction pPars->fUseOldCnf = 0; // use old CNF construction
pPars->fUseGlucose = 0; // use Glucose 3.0 pPars->fUseGlucose = 0; // use Glucose 3.0
pPars->fUseEliminate = 0; // use variable elimination
pPars->fVerbose = 0; // verbose pPars->fVerbose = 0; // verbose
pPars->fVeryVerbose = 0; // very verbose pPars->fVeryVerbose = 0; // very verbose
pPars->fNotVerbose = 0; // skip line-by-line print-out pPars->fNotVerbose = 0; // skip line-by-line print-out
@ -40026,7 +40027,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->pFuncOnFrameDone = pAbc->pFuncOnFrameDone; // frame done callback pPars->pFuncOnFrameDone = pAbc->pFuncOnFrameDone; // frame done callback
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PCFATgvwh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "PCFATgevwh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -40088,6 +40089,9 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'g': case 'g':
pPars->fUseGlucose ^= 1; pPars->fUseGlucose ^= 1;
break; break;
case 'e':
pPars->fUseEliminate ^= 1;
break;
case 'v': case 'v':
pPars->fVerbose ^= 1; pPars->fVerbose ^= 1;
break; break;
@ -40116,7 +40120,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-gvwh]\n" ); Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-gevwh]\n" );
Abc_Print( -2, "\t performs bounded model checking\n" ); Abc_Print( -2, "\t performs bounded model checking\n" );
Abc_Print( -2, "\t-P num : the number of parallel solvers [default = %d]\n", pPars->nProcs ); Abc_Print( -2, "\t-P num : the number of parallel solvers [default = %d]\n", pPars->nProcs );
Abc_Print( -2, "\t-C num : the SAT solver conflict limit [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-C num : the SAT solver conflict limit [default = %d]\n", pPars->nConfLimit );
@ -40124,6 +40128,7 @@ usage:
Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n", pPars->nFramesAdd ); Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n", pPars->nFramesAdd );
Abc_Print( -2, "\t-T num : approximate timeout in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-T num : approximate timeout in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-g : toggle using Glucose 3.0 [default = %s]\n", pPars->fUseGlucose? "Glucose" : "Satoko" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 [default = %s]\n", pPars->fUseGlucose? "Glucose" : "Satoko" );
Abc_Print( -2, "\t-e : toggle using variable eliminatation [default = %s]\n", pPars->fUseEliminate?"yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");

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

@ -95,6 +95,7 @@ struct Bmc_AndPar_t_
int fUseSynth; // use synthesis int fUseSynth; // use synthesis
int fUseOldCnf; // use old CNF construction int fUseOldCnf; // use old CNF construction
int fUseGlucose; // use Glucose 3.0 as the default solver int fUseGlucose; // use Glucose 3.0 as the default solver
int fUseEliminate; // use variable elimination
int fVerbose; // verbose int fVerbose; // verbose
int fVeryVerbose; // very verbose int fVeryVerbose; // very verbose
int fNotVerbose; // skip line-by-line print-out int fNotVerbose; // skip line-by-line print-out

11
src/sat/bmc/bmcBmcG.c
View File

@ -42,7 +42,6 @@ struct Bmcg_Man_t_
Vec_Int_t vCiMap; // maps CIs of pFrames into CIs/frames of GIA Vec_Int_t vCiMap; // maps CIs of pFrames into CIs/frames of GIA
bmcg_sat_solver * pSats[PAR_THR_MAX]; // concurrent SAT solvers bmcg_sat_solver * pSats[PAR_THR_MAX]; // concurrent SAT solvers
int nSatVars; // number of SAT variables used int nSatVars; // number of SAT variables used
int nSatVarsOld; // number of SAT variables used
int fStopNow; // signal when it is time to stop int fStopNow; // signal when it is time to stop
abctime timeUnf; // runtime of unfolding abctime timeUnf; // runtime of unfolding
abctime timeCnf; // runtime of CNF generation abctime timeCnf; // runtime of CNF generation
@ -90,7 +89,7 @@ Bmcg_Man_t * Bmcg_ManStart( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
// p->pSats[i]->SolverType = i; // p->pSats[i]->SolverType = i;
bmcg_sat_solver_addvar( p->pSats[i] ); bmcg_sat_solver_addvar( p->pSats[i] );
bmcg_sat_solver_addclause( p->pSats[i], &Lit, 1 ); bmcg_sat_solver_addclause( p->pSats[i], &Lit, 1 );
bmcg_sat_solver_setstop( p->pSats[i], &p->fStopNow ); bmcg_sat_solver_set_stop( p->pSats[i], &p->fStopNow );
} }
p->nSatVars = 1; p->nSatVars = 1;
return p; return p;
@ -166,7 +165,7 @@ int Bmcg_ManCollect_rec( Bmcg_Man_t * p, int iObj )
return iLitClean; return iLitClean;
pObj = Gia_ManObj( p->pFrames, iObj ); pObj = Gia_ManObj( p->pFrames, iObj );
iSatVar = Vec_IntEntry( &p->vFr2Sat, iObj ); iSatVar = Vec_IntEntry( &p->vFr2Sat, iObj );
if ( iSatVar > 0 || Gia_ObjIsCi(pObj) ) if ( (iSatVar > 0 && !bmcg_sat_solver_var_is_elim(p->pSats[0], iSatVar)) || Gia_ObjIsCi(pObj) )
iLitClean = Gia_ManAppendCi( p->pClean ); iLitClean = Gia_ManAppendCi( p->pClean );
else if ( Gia_ObjIsAnd(pObj) ) else if ( Gia_ObjIsAnd(pObj) )
{ {
@ -319,11 +318,12 @@ Abc_Cex_t * Bmcg_ManGenerateCex( Bmcg_Man_t * p, int i, int f, int s )
void Bmcg_ManAddCnf( Bmcg_Man_t * p, bmcg_sat_solver * pSat, Cnf_Dat_t * pCnf ) void Bmcg_ManAddCnf( Bmcg_Man_t * p, bmcg_sat_solver * pSat, Cnf_Dat_t * pCnf )
{ {
int i; int i;
for ( i = p->nSatVarsOld; i < p->nSatVars; i++ ) bmcg_sat_solver_set_nvars( pSat, p->nSatVars );
bmcg_sat_solver_addvar( pSat );
for ( i = 0; i < pCnf->nClauses; i++ ) for ( i = 0; i < pCnf->nClauses; i++ )
if ( !bmcg_sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) if ( !bmcg_sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
assert( 0 ); assert( 0 );
if ( p->pPars->fUseEliminate )
bmcg_sat_solver_eliminate( pSat, 0 );
} }
int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{ {
@ -345,7 +345,6 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
} }
nClauses += pCnf->nClauses; nClauses += pCnf->nClauses;
Bmcg_ManAddCnf( p, p->pSats[0], pCnf ); Bmcg_ManAddCnf( p, p->pSats[0], pCnf );
p->nSatVarsOld = p->nSatVars;
Cnf_DataFree( pCnf ); Cnf_DataFree( pCnf );
assert( Gia_ManPoNum(p->pFrames) == (f + pPars->nFramesAdd) * Gia_ManPoNum(pGia) ); assert( Gia_ManPoNum(p->pFrames) == (f + pPars->nFramesAdd) * Gia_ManPoNum(pGia) );
for ( k = 0; k < pPars->nFramesAdd; k++ ) for ( k = 0; k < pPars->nFramesAdd; k++ )

75
src/sat/glucose/AbcGlucose.cpp
View File

@ -54,19 +54,19 @@ extern "C" {
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Gluco::Solver * glucose_solver_start() Gluco::SimpSolver * glucose_solver_start()
{ {
Solver * S = new Solver; SimpSolver * S = new SimpSolver;
S->setIncrementalMode(); S->setIncrementalMode();
return S; return S;
} }
void glucose_solver_stop(Gluco::Solver* S) void glucose_solver_stop(Gluco::SimpSolver* S)
{ {
delete S; delete S;
} }
int glucose_solver_addclause(Gluco::Solver* S, int * plits, int nlits) int glucose_solver_addclause(Gluco::SimpSolver* S, int * plits, int nlits)
{ {
vec<Lit> lits; vec<Lit> lits;
for ( int i = 0; i < nlits; i++,plits++) for ( int i = 0; i < nlits; i++,plits++)
@ -81,14 +81,14 @@ int glucose_solver_addclause(Gluco::Solver* S, int * plits, int nlits)
return S->addClause(lits); // returns 0 if the problem is UNSAT return S->addClause(lits); // returns 0 if the problem is UNSAT
} }
void glucose_solver_setcallback(Gluco::Solver* S, void * pman, int(*pfunc)(void*, int, int*)) void glucose_solver_setcallback(Gluco::SimpSolver* S, void * pman, int(*pfunc)(void*, int, int*))
{ {
S->pCnfMan = pman; S->pCnfMan = pman;
S->pCnfFunc = pfunc; S->pCnfFunc = pfunc;
S->nCallConfl = 1000; S->nCallConfl = 1000;
} }
int glucose_solver_solve(Gluco::Solver* S, int * plits, int nlits) int glucose_solver_solve(Gluco::SimpSolver* S, int * plits, int nlits)
{ {
vec<Lit> lits; vec<Lit> lits;
for (int i=0;i<nlits;i++,plits++) for (int i=0;i<nlits;i++,plits++)
@ -97,22 +97,22 @@ int glucose_solver_solve(Gluco::Solver* S, int * plits, int nlits)
p.x = *plits; p.x = *plits;
lits.push(p); lits.push(p);
} }
Gluco::lbool res = S->solveLimited(lits); Gluco::lbool res = S->solveLimited(lits, 0);
return (res == l_True ? 1 : res == l_False ? -1 : 0); return (res == l_True ? 1 : res == l_False ? -1 : 0);
} }
int glucose_solver_addvar(Gluco::Solver* S) int glucose_solver_addvar(Gluco::SimpSolver* S)
{ {
S->newVar(); S->newVar();
return S->nVars() - 1; return S->nVars() - 1;
} }
int glucose_solver_read_cex_varvalue(Gluco::Solver* S, int ivar) int glucose_solver_read_cex_varvalue(Gluco::SimpSolver* S, int ivar)
{ {
return S->model[ivar] == l_True; return S->model[ivar] == l_True;
} }
void glucose_solver_setstop(Gluco::Solver* S, int * pstop) void glucose_solver_setstop(Gluco::SimpSolver* S, int * pstop)
{ {
S->pstop = pstop; S->pstop = pstop;
} }
@ -155,69 +155,92 @@ bmcg_sat_solver * bmcg_sat_solver_start()
} }
void bmcg_sat_solver_stop(bmcg_sat_solver* s) void bmcg_sat_solver_stop(bmcg_sat_solver* s)
{ {
glucose_solver_stop((Gluco::Solver*)s); glucose_solver_stop((Gluco::SimpSolver*)s);
} }
int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits) int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits)
{ {
return glucose_solver_addclause((Gluco::Solver*)s,plits,nlits); return glucose_solver_addclause((Gluco::SimpSolver*)s,plits,nlits);
} }
void bmcg_sat_solver_setcallback(bmcg_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*)) void bmcg_sat_solver_setcallback(bmcg_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*))
{ {
glucose_solver_setcallback((Gluco::Solver*)s,pman,pfunc); glucose_solver_setcallback((Gluco::SimpSolver*)s,pman,pfunc);
} }
int bmcg_sat_solver_solve(bmcg_sat_solver* s, int * plits, int nlits) int bmcg_sat_solver_solve(bmcg_sat_solver* s, int * plits, int nlits)
{ {
return glucose_solver_solve((Gluco::Solver*)s,plits,nlits); return glucose_solver_solve((Gluco::SimpSolver*)s,plits,nlits);
}
int bmcg_sat_solver_final(bmcg_sat_solver* s, int ** ppArray)
{
*ppArray = (int *)(Lit *)((Gluco::SimpSolver*)s)->conflict;
return ((Gluco::SimpSolver*)s)->conflict.size();
} }
int bmcg_sat_solver_addvar(bmcg_sat_solver* s) int bmcg_sat_solver_addvar(bmcg_sat_solver* s)
{ {
return glucose_solver_addvar((Gluco::Solver*)s); return glucose_solver_addvar((Gluco::SimpSolver*)s);
}
void bmcg_sat_solver_set_nvars( bmcg_sat_solver* s, int nvars )
{
int i;
for ( i = bmcg_sat_solver_varnum(s); i < nvars; i++ )
bmcg_sat_solver_addvar(s);
}
int bmcg_sat_solver_eliminate( bmcg_sat_solver* s, int turn_off_elim )
{
return ((Gluco::SimpSolver*)s)->eliminate(turn_off_elim != 0);
}
int bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v )
{
return ((Gluco::SimpSolver*)s)->isEliminated(v);
} }
int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver* s, int ivar) int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver* s, int ivar)
{ {
return glucose_solver_read_cex_varvalue((Gluco::Solver*)s, ivar); return glucose_solver_read_cex_varvalue((Gluco::SimpSolver*)s, ivar);
} }
void bmcg_sat_solver_setstop(bmcg_sat_solver* s, int * pstop) void bmcg_sat_solver_set_stop(bmcg_sat_solver* s, int * pstop)
{ {
glucose_solver_setstop((Gluco::Solver*)s, pstop); glucose_solver_setstop((Gluco::SimpSolver*)s, pstop);
} }
abctime bmcg_sat_solver_set_runtime_limit(bmcg_sat_solver* s, abctime Limit) abctime bmcg_sat_solver_set_runtime_limit(bmcg_sat_solver* s, abctime Limit)
{ {
abctime nRuntimeLimit = ((Gluco::Solver*)s)->nRuntimeLimit; abctime nRuntimeLimit = ((Gluco::SimpSolver*)s)->nRuntimeLimit;
((Gluco::Solver*)s)->nRuntimeLimit = Limit; ((Gluco::SimpSolver*)s)->nRuntimeLimit = Limit;
return nRuntimeLimit; return nRuntimeLimit;
} }
void bmcg_sat_solver_set_conflict_budget(bmcg_sat_solver* s, int Limit) void bmcg_sat_solver_set_conflict_budget(bmcg_sat_solver* s, int Limit)
{ {
if ( Limit > 0 ) if ( Limit > 0 )
((Gluco::Solver*)s)->setConfBudget( (int64_t)Limit ); ((Gluco::SimpSolver*)s)->setConfBudget( (int64_t)Limit );
else else
((Gluco::Solver*)s)->budgetOff(); ((Gluco::SimpSolver*)s)->budgetOff();
} }
int bmcg_sat_solver_varnum(bmcg_sat_solver* s) int bmcg_sat_solver_varnum(bmcg_sat_solver* s)
{ {
return ((Gluco::Solver*)s)->nVars(); return ((Gluco::SimpSolver*)s)->nVars();
} }
int bmcg_sat_solver_clausenum(bmcg_sat_solver* s) int bmcg_sat_solver_clausenum(bmcg_sat_solver* s)
{ {
return ((Gluco::Solver*)s)->nClauses(); return ((Gluco::SimpSolver*)s)->nClauses();
} }
int bmcg_sat_solver_learntnum(bmcg_sat_solver* s) int bmcg_sat_solver_learntnum(bmcg_sat_solver* s)
{ {
return ((Gluco::Solver*)s)->nLearnts(); return ((Gluco::SimpSolver*)s)->nLearnts();
} }
int bmcg_sat_solver_conflictnum(bmcg_sat_solver* s) int bmcg_sat_solver_conflictnum(bmcg_sat_solver* s)
{ {
return ((Gluco::Solver*)s)->conflicts; return ((Gluco::SimpSolver*)s)->conflicts;
} }
/**Function************************************************************* /**Function*************************************************************

6
src/sat/glucose/AbcGlucose.h
View File

@ -70,9 +70,13 @@ extern void bmcg_sat_solver_stop( bmcg_sat_solver* s );
extern int bmcg_sat_solver_addclause( bmcg_sat_solver* s, int * plits, int nlits ); extern int bmcg_sat_solver_addclause( bmcg_sat_solver* s, int * plits, int nlits );
extern void bmcg_sat_solver_setcallback( bmcg_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*) ); extern void bmcg_sat_solver_setcallback( bmcg_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*) );
extern int bmcg_sat_solver_solve( bmcg_sat_solver* s, int * plits, int nlits ); extern int bmcg_sat_solver_solve( bmcg_sat_solver* s, int * plits, int nlits );
extern int bmcg_sat_solver_final( bmcg_sat_solver* s, int ** ppArray );
extern int bmcg_sat_solver_addvar( bmcg_sat_solver* s ); extern int bmcg_sat_solver_addvar( bmcg_sat_solver* s );
extern void bmcg_sat_solver_set_nvars( bmcg_sat_solver* s, int nvars );
extern int bmcg_sat_solver_eliminate( bmcg_sat_solver* s, int turn_off_elim );
extern int bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v );
extern int bmcg_sat_solver_read_cex_varvalue( bmcg_sat_solver* s, int ); extern int bmcg_sat_solver_read_cex_varvalue( bmcg_sat_solver* s, int );
extern void bmcg_sat_solver_setstop( bmcg_sat_solver* s, int * ); extern void bmcg_sat_solver_set_stop( bmcg_sat_solver* s, int * pstop );
extern abctime bmcg_sat_solver_set_runtime_limit( bmcg_sat_solver* s, abctime Limit ); extern abctime bmcg_sat_solver_set_runtime_limit( bmcg_sat_solver* s, abctime Limit );
extern void bmcg_sat_solver_set_conflict_budget( bmcg_sat_solver* s, int Limit ); extern void bmcg_sat_solver_set_conflict_budget( bmcg_sat_solver* s, int Limit );
extern int bmcg_sat_solver_varnum( bmcg_sat_solver* s ); extern int bmcg_sat_solver_varnum( bmcg_sat_solver* s );

2
src/sat/glucose/SimpSolver.h
View File

@ -167,7 +167,7 @@ class SimpSolver : public Solver {
// Implementation of inline methods: // Implementation of inline methods:
inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v] != 0; } inline bool SimpSolver::isEliminated (Var v) const { return eliminated.size() ? eliminated[v] != 0 : 0; }
inline void SimpSolver::updateElimHeap(Var v) { inline void SimpSolver::updateElimHeap(Var v) {
assert(use_simplification); assert(use_simplification);
// if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef) // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)