From a415866df0ab1d5d26af83018f4a2ddf1391fca3 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 26 Oct 2012 17:32:18 +0200
Subject: [PATCH] In case !--inplace, report results nicely as well
---
src/main/scala/leon/synthesis/SynthesisPhase.scala | 7 +++++++
src/main/scala/leon/synthesis/Synthesizer.scala | 8 --------
2 files changed, 7 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 998a1be17..49e17e441 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -3,6 +3,7 @@ package synthesis
import purescala.TreeOps.simplifyLets
import purescala.Trees.Expr
+import purescala.ScalaPrinter
import purescala.Definitions.Program
object SynthesisPhase extends LeonPhase[Program, Program] {
@@ -46,6 +47,12 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
for (file <- ctx.files) {
new FileInterface(ctx.reporter, file).updateFile(chooseToExprs)
}
+ } else {
+ for ((chs, ex) <- chooseToExprs) {
+ ctx.reporter.info("-"*80)
+ ctx.reporter.info("For: "+chs)
+ ctx.reporter.info("Synthesized Code:\n"+ScalaPrinter(ex))
+ }
}
p
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 741915bab..0dc4cb283 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -110,18 +110,10 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivation
val as = (variablesOf(pred)--xs).toList
val phi = pred
- info("")
- info("")
- info("In Function "+f.id+":")
- info("-"*80)
-
val sol = synthesize(Problem(as, phi, xs), rules)
solutions += ch -> sol
- info("Scala code:")
- info(ScalaPrinter(simplifyLets(sol.toExpr)))
-
a
case _ =>
a
--
GitLab