Support asString for debugging synthesis problems/solutions

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)
 

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 = {

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))

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)}"
     }