Adding Glucose API to return a CEX.

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);

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 );

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) 
 {