summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/preprocessing/assertion_pipeline.cpp29
-rw-r--r--src/preprocessing/assertion_pipeline.h45
-rw-r--r--src/preprocessing/passes/apply_substs.cpp7
-rw-r--r--src/preprocessing/passes/non_clausal_simp.cpp15
-rw-r--r--src/preprocessing/preprocessing_pass_context.cpp1
-rw-r--r--src/preprocessing/preprocessing_pass_context.h7
-rw-r--r--src/smt/smt_engine.cpp8
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<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
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<Node> 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<unsigned> 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<bool>(true));
+ d_assertions.enableStoreSubstsInAsserts();
+ }
+ else
+ {
+ d_assertions.disableStoreSubstsInAsserts();
}
// Add dummy assertion in last position - to be used as a
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback