From: Morgan Deters Date: Mon, 23 Sep 2013 23:56:01 +0000 (-0400) Subject: Revert Clark's last commit, at his request; there are some bugs. X-Git-Tag: cvc5-1.0.0~7287^2~6 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5d1f359e22927f2bec78ba6a407485f65bc6ae0b;p=cvc5.git Revert Clark's last commit, at his request; there are some bugs. This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a5effc1e8..91eae8915 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -307,6 +307,23 @@ private: /** 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 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 d_lastSubstitutionPosAtEntryToProcessAssertions; + static const bool d_doConstantProp = true; /** @@ -390,7 +407,9 @@ public: 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); } @@ -1726,15 +1745,12 @@ bool SmtEnginePrivate::nonClausalSimplify() { // 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); } @@ -1763,20 +1779,41 @@ bool SmtEnginePrivate::nonClausalSimplify() { } } + 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 > equations; // constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true); // if (equations.empty()) { @@ -1811,7 +1848,6 @@ bool SmtEnginePrivate::nonClausalSimplify() { Assert(!t.isConst()); Assert(constantPropagations.apply(t) == t); Assert(d_topLevelSubstitutions.apply(t) == t); - Assert(newSubstitutions.apply(t) == t); constantPropagations.addSubstitution(t, c); // vector > equations;a // constantPropagations.simplifyLHS(t, c, equations, true); @@ -1837,11 +1873,10 @@ bool SmtEnginePrivate::nonClausalSimplify() { // 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()); @@ -1865,17 +1900,14 @@ bool SmtEnginePrivate::nonClausalSimplify() { // 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 ); } } @@ -1883,7 +1915,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { 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) { @@ -1914,23 +1946,29 @@ bool SmtEnginePrivate::nonClausalSimplify() { 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); } @@ -1954,11 +1992,10 @@ bool SmtEnginePrivate::nonClausalSimplify() { } 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); @@ -1973,11 +2010,6 @@ bool SmtEnginePrivate::nonClausalSimplify() { << 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)); @@ -2807,6 +2839,8 @@ void SmtEnginePrivate::processAssertions() { 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(): " diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 87aadf3f0..3e75dd258 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -17,7 +17,6 @@ #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" diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index c4f06e396..c12129d01 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -29,7 +29,7 @@ struct substitution_stack_element { : 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; @@ -50,8 +50,8 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { 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; } @@ -59,7 +59,7 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { 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; } @@ -68,9 +68,9 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { 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; } @@ -80,17 +80,17 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { // 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 { @@ -98,15 +98,15 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { 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 @@ -115,33 +115,34 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { // 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 @@ -159,10 +160,10 @@ void SubstitutionMap::simplifyRHS(TNode x, TNode t) { 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(); @@ -170,7 +171,7 @@ void SubstitutionMap::simplifyRHS(TNode x, TNode t) { // 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. @@ -282,24 +283,6 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) } } - -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(); @@ -328,7 +311,7 @@ Node SubstitutionMap::apply(TNode t) { } // 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)); diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 5a478a250..bde7dfdbc 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -68,11 +68,8 @@ private: /** 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 { @@ -101,15 +98,13 @@ private: 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) { } /** @@ -117,11 +112,6 @@ public: */ 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 */ @@ -180,13 +170,13 @@ public: // 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 >& equalities, @@ -198,8 +188,6 @@ public: bool rewrite = true); */ - bool isSolvedForm() const { return d_solvedForm; } - /** * Print to the output stream */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 9a23d5518..a1a835170 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -17,7 +17,6 @@ #include "theory/theory.h" #include "util/cvc4_assert.h" #include "theory/quantifiers_engine.h" -#include "theory/substitutions.h" #include @@ -207,27 +206,5 @@ void Theory::computeRelevantTerms(set& termSet) } -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 */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 94afdb1d0..d1734674d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -23,6 +23,7 @@ #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" @@ -48,7 +49,6 @@ class TheoryEngine; namespace theory { class QuantifiersEngine; -class SubstitutionMap; class TheoryModel; namespace rrinst { @@ -576,7 +576,25 @@ public: * 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 diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 40713fa41..94ab47d23 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -21,7 +21,6 @@ #define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H #include "theory/rewriter.h" -#include "theory/substitutions.h" namespace CVC4 { namespace theory {