diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala index 6cd021597278b796aa37ddc9f4b229e46622f4de..5eb38b53677a2666f87e1f839314c45e61333aa9 100644 --- a/src/main/scala/leon/purescala/TreeOps.scala +++ b/src/main/scala/leon/purescala/TreeOps.scala @@ -1,6 +1,7 @@ package leon package purescala +import leon.Extensions.Solver object TreeOps { import Common._ @@ -1047,4 +1048,20 @@ object TreeOps { genericTransform[PMContext](pre, noPost, noCombiner)(PMContext())(e)._1 } + + def simplifyTautologies(solver : Solver)(expr : Expr) : Expr = { + def pre(e : Expr) = e match { + case IfExpr(cond, then, elze) => solver.solve(cond) match { + case Some(true) => then + case Some(false) => solver.solve(Not(cond)) match { + case Some(true) => elze + case _ => e + } + case None => e + } + case _ => e + } + + simpleTransform(pre, identity)(expr) + } } diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala index e61c6f3d008b84e230fff84bfb81940dbc75b7c0..e54d7c26190f2d9d79b7482af81abc3067f0b462 100644 --- a/src/main/scala/leon/synthesis/SynthesisPhase.scala +++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala @@ -3,7 +3,7 @@ package synthesis import purescala.TreeOps._ import solvers.TrivialSolver -import solvers.z3.FairZ3Solver +import solvers.z3.{FairZ3Solver,UninterpretedZ3Solver} import purescala.Trees.Expr import purescala.ScalaPrinter @@ -24,6 +24,8 @@ object SynthesisPhase extends LeonPhase[Program, Program] { new TrivialSolver(quietReporter), new FairZ3Solver(quietReporter) ) + val uninterpretedZ3 = new UninterpretedZ3Solver(quietReporter) + uninterpretedZ3.setProgram(p) var inPlace = false var genTrees = false @@ -41,6 +43,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] { // Simplify expressions val simplifiers = List[Expr => Expr]( + simplifyTautologies(uninterpretedZ3)(_), simplifyLets _, patternMatchReconstruction _ )