diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-09 00:22:33 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-09 00:22:33 +0000 |
commit | 4a266eaff4301b26383a1b667265055c9d4ce797 (patch) | |
tree | 18916e061e74423afc3b0ebe3f2ca3c2c2434280 /src/theory | |
parent | e256e63588a867b9ea82e03cfc684c2ea2ca1738 (diff) |
adding mergePredicates method to the equality engine to be able to
assert equalities betweeen predicates
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 8 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 5 |
2 files changed, 13 insertions, 0 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 6cef3dff5..97dcbad86 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -353,6 +353,14 @@ void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason) { propagate(); } +void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) { + Debug("equality") << d_name << "::eq::mergePredicats(" << p << "," << q << ")" << std::endl; + Assert(p.getKind() != kind::EQUAL, "Use assertEquality instead"); + Assert(q.getKind() != kind::EQUAL, "Use assertEquality instead"); + assertEqualityInternal(p, q, reason); + propagate(); +} + void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) { 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 e32a34707..5d5e0f1f3 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -697,6 +697,11 @@ public: void assertPredicate(TNode p, bool polarity, TNode reason); /** + * 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 |