/** The top level substitutions */
SubstitutionMap d_topLevelSubstitutions;
+ /**
+ * d_lastSubstitutionPos points to the last
+ * substitution that was added to d_topLevelSubstitutions.
+ * If d_lastSubstitutionPos == d_topLevelSubstitutions.end(), there
+ * are no substitutions.
+ */
+ context::CDO<SubstitutionMap::iterator> d_lastSubstitutionPos;
+ /**
+ * In incremental settings, substitutions cannot be performed
+ * "backward," only forward. So we need to keep all substitutions
+ * around as assertions. This iterator remembers the last
+ * substitution at the time processAssertions was called. All
+ * substitutions added since then need to be included in the set of
+ * assertions in incremental mode.
+ */
+ context::CDO<SubstitutionMap::iterator> d_lastSubstitutionPosAtEntryToProcessAssertions;
+
static const bool d_doConstantProp = true;
/**
d_modZero(),
d_iteSkolemMap(),
d_iteRemover(smt.d_userContext),
- d_topLevelSubstitutions(smt.d_userContext, true, true)
+ d_topLevelSubstitutions(smt.d_userContext),
+ d_lastSubstitutionPos(smt.d_userContext, d_topLevelSubstitutions.end()),
+ d_lastSubstitutionPosAtEntryToProcessAssertions(smt.d_userContext, d_topLevelSubstitutions.end())
{
d_smt.d_nodeManager->subscribeEvents(this);
}
// No, conflict, go through the literals and solve them
SubstitutionMap constantPropagations(d_smt.d_context);
- SubstitutionMap newSubstitutions(d_smt.d_context, true, true);
- SubstitutionMap::iterator pos;
unsigned j = 0;
for(unsigned i = 0, i_end = d_nonClausalLearnedLiterals.size(); i < i_end; ++ i) {
// Simplify the literal we learned wrt previous substitutions
Node learnedLiteral = d_nonClausalLearnedLiterals[i];
Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
- Assert(d_topLevelSubstitutions.apply(learnedLiteral) == learnedLiteral);
- Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral);
+ Node learnedLiteralNew = d_topLevelSubstitutions.apply(learnedLiteral);
if (learnedLiteral != learnedLiteralNew) {
learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
}
}
}
+ SubstitutionMap::iterator pos = d_lastSubstitutionPos;
+#ifdef CVC4_ASSERTIONS
+ // Check that d_lastSubstitutionPos really points to the last substitution
+ if (pos != d_topLevelSubstitutions.end()) {
+ ++pos;
+ Assert(pos == d_topLevelSubstitutions.end());
+ pos = d_lastSubstitutionPos;
+ }
+#endif
+
// Solve it with the corresponding theory, possibly adding new
- // substitutions to newSubstitutions
+ // substitutions to d_topLevelSubstitutions
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "solving " << learnedLiteral << endl;
-
Theory::PPAssertStatus solveStatus =
- d_smt.d_theoryEngine->solve(learnedLiteral, newSubstitutions);
+ d_smt.d_theoryEngine->solve(learnedLiteral, d_topLevelSubstitutions);
switch (solveStatus) {
case Theory::PP_ASSERT_STATUS_SOLVED: {
+ // Update d_lastSubstitutionPos
+ if (pos == d_topLevelSubstitutions.end()) {
+ pos = d_topLevelSubstitutions.begin();
+ }
+ SubstitutionMap::iterator next = pos;
+ ++next;
+ while (next != d_topLevelSubstitutions.end()) {
+ pos = next;
+ ++next;
+ }
+ d_lastSubstitutionPos = pos;
+
// The literal should rewrite to true
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "solved " << learnedLiteral << endl;
- Assert(Rewriter::rewrite(newSubstitutions.apply(learnedLiteral)).isConst());
+ Assert(Rewriter::rewrite(d_topLevelSubstitutions.apply(learnedLiteral)).isConst());
// vector<pair<Node, Node> > equations;
// constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true);
// if (equations.empty()) {
Assert(!t.isConst());
Assert(constantPropagations.apply(t) == t);
Assert(d_topLevelSubstitutions.apply(t) == t);
- Assert(newSubstitutions.apply(t) == t);
constantPropagations.addSubstitution(t, c);
// vector<pair<Node,Node> > equations;a
// constantPropagations.simplifyLHS(t, c, equations, true);
// 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a
// constant propagation too
// 4. each lhs of constantPropagations is different from each rhs
- for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) {
+ pos = d_topLevelSubstitutions.begin();
+ for (; pos != d_topLevelSubstitutions.end(); ++pos) {
Assert((*pos).first.isVar());
- Assert(d_topLevelSubstitutions.apply((*pos).first) == (*pos).first);
- Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second);
- Assert(newSubstitutions.apply(newSubstitutions.apply((*pos).second)) == newSubstitutions.apply((*pos).second));
+ // Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second);
}
for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
Assert((*pos).second.isConst());
// Resize the learnt
d_nonClausalLearnedLiterals.resize(j);
- // If not in incremental mode, must add substitutions to model
- if( !options::incrementalSolving() &&
- !options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL ) {
- TheoryModel* m = d_smt.d_theoryEngine->getModel();
- if(m != NULL) {
- for(pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) {
- Node n = (*pos).first;
- Node v = newSubstitutions.apply((*pos).second);
- Trace("model") << "Add substitution : " << n << " " << v << endl;
- m->addSubstitution( n, v );
- }
+ //must add substitutions to model
+ TheoryModel* m = d_smt.d_theoryEngine->getModel();
+ if(m != NULL) {
+ for( SubstitutionMap::iterator pos = d_topLevelSubstitutions.begin(); pos != d_topLevelSubstitutions.end(); ++pos) {
+ Node n = (*pos).first;
+ Node v = (*pos).second;
+ Trace("model") << "Add substitution : " << n << " " << v << endl;
+ m->addSubstitution( n, v );
}
}
Trace("debugging") << "NonClausal simplify pre-preprocess\n";
for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
Node assertion = d_assertionsToPreprocess[i];
- Node assertionNew = newSubstitutions.apply(assertion);
+ Node assertionNew = d_topLevelSubstitutions.apply(assertion);
Trace("debugging") << "assertion = " << assertion << endl;
Trace("debugging") << "assertionNew = " << assertionNew << endl;
if (assertion != assertionNew) {
Assert(d_realAssertionsEnd <= d_assertionsToCheck.size());
learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd - 1];
- // If in incremental mode, add substitutions to the list of assertions
if( options::incrementalSolving() ||
options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL ) {
- pos = newSubstitutions.begin();
- for (; pos != newSubstitutions.end(); ++pos) {
+ // Keep substitutions
+ SubstitutionMap::iterator pos = d_lastSubstitutionPosAtEntryToProcessAssertions;
+ if(pos == d_topLevelSubstitutions.end()) {
+ pos = d_topLevelSubstitutions.begin();
+ } else {
+ ++pos;
+ }
+
+ while(pos != d_topLevelSubstitutions.end()) {
// Add back this substitution as an assertion
- TNode lhs = (*pos).first, rhs = newSubstitutions.apply((*pos).second);
+ TNode lhs = (*pos).first, rhs = d_topLevelSubstitutions.apply((*pos).second);
Node n = NodeManager::currentNM()->mkNode(lhs.getType().isBoolean() ? kind::IFF : kind::EQUAL, lhs, rhs);
learnedBuilder << n;
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl;
+ ++pos;
}
}
for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
Node learned = d_nonClausalLearnedLiterals[i];
- Assert(d_topLevelSubstitutions.apply(learned) == learned);
- Node learnedNew = newSubstitutions.apply(learned);
+ Node learnedNew = d_topLevelSubstitutions.apply(learned);
if (learned != learnedNew) {
learned = Rewriter::rewrite(learnedNew);
}
}
d_nonClausalLearnedLiterals.clear();
-
- for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
+ SubstitutionMap::iterator pos = constantPropagations.begin();
+ for (; pos != constantPropagations.end(); ++pos) {
Node cProp = (*pos).first.eqNode((*pos).second);
- Assert(d_topLevelSubstitutions.apply(cProp) == cProp);
- Node cPropNew = newSubstitutions.apply(cProp);
+ Node cPropNew = d_topLevelSubstitutions.apply(cProp);
if (cProp != cPropNew) {
cProp = Rewriter::rewrite(cPropNew);
Assert(Rewriter::rewrite(cProp) == cProp);
<< cProp << endl;
}
- // Add new substitutions to topLevelSubstitutions
- // Note that we don't have to keep rhs's in full solved form
- // because SubstitutionMap::apply does a fixed-point iteration when substituting
- d_topLevelSubstitutions.addSubstitutions(newSubstitutions);
-
if(learnedBuilder.getNumChildren() > 1) {
d_assertionsToCheck[d_realAssertionsEnd - 1] =
Rewriter::rewrite(Node(learnedBuilder));
dumpAssertions("pre-substitution", d_assertionsToPreprocess);
+ // Record current last substitution
+ d_lastSubstitutionPosAtEntryToProcessAssertions = d_lastSubstitutionPos.get();
// Apply the substitutions we already have, and normalize
Chat() << "applying substitutions..." << endl;
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
#include "theory/theory.h"
#include "theory/booleans/theory_bool.h"
#include "theory/booleans/circuit_propagator.h"
-#include "theory/substitutions.h"
#include "theory/valuation.h"
#include "util/boolean_simplification.h"
: node(node), children_added(false) {}
};/* struct substitution_stack_element */
-Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
+Node SubstitutionMap::internalSubstitute(TNode t) {
Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << endl;
Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << endl;
// If node already in the cache we're done, pop from the stack
- NodeCache::iterator find = cache.find(current);
- if (find != cache.end()) {
+ NodeCache::iterator find = d_substitutionCache.find(current);
+ if (find != d_substitutionCache.end()) {
toVisit.pop_back();
continue;
}
if (!d_substituteUnderQuantifiers &&
(current.getKind() == kind::FORALL || current.getKind() == kind::EXISTS)) {
Debug("substitution::internal") << "--not substituting under quantifier" << endl;
- cache[current] = current;
+ d_substitutionCache[current] = current;
toVisit.pop_back();
continue;
}
if (find2 != d_substitutions.end()) {
Node rhs = (*find2).second;
Assert(rhs != current);
- internalSubstitute(rhs, cache);
- d_substitutions[current] = cache[rhs];
- cache[current] = cache[rhs];
+ internalSubstitute(rhs);
+ d_substitutions[current] = d_substitutionCache[rhs];
+ d_substitutionCache[current] = d_substitutionCache[rhs];
toVisit.pop_back();
continue;
}
// Children have been processed, so substitute
NodeBuilder<> builder(current.getKind());
if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
- builder << Node(cache[current.getOperator()]);
+ builder << Node(d_substitutionCache[current.getOperator()]);
}
for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
- Assert(cache.find(current[i]) != cache.end());
- builder << Node(cache[current[i]]);
+ Assert(d_substitutionCache.find(current[i]) != d_substitutionCache.end());
+ builder << Node(d_substitutionCache[current[i]]);
}
// Mark the substitution and continue
Node result = builder;
if (result != current) {
- find = cache.find(result);
- if (find != cache.end()) {
+ find = d_substitutionCache.find(result);
+ if (find != d_substitutionCache.end()) {
result = find->second;
}
else {
if (find2 != d_substitutions.end()) {
Node rhs = (*find2).second;
Assert(rhs != result);
- internalSubstitute(rhs, cache);
- d_substitutions[result] = cache[rhs];
- cache[result] = cache[rhs];
- result = cache[rhs];
+ internalSubstitute(rhs);
+ d_substitutions[result] = d_substitutionCache[rhs];
+ d_substitutionCache[result] = d_substitutionCache[rhs];
+ result = d_substitutionCache[rhs];
}
}
}
Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl;
- cache[current] = result;
+ d_substitutionCache[current] = result;
toVisit.pop_back();
} else {
// Mark that we have added the children if any
// We need to add the operator, if any
if(current.getMetaKind() == kind::metakind::PARAMETERIZED) {
TNode opNode = current.getOperator();
- NodeCache::iterator opFind = cache.find(opNode);
- if (opFind == cache.end()) {
+ NodeCache::iterator opFind = d_substitutionCache.find(opNode);
+ if (opFind == d_substitutionCache.end()) {
toVisit.push_back(opNode);
}
}
// We need to add the children
for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
TNode childNode = *child_it;
- NodeCache::iterator childFind = cache.find(childNode);
- if (childFind == cache.end()) {
+ NodeCache::iterator childFind = d_substitutionCache.find(childNode);
+ if (childFind == d_substitutionCache.end()) {
toVisit.push_back(childNode);
}
}
} else {
// No children, so we're done
Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << endl;
- cache[current] = current;
+ d_substitutionCache[current] = current;
toVisit.pop_back();
}
}
}
// Return the substituted version
- return cache[t];
+ return d_substitutionCache[t];
}/* SubstitutionMap::internalSubstitute() */
+ /*
void SubstitutionMap::simplifyRHS(const SubstitutionMap& subMap)
{
// Put the new substitutions into the old ones
tempCache[x] = t;
// Put the new substitution into the old ones
- NodeMap::iterator it = d_substitutions.begin();
- NodeMap::iterator it_end = d_substitutions.end();
+ NodeMap::iterator it = d_substitutionsOld.begin();
+ NodeMap::iterator it_end = d_substitutionsOld.end();
for(; it != it_end; ++ it) {
- d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache);
+ d_substitutionsOld[(*it).first] = internalSubstituteOld((*it).second, tempCache);
}
// it = d_substitutionsLazy.begin();
// it_end = d_substitutionsLazy.end();
// d_substitutionsLazy[(*it).first] = internalSubstitute((*it).second, tempCache);
// }
}
-
+*/
/* We use subMap to simplify the left-hand sides of the current substitution map. If rewrite is true,
* we also apply the rewriter to the result.
}
}
-
-void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateCache)
-{
- SubstitutionMap::NodeMap::const_iterator it = subMap.begin();
- SubstitutionMap::NodeMap::const_iterator it_end = subMap.end();
- for (; it != it_end; ++ it) {
- Assert(d_substitutions.find((*it).first) == d_substitutions.end());
- d_substitutions[(*it).first] = (*it).second;
- if (!invalidateCache) {
- d_substitutionCache[(*it).first] = d_substitutions[(*it).first];
- }
- }
- if (invalidateCache) {
- d_cacheInvalidated = true;
- }
-}
-
-
static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
}
// Perform the substitution
- Node result = internalSubstitute(t, d_substitutionCache);
+ Node result = internalSubstitute(t);
Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl;
// Assert(check(result, d_substitutions));
/** Has the cache been invalidated? */
bool d_cacheInvalidated;
- /** Whether to keep substitutions in solved form */
- bool d_solvedForm;
-
/** Internal method that performs substitution */
- Node internalSubstitute(TNode t, NodeCache& cache);
+ Node internalSubstitute(TNode t);
/** Helper class to invalidate cache on user pop */
class CacheInvalidator : public context::ContextNotifyObj {
public:
- SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true, bool solvedForm = false) :
+ SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true) :
d_context(context),
d_substitutions(context),
d_substitutionCache(),
d_substituteUnderQuantifiers(substituteUnderQuantifiers),
d_cacheInvalidated(false),
- d_solvedForm(solvedForm),
- d_cacheInvalidator(context, d_cacheInvalidated)
- {
+ d_cacheInvalidator(context, d_cacheInvalidated) {
}
/**
*/
void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
- /**
- * Merge subMap into current set of substitutions
- */
- void addSubstitutions(SubstitutionMap& subMap, bool invalidateCache = true);
-
/**
* Returns true iff x is in the substitution map
*/
// should best interact with cache invalidation on context
// pops.
+ /*
// Simplify right-hand sides of current map using the given substitutions
void simplifyRHS(const SubstitutionMap& subMap);
// Simplify right-hand sides of current map with lhs -> rhs
void simplifyRHS(TNode lhs, TNode rhs);
- /*
// Simplify left-hand sides of current map using the given substitutions
void simplifyLHS(const SubstitutionMap& subMap,
std::vector<std::pair<Node,Node> >& equalities,
bool rewrite = true);
*/
- bool isSolvedForm() const { return d_solvedForm; }
-
/**
* Print to the output stream
*/
#include "theory/theory.h"
#include "util/cvc4_assert.h"
#include "theory/quantifiers_engine.h"
-#include "theory/substitutions.h"
#include <vector>
}
-Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstitutions)
-{
- if (in.getKind() == kind::EQUAL) {
- if (in[0].isVar() && !in[1].hasSubterm(in[0])) {
- outSubstitutions.addSubstitution(in[0], in[1]);
- return PP_ASSERT_STATUS_SOLVED;
- }
- if (in[1].isVar() && !in[0].hasSubterm(in[1])) {
- outSubstitutions.addSubstitution(in[1], in[0]);
- return PP_ASSERT_STATUS_SOLVED;
- }
- if (in[0].isConst() && in[1].isConst()) {
- if (in[0] != in[1]) {
- return PP_ASSERT_STATUS_CONFLICT;
- }
- }
- }
-
- return PP_ASSERT_STATUS_UNSOLVED;
-}
-
-
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#include "expr/attribute.h"
#include "expr/command.h"
#include "theory/valuation.h"
+#include "theory/substitutions.h"
#include "theory/output_channel.h"
#include "theory/logic_info.h"
#include "theory/options.h"
namespace theory {
class QuantifiersEngine;
-class SubstitutionMap;
class TheoryModel;
namespace rrinst {
* Given a literal, add the solved substitutions to the map, if any.
* The method should return true if the literal can be safely removed.
*/
- virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+ virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+ if (in.getKind() == kind::EQUAL) {
+ if (in[0].isVar() && !in[1].hasSubterm(in[0])) {
+ outSubstitutions.addSubstitution(in[0], in[1]);
+ return PP_ASSERT_STATUS_SOLVED;
+ }
+ if (in[1].isVar() && !in[0].hasSubterm(in[1])) {
+ outSubstitutions.addSubstitution(in[1], in[0]);
+ return PP_ASSERT_STATUS_SOLVED;
+ }
+ if (in[0].isConst() && in[1].isConst()) {
+ if (in[0] != in[1]) {
+ return PP_ASSERT_STATUS_CONFLICT;
+ }
+ }
+ }
+
+ return PP_ASSERT_STATUS_UNSOLVED;
+ }
/**
* Given an atom of the theory coming from the input formula, this
#define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H
#include "theory/rewriter.h"
-#include "theory/substitutions.h"
namespace CVC4 {
namespace theory {
projects / cvc5.git / commitdiff