From 99e0058cc418bbd3cc80a4bbac117e212635043e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 23 Oct 2012 18:51:51 +0200
Subject: [PATCH] Simplify outer If in case it's not necessary
---
src/main/scala/leon/synthesis/Solution.scala | 10 ++++++++++
src/main/scala/leon/synthesis/Synthesizer.scala | 2 +-
2 files changed, 11 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index f9e9f28c3..25e0d5899 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -7,6 +7,16 @@ import leon.purescala.Trees._
// ⟨ P | T ⟩
case class Solution(pre: Expr, term: Expr, score: Score = 0) {
override def toString = "⟨ "+pre+" | "+term+" ⟩"
+
+ def toExpr = {
+ if (pre == BooleanLiteral(true)) {
+ term
+ } else if (pre == BooleanLiteral(false)) {
+ Error("Impossible program").setType(term.getType)
+ } else {
+ IfExpr(pre, term, Error("Precondition failed").setType(term.getType))
+ }
+ }
}
object Solution {
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index e894cfcfb..8a2426f3b 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -96,7 +96,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
val sol = synthesize(Problem(as, phi, xs), rules)
info("Scala code:")
- info(ScalaPrinter(IfExpr(sol.pre, sol.term, Error("Precondition failed").setType(sol.term.getType))))
+ info(ScalaPrinter(sol.toExpr))
a
case _ =>
--
GitLab