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 | |
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')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 6 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 5 |
2 files changed, 0 insertions, 11 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index b6896e45d..e3d002138 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -449,12 +449,6 @@ void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsig propagate(); } -void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) { - Debug("equality") << d_name << "::eq::mergePredicates(" << p << "," << q << ")" << std::endl; - assertEqualityInternal(p, q, reason); - propagate(); -} - void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) { Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl; if (polarity) { 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 |