#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)
{
}
}
}
+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
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;
/** 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 */
// 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;
}
// 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;
}
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())
{
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()
: 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)
/* 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()
{
/** 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;
// 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
projects / cvc5.git / commitdiff