summaryrefslogtreecommitdiff
path: root/src/prop/bvminisat/bvminisat.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/bvminisat/bvminisat.h')
-rw-r--r--src/prop/bvminisat/bvminisat.h8
1 files changed, 7 insertions, 1 deletions
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index cd2a2c6b9..60cdd1c28 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -54,6 +54,10 @@ private:
context::CDO<unsigned> d_assertionsRealCount;
context::CDO<unsigned> d_lastPropagation;
+protected:
+
+ void contextNotifyPop();
+
public:
BVMinisatSatSolver() :
@@ -70,10 +74,12 @@ public:
SatVariable newVar(bool theoryAtom = false);
+ SatVariable trueVar() { return d_minisat->trueVar(); }
+ SatVariable falseVar() { return d_minisat->falseVar(); }
+
void markUnremovable(SatLiteral lit);
void interrupt();
- void notify();
SatValue solve();
SatValue solve(long unsigned int&);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback