Fixed a performance issue with unconstrained simplifier

1 files changed, 10 insertions, 2 deletions

diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 711ff9b72..c32dee635 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -102,9 +102,17 @@ public:
   }
 
   /**
-   * Adds a substitution from x to t
+   * 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.
    */
-  void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
+  void addSubstitution(TNode x, TNode t,
+                       bool invalidateCache = true,
+                       bool backSub = true,
+                       bool forwardSub = false);
 
   /**
    * Returns true iff x is in the substitution map