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

perf(kernel/level): apply two simple normalization rules at mk_max

Browse source 
They are variations of:
max l1 (max l1 l2) == (max l1 l2)
This commit is contained in:
Leonardo de Moura 2014-11-16 18:16:57 -08:00
parent 53ac754328
commit e81d9c9184
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/level.cpp
View file

@ -219,6 +219,10 @@ level mk_max(level const & l1, level const & l2) {
return l2;
} else if (is_zero(l2)) {
return l1;
} else if (is_max(l2) && (max_lhs(l2) == l1 || max_rhs(l2) == l1)) {
return l2; // if l2 == (max l1 l'), then max l1 l2 == l2
} else if (is_max(l1) && (max_lhs(l1) == l2 || max_rhs(l1) == l2)) {
return l1; // if l1 == (max l2 l'), then max l1 l2 == l1
} else {
auto p1 = to_offset(l1);
auto p2 = to_offset(l2);