diff options
Diffstat (limited to 'src/prop/sat.h')
-rw-r--r-- | src/prop/sat.h | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h index 2521f3ee7..39977a96b 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -70,6 +70,10 @@ inline SatVariable literalToVariable(SatLiteral lit) { return Minisat::var(lit); } +inline SatLiteral variableToLiteral(SatVariable var) { + return Minisat::mkLit(var); +} + inline bool literalSign(SatLiteral lit) { return Minisat::sign(lit); } @@ -208,7 +212,7 @@ public: TheoryEngine* theoryEngine, context::Context* context); - ~SatSolver(); + virtual ~SatSolver(); bool solve(); @@ -242,6 +246,11 @@ public: void removeClausesAboveLevel(int level); + /** + * Notifies of a new variable at a decision level. + */ + void variableNotify(SatVariable var); + void unregisterVar(SatLiteral lit); void renewVar(SatLiteral lit, int level = -1); |