diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-04-30 14:42:28 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-04-30 14:42:28 +0000 |
commit | 97555307af3415d6fbbac3fc9dccdafec51056b7 (patch) | |
tree | 56b47f809268d5b8ae21594d22cbec7ced8f46aa /src/prop | |
parent | 9ac1cb18f03a5edf4b50532d29e195f74d6a83c2 (diff) |
Added map from skolem variables to new ite formulas in ite removal.
d_sharedTermsExist is now set based on logicInfo instead of dynamically when
shared terms are found.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/prop_engine.cpp | 6 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 5 |
2 files changed, 1 insertions, 10 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 212a99a8e..03746c9b2 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -91,15 +91,11 @@ PropEngine::~PropEngine() { delete d_satSolver; } -void PropEngine::processAssertionsStart() { - d_theoryEngine->preprocessStart(); -} - void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as non-removable - d_cnfStream->convertAndAssert(d_theoryEngine->preprocess(node), false, false); + d_cnfStream->convertAndAssert(node, false, false); } void PropEngine::assertLemma(TNode node, bool negated, bool removable) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 3d114db3a..9e49cf3f1 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -174,11 +174,6 @@ public: void shutdown() { } /** - * Signal that a new round of assertions is ready so we can notify the theory engine - */ - void processAssertionsStart(); - - /** * Converts the given formula to CNF and assert the CNF to the SAT solver. * The formula is asserted permanently for the current context. * @param node the formula to assert |