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