From 8416ebeed6c769179b335e6b421d2f751cbfffaf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com> Date: Thu, 22 Nov 2012 18:45:11 +0100 Subject: [PATCH] some highly specialized optimization --- src/main/scala/leon/purescala/TreeOps.scala | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala index fc3f06d22..a7a47c8a6 100644 --- a/src/main/scala/leon/purescala/TreeOps.scala +++ b/src/main/scala/leon/purescala/TreeOps.scala @@ -1371,6 +1371,7 @@ object TreeOps { case Plus(e, IntLiteral(0)) => e case Plus(e1, UMinus(e2)) => Minus(e1, e2) case Plus(Plus(e, IntLiteral(i1)), IntLiteral(i2)) => Plus(e, IntLiteral(i1+i2)) + case Plus(Plus(IntLiteral(i1), e), IntLiteral(i2)) => Plus(IntLiteral(i1+i2), e) case Minus(e, IntLiteral(0)) => e case Minus(IntLiteral(0), e) => UMinus(e) @@ -1399,7 +1400,14 @@ object TreeOps { case Division(e, IntLiteral(1)) => e //here we put more expensive rules + //btw, I know those are not the most general rules, but they lead to good optimizations :) + case Plus(UMinus(Plus(e1, e2)), e3) if e1 == e3 => UMinus(e2) + case Plus(UMinus(Plus(e1, e2)), e3) if e2 == e3 => UMinus(e1) case Minus(e1, e2) if e1 == e2 => IntLiteral(0) + case Minus(Plus(e1, e2), Plus(e3, e4)) if e1 == e4 && e2 == e3 => IntLiteral(0) + case Minus(Plus(e1, e2), Plus(Plus(e3, e4), e5)) if e1 == e4 && e2 == e3 => UMinus(e5) + + //default case e => e } def fix[A](f: (A) => A)(a: A): A = { -- GitLab