From 4a266eaff4301b26383a1b667265055c9d4ce797 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Tue, 9 Oct 2012 00:22:33 +0000 Subject: [PATCH] adding mergePredicates method to the equality engine to be able to assert equalities betweeen predicates --- src/theory/uf/equality_engine.cpp | 8 ++++++++ src/theory/uf/equality_engine.h | 5 +++++ 2 files changed, 13 insertions(+) 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 @@ -696,6 +696,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. * -- 2.30.2