Introduce 't' command for manual to print current tree

src/main/scala/leon/synthesis/PartialSolution.scala

@@ -6,10 +6,9 @@ package synthesis
 import purescala.Expressions._
 
 import graph._
+import strategies._
 
-class PartialSolution(search: Search, includeUntrusted: Boolean = false) {
-  val g = search.g
-  val strat = search.strat
+class PartialSolution(strat: Strategy, includeUntrusted: Boolean = false) {
 
   def includeSolution(s: Solution) = {
     includeUntrusted || s.isTrusted
@@ -50,11 +49,6 @@ class PartialSolution(search: Search, includeUntrusted: Boolean = false) {
 
   }
 
-
-  def getSolution: Solution = {
-    getSolutionFor(g.root)
-  }
-
   def getSolutionFor(n: Node): Solution = {
     n match {
       case on: OrNode =>

src/main/scala/leon/synthesis/Synthesizer.scala

@@ -121,7 +121,7 @@ class Synthesizer(val context : LeonContext,
     }(DebugSectionReport)
 
     (s, if (result.isEmpty && allowPartial) {
-      Stream((new PartialSolution(s, true).getSolution, false))
+      Stream((new PartialSolution(s.strat, true).getSolutionFor(s.g.root), false))
     } else {
       // Discard invalid solutions
       result collect {
@@ -155,7 +155,7 @@ class Synthesizer(val context : LeonContext,
         reporter.error("Solution was invalid:")
         reporter.error(fds.map(ScalaPrinter(_)).mkString("\n\n"))
         reporter.error(vcreport.summaryString)
-        (new PartialSolution(search, false).getSolution, Some(false))
+        (new PartialSolution(search.strat, false).getSolutionFor(search.g.root), Some(false))
       }
     } finally {
       solverf.shutdown()

src/main/scala/leon/synthesis/rules/CEGISLike.scala

@@ -327,7 +327,7 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
       private val (innerProgram, origFdMap) = {
 
         val outerSolution = {
-          new PartialSolution(hctx.search, true)
+          new PartialSolution(hctx.search.strat, true)
             .solutionAround(hctx.currentNode)(FunctionInvocation(solFd.typed, p.as.map(_.toVariable)))
             .getOrElse(ctx.reporter.fatalError("Unable to get outer solution"))
         }

src/main/scala/leon/synthesis/rules/IntroduceRecCall.scala

@@ -54,7 +54,7 @@ case object IntroduceRecCall extends Rule("Introduce rec. calls") {
 
         def apply(nohctx: SearchContext) = {
 
-          val psol = new PartialSolution(hctx.search, true)
+          val psol = new PartialSolution(hctx.search.strat, true)
             .solutionAround(hctx.currentNode)(Error(p.outType, "Encountered choose!"))
             .getOrElse(hctx.sctx.context.reporter.fatalError("Unable to get outer solution"))
             .term

src/main/scala/leon/synthesis/strategies/ManualStrategy.scala

@@ -4,6 +4,8 @@ package leon
 package synthesis
 package strategies
 
+import purescala.Common.FreshIdentifier
+
 import graph._
 
 class ManualStrategy(ctx: LeonContext, initCmd: Option[String], strat: Strategy) extends Strategy {
@@ -17,6 +19,7 @@ class ManualStrategy(ctx: LeonContext, initCmd: Option[String], strat: Strategy)
   case object Quit extends Command
   case object Noop extends Command
   case object Best extends Command
+  case object Tree extends Command
 
   // Manual search state:
   var rootNode: Node    = _
@@ -156,6 +159,20 @@ class ManualStrategy(ctx: LeonContext, initCmd: Option[String], strat: Strategy)
 
           manualGetNext()
 
+        case Tree =>
+          val hole = FreshIdentifier("\u001b[1;31m??? \u001b[0m", c.p.outType)
+          val ps = new PartialSolution(this, true)
+
+          ps.solutionAround(c)(hole.toVariable) match {
+            case Some(sol) =>
+              println("-"*120)
+              println(sol.toExpr.asString)
+            case None =>
+              error("woot!")
+          }
+          manualGetNext()
+
+
         case Best =>
           strat.bestNext(c) match {
             case Some(n) =>
@@ -228,6 +245,9 @@ class ManualStrategy(ctx: LeonContext, initCmd: Option[String], strat: Strategy)
         Cd(path.map(_.toInt)) :: parseCommands(ts.drop(path.size))
       }
 
+    case "t" :: ts =>
+      Tree :: parseCommands(ts)
+
     case "b" :: ts =>
       Best :: parseCommands(ts)