diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-18 09:36:08 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-18 09:36:08 -0700 |
| commit | 36858c5365c73b8702deccbbac90279f8917a7ca (patch) | |
| tree | df0e6430054c098b19f486df57569ae1e4b93361 /src/sat | |
| parent | 12d21480de5f5434df72f577afcc7208b2dc0683 (diff) | |
| download | abc-36858c5365c73b8702deccbbac90279f8917a7ca.tar.gz abc-36858c5365c73b8702deccbbac90279f8917a7ca.tar.bz2 abc-36858c5365c73b8702deccbbac90279f8917a7ca.zip | |
Enabling Glucose in SAT sweeping: &fraig -g.
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/glucose/AbcGlucose.cpp | 10 | ||||
| -rw-r--r-- | src/sat/glucose/AbcGlucose.h | 6 |
2 files changed, 16 insertions, 0 deletions
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index 064c723e..7d56cc56 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -71,6 +71,11 @@ void glucose_solver_stop(Gluco::SimpSolver* S) delete S; } +void glucose_solver_reset(Gluco::SimpSolver* S) +{ + S->reset(); +} + int glucose_solver_addclause(Gluco::SimpSolver* S, int * plits, int nlits) { vec<Lit> lits; @@ -142,6 +147,11 @@ void bmcg_sat_solver_stop(bmcg_sat_solver* s) { glucose_solver_stop((Gluco::SimpSolver*)s); } +void bmcg_sat_solver_reset(bmcg_sat_solver* s) +{ + glucose_solver_reset((Gluco::SimpSolver*)s); +} + int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits) { diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h index e36b7a24..04bc264b 100644 --- a/src/sat/glucose/AbcGlucose.h +++ b/src/sat/glucose/AbcGlucose.h @@ -33,6 +33,11 @@ ABC_NAMESPACE_HEADER_START +#define GLUCOSE_UNSAT -1 +#define GLUCOSE_SAT 1 +#define GLUCOSE_UNDEC 0 + + //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// @@ -67,6 +72,7 @@ typedef void bmcg_sat_solver; extern bmcg_sat_solver * bmcg_sat_solver_start(); extern void bmcg_sat_solver_stop( bmcg_sat_solver* s ); +extern void bmcg_sat_solver_reset( 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 ); |