michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/blast/congruence_closure): add is_eqv

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-17 19:10:00 -08:00
parent d833410f0d
commit 3734cc671a
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/blast/congruence_closure.cpp
View file

@ -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<expr> congruence_closure::get_eqv_proof(name const & rel_name, expr const & e1, expr const & e2) const {
optional<expr> congruence_closure::get_eqv_proof(name const & R, expr const & e1, expr const & e2) const {
// TODO(Leo):
return none_expr();
}