diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-12 08:30:33 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-12 08:30:33 -0800 |
| commit | 890aa684ab44a09c2e6af4ec50d438506a8fbecb (patch) | |
| tree | 10e39ee73a170fe63e4712f46c03bd526d86db7b | |
| parent | 83519c320c1d335675e97f144cff109200141770 (diff) | |
| download | abc-890aa684ab44a09c2e6af4ec50d438506a8fbecb.tar.gz abc-890aa684ab44a09c2e6af4ec50d438506a8fbecb.tar.bz2 abc-890aa684ab44a09c2e6af4ec50d438506a8fbecb.zip | |
Adding Glucose API to return a CEX.
| -rw-r--r-- | src/sat/glucose/AbcGlucose.cpp | 19 | ||||
| -rw-r--r-- | src/sat/glucose/AbcGlucose.h | 1 | ||||
| -rw-r--r-- | src/sat/glucose/Solver.h | 2 |
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) { |