From 3734cc671ab37fd43eb7a5a1dbc1ab0f28ba14fb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Nov 2015 19:10:00 -0800 Subject: [PATCH] feat(library/blast/congruence_closure): add is_eqv --- src/library/blast/congruence_closure.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/library/blast/congruence_closure.cpp b/src/library/blast/congruence_closure.cpp index bd9125a04..06238f76a 100644 --- a/src/library/blast/congruence_closure.cpp +++ b/src/library/blast/congruence_closure.cpp @@ -264,11 +264,14 @@ void congruence_closure::add(hypothesis_idx hidx) { } bool congruence_closure::is_eqv(name const & R, expr const & e1, expr const & e2) const { - // TODO(Leo): - return false; + auto n1 = m_entries.find(eqc_key(R, e1)); + if (!n1) return false; + auto n2 = m_entries.find(eqc_key(R, e2)); + if (!n2) return false; + return n1->m_root == n2->m_root; } -optional congruence_closure::get_eqv_proof(name const & rel_name, expr const & e1, expr const & e2) const { +optional congruence_closure::get_eqv_proof(name const & R, expr const & e1, expr const & e2) const { // TODO(Leo): return none_expr(); }