summaryrefslogtreecommitdiff
path: root/src/theory/uf/equality_engine.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-04-14 11:42:00 -0500
committerGitHub <noreply@github.com>2020-04-14 11:42:00 -0500
commitcf8d103b11261d3b4425dab74008dffd903b8121 (patch)
treef67178350d92861520913ae7556bc8fc38c8b392 /src/theory/uf/equality_engine.h
parentad8729d3a0060ed635b8a82e9ed323966cc2f49d (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.h5
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback