diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-14 22:15:37 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-09-14 22:15:37 -0700 |
| commit | 2060f439c873c8b1928cbd5f54967571176f2aba (patch) | |
| tree | 45fab904b632b6174ee66807081465693a5da83f /src/smt | |
| parent | c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010 (diff) | |
Refactor how assertions are added to decision engine (#2396)
Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 73264daa5..eeacb9c3f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -568,7 +568,7 @@ class SmtEnginePrivate : public NodeManagerListener { d_managedReplayLog(), d_listenerRegistrations(new ListenerRegistrationList()), d_propagator(true, true), - d_assertions(d_smt.d_userContext), + d_assertions(), d_assertionsProcessed(smt.d_userContext, false), d_fakeContext(), d_abstractValueMap(&d_fakeContext), @@ -715,7 +715,7 @@ class SmtEnginePrivate : public NodeManagerListener { Node applySubstitutions(TNode node) { return Rewriter::rewrite( - d_assertions.getTopLevelSubstitutions().apply(node)); + d_preprocessingPassContext->getTopLevelSubstitutions().apply(node)); } /** @@ -3113,7 +3113,8 @@ void SmtEnginePrivate::processAssertions() { spendResource(options::preprocessStep()); Assert(d_smt.d_fullyInited); Assert(d_smt.d_pendingPops == 0); - SubstitutionMap& top_level_substs = d_assertions.getTopLevelSubstitutions(); + SubstitutionMap& top_level_substs = + d_preprocessingPassContext->getTopLevelSubstitutions(); // Dump the assertions dumpAssertions("pre-everything", d_assertions); @@ -3138,7 +3139,7 @@ void SmtEnginePrivate::processAssertions() { // proper data structure. // Placeholder for storing substitutions - d_assertions.getSubstitutionsIndex() = d_assertions.size(); + d_preprocessingPassContext->setSubstitutionsIndex(d_assertions.size()); d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true)); } @@ -3478,9 +3479,7 @@ void SmtEnginePrivate::processAssertions() { if(noConflict) { Chat() << "pushing to decision engine..." << endl; Assert(iteRewriteAssertionsEnd == d_assertions.size()); - d_smt.d_decisionEngine->addAssertions(d_assertions.ref(), - d_assertions.getRealAssertionsEnd(), - getIteSkolemMap()); + d_smt.d_decisionEngine->addAssertions(d_assertions); } // end: INVARIANT to maintain: no reordering of assertions or |