summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-09-18 09:36:08 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2017-09-18 09:36:08 -0700
commit36858c5365c73b8702deccbbac90279f8917a7ca (patch)
treedf0e6430054c098b19f486df57569ae1e4b93361 /src/sat
parent12d21480de5f5434df72f577afcc7208b2dc0683 (diff)
downloadabc-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.cpp10
-rw-r--r--src/sat/glucose/AbcGlucose.h6
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 );