From 6c878c1cf54620b10bac95e5765d0d03bf718f5c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 27 Sep 2019 10:57:58 -0700 Subject: [PATCH] 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). --- src/preprocessing/assertion_pipeline.cpp | 29 +++++++++++- src/preprocessing/assertion_pipeline.h | 45 +++++++++++++++++++ src/preprocessing/passes/apply_substs.cpp | 7 +-- src/preprocessing/passes/non_clausal_simp.cpp | 15 ++----- .../preprocessing_pass_context.cpp | 1 - .../preprocessing_pass_context.h | 7 --- src/smt/smt_engine.cpp | 8 ++-- 7 files changed, 82 insertions(+), 30 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& ns) } } +void AssertionPipeline::enableStoreSubstsInAsserts() +{ + d_storeSubstsInAsserts = true; + d_substsIndex = d_nodes.size(); + d_nodes.push_back(NodeManager::currentNM()->mkConst(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 diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index cc9d1c2af..b133bc490 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -95,6 +95,37 @@ class AssertionPipeline void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); } + /** + * Returns true if substitutions must be stored as assertions. This is for + * example the case when we do incremental solving. + */ + bool storeSubstsInAsserts() { return d_storeSubstsInAsserts; } + + /** + * Enables storing substitutions as assertions. + */ + void enableStoreSubstsInAsserts(); + + /** + * Disables storing substitutions as assertions. + */ + void disableStoreSubstsInAsserts(); + + /** + * Adds a substitution node of the form (= lhs rhs) to the assertions. + */ + void addSubstitutionNode(Node n); + + /** + * Checks whether the assertion at a given index represents substitutions. + * + * @param i The index in question + */ + bool isSubstsIndex(size_t i) + { + return d_storeSubstsInAsserts && i == d_substsIndex; + } + private: /** The list of current assertions */ std::vector d_nodes; @@ -108,6 +139,20 @@ class AssertionPipeline /** Size of d_nodes when preprocessing starts */ size_t d_realAssertionsEnd; + /** + * If true, we store the substitutions as assertions. This is necessary when + * doing incremental solving because we cannot apply them to existing + * assertions while preprocessing new assertions. + */ + bool d_storeSubstsInAsserts; + + /** + * The index of the assertions that holds the substitutions. + * + * TODO(#2473): replace by separate vector of substitution assertions. + */ + size_t d_substsIndex; + /** Index of the first assumption */ size_t d_assumptionsStart; /** The number of assumptions */ diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index ddacc20c0..791bb2dc7 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -41,17 +41,12 @@ PreprocessingPassResult ApplySubsts::applyInternal( // TODO(#1255): Substitutions in incremental mode should be managed with a // proper data structure. - // When solving incrementally, all substitutions are piled into the - // assertion at d_substitutionsIndex: we don't want to apply substitutions - // to this assertion or information will be lost. - unsigned substs_index = d_preprocContext->getSubstitutionsIndex(); theory::SubstitutionMap& substMap = d_preprocContext->getTopLevelSubstitutions(); unsigned size = assertionsToPreprocess->size(); - unsigned substitutionAssertion = substs_index > 0 ? substs_index : size; for (unsigned i = 0; i < size; ++i) { - if (i == substitutionAssertion) + if (assertionsToPreprocess->isSubstsIndex(i)) { continue; } diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 4a0f38689..139bf96a9 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -76,13 +76,12 @@ PreprocessingPassResult NonClausalSimp::applyInternal( // Assert all the assertions to the propagator Trace("non-clausal-simplify") << "asserting to propagator" << std::endl; - unsigned substs_index = d_preprocContext->getSubstitutionsIndex(); for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { Assert(Rewriter::rewrite((*assertionsToPreprocess)[i]) == (*assertionsToPreprocess)[i]); // Don't reprocess substitutions - if (substs_index > 0 && i == substs_index) + if (assertionsToPreprocess->isSubstsIndex(i)) { continue; } @@ -344,14 +343,13 @@ PreprocessingPassResult NonClausalSimp::applyInternal( TheoryModel* m = d_preprocContext->getTheoryEngine()->getModel(); Assert(m != nullptr); NodeManager* nm = NodeManager::currentNM(); - NodeBuilder<> substitutionsBuilder(kind::AND); for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) { Node lhs = (*pos).first; Node rhs = newSubstitutions.apply((*pos).second); // If using incremental, we must check whether this variable has occurred // before now. If it hasn't we can add this as a substitution. - if (substs_index == 0 + if (!assertionsToPreprocess->storeSubstsInAsserts() || d_preprocContext->getSymsInAssertions().find(lhs) == d_preprocContext->getSymsInAssertions().end()) { @@ -366,16 +364,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal( Trace("non-clausal-simplify") << "substitute: will notify SAT layer of substitution: " << eq << std::endl; - substitutionsBuilder << eq; + assertionsToPreprocess->addSubstitutionNode(eq); } } - // add to the last assertion if necessary - if (substitutionsBuilder.getNumChildren() > 0) - { - substitutionsBuilder << (*assertionsToPreprocess)[substs_index]; - assertionsToPreprocess->replace( - substs_index, Rewriter::rewrite(Node(substitutionsBuilder))); - } NodeBuilder<> learnedBuilder(kind::AND); Assert(assertionsToPreprocess->getRealAssertionsEnd() diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 2d25502d1..b04c05b9e 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -29,7 +29,6 @@ PreprocessingPassContext::PreprocessingPassContext( : d_smt(smt), d_resourceManager(resourceManager), d_iteRemover(iteRemover), - d_substitutionsIndex(smt->d_userContext, 0), d_topLevelSubstitutions(smt->d_userContext), d_circuitPropagator(circuitPropagator), d_symsInAssertions(smt->d_userContext) diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index e37680538..37744151c 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -71,10 +71,6 @@ class PreprocessingPassContext /* Widen the logic to include the given theory. */ void widenLogic(theory::TheoryId id); - unsigned getSubstitutionsIndex() const { return d_substitutionsIndex.get(); } - - void setSubstitutionsIndex(unsigned i) { d_substitutionsIndex = i; } - /** Gets a reference to the top-level substitution map */ theory::SubstitutionMap& getTopLevelSubstitutions() { @@ -101,9 +97,6 @@ class PreprocessingPassContext /** Instance of the ITE remover */ RemoveTermFormulas* d_iteRemover; - /* Index for where to store substitutions */ - context::CDO d_substitutionsIndex; - /* The top level substitutions */ theory::SubstitutionMap d_topLevelSubstitutions; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 305c36d13..f451d12bd 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3168,9 +3168,11 @@ void SmtEnginePrivate::processAssertions() { // TODO(b/1255): Substitutions in incremental mode should be managed with a // proper data structure. - // Placeholder for storing substitutions - d_preprocessingPassContext->setSubstitutionsIndex(d_assertions.size()); - d_assertions.push_back(NodeManager::currentNM()->mkConst(true)); + d_assertions.enableStoreSubstsInAsserts(); + } + else + { + d_assertions.disableStoreSubstsInAsserts(); } // Add dummy assertion in last position - to be used as a -- 2.30.2