Adding Glucose API to return a CEX.

1 files changed, 19 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);