diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-05 19:48:30 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-05 19:48:30 +0000 |
commit | f5ce374d107882e4385f8b0deed3ef1129f49c79 (patch) | |
tree | 293f9fd11581677561e743322bd0743b9d0c4c23 /src/theory/substitutions.h | |
parent | dd0ca308c3299155bfab89ade6cfd0a70b9abda5 (diff) |
Fixed a performance issue with unconstrained simplifier
Diffstat (limited to 'src/theory/substitutions.h')
-rw-r--r-- | src/theory/substitutions.h | 12 |
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 |