diff options
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 |