diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-11-09 21:57:06 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-11-09 21:57:06 +0000 |
commit | df5f7fe03fda041429548bcb39abb8916ca2e291 (patch) | |
tree | 46b08f3e35ee9c3d4c551d82f3e7e36582383f39 /src/prop/prop_engine.cpp | |
parent | 1f07775e9205b3f9e172a1ad218a9015b7265b58 (diff) |
Lemmas on demand work, push-pop, some cleanup.
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 5851f3990..45d941553 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -22,7 +22,6 @@ #include "theory/theory_engine.h" #include "util/Assert.h" -#include "util/decision_engine.h" #include "util/options.h" #include "util/output.h" #include "util/result.h" @@ -57,11 +56,9 @@ public: } }; -PropEngine::PropEngine(DecisionEngine* de, TheoryEngine* te, +PropEngine::PropEngine(TheoryEngine* te, Context* context, const Options& opts) : d_inCheckSat(false), - // d_options(opts), - d_decisionEngine(de), d_theoryEngine(te), d_context(context) { Debug("prop") << "Constructing the PropEngine" << endl; @@ -85,9 +82,9 @@ void PropEngine::assertFormula(TNode node) { void PropEngine::assertLemma(TNode node) { Assert(d_inCheckSat, "Sat solver should be in solve()!"); - Debug("prop") << "assertFormula(" << node << ")" << endl; + Debug("prop::lemma") << "assertLemma(" << node << ")" << endl; // Assert as removable - d_cnfStream->convertAndAssert(node, false, false); + d_cnfStream->convertAndAssert(node, true, false); } @@ -101,8 +98,8 @@ void PropEngine::printSatisfyingAssignment(){ end = transCache.end(); i != end; ++i) { - pair<Node, SatLiteral> curr = *i; - SatLiteral l = curr.second; + pair<Node, CnfStream::TranslationInfo> curr = *i; + SatLiteral l = curr.second.literal; if(!sign(l)) { Node n = curr.first; SatLiteralValue value = d_satSolver->value(l); @@ -150,11 +147,13 @@ Node PropEngine::getValue(TNode node) { void PropEngine::push() { Assert(!d_inCheckSat, "Sat solver in solve()!"); + d_satSolver->push(); Debug("prop") << "push()" << endl; } void PropEngine::pop() { Assert(!d_inCheckSat, "Sat solver in solve()!"); + d_satSolver->pop(); Debug("prop") << "pop()" << endl; } |