Adding constant propagation code - needs more testing - off by default

1 files changed, 21 insertions, 0 deletions

diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index ee2a15f6f..32ed35074 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -91,6 +91,10 @@ private:
    */
   CacheInvalidator d_cacheInvalidator;
 
+  // Helper list and method for simplifyLHS methods
+  std::vector<std::pair<Node, Node> > d_worklist;
+  void processWorklist(std::vector<std::pair<Node, Node> >& equalities, bool rewrite);
+
 public:
 
   SubstitutionMap(context::Context* context) :
@@ -158,10 +162,27 @@ 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,
+                   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<std::pair<Node,Node> >& equalities,
+                   bool rewrite = true);
+
   /**
    * Print to the output stream
    */
   void print(std::ostream& out) const;
+  void debugPrint() const;
 
 };/* class SubstitutionMap */