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

fix(library/blast/congruence_closure): bug in add_eqv_step

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-23 14:26:33 -08:00
parent f1a3f8ec9d
commit f4a7268bd7
2 changed files with 22 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -754,7 +754,7 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
m_entries.insert(eqc_key(R, e1), new_n1);
// The hash code for the parents is going to change
remove_parents(R, e1);
remove_parents(R, e1_root);
// force all m_root fields in e1 equivalence class to point to e2_root
bool propagate = R == get_iff_name() && is_true_or_false(e2_root);
@ -771,7 +771,7 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
it = new_it_n.m_next;
} while (it != e1);
reinsert_parents(R, e1);
reinsert_parents(R, e1_root);
// update next of e1_root and e2_root, and size of e2_root
r1 = m_entries.find(eqc_key(R, e1_root));

20
tests/lean/run/blast_cc13.lean Normal file
View file

@ -0,0 +1,20 @@
set_option blast.subst false
set_option blast.simp false
set_option blast.init_depth 10
set_option blast.inc_depth 100
example (p : nat → nat → Prop) (f : nat → nat) (a b c d : nat) :
p (f a) (f b) → a = c → b = d → b = c → p (f c) (f c) :=
by blast
example (p : nat → nat → Prop) (a b c d : nat) :
p a b → a = c → b = d → p c d :=
by blast
example (p : nat → nat → Prop) (f : nat → nat) (a b c d : nat) :
p (f (f (f (f (f (f a))))))
(f (f (f (f (f (f b)))))) →
a = c → b = d → b = c →
p (f (f (f (f (f (f c))))))
(f (f (f (f (f (f c)))))) :=
by blast