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

fix(library/compiler/csimp): missing optimization opportunity

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-05 16:16:24 -07:00
parent 7b835f3d02
commit 1e198ca72e
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/compiler/csimp.cpp
View file

@ -1580,13 +1580,13 @@ class csimp_fn {
} else if (is_constant(fn)) {
unsigned nargs = get_app_num_args(e);
if (nargs == 1) {
expr a1 = find(app_arg(e));
expr a1 = find(visit_arg(app_arg(e)));
if (optional<expr> r = fold_un_op(m_before_erasure, fn, a1)) {
return *r;
}
} else if (nargs == 2) {
expr a1 = find(app_arg(app_fn(e)));
expr a2 = find(app_arg(e));
expr a1 = find(visit_arg(app_arg(app_fn(e))));
expr a2 = find(visit_arg(app_arg(e)));
if (optional<expr> r = fold_bin_op(m_before_erasure, fn, a1, a2)) {
return *r;
}