--manual takes a script as optional argument to automate repeat

src/main/scala/leon/synthesis/SynthesisPhase.scala

@@ -21,7 +21,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
     LeonFlagOptionDef( "inplace",         "--inplace",         "Debug level"),
     LeonFlagOptionDef( "allseeing",       "--allseeing",       "Also synthesize functions using holes"),
     LeonValueOptionDef("parallel",        "--parallel[=N]",    "Parallel synthesis search using N workers", Some("5")),
-    LeonFlagOptionDef( "manual",          "--manual",          "Manual search"),
+    LeonValueOptionDef( "manual",         "--manual[=cmd]",    "Manual search", Some("")),
     LeonFlagOptionDef( "derivtrees",      "--derivtrees",      "Generate derivation trees"),
     LeonFlagOptionDef( "firstonly",       "--firstonly",       "Stop as soon as one synthesis solution is found", true),
     LeonValueOptionDef("timeout",         "--timeout=T",       "Timeout after T seconds when searching for synthesis solutions .."),
@@ -41,8 +41,8 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
     var options = SynthesisSettings()
 
     for(opt <- ctx.options) opt match {
-      case LeonFlagOption("manual", v) =>
-        options = options.copy(manualSearch = v)
+      case LeonValueOption("manual", cmd) =>
+        options = options.copy(manualSearch = Some(cmd))
 
       case LeonFlagOption("allseeing", v) =>
         options = options.copy(allSeeing = v)
@@ -106,7 +106,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
       case _ =>
     }
 
-    if (options.manualSearch) {
+    if (options.manualSearch.isDefined) {
       options = options.copy(
         rules = rules.AsChoose +:
                 options.rules

src/main/scala/leon/synthesis/SynthesisSettings.scala

@@ -16,7 +16,7 @@ case class SynthesisSettings(
   timeoutMs: Option[Long]             = None,
   costModel: CostModel                = CostModels.default,
   rules: Seq[Rule]                    = Rules.all,
-  manualSearch: Boolean               = false,
+  manualSearch: Option[String]        = None,
   searchBound: Option[Int]            = None,
   selectedSolvers: Set[String]        = Set("fairz3"),
   functionsToIgnore: Set[FunDef]      = Set(),

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

@@ -28,8 +28,8 @@ class Synthesizer(val context : LeonContext,
   val reporter = context.reporter
 
   def getSearch(): Search = {
-    if (settings.manualSearch) {
-      new ManualSearch(context, ci, problem, settings.costModel)
+    if (settings.manualSearch.isDefined) {
+      new ManualSearch(context, ci, problem, settings.costModel, settings.manualSearch)
     } else if (settings.searchWorkers > 1) {
       ???
       //new ParallelSearch(this, problem, options.searchWorkers)

src/main/scala/leon/synthesis/graph/Search.scala

@@ -124,7 +124,7 @@ class SimpleSearch(ctx: LeonContext, ci: ChooseInfo, p: Problem, costModel: Cost
   }
 }
 
-class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel: CostModel) extends Search(ctx, ci, problem, costModel) {
+class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel: CostModel, initCmd: Option[String]) extends Search(ctx, ci, problem, costModel) {
   import ctx.reporter._
 
   abstract class Command
@@ -135,7 +135,7 @@ class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel
 
   // Manual search state:
   var cd       = List[Int]()
-  var cmdQueue = List[Command]()
+  var cmdQueue = initCmd.map( str => parseCommands(parseString(str))).getOrElse(Nil)
 
   def getNextCommand(): Command = cmdQueue match {
     case c :: cs =>
@@ -144,13 +144,17 @@ class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel
 
     case Nil =>
       print("Next action? (q to quit) "+cd.mkString(" ")+" $ ")
-      val line = scala.io.StdIn.readLine().trim
-      val parts = line.split("\\s+").toList
+      val line = scala.io.StdIn.readLine()
+      val parts = parseString(line)
 
       cmdQueue = parseCommands(parts)
       getNextCommand()
   }
 
+  def parseString(s: String): List[String] = {
+    s.trim.split("\\s+|,").toList
+  }
+
   def parseCommands(tokens: List[String]): List[Command] = tokens match {
     case "cd" :: ".." :: ts =>
       Parent :: parseCommands(ts)
@@ -167,7 +171,7 @@ class ManualSearch(ctx: LeonContext, ci: ChooseInfo, problem: Problem, costModel
     case "q" :: ts =>
       Quit :: Nil
 
-    case Nil =>
+    case Nil  | "" :: Nil =>
       Nil
 
     case ts =>