max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/defeq_canonizer): bugs found by Daniel

Browse source 
This is a cleanup of
10d23f0075
This commit is contained in:
Leonardo de Moura 2016-07-04 17:22:37 -07:00
parent d3cfd39278
commit cda867b124
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/defeq_canonizer.cpp
View file

@ -15,7 +15,7 @@ struct defeq_canonize_cache {
environment m_env;
/* Canonical mapping I -> J (i.e., J is the canonical expression for I).
Invariant: locals_subset(J, I) */
expr_map<expr> m_C;
expr_struct_map<expr> m_C;
/* Mapping from head symbol N to list of expressions es s.t.
for each e in es, head_symbol(e) = N. */
name_map<list<expr>> m_M;
@ -116,6 +116,7 @@ struct defeq_canonize_fn {
if (get_weight(e) < get_weight(*new_e) && locals_subset(e, *new_e)) {
replace_C(*new_e, e);
replace_M(*h, *new_e, e);
insert_C(e, e);
return e;
} else {
insert_C(e, *new_e);