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

fix(library/blast/congruence_closure): bug in congruence closure proof extraction

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-30 10:37:44 -07:00
parent 5844e96734
commit a8bb4ba109
3 changed files with 21 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -654,20 +654,20 @@ void congruence_closure::internalize(expr const & e) {
This method "inverts" the proof. That is, the m_target goes from root(e) to e after This method "inverts" the proof. That is, the m_target goes from root(e) to e after
we execute it. we execute it.
*/ */
void congruence_closure::invert_trans(name const & R, expr const & e, optional<expr> new_target, optional<expr> new_proof) { void congruence_closure::invert_trans(name const & R, expr const & e, bool new_flipped, optional<expr> new_target, optional<expr> new_proof) {
eqc_key k(R, e); eqc_key k(R, e);
auto n = m_entries.find(k); auto n = m_entries.find(k);
lean_assert(n); lean_assert(n);
entry new_n = *n; entry new_n = *n;
if (n->m_target) if (n->m_target)
invert_trans(R, *new_n.m_target, some_expr(e), new_n.m_proof); invert_trans(R, *new_n.m_target, !new_n.m_flipped, some_expr(e), new_n.m_proof);
new_n.m_target = new_target; new_n.m_target = new_target;
new_n.m_proof = new_proof; new_n.m_proof = new_proof;
new_n.m_flipped = !new_n.m_flipped; new_n.m_flipped = new_flipped;
m_entries.insert(k, new_n); m_entries.insert(k, new_n);
} }
void congruence_closure::invert_trans(name const & R, expr const & e) { void congruence_closure::invert_trans(name const & R, expr const & e) {
invert_trans(R, e, none_expr(), none_expr()); invert_trans(R, e, false, none_expr(), none_expr());
} }
void congruence_closure::remove_parents(name const & R, expr const & e) { void congruence_closure::remove_parents(name const & R, expr const & e) {

2
src/library/blast/congruence_closure.h
View file

@ -129,7 +129,7 @@ class congruence_closure {
void mk_entry(name const & R, expr const & e, bool to_propagate); void mk_entry(name const & R, expr const & e, bool to_propagate);
void add_occurrence(name const & Rp, expr const & parent, name const & Rc, expr const & child); void add_occurrence(name const & Rp, expr const & parent, name const & Rc, expr const & child);
void add_congruence_table(ext_congr_lemma const & lemma, expr const & e); void add_congruence_table(ext_congr_lemma const & lemma, expr const & e);
void invert_trans(name const & R, expr const & e, optional<expr> new_target, optional<expr> new_proof); void invert_trans(name const & R, expr const & e, bool new_flipped, optional<expr> new_target, optional<expr> new_proof);
void invert_trans(name const & R, expr const & e); void invert_trans(name const & R, expr const & e);
void remove_parents(name const & R, expr const & e); void remove_parents(name const & R, expr const & e);
void reinsert_parents(name const & R, expr const & e); void reinsert_parents(name const & R, expr const & e);

16
tests/lean/run/blast_ematch4.lean Normal file
View file

@ -0,0 +1,16 @@
import data.nat
open algebra nat
section
open nat
set_option blast.simp false
set_option blast.subst false
set_option blast.ematch true
attribute add.comm [forward]
attribute add.assoc [forward]
example (a b c : nat) : a + b + b + c = c + b + a + b :=
by blast
end