From: Kshitij Bansal Date: Fri, 28 Mar 2014 22:33:38 +0000 (-0400) Subject: rm old unused code X-Git-Tag: cvc5-1.0.0~6993^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=feef8c2243734f8e6703164ee4d9a5980b7b1eb6;p=cvc5.git rm old unused code --- diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index c4f06e396..9b9fc56d7 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -172,96 +172,6 @@ void SubstitutionMap::simplifyRHS(TNode x, TNode t) { } -/* 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. - * We want to maintain the invariant that all lhs are distinct from each other and from all rhs. - * If for some l -> r, l reduces to l', we try to add a new rule l' -> r. There are two cases - * where this fails - * (i) if l' is equal to some ll (in a rule ll -> rr), then if r != rr we add (r,rr) to the equation list - * (i) if l' is equalto some rr (in a rule ll -> rr), then if r != rr we add (r,rr) to the equation list - */ -/* -void SubstitutionMap::simplifyLHS(const SubstitutionMap& subMap, vector >& equalities, bool rewrite) -{ - Assert(d_worklist.empty()); - // First, apply subMap to every LHS in d_substitutions - NodeMap::iterator it = d_substitutions.begin(); - NodeMap::iterator it_end = d_substitutions.end(); - Node newLeft; - for(; it != it_end; ++ it) { - newLeft = subMap.apply((*it).first); - if (newLeft != (*it).first) { - if (rewrite) { - newLeft = Rewriter::rewrite(newLeft); - } - d_worklist.push_back(pair(newLeft, (*it).second)); - } - } - processWorklist(equalities, rewrite); - Assert(d_worklist.empty()); -} - - -void SubstitutionMap::simplifyLHS(TNode lhs, TNode rhs, vector >& equalities, bool rewrite) -{ - Assert(d_worklist.empty()); - d_worklist.push_back(pair(lhs,rhs)); - processWorklist(equalities, rewrite); - Assert(d_worklist.empty()); -} - - -void SubstitutionMap::processWorklist(vector >& equalities, bool rewrite) -{ - // Add each new rewrite rule, taking care not to invalidate invariants and looking - // for any new rewrite rules we can learn - Node newLeft, newRight; - while (!d_worklist.empty()) { - newLeft = d_worklist.back().first; - newRight = d_worklist.back().second; - d_worklist.pop_back(); - - NodeCache tempCache; - tempCache[newLeft] = newRight; - - Node newLeft2; - unsigned size = d_worklist.size(); - bool addThisRewrite = true; - NodeMap::iterator it = d_substitutions.begin(); - NodeMap::iterator it_end = d_substitutions.end(); - - for(; it != it_end; ++ it) { - - // Check for invariant violation. If new rewrite is redundant, do nothing - // Otherwise, add an equality to the output equalities - // In either case undo any work done by this rewrite - if (newLeft == (*it).first || newLeft == (*it).second) { - if ((*it).second != newRight) { - equalities.push_back(pair((*it).second, newRight)); - } - while (d_worklist.size() > size) { - d_worklist.pop_back(); - } - addThisRewrite = false; - break; - } - - newLeft2 = internalSubstituteOld((*it).first, tempCache); - if (newLeft2 != (*it).first) { - if (rewrite) { - newLeft2 = Rewriter::rewrite(newLeft2); - } - d_worklist.push_back(pair(newLeft2, (*it).second)); - } - } - if (addThisRewrite) { - d_substitutions[newLeft] = newRight; - d_cacheInvalidated = true; - } - } -} -*/ - void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) { Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << endl; diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 5a478a250..8572a6abd 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -95,10 +95,6 @@ private: */ CacheInvalidator d_cacheInvalidator; - // Helper list and method for simplifyLHS methods - // std::vector > d_worklist; - // void processWorklist(std::vector >& equalities, bool rewrite); - public: SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true, bool solvedForm = false) : @@ -186,18 +182,6 @@ public: // 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, - bool rewrite = true); - - // Simplify left-hand sides of current map with lhs -> rhs and then add lhs -> rhs to the substitutions set - void simplifyLHS(TNode lhs, TNode rhs, - std::vector >& equalities, - bool rewrite = true); - */ - bool isSolvedForm() const { return d_solvedForm; } /**