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 /src/sat/glucose/Solver.h | |
| parent | 83519c320c1d335675e97f144cff109200141770 (diff) | |
| download | abc-890aa684ab44a09c2e6af4ec50d438506a8fbecb.tar.gz abc-890aa684ab44a09c2e6af4ec50d438506a8fbecb.tar.bz2 abc-890aa684ab44a09c2e6af4ec50d438506a8fbecb.zip | |
Adding Glucose API to return a CEX.
Diffstat (limited to 'src/sat/glucose/Solver.h')
| -rw-r--r-- | src/sat/glucose/Solver.h | 2 |
1 files changed, 2 insertions, 0 deletions
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) { |