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/theory_model.cpp | |
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/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index dae7261e5..e96bee410 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -483,8 +483,10 @@ bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, first = false; } else { - Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl; - d_equalityEngine->mergePredicates(*eqc_i, rep, Node::null()); + Node eq = (*eqc_i).eqNode(rep); + Trace("model-builder-assertions") + << "(assert " << eq << ");" << std::endl; + d_equalityEngine->assertEquality(eq, true, Node::null()); if (!d_equalityEngine->consistent()) { return false; |