From f205acb8c3c9b674b4166f163d80e47d83d53228 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 29 Jun 2015 17:46:43 +0200
Subject: [PATCH] Support asString for debugging synthesis problems/solutions
---
src/main/scala/leon/synthesis/Problem.scala | 8 ++++++++
src/main/scala/leon/synthesis/Solution.scala | 5 +++++
src/main/scala/leon/synthesis/graph/Graph.scala | 8 +++++---
src/main/scala/leon/synthesis/graph/Search.scala | 2 +-
4 files changed, 19 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index cfaa57e50..164b1a102 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -18,6 +18,14 @@ case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List
def inType = tupleTypeWrap(as.map(_.getType))
def outType = tupleTypeWrap(xs.map(_.getType))
+ def asString(implicit ctx: LeonContext): String = {
+ val pcws = and(ws, pc)
+
+ val tbInfo = "/"+tb.valids.size+","+tb.invalids.size+"/"
+
+ "⟦ "+as.map(_.asString).mkString(";")+", "+(if (pcws != BooleanLiteral(true)) pcws.asString+" ≺ " else "")+" ⟨ "+phi.asString+" ⟩ "+xs.map(_.asString).mkString(";")+" ⟧ "+tbInfo
+ }
+
override def toString = {
val pcws = and(ws, pc)
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 9d7444268..812b75353 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -15,6 +15,11 @@ import leon.utils.Simplifiers
// Defines a synthesis solution of the form:
// ⟨ P | T ⟩
class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrusted: Boolean = true) {
+
+ def asString(implicit ctx: LeonContext) = {
+ "⟨ "+pre.asString+" | "+defs.map(_.asString).mkString(" ")+" "+term.asString+" ⟩"
+ }
+
override def toString = "⟨ "+pre+" | "+defs.mkString(" ")+" "+term+" ⟩"
def guardedTerm = {
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index 438fbb850..c4e13648b 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -104,11 +104,13 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
require(!isExpanded)
isExpanded = true
+ implicit val ctx = hctx.sctx.context
+
import hctx.sctx.reporter.info
val prefix = f"[${Option(ri.rule).getOrElse("?")}%-20s] "
- info(prefix+ri.problem)
+ info(prefix+ri.problem.asString)
ri.apply(hctx) match {
case RuleClosed(sols) =>
@@ -123,7 +125,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
info(prefix+"Failed")
} else {
val sol = sols.head
- info(prefix+"Solved"+(if(sol.isTrusted) "" else " (untrusted)")+" with: "+sol+"...")
+ info(prefix+"Solved"+(if(sol.isTrusted) "" else " (untrusted)")+" with: "+sol.asString+"...")
}
parents.foreach{ p =>
@@ -136,7 +138,7 @@ class AndNode(cm: CostModel, parent: Option[Node], val ri: RuleInstantiation) ex
case RuleExpanded(probs) =>
info(prefix+"Decomposed into:")
for(p <- probs) {
- info(prefix+" - "+p)
+ info(prefix+" - "+p.asString)
}
descendents = probs.map(p => new OrNode(cm, Some(this), p))
diff --git a/src/main/scala/leon/synthesis/graph/Search.scala b/src/main/scala/leon/synthesis/graph/Search.scala
index b02063dd4..501004cfa 100644
--- a/src/main/scala/leon/synthesis/graph/Search.scala
+++ b/src/main/scala/leon/synthesis/graph/Search.scala
@@ -217,7 +217,7 @@ class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel
val app = an.ri
s"(${n.cost.asString}) ${indent(app)}"
case on: OrNode =>
- val p = on.p
+ val p = on.p.asString(ctx)
s"(${n.cost.asString}) ${indent(p)}"
}
--
GitLab