From c46cc9a5312afcfdc5a8ff6779dce1f2f048d3c1 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 21 Apr 2016 16:55:29 +0200
Subject: [PATCH] Improve printing in synthesis
---
src/main/scala/leon/synthesis/Problem.scala | 14 +++++++-------
src/main/scala/leon/synthesis/Search.scala | 1 -
src/main/scala/leon/synthesis/graph/Graph.scala | 2 +-
.../leon/synthesis/rules/IntroduceRecCalls.scala | 2 +-
4 files changed, 9 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 5e97203c3..52f9d7bd0 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -26,8 +26,7 @@ import Witnesses._
*/
case class Problem(as: List[Identifier], ws: Expr, pc: Path, phi: Expr, xs: List[Identifier], eb: ExamplesBank = ExamplesBank.empty) extends Printable {
- // Activate this for debugging...
- // assert(eb.examples.forall(_.ins.size == as.size))
+ // require(eb.examples.forall(_.ins.size == as.size))
val TopLevelAnds(wsList) = ws
@@ -37,15 +36,16 @@ case class Problem(as: List[Identifier], ws: Expr, pc: Path, phi: Expr, xs: List
def allAs = as ++ (pc.bindings.map(_._1) diff wsList.collect{ case Inactive(i) => i })
def asString(implicit ctx: LeonContext): String = {
+ def pad(padding: String, text: String) = text.lines.mkString(s"\n|$padding")
val pcws = pc withCond ws
val ebInfo = "/"+eb.valids.size+","+eb.invalids.size+"/"
- s"""|⟦ ${if (as.nonEmpty) as.map(_.asString).mkString(", ") else "()"}
- | ${pcws.toClause.asString} ≺
- | ⟨ ${phi.asString} ⟩
- | ${if (xs.nonEmpty) xs.map(_.asString).mkString(", ") else "()"}
- |⟧ $ebInfo""".stripMargin
+ s"""|⟦ \u0305α ${if (as.nonEmpty) as.map(_.asString).mkString(", ") else "()"}
+ | Π ${pad(" ", pcws.fullClause.asString)}
+ | φ ${pad(" ", phi.asString)}
+ | \u0305x ${if (xs.nonEmpty) xs.map(_.asString).mkString(", ") else "()"}
+ |⟧ $ebInfo""".stripMargin
}
def withWs(es: Traversable[Expr]) = {
diff --git a/src/main/scala/leon/synthesis/Search.scala b/src/main/scala/leon/synthesis/Search.scala
index 564c630fc..e9501009d 100644
--- a/src/main/scala/leon/synthesis/Search.scala
+++ b/src/main/scala/leon/synthesis/Search.scala
@@ -8,7 +8,6 @@ import graph._
import scala.annotation.tailrec
-import scala.collection.mutable.ArrayBuffer
import leon.utils.Interruptible
import java.util.concurrent.atomic.AtomicBoolean
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index 59ae2ae37..1a0c1440e 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -82,7 +82,7 @@ class AndNode(parent: Option[Node], val ri: RuleInstantiation) extends Node(pare
import hctx.reporter.info
- val prefix = f"[${Option(ri.rule.asString).getOrElse("?")}%-20s]"
+ val prefix = f"[${Option(ri).map(_.asString).getOrElse("?")}%-20s]"
info(pad(prefix, ri.problem.asString))
diff --git a/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala b/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
index 8c2f14cc2..2d2999871 100644
--- a/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
+++ b/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
@@ -53,7 +53,7 @@ case object IntroduceRecCalls extends NormalizingRule("Introduce rec. calls") {
val onSuccess = forwardMap(letTuple(recs.map(_._1), tupleWrap(calls), _))
- List(new RuleInstantiation(s"Introduce recursive calls ${calls mkString ", "}", SolutionBuilderDecomp(List(p.outType), onSuccess)) {
+ List(new RuleInstantiation(s"Introduce calls ${calls mkString ", "}", SolutionBuilderDecomp(List(p.outType), onSuccess)) {
def apply(nohctx: SearchContext): RuleApplication = {
--
GitLab