From b849eeef09465da1100cd6a94beacc893849fb25 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Thu, 14 Jun 2012 19:37:31 +0000 Subject: New substitutions implementation - fixes performance issue seen in nonclausal simplification for some benchmarks --- src/theory/substitutions.h | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) (limited to 'src/theory/substitutions.h') diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 32ed35074..cf751b69e 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -68,7 +68,7 @@ private: bool d_cacheInvalidated; /** Internal method that performs substitution */ - Node internalSubstitute(TNode t, NodeCache& substitutionCache); + Node internalSubstitute(TNode t); /** Helper class to invalidate cache on user pop */ class CacheInvalidator : public context::ContextNotifyObj { @@ -92,8 +92,8 @@ private: CacheInvalidator d_cacheInvalidator; // Helper list and method for simplifyLHS methods - std::vector > d_worklist; - void processWorklist(std::vector >& equalities, bool rewrite); + // std::vector > d_worklist; + // void processWorklist(std::vector >& equalities, bool rewrite); public: @@ -106,17 +106,10 @@ public: } /** - * Adds a substitution from x to t. Typically you also want to apply this - * substitution to the existing set (backSub), but you do not need to - * apply the existing set to the new substitution (forwardSub). However, - * the method allows you to do either. Probably you should not do both, - * as it will be very difficult to maintain the invariant that no - * left-hand side appears on any right-hand side. + * Adds a substitution from x to t. */ void addSubstitution(TNode x, TNode t, - bool invalidateCache = true, - bool backSub = true, - bool forwardSub = false); + bool invalidateCache = true); /** * Returns true iff x is in the substitution map @@ -162,6 +155,7 @@ 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); @@ -177,6 +171,7 @@ public: void simplifyLHS(TNode lhs, TNode rhs, std::vector >& equalities, bool rewrite = true); + */ /** * Print to the output stream -- cgit v1.2.3