Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.h

for faster compilation

1 files changed, 16 insertions, 4 deletions

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)
+    {
   }
 
   /**
@@ -113,6 +118,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
    */
   bool hasSubstitution(TNode x) const {
@@ -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<std::pair<Node,Node> >& equalities,
@@ -188,6 +198,8 @@ public:
                    bool rewrite = true);
   */
 
+  bool isSolvedForm() const { return d_solvedForm; }
+
   /**
    * Print to the output stream
    */