Skip to content
Snippets Groups Projects
Commit 1c34c7c2 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Implement --functions option for synthesis

parent 55937a49
No related branches found
No related tags found
No related merge requests found
......@@ -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))
}
......@@ -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)
......
......@@ -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
......
......@@ -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) = (
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment