From ccd1ca4c32e8a3eac8b18911a7b2d32b55203707 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Tue, 24 Sep 2013 16:56:06 -0700 Subject: [PATCH] Reduce compiler dependencies on substitutions.h, Some new functionality in substitutions.h/cpp --- src/theory/arith/arith_static_learner.h | 1 - src/theory/booleans/theory_bool.cpp | 1 + src/theory/bv/bv_subtheory_bitblast.h | 1 - src/theory/ite_simplifier.h | 2 - src/theory/substitutions.cpp | 75 +++++++++++++++---------- src/theory/substitutions.h | 20 +++++-- src/theory/theory.cpp | 23 ++++++++ src/theory/theory.h | 22 +------- src/theory/theory_engine.h | 1 - src/theory/uf/theory_uf_rewriter.h | 1 + 10 files changed, 89 insertions(+), 58 deletions(-) diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index c4bf92a16..d8407eeba 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -23,7 +23,6 @@ #include "util/statistics_registry.h" #include "theory/arith/arith_utilities.h" -#include "theory/substitutions.h" #include "context/context.h" #include "context/cdlist.h" diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 3e75dd258..895f4a279 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -19,6 +19,7 @@ #include "theory/booleans/circuit_propagator.h" #include "theory/valuation.h" #include "util/boolean_simplification.h" +#include "theory/substitutions.h" #include #include diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 71e80238d..f1204dbdf 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -19,7 +19,6 @@ #pragma once #include "theory/bv/bv_subtheory.h" -#include "theory/substitutions.h" namespace CVC4 { namespace theory { namespace bv { diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h index 2329cd970..07fa0dedb 100644 --- a/src/theory/ite_simplifier.h +++ b/src/theory/ite_simplifier.h @@ -31,9 +31,7 @@ #include "prop/prop_engine.h" #include "context/cdhashset.h" #include "theory/theory.h" -#include "theory/substitutions.h" #include "theory/rewriter.h" -#include "theory/substitutions.h" #include "theory/shared_terms_database.h" #include "theory/term_registration_visitor.h" #include "theory/valuation.h" diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index c12129d01..c4f06e396 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) { +Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << endl; @@ -50,8 +50,8 @@ Node SubstitutionMap::internalSubstitute(TNode t) { 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 = d_substitutionCache.find(current); - if (find != d_substitutionCache.end()) { + NodeCache::iterator find = cache.find(current); + if (find != cache.end()) { toVisit.pop_back(); continue; } @@ -59,7 +59,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) { if (!d_substituteUnderQuantifiers && (current.getKind() == kind::FORALL || current.getKind() == kind::EXISTS)) { Debug("substitution::internal") << "--not substituting under quantifier" << endl; - d_substitutionCache[current] = current; + cache[current] = current; toVisit.pop_back(); continue; } @@ -68,9 +68,9 @@ Node SubstitutionMap::internalSubstitute(TNode t) { if (find2 != d_substitutions.end()) { Node rhs = (*find2).second; Assert(rhs != current); - internalSubstitute(rhs); - d_substitutions[current] = d_substitutionCache[rhs]; - d_substitutionCache[current] = d_substitutionCache[rhs]; + internalSubstitute(rhs, cache); + d_substitutions[current] = cache[rhs]; + cache[current] = cache[rhs]; toVisit.pop_back(); continue; } @@ -80,17 +80,17 @@ Node SubstitutionMap::internalSubstitute(TNode t) { // Children have been processed, so substitute NodeBuilder<> builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << Node(d_substitutionCache[current.getOperator()]); + builder << Node(cache[current.getOperator()]); } for (unsigned i = 0; i < current.getNumChildren(); ++ i) { - Assert(d_substitutionCache.find(current[i]) != d_substitutionCache.end()); - builder << Node(d_substitutionCache[current[i]]); + Assert(cache.find(current[i]) != cache.end()); + builder << Node(cache[current[i]]); } // Mark the substitution and continue Node result = builder; if (result != current) { - find = d_substitutionCache.find(result); - if (find != d_substitutionCache.end()) { + find = cache.find(result); + if (find != cache.end()) { result = find->second; } else { @@ -98,15 +98,15 @@ Node SubstitutionMap::internalSubstitute(TNode t) { if (find2 != d_substitutions.end()) { Node rhs = (*find2).second; Assert(rhs != result); - internalSubstitute(rhs); - d_substitutions[result] = d_substitutionCache[rhs]; - d_substitutionCache[result] = d_substitutionCache[rhs]; - result = d_substitutionCache[rhs]; + internalSubstitute(rhs, cache); + d_substitutions[result] = cache[rhs]; + cache[result] = cache[rhs]; + result = cache[rhs]; } } } Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl; - d_substitutionCache[current] = result; + cache[current] = result; toVisit.pop_back(); } else { // Mark that we have added the children if any @@ -115,34 +115,33 @@ Node SubstitutionMap::internalSubstitute(TNode t) { // We need to add the operator, if any if(current.getMetaKind() == kind::metakind::PARAMETERIZED) { TNode opNode = current.getOperator(); - NodeCache::iterator opFind = d_substitutionCache.find(opNode); - if (opFind == d_substitutionCache.end()) { + NodeCache::iterator opFind = cache.find(opNode); + if (opFind == cache.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 = d_substitutionCache.find(childNode); - if (childFind == d_substitutionCache.end()) { + NodeCache::iterator childFind = cache.find(childNode); + if (childFind == cache.end()) { toVisit.push_back(childNode); } } } else { // No children, so we're done Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << endl; - d_substitutionCache[current] = current; + cache[current] = current; toVisit.pop_back(); } } } // Return the substituted version - return d_substitutionCache[t]; + return cache[t]; }/* SubstitutionMap::internalSubstitute() */ - /* void SubstitutionMap::simplifyRHS(const SubstitutionMap& subMap) { // Put the new substitutions into the old ones @@ -160,10 +159,10 @@ void SubstitutionMap::simplifyRHS(TNode x, TNode t) { tempCache[x] = t; // Put the new substitution into the old ones - NodeMap::iterator it = d_substitutionsOld.begin(); - NodeMap::iterator it_end = d_substitutionsOld.end(); + NodeMap::iterator it = d_substitutions.begin(); + NodeMap::iterator it_end = d_substitutions.end(); for(; it != it_end; ++ it) { - d_substitutionsOld[(*it).first] = internalSubstituteOld((*it).second, tempCache); + d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache); } // it = d_substitutionsLazy.begin(); // it_end = d_substitutionsLazy.end(); @@ -171,7 +170,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. @@ -283,6 +282,24 @@ 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(); @@ -311,7 +328,7 @@ Node SubstitutionMap::apply(TNode t) { } // Perform the substitution - Node result = internalSubstitute(t); + Node result = internalSubstitute(t, d_substitutionCache); 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 bde7dfdbc..5a478a250 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -68,8 +68,11 @@ 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); + Node internalSubstitute(TNode t, NodeCache& cache); /** Helper class to invalidate cache on user pop */ class CacheInvalidator : public context::ContextNotifyObj { @@ -98,13 +101,15 @@ private: public: - SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true) : + SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true, bool solvedForm = false) : d_context(context), d_substitutions(context), d_substitutionCache(), d_substituteUnderQuantifiers(substituteUnderQuantifiers), d_cacheInvalidated(false), - d_cacheInvalidator(context, d_cacheInvalidated) { + d_solvedForm(solvedForm), + d_cacheInvalidator(context, d_cacheInvalidated) + { } /** @@ -112,6 +117,11 @@ 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 */ @@ -170,13 +180,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, @@ -188,6 +198,8 @@ 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 a1a835170..9a23d5518 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -17,6 +17,7 @@ #include "theory/theory.h" #include "util/cvc4_assert.h" #include "theory/quantifiers_engine.h" +#include "theory/substitutions.h" #include @@ -206,5 +207,27 @@ 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 d1734674d..21a5aacf5 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -23,7 +23,6 @@ #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" @@ -50,6 +49,7 @@ namespace theory { class QuantifiersEngine; class TheoryModel; +class SubstitutionMap; namespace rrinst { class CandidateGenerator; @@ -576,25 +576,7 @@ 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) { - 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; - } + virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); /** * Given an atom of the theory coming from the input formula, this diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index fcbec2a41..53ff4d167 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -28,7 +28,6 @@ #include "prop/prop_engine.h" #include "context/cdhashset.h" #include "theory/theory.h" -#include "theory/substitutions.h" #include "theory/rewriter.h" #include "theory/substitutions.h" #include "theory/shared_terms_database.h" diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 94ab47d23..40713fa41 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -21,6 +21,7 @@ #define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H #include "theory/rewriter.h" +#include "theory/substitutions.h" namespace CVC4 { namespace theory { -- 2.30.2