diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala index 98551cbc108a6b6f0c4ea74f081584049b65adf4..e5b8d1f5827e2a7d8aa35c5e527fa1145785ebc6 100644 --- a/src/main/scala/leon/purescala/TreeOps.scala +++ b/src/main/scala/leon/purescala/TreeOps.scala @@ -1040,13 +1040,43 @@ object TreeOps { simplePreTransform(pre)(e) } + def decomposeIfs(e: Expr): Expr = { + def pre(e: Expr): Expr = e match { + case IfExpr(cond, then, elze) => + val TopLevelOrs(orcases) = toDNF(cond) + + if (!orcases.tail.isEmpty) { + pre(IfExpr(orcases.head, then, IfExpr(Or(orcases.tail), then, elze))) + } else { + val TopLevelAnds(andcases) = orcases.head + + val (andis, andnotis) = andcases.partition(_.isInstanceOf[CaseClassInstanceOf]) + + if (andis.isEmpty || andnotis.isEmpty) { + e + } else { + IfExpr(And(andis), IfExpr(And(andnotis), then, elze), elze) + } + } + case _ => + e + } + + simplePreTransform(pre)(e) + } + def patternMatchReconstruction(e: Expr): Expr = { case class PMContext() def pre(e: Expr, c: PMContext): (Expr, PMContext) = e match { case IfExpr(cond, then, elze) => val TopLevelOrs(cases) = toDNF(cond) - //println("Found Cases: "+cases) + // find one variable on which we will match: + val casematches = for (caze <- cases) yield { + val TopLevelAnds(conds) = caze + + conds.filter(_.isInstanceOf[CaseClassInstanceOf]) + } (e, c) case _ => diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala index e54d7c26190f2d9d79b7482af81abc3067f0b462..3f1c80a8f6c7f7a55f620177f449147eab1d56e7 100644 --- a/src/main/scala/leon/synthesis/SynthesisPhase.scala +++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala @@ -45,7 +45,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] { val simplifiers = List[Expr => Expr]( simplifyTautologies(uninterpretedZ3)(_), simplifyLets _, - patternMatchReconstruction _ + decomposeIfs _ ) val chooseToExprs = solutions.mapValues(sol => simplifiers.foldLeft(sol.toExpr){ (x, sim) => sim(x) })