diff options
Diffstat (limited to 'src/theory/uf/equality_engine.h')
| -rw-r--r-- | src/theory/uf/equality_engine.h | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 13b8898d5..01ae6bfb4 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -613,9 +613,16 @@ public: /** * Get an explanation of the equality t1 = t2. Returns the asserted equalities that * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere - * else. TODO: mark the phantom equalities (skolems). + * else. + */ + void explainEquality(TNode t1, TNode t2, std::vector<TNode>& equalities) const; + + /** + * Get an explanation of the equality t1 = t2. Returns the asserted equalities that + * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere + * else. */ - void getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const; + void explainDisequality(TNode t1, TNode t2, std::vector<TNode>& equalities) const; /** * Add term to the trigger terms. The notify class will get notified when two |