From af4c76e21a28beac14886e68a5f7ce29e5e7303b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 7 Sep 2017 19:37:46 -0700 Subject: Disabling CNF simplification in &bmcs -g. --- src/sat/bmc/bmcBmcG.c | 5 ++-- src/sat/bmc/bmcBmcS.c | 2 ++ src/sat/glucose/AbcGlucose.cpp | 56 ++++++++++++++++++++++-------------------- 3 files changed, 34 insertions(+), 29 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bmc/bmcBmcG.c b/src/sat/bmc/bmcBmcG.c index 3dadfb20..8fef2ef6 100644 --- a/src/sat/bmc/bmcBmcG.c +++ b/src/sat/bmc/bmcBmcG.c @@ -337,7 +337,7 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) if ( pCnf == NULL ) { Bmcg_ManPrintFrame( p, f, nClauses, -1, clkStart ); - if( pPars->pFuncOnFrameDone) + if( pPars->pFuncOnFrameDone ) for ( k = 0; k < pPars->nFramesAdd; k++ ) for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) pPars->pFuncOnFrameDone(f+k, i, 0); @@ -372,6 +372,7 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) pPars->iFrame = f+k; pGia->pCexSeq = Bmcg_ManGenerateCex( p, i, f+k, 0 ); pPars->nFailOuts++; + Bmcg_ManPrintFrame( p, f+k, nClauses, -1, clkStart ); if ( !pPars->fNotVerbose ) { int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) ); @@ -379,7 +380,7 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) nOutDigits, i, f+k, nOutDigits, pPars->nFailOuts, nOutDigits, Gia_ManPoNum(pGia) ); fflush( stdout ); } - if( pPars->pFuncOnFrameDone) + if( pPars->pFuncOnFrameDone ) pPars->pFuncOnFrameDone(f+k, i, 1); } break; diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index 6a5c2a85..8bfda56b 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -682,6 +682,7 @@ int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) pPars->iFrame = f+k; pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f+k, 0 ); pPars->nFailOuts++; + Bmcs_ManPrintFrame( p, f+k, nClauses, -1, clkStart ); if ( !pPars->fNotVerbose ) { int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) ); @@ -872,6 +873,7 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) pPars->iFrame = f+k; pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f+k, Solver ); pPars->nFailOuts++; + Bmcs_ManPrintFrame( p, f+k, nClauses, Solver, clkStart ); if ( !pPars->fNotVerbose ) { int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) ); diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index caacac10..026a792e 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -54,19 +54,19 @@ extern "C" { SeeAlso [] ***********************************************************************/ -Gluco::SimpSolver * glucose_solver_start() +Gluco::Solver * glucose_solver_start() { - SimpSolver * S = new SimpSolver; + Solver * S = new Solver; S->setIncrementalMode(); return S; } -void glucose_solver_stop(Gluco::SimpSolver* S) +void glucose_solver_stop(Gluco::Solver* S) { delete S; } -int glucose_solver_addclause(Gluco::SimpSolver* S, int * plits, int nlits) +int glucose_solver_addclause(Gluco::Solver* S, int * plits, int nlits) { vec lits; for ( int i = 0; i < nlits; i++,plits++) @@ -81,14 +81,14 @@ int glucose_solver_addclause(Gluco::SimpSolver* S, int * plits, int nlits) return S->addClause(lits); // returns 0 if the problem is UNSAT } -void glucose_solver_setcallback(Gluco::SimpSolver* S, void * pman, int(*pfunc)(void*, int, int*)) +void glucose_solver_setcallback(Gluco::Solver* S, void * pman, int(*pfunc)(void*, int, int*)) { S->pCnfMan = pman; S->pCnfFunc = pfunc; S->nCallConfl = 1000; } -int glucose_solver_solve(Gluco::SimpSolver* S, int * plits, int nlits) +int glucose_solver_solve(Gluco::Solver* S, int * plits, int nlits) { vec lits; for (int i=0;isolveLimited(lits, 0); + Gluco::lbool res = S->solveLimited(lits); return (res == l_True ? 1 : res == l_False ? -1 : 0); } -int glucose_solver_addvar(Gluco::SimpSolver* S) +int glucose_solver_addvar(Gluco::Solver* S) { S->newVar(); return S->nVars() - 1; } -int glucose_solver_read_cex_varvalue(Gluco::SimpSolver* S, int ivar) +int glucose_solver_read_cex_varvalue(Gluco::Solver* S, int ivar) { return S->model[ivar] == l_True; } -void glucose_solver_setstop(Gluco::SimpSolver* S, int * pstop) +void glucose_solver_setstop(Gluco::Solver* S, int * pstop) { S->pstop = pstop; } @@ -155,33 +155,33 @@ bmcg_sat_solver * bmcg_sat_solver_start() } void bmcg_sat_solver_stop(bmcg_sat_solver* s) { - glucose_solver_stop((Gluco::SimpSolver*)s); + glucose_solver_stop((Gluco::Solver*)s); } int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits) { - return glucose_solver_addclause((Gluco::SimpSolver*)s,plits,nlits); + return glucose_solver_addclause((Gluco::Solver*)s,plits,nlits); } void bmcg_sat_solver_setcallback(bmcg_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*)) { - glucose_solver_setcallback((Gluco::SimpSolver*)s,pman,pfunc); + glucose_solver_setcallback((Gluco::Solver*)s,pman,pfunc); } int bmcg_sat_solver_solve(bmcg_sat_solver* s, int * plits, int nlits) { - return glucose_solver_solve((Gluco::SimpSolver*)s,plits,nlits); + return glucose_solver_solve((Gluco::Solver*)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(); + *ppArray = (int *)(Lit *)((Gluco::Solver*)s)->conflict; + return ((Gluco::Solver*)s)->conflict.size(); } int bmcg_sat_solver_addvar(bmcg_sat_solver* s) { - return glucose_solver_addvar((Gluco::SimpSolver*)s); + return glucose_solver_addvar((Gluco::Solver*)s); } void bmcg_sat_solver_set_nvars( bmcg_sat_solver* s, int nvars ) @@ -193,54 +193,56 @@ void bmcg_sat_solver_set_nvars( bmcg_sat_solver* s, int nvars ) int bmcg_sat_solver_eliminate( bmcg_sat_solver* s, int turn_off_elim ) { + return 1; return ((Gluco::SimpSolver*)s)->eliminate(turn_off_elim != 0); } int bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v ) { + return 0; 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::SimpSolver*)s, ivar); + return glucose_solver_read_cex_varvalue((Gluco::Solver*)s, ivar); } void bmcg_sat_solver_set_stop(bmcg_sat_solver* s, int * pstop) { - glucose_solver_setstop((Gluco::SimpSolver*)s, pstop); + glucose_solver_setstop((Gluco::Solver*)s, pstop); } abctime bmcg_sat_solver_set_runtime_limit(bmcg_sat_solver* s, abctime Limit) { - abctime nRuntimeLimit = ((Gluco::SimpSolver*)s)->nRuntimeLimit; - ((Gluco::SimpSolver*)s)->nRuntimeLimit = Limit; + abctime nRuntimeLimit = ((Gluco::Solver*)s)->nRuntimeLimit; + ((Gluco::Solver*)s)->nRuntimeLimit = Limit; return nRuntimeLimit; } void bmcg_sat_solver_set_conflict_budget(bmcg_sat_solver* s, int Limit) { if ( Limit > 0 ) - ((Gluco::SimpSolver*)s)->setConfBudget( (int64_t)Limit ); + ((Gluco::Solver*)s)->setConfBudget( (int64_t)Limit ); else - ((Gluco::SimpSolver*)s)->budgetOff(); + ((Gluco::Solver*)s)->budgetOff(); } int bmcg_sat_solver_varnum(bmcg_sat_solver* s) { - return ((Gluco::SimpSolver*)s)->nVars(); + return ((Gluco::Solver*)s)->nVars(); } int bmcg_sat_solver_clausenum(bmcg_sat_solver* s) { - return ((Gluco::SimpSolver*)s)->nClauses(); + return ((Gluco::Solver*)s)->nClauses(); } int bmcg_sat_solver_learntnum(bmcg_sat_solver* s) { - return ((Gluco::SimpSolver*)s)->nLearnts(); + return ((Gluco::Solver*)s)->nLearnts(); } int bmcg_sat_solver_conflictnum(bmcg_sat_solver* s) { - return ((Gluco::SimpSolver*)s)->conflicts; + return ((Gluco::Solver*)s)->conflicts; } /**Function************************************************************* -- cgit v1.2.3