summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2020-11-12 08:30:33 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2020-11-12 08:30:33 -0800
commit890aa684ab44a09c2e6af4ec50d438506a8fbecb (patch)
tree10e39ee73a170fe63e4712f46c03bd526d86db7b
parent83519c320c1d335675e97f144cff109200141770 (diff)
downloadabc-890aa684ab44a09c2e6af4ec50d438506a8fbecb.tar.gz
abc-890aa684ab44a09c2e6af4ec50d438506a8fbecb.tar.bz2
abc-890aa684ab44a09c2e6af4ec50d438506a8fbecb.zip
Adding Glucose API to return a CEX.
-rw-r--r--src/sat/glucose/AbcGlucose.cpp19
-rw-r--r--src/sat/glucose/AbcGlucose.h1
-rw-r--r--src/sat/glucose/Solver.h2
3 files changed, 22 insertions, 0 deletions
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index 247bc89a..5ff2b120 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -116,6 +116,11 @@ int glucose_solver_addvar(Gluco::SimpSolver* S)
return S->nVars() - 1;
}
+int * glucose_solver_read_cex(Gluco::SimpSolver* S )
+{
+ return S->getCex();
+}
+
int glucose_solver_read_cex_varvalue(Gluco::SimpSolver* S, int ivar)
{
return S->model[ivar] == l_True;
@@ -208,6 +213,10 @@ int bmcg_sat_solver_elim_varnum(bmcg_sat_solver* s)
return ((Gluco::SimpSolver*)s)->eliminated_vars;
}
+int * bmcg_sat_solver_read_cex(bmcg_sat_solver* s)
+{
+ return glucose_solver_read_cex((Gluco::SimpSolver*)s);
+}
int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver* s, int ivar)
{
return glucose_solver_read_cex_varvalue((Gluco::SimpSolver*)s, ivar);
@@ -383,6 +392,11 @@ int glucose_solver_addvar(Gluco::Solver* S)
return S->nVars() - 1;
}
+int * glucose_solver_read_cex(Gluco::Solver* S )
+{
+ return S->getCex();
+}
+
int glucose_solver_read_cex_varvalue(Gluco::Solver* S, int ivar)
{
return S->model[ivar] == l_True;
@@ -470,6 +484,11 @@ int bmcg_sat_solver_elim_varnum(bmcg_sat_solver* s)
// return ((Gluco::SimpSolver*)s)->eliminated_vars;
}
+int * bmcg_sat_solver_read_cex(bmcg_sat_solver* s)
+{
+ return glucose_solver_read_cex((Gluco::Solver*)s);
+}
+
int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver* s, int ivar)
{
return glucose_solver_read_cex_varvalue((Gluco::Solver*)s, ivar);
diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h
index 4489adc7..026c22ee 100644
--- a/src/sat/glucose/AbcGlucose.h
+++ b/src/sat/glucose/AbcGlucose.h
@@ -83,6 +83,7 @@ extern int bmcg_sat_solver_eliminate( bmcg_sat_solver* s, int turn
extern int bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v );
extern void bmcg_sat_solver_var_set_frozen( bmcg_sat_solver* s, int v, int freeze );
extern int bmcg_sat_solver_elim_varnum(bmcg_sat_solver* s);
+extern int * bmcg_sat_solver_read_cex( bmcg_sat_solver* s );
extern int bmcg_sat_solver_read_cex_varvalue( bmcg_sat_solver* s, int );
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 );
diff --git a/src/sat/glucose/Solver.h b/src/sat/glucose/Solver.h
index df72660a..43b13db7 100644
--- a/src/sat/glucose/Solver.h
+++ b/src/sat/glucose/Solver.h
@@ -116,6 +116,7 @@ public:
int nLearnts () const; // The current number of learnt clauses.
int nVars () const; // The current number of variables.
int nFreeVars () const;
+ int * getCex () const;
// Incremental mode
void setIncrementalMode();
@@ -418,6 +419,7 @@ inline int Solver::nClauses () const { return clauses.size(); }
inline int Solver::nLearnts () const { return learnts.size(); }
inline int Solver::nVars () const { return vardata.size(); }
inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
+inline int * Solver::getCex () const { return NULL; }
inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
inline void Solver::setDecisionVar(Var v, bool b)
{