diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-14 11:42:00 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-14 11:42:00 -0500 |
commit | cf8d103b11261d3b4425dab74008dffd903b8121 (patch) | |
tree | f67178350d92861520913ae7556bc8fc38c8b392 /src/theory/uf/equality_engine.h | |
parent | ad8729d3a0060ed635b8a82e9ed323966cc2f49d (diff) |
Remove mergePredicates from EqualityEngine interface (#4305)
This function was equivalent to asserting an equality. Removing it for the sake of simplicity.
Diffstat (limited to 'src/theory/uf/equality_engine.h')
-rw-r--r-- | src/theory/uf/equality_engine.h | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 041625568..0ae95b34a 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -804,11 +804,6 @@ public: void assertPredicate(TNode p, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY); /** - * Adds predicate p and q and makes them equal. - */ - void mergePredicates(TNode p, TNode q, TNode reason); - - /** * Adds an equality eq with the given polarity to the database. * * @param eq the (non-negated) equality |