diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-09-27 10:57:58 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-27 10:57:58 -0700 |
commit | 6c878c1cf54620b10bac95e5765d0d03bf718f5c (patch) | |
tree | e173b16c2d36abd2953a29e8659cb9bafec1c068 /src/preprocessing/assertion_pipeline.cpp | |
parent | 64e8ad696a1accdf489a3073cc480f591be04c39 (diff) |
Make substitution index context-independent (#2474)
When we do solving in incremental mode, we store substitutions at a
special index in our list of assertions. Previously, we used a
context-dependent variable for that. However, this is not needed since
the list of assertions just consists of the assertions currently being
processed, which are independent of the assertions seen so far. This
commit changes the index to be an ordinary integer and moves it to the
AssertionPipeline. Additionally, it abstracts access to the index in
preparation for splitting AssertionPipeline into three vectors (see
issue #2473).
Diffstat (limited to 'src/preprocessing/assertion_pipeline.cpp')
-rw-r--r-- | src/preprocessing/assertion_pipeline.cpp | 29 |
1 files changed, 28 insertions, 1 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 382b1eb63..7408f4ba3 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -18,12 +18,17 @@ #include "expr/node_manager.h" #include "proof/proof.h" #include "proof/proof_manager.h" +#include "theory/rewriter.h" namespace CVC4 { namespace preprocessing { AssertionPipeline::AssertionPipeline() - : d_realAssertionsEnd(0), d_assumptionsStart(0), d_numAssumptions(0) + : d_realAssertionsEnd(0), + d_storeSubstsInAsserts(false), + d_substsIndex(0), + d_assumptionsStart(0), + d_numAssumptions(0) { } @@ -84,5 +89,27 @@ void AssertionPipeline::replace(size_t i, const std::vector<Node>& ns) } } +void AssertionPipeline::enableStoreSubstsInAsserts() +{ + d_storeSubstsInAsserts = true; + d_substsIndex = d_nodes.size(); + d_nodes.push_back(NodeManager::currentNM()->mkConst<bool>(true)); +} + +void AssertionPipeline::disableStoreSubstsInAsserts() +{ + d_storeSubstsInAsserts = false; +} + +void AssertionPipeline::addSubstitutionNode(Node n) +{ + Assert(d_storeSubstsInAsserts); + Assert(n.getKind() == kind::EQUAL); + d_nodes[d_substsIndex] = theory::Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::AND, n, d_nodes[d_substsIndex])); + Assert(theory::Rewriter::rewrite(d_nodes[d_substsIndex]) + == d_nodes[d_substsIndex]); +} + } // namespace preprocessing } // namespace CVC4 |