From ba0d855fd4eed9439e4ce4fa6eb778cbb2250708 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 7 Sep 2017 19:16:13 -0700 Subject: Trying to enable CNF simplification in &bmcs -g. --- src/base/abci/abc.c | 9 +++-- src/sat/bmc/bmc.h | 1 + src/sat/bmc/bmcBmcG.c | 11 +++---- src/sat/glucose/AbcGlucose.cpp | 75 +++++++++++++++++++++++++++--------------- src/sat/glucose/AbcGlucose.h | 18 ++++++---- src/sat/glucose/SimpSolver.h | 2 +- 6 files changed, 74 insertions(+), 42 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6c5e762a..66c0ecca 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -40017,6 +40017,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fUseSynth = 0; // use synthesis pPars->fUseOldCnf = 0; // use old CNF construction pPars->fUseGlucose = 0; // use Glucose 3.0 + pPars->fUseEliminate = 0; // use variable elimination pPars->fVerbose = 0; // verbose pPars->fVeryVerbose = 0; // very verbose 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 Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PCFATgvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PCFATgevwh" ) ) != EOF ) { switch ( c ) { @@ -40088,6 +40089,9 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'g': pPars->fUseGlucose ^= 1; break; + case 'e': + pPars->fUseEliminate ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -40116,7 +40120,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; 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-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 ); @@ -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-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-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-w : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 2585c773..8e249339 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -95,6 +95,7 @@ struct Bmc_AndPar_t_ int fUseSynth; // use synthesis int fUseOldCnf; // use old CNF construction int fUseGlucose; // use Glucose 3.0 as the default solver + int fUseEliminate; // use variable elimination int fVerbose; // verbose int fVeryVerbose; // very verbose int fNotVerbose; // skip line-by-line print-out diff --git a/src/sat/bmc/bmcBmcG.c b/src/sat/bmc/bmcBmcG.c index 27d6b8d3..3dadfb20 100644 --- a/src/sat/bmc/bmcBmcG.c +++ b/src/sat/bmc/bmcBmcG.c @@ -42,7 +42,6 @@ struct Bmcg_Man_t_ Vec_Int_t vCiMap; // maps CIs of pFrames into CIs/frames of GIA bmcg_sat_solver * pSats[PAR_THR_MAX]; // concurrent SAT solvers int nSatVars; // number of SAT variables used - int nSatVarsOld; // number of SAT variables used int fStopNow; // signal when it is time to stop abctime timeUnf; // runtime of unfolding 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; bmcg_sat_solver_addvar( p->pSats[i] ); 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; return p; @@ -166,7 +165,7 @@ int Bmcg_ManCollect_rec( Bmcg_Man_t * p, int iObj ) return iLitClean; pObj = Gia_ManObj( p->pFrames, 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 ); 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 ) { int i; - for ( i = p->nSatVarsOld; i < p->nSatVars; i++ ) - bmcg_sat_solver_addvar( pSat ); + bmcg_sat_solver_set_nvars( pSat, p->nSatVars ); for ( i = 0; i < pCnf->nClauses; i++ ) if ( !bmcg_sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) assert( 0 ); + if ( p->pPars->fUseEliminate ) + bmcg_sat_solver_eliminate( pSat, 0 ); } 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; Bmcg_ManAddCnf( p, p->pSats[0], pCnf ); - p->nSatVarsOld = p->nSatVars; Cnf_DataFree( pCnf ); assert( Gia_ManPoNum(p->pFrames) == (f + pPars->nFramesAdd) * Gia_ManPoNum(pGia) ); for ( k = 0; k < pPars->nFramesAdd; k++ ) diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index 141ecbde..caacac10 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -54,19 +54,19 @@ extern "C" { SeeAlso [] ***********************************************************************/ -Gluco::Solver * glucose_solver_start() +Gluco::SimpSolver * glucose_solver_start() { - Solver * S = new Solver; + SimpSolver * S = new SimpSolver; S->setIncrementalMode(); return S; } -void glucose_solver_stop(Gluco::Solver* S) +void glucose_solver_stop(Gluco::SimpSolver* 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 lits; 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 } -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->pCnfFunc = pfunc; 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 lits; for (int i=0;isolveLimited(lits); + Gluco::lbool res = S->solveLimited(lits, 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(); 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; } -void glucose_solver_setstop(Gluco::Solver* S, int * pstop) +void glucose_solver_setstop(Gluco::SimpSolver* S, int * pstop) { S->pstop = pstop; } @@ -155,69 +155,92 @@ bmcg_sat_solver * bmcg_sat_solver_start() } 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) { - 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*)) { - 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) { - 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) { - 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) { - 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 nRuntimeLimit = ((Gluco::Solver*)s)->nRuntimeLimit; - ((Gluco::Solver*)s)->nRuntimeLimit = Limit; + abctime nRuntimeLimit = ((Gluco::SimpSolver*)s)->nRuntimeLimit; + ((Gluco::SimpSolver*)s)->nRuntimeLimit = Limit; return nRuntimeLimit; } void bmcg_sat_solver_set_conflict_budget(bmcg_sat_solver* s, int Limit) { if ( Limit > 0 ) - ((Gluco::Solver*)s)->setConfBudget( (int64_t)Limit ); + ((Gluco::SimpSolver*)s)->setConfBudget( (int64_t)Limit ); else - ((Gluco::Solver*)s)->budgetOff(); + ((Gluco::SimpSolver*)s)->budgetOff(); } 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) { - return ((Gluco::Solver*)s)->nClauses(); + return ((Gluco::SimpSolver*)s)->nClauses(); } 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) { - return ((Gluco::Solver*)s)->conflicts; + return ((Gluco::SimpSolver*)s)->conflicts; } /**Function************************************************************* diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h index 4e3f13a5..c0078845 100644 --- a/src/sat/glucose/AbcGlucose.h +++ b/src/sat/glucose/AbcGlucose.h @@ -70,15 +70,19 @@ 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 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_final( bmcg_sat_solver* s, int ** ppArray ); 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 void bmcg_sat_solver_setstop( bmcg_sat_solver* s, int * ); -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 int bmcg_sat_solver_varnum(bmcg_sat_solver* s); -extern int bmcg_sat_solver_clausenum(bmcg_sat_solver* s); -extern int bmcg_sat_solver_learntnum(bmcg_sat_solver* s); -extern int bmcg_sat_solver_conflictnum(bmcg_sat_solver* s); +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 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_clausenum( bmcg_sat_solver* s ); +extern int bmcg_sat_solver_learntnum( bmcg_sat_solver* s ); +extern int bmcg_sat_solver_conflictnum( bmcg_sat_solver* s ); extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars ); extern int Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars ); diff --git a/src/sat/glucose/SimpSolver.h b/src/sat/glucose/SimpSolver.h index 3f02f13e..0f619b19 100644 --- a/src/sat/glucose/SimpSolver.h +++ b/src/sat/glucose/SimpSolver.h @@ -167,7 +167,7 @@ class SimpSolver : public Solver { // 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) { assert(use_simplification); // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef) -- cgit v1.2.3