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

fix(library/blast/simplifier): loop rewrite rules

Browse source
This commit is contained in:
Daniel Selsam 2015-11-05 21:29:47 -08:00 committed by Leonardo de Moura
parent 25f507e46f
commit a304f6a9df
1 changed files with 12 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/blast/simplifier.cpp
View file

@ -370,8 +370,18 @@ result simplifier::rewrite(expr const & e) {
list<simp_rule> const * srs = sr->find_simp(e);
if (!srs) return r;
for_each(*srs,[&](simp_rule const & sr) { r = join(r,rewrite(r.get_new(),sr)); });
bool modified = true;
while (modified) {
modified = false;
for_each(*srs,[&](simp_rule const & sr) {
result r_rew = rewrite(r.get_new(),sr);
if (r_rew.is_none()) return;
r = join(r,r_rew);
modified = true;
}
);
}
return r;
}