diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-09 12:44:03 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-09 12:44:03 -0600 |
| commit | b1f4694c582a315feccb4c0c7e1a683583ff29e8 (patch) | |
| tree | 9f18c1564867206a4abbd1bb51dcb190359cd5c7 /src/smt | |
| parent | 59cd96a33b8f32405be2a20fc8230efc33b8dcdc (diff) | |
Make decision engine independent of AssertionsPipeline (#5626)
This PR makes decision engine independent of AssertionsPipeline, which consequently allows some of the key PropEngine interfaces to be consolidated. It also modifies PropEngine to take TrustNode for assertLemma, which is the first step for making PropEngine manage proofs from TheoryEngine.
This is in preparation for modifying the interplay between PropEngine, TheoryEngine, TheoryPreprocessor, and new proposed SAT relevancy heuristic.
There are no intended behavior changes in this PR.
Marking "major" since this impacts several current directions (including proof-new integration, lazy theory preprocessing, SAT relevancy).
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_solver.cpp | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 26a2ff3e1..c18dfe8ac 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -224,14 +224,11 @@ void SmtSolver::processAssertions(Assertions& as) // process the assertions with the preprocessor bool noConflict = d_pp.process(as); - // notify theory engine new preprocessed assertions - d_theoryEngine->notifyPreprocessedAssertions(ap.ref()); - // Push the formula to decision engine if (noConflict) { - Chat() << "pushing to decision engine..." << endl; - d_propEngine->addAssertionsToDecisionEngine(ap); + Chat() << "notifying theory engine and decision engine..." << std::endl; + d_propEngine->notifyPreprocessedAssertions(ap); } // end: INVARIANT to maintain: no reordering of assertions or |