diff options
Diffstat (limited to 'src/theory/uf/equality_engine.h')
| -rw-r--r-- | src/theory/uf/equality_engine.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 7314b6552..d8757926a 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -632,6 +632,11 @@ public: TNode getRepresentative(TNode t) const; /** + * Add all the terms where the given term appears in (directly or implicitly). + */ + void getUseListTerms(TNode t, std::set<TNode>& output); + + /** * Returns true if the two nodes are in the same class. */ bool areEqual(TNode t1, TNode t2) const; @@ -663,6 +668,11 @@ public: bool isTriggerTerm(TNode t) const; /** + * Returns the representative trigger term (isTriggerTerm(t)) should be true. + */ + TNode getTriggerTermRepresentative(TNode t) const; + + /** * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with * trigger. */ |