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/sat/glucose/AbcGlucose.h | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) (limited to 'src/sat/glucose/AbcGlucose.h') 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 ); -- cgit v1.2.3