diff options
Diffstat (limited to 'src/prop/sat.h')
-rw-r--r-- | src/prop/sat.h | 43 |
1 files changed, 42 insertions, 1 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h index 550de5527..6e244d9d7 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -103,6 +103,12 @@ public: virtual void addClause(SatClause& clause, bool lemma) = 0; /** Create a new boolean variable in the solver. */ virtual SatVariable newVar(bool theoryAtom = false) = 0; + /** Get the current decision level of the solver */ + virtual int getLevel() const = 0; + /** Unregister the variable (of the literal) from solving */ + virtual void unregisterVar(SatLiteral lit) = 0; + /** Register the variable (of the literal) for solving */ + virtual void renewVar(SatLiteral lit, int level = -1) = 0; }; /** @@ -226,6 +232,21 @@ public: void setCnfStream(CnfStream* cnfStream); SatLiteralValue value(SatLiteral l); + + int getLevel() const; + + void push(); + + void pop(); + + void removeClausesAboveLevel(int level); + + void unregisterVar(SatLiteral lit); + + void renewVar(SatLiteral lit, int level = -1); + + TNode getNode(SatLiteral lit); + };/* class SatSolver */ /* Functions that delegate to the concrete SAT solver. */ @@ -241,7 +262,7 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, d_statistics() { // Create the solver - d_minisat = new Minisat::SimpSolver(this, d_context); + d_minisat = new Minisat::SimpSolver(this, d_context, options.incrementalSolving); // Setup the verbosity d_minisat->verbosity = (options.verbosity > 0) ? 1 : -1; @@ -273,6 +294,26 @@ inline SatLiteralValue SatSolver::value(SatLiteral l) { return d_minisat->modelValue(l); } +inline void SatSolver::push() { + d_minisat->push(); +} + +inline void SatSolver::pop() { + d_minisat->pop(); +} + +inline int SatSolver::getLevel() const { + return d_minisat->getAssertionLevel(); +} + +inline void SatSolver::unregisterVar(SatLiteral lit) { + d_minisat->unregisterVar(lit); +} + +inline void SatSolver::renewVar(SatLiteral lit, int level) { + d_minisat->renewVar(lit, level); +} + #endif /* __CVC4_USE_MINISAT */ inline size_t |