From 304ac9f5c23e64bd7c5f5a8d5c88c87fd9e2d269 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Thu, 15 Jan 2015 16:05:07 +0100
Subject: [PATCH] --manual takes a script as optional argument to automate
repeat
---
src/main/scala/leon/synthesis/SynthesisPhase.scala | 8 ++++----
.../scala/leon/synthesis/SynthesisSettings.scala | 2 +-
src/main/scala/leon/synthesis/Synthesizer.scala | 4 ++--
src/main/scala/leon/synthesis/graph/Search.scala | 14 +++++++++-----
4 files changed, 16 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index a0aff1783..0944851f5 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/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
diff --git a/src/main/scala/leon/synthesis/SynthesisSettings.scala b/src/main/scala/leon/synthesis/SynthesisSettings.scala
index 126f79943..5f279ee5d 100644
--- a/src/main/scala/leon/synthesis/SynthesisSettings.scala
+++ b/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(),
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index b9bae7dad..6ba4adebf 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/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)
diff --git a/src/main/scala/leon/synthesis/graph/Search.scala b/src/main/scala/leon/synthesis/graph/Search.scala
index 4e851ef70..82e3e1175 100644
--- a/src/main/scala/leon/synthesis/graph/Search.scala
+++ b/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 =>
--
GitLab