diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-23 19:56:01 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-23 19:57:59 -0400 |
commit | 5d1f359e22927f2bec78ba6a407485f65bc6ae0b (patch) | |
tree | 6054d3a41eaeae7709581b86ae8aabdaccd258c9 /src/theory | |
parent | 9775bced75843c6f01e9524c2d0e7021535e3ec0 (diff) |
Revert Clark's last commit, at his request; there are some bugs.
This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 1 | ||||
-rw-r--r-- | src/theory/substitutions.cpp | 75 | ||||
-rw-r--r-- | src/theory/substitutions.h | 20 | ||||
-rw-r--r-- | src/theory/theory.cpp | 23 | ||||
-rw-r--r-- | src/theory/theory.h | 22 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 1 |
6 files changed, 53 insertions, 89 deletions
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) { } /** @@ -118,11 +113,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 */ bool hasSubstitution(TNode x) const { @@ -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<std::pair<Node,Node> >& 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 <vector> @@ -207,27 +206,5 @@ void Theory::computeRelevantTerms(set<Node>& 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 { |