From 1c34c7c2bdd56a6d42019bdc4a82afa54dc1711c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 31 Oct 2012 16:06:35 +0100
Subject: [PATCH] Implement --functions option for synthesis
---
src/main/scala/leon/LeonOption.scala | 4 ++++
.../scala/leon/synthesis/SynthesisPhase.scala | 15 ++++++++++-----
src/main/scala/leon/synthesis/Synthesizer.scala | 6 ++++--
testcases/synthesis/SortedList.scala | 2 ++
4 files changed, 20 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 0340e7461..a2ceda071 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -23,3 +23,7 @@ case class LeonFlagOptionDef(name: String, usageOption: String, usageDesc: Strin
case class LeonValueOptionDef(name: String, usageOption: String, usageDesc: String) extends LeonOptionDef {
val isFlag = false
}
+
+object ListValue {
+ def unapply(value: String): Option[Seq[String]] = Some(value.split(':').map(_.trim).filter(!_.isEmpty))
+}
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 6e809dc47..835e86f0f 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -14,8 +14,9 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
val description = "Synthesis"
override def definedOptions = Set(
- LeonFlagOptionDef("inplace", "--inplace", "Debug level"),
- LeonFlagOptionDef("derivtrees", "--derivtrees", "Generate derivation trees")
+ LeonFlagOptionDef( "inplace", "--inplace", "Debug level"),
+ LeonFlagOptionDef( "derivtrees", "--derivtrees", "Generate derivation trees"),
+ LeonValueOptionDef("functions", "--functions=f1:f2", "Limit synthesis of choose found within f1,f2,..")
)
def run(ctx: LeonContext)(p: Program): Program = {
@@ -27,17 +28,21 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
val uninterpretedZ3 = new UninterpretedZ3Solver(quietReporter)
uninterpretedZ3.setProgram(p)
- var inPlace = false
- var genTrees = false
+ var inPlace = false
+ var genTrees = false
+ var filterFun: Option[Seq[String]] = None
+
for(opt <- ctx.options) opt match {
case LeonFlagOption("inplace") =>
inPlace = true
+ case LeonValueOption("functions", ListValue(fs)) =>
+ filterFun = Some(fs)
case LeonFlagOption("derivtrees") =>
genTrees = true
case _ =>
}
- val synth = new Synthesizer(ctx.reporter, solvers, genTrees)
+ val synth = new Synthesizer(ctx.reporter, solvers, genTrees, filterFun.map(_.toSet))
val solutions = synth.synthesizeAll(p)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 91ba9d37f..295b6e143 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -12,7 +12,7 @@ import java.io.File
import collection.mutable.PriorityQueue
-class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivationTrees: Boolean) {
+class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivationTrees: Boolean, filterFuns: Option[Set[String]]) {
import r.{error,warning,info,fatalError}
private[this] var solution: Option[Solution] = None
@@ -121,7 +121,9 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver], generateDerivation
// Look for choose()
for (f <- program.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) {
- treeCatamorphism(x => x, noop, actOnChoose(f), f.body.get)
+ if (filterFuns.isEmpty || filterFuns.get.contains(f.id.toString)) {
+ treeCatamorphism(x => x, noop, actOnChoose(f), f.body.get)
+ }
}
solutions
diff --git a/testcases/synthesis/SortedList.scala b/testcases/synthesis/SortedList.scala
index af05150bf..b63c42352 100644
--- a/testcases/synthesis/SortedList.scala
+++ b/testcases/synthesis/SortedList.scala
@@ -20,6 +20,8 @@ object SortedList {
case Cons(i, t) => Set(i) ++ content(t)
}
+ def groundSynth() = choose{ (out: List) => size(out) == 5 }
+
def insertSynth(in: List, v: Int) = choose{ (out: List) => content(out) == content(in) ++ Set(v) }
def insert1(l: List, v: Int) = (
--
GitLab