From 36858c5365c73b8702deccbbac90279f8917a7ca Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 18 Sep 2017 09:36:08 -0700 Subject: Enabling Glucose in SAT sweeping: &fraig -g. --- src/sat/glucose/AbcGlucose.cpp | 10 ++++++++++ src/sat/glucose/AbcGlucose.h | 6 ++++++ 2 files changed, 16 insertions(+) (limited to 'src/sat/glucose') 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 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 ); -- cgit v1.2.3