diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-07 19:16:13 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-07 19:16:13 -0700 |
| commit | ba0d855fd4eed9439e4ce4fa6eb778cbb2250708 (patch) | |
| tree | a348bf91fc74532e874613c9d3628d4af02460d5 /src/sat/glucose/AbcGlucose.h | |
| parent | 68b59b8a1e09722cd71490c91904d5c3104535fa (diff) | |
| download | abc-ba0d855fd4eed9439e4ce4fa6eb778cbb2250708.tar.gz abc-ba0d855fd4eed9439e4ce4fa6eb778cbb2250708.tar.bz2 abc-ba0d855fd4eed9439e4ce4fa6eb778cbb2250708.zip | |
Trying to enable CNF simplification in &bmcs -g.
Diffstat (limited to 'src/sat/glucose/AbcGlucose.h')
| -rw-r--r-- | src/sat/glucose/AbcGlucose.h | 18 |
1 files changed, 11 insertions, 7 deletions
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 ); |