diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 392c7af337b8901a7c2378f248b1053c1c797a75..0b1fa4acd9e67a111cd72e413430d0957ecd1e77 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -74,6 +74,18 @@ object Extractors {
case Concat(t1,t2) => Some((t1,t2,Concat))
case ListAt(t1,t2) => Some((t1,t2,ListAt))
case Let(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => Let(binders, e, body)))
+ case LetDef(fd, body) =>
+ fd.body match {
+ case Some(b) =>
+ Some((b, body, (b: Expr, body: Expr) => {
+ val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ nfd.body = Some(b)
+
+ LetDef(nfd, body)
+ }))
+ case _ =>
+ None
+ }
case LetTuple(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => LetTuple(binders, e, body)))
case wh@While(t1, t2) => Some((t1,t2, (t1, t2) => While(t1, t2).setInvariant(wh.invariant).setPosInfo(wh)))
case ex: BinaryExtractable => ex.extract
diff --git a/src/main/scala/leon/synthesis/Complexity.scala b/src/main/scala/leon/synthesis/Complexity.scala
index 8106beed5d6ba3ae23e1253ba99f82b02e04d647..cea557ca3b729cd31e10ac747a12481b3ac67ca2 100644
--- a/src/main/scala/leon/synthesis/Complexity.scala
+++ b/src/main/scala/leon/synthesis/Complexity.scala
@@ -10,26 +10,23 @@ abstract class Complexity[T <: Complexity[T]] extends Ordered[T] {
def value : Int
}
-case class TaskComplexity(t: Task) extends Complexity[TaskComplexity] {
- def value= {
- Option(t.rule) match {
- case Some(r) =>
- 100*t.problem.complexity.value + (100-r.priority) + t.minSolutionCost
- case None =>
- 0
- }
- }
+abstract class SolutionComplexity extends Complexity[SolutionComplexity] {
+ def value: Int
}
-case class SolutionComplexity(s: Solution) extends Complexity[SolutionComplexity] {
+case class ConcreteSolutionComplexity(s: Solution) extends SolutionComplexity {
lazy val value = {
val chooses = collectChooses(s.term)
- val chooseCost = 1000 * chooses.foldLeft(0)((i, c) => i + (math.pow(2, c.vars.size).toInt + formulaSize(c.pred)))
+ val chooseCost = chooses.foldLeft(0)((i, c) => i + (1000 * math.pow(2, c.vars.size).toInt + formulaSize(c.pred)))
formulaSize(s.pre) + formulaSize(s.term) + chooseCost
}
}
+case class FixedSolutionComplexity(c: Int) extends SolutionComplexity {
+ val value = c
+}
+
case class ProblemComplexity(p: Problem) extends Complexity[ProblemComplexity] {
lazy val value = {
math.pow(2, p.xs.size).toInt + formulaSize(p.phi)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index f96ecacbfe88a6949eae7135c9742924fc56212c..0e39e3f9cbf2c47c56addddca760a62d7fc6bcce 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -72,7 +72,7 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
}
-class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8, 100) {
+class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8, 500) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -81,7 +81,7 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8, 1
val tpe = TupleType(p.xs.map(_.getType))
val inductOn = FreshIdentifier(origId.name, true).setType(origId.getType)
-
+
val postXs = p.xs map (id => FreshIdentifier("r", true).setType(id.getType))
val postXsMap = (p.xs zip postXs).toMap.mapValues(Variable(_))
@@ -94,7 +94,7 @@ class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8, 1
val subGT = Problem(inductOn :: postXs, And(Seq(newPhi, GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT)), p.xs)
val subLT = Problem(inductOn :: postXs, And(Seq(newPhi, LessThan(Variable(inductOn), IntLiteral(0)), postCondLT)), p.xs)
- val onSuccess: List[Solution] => Solution = {
+ val onSuccess: List[Solution] => Solution = {
case List(base, gt, lt) =>
val newFun = new FunDef(FreshIdentifier("rec", true), tpe, Seq(VarDecl(inductOn, inductOn.getType)))
newFun.body = Some(
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 51e1c02eabbb60055d14fa778eed6ad67d2000bb..213793663c43bb02e881c6f849a2349dd527ceda 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -41,7 +41,7 @@ abstract class Rule(val name: String, val synth: Synthesizer, val priority: Prio
override def toString = name
}
-class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 30, 0) {
+class OnePoint(synth: Synthesizer) extends Rule("One-point", synth, 30, 5) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -102,7 +102,7 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth, 50, 0) {
}
}
-class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 20, 0) {
+class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 20, 10) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
p.phi match {
@@ -122,7 +122,7 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth, 20, 0) {
}
}
-class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20, 0) {
+class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20, 1) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -154,7 +154,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20, 0) {
}
}
-class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 10, 0) {
+class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 10, 1) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
val unused = p.as.toSet -- variablesOf(p.phi)
@@ -169,7 +169,7 @@ class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth, 10, 0)
}
}
-class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", synth, 10, 0) {
+class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", synth, 10, 5) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
val unconstr = p.xs.toSet -- variablesOf(p.phi)
@@ -193,7 +193,7 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy
}
object Unification {
- class DecompTrivialClash(synth: Synthesizer) extends Rule("Unif Dec./Clash/Triv.", synth, 20, 0) {
+ class DecompTrivialClash(synth: Synthesizer) extends Rule("Unif Dec./Clash/Triv.", synth, 20, 5) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
@@ -248,7 +248,7 @@ object Unification {
}
-class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 20, 0) {
+class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 20, 10) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 3fcf16eba23ab474d2d1f308e8a69b0553b09227..573ff7c56abfeab733c45c96583052e4e3270b80 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -9,7 +9,7 @@ import leon.purescala.TreeOps.simplifyLets
class Solution(val pre: Expr, val term: Expr) {
override def toString = "⟨ "+pre+" | "+term+" ⟩"
- lazy val complexity: SolutionComplexity = new SolutionComplexity(this)
+ lazy val complexity: SolutionComplexity = new ConcreteSolutionComplexity(this)
def toExpr = {
if (pre == BooleanLiteral(true)) {
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 7adfb5aef6d21fd473cc1565ce7814578084c336..f51749d8203232f8613cdae00423531241d86d3d 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -17,15 +17,16 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
LeonFlagOptionDef( "inplace", "--inplace", "Debug level"),
LeonFlagOptionDef( "derivtrees", "--derivtrees", "Generate derivation trees"),
LeonFlagOptionDef( "firstonly", "--firstonly", "Stop as soon as one synthesis solution is found"),
+ LeonValueOptionDef("timeout", "--timeout=T", "Timeout after T seconds when searching for synthesis solutions .."),
LeonValueOptionDef("functions", "--functions=f1:f2", "Limit synthesis of choose found within f1,f2,..")
)
def run(ctx: LeonContext)(p: Program): Program = {
- val reporter = new SilentReporter
- val solvers = List(
- new TrivialSolver(reporter),
- new FairZ3Solver(reporter)
- )
+ val reporter = new QuietReporter
+
+ val mainSolver = new FairZ3Solver(reporter)
+ mainSolver.setProgram(p)
+
val uninterpretedZ3 = new UninterpretedZ3Solver(reporter)
uninterpretedZ3.setProgram(p)
@@ -33,12 +34,19 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
var genTrees = false
var firstOnly = false
var filterFun: Option[Seq[String]] = None
+ var timeoutMs: Option[Long] = None
for(opt <- ctx.options) opt match {
case LeonFlagOption("inplace") =>
inPlace = true
case LeonValueOption("functions", ListValue(fs)) =>
filterFun = Some(fs)
+ case LeonValueOption("timeout", t) =>
+ try {
+ timeoutMs = Some(t.toLong)
+ } catch {
+ case _: Throwable =>
+ }
case LeonFlagOption("firstonly") =>
firstOnly = true
case LeonFlagOption("derivtrees") =>
@@ -46,10 +54,9 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
case _ =>
}
- val synth = new Synthesizer(ctx.reporter, solvers, genTrees, filterFun.map(_.toSet), firstOnly)
+ val synth = new Synthesizer(ctx.reporter, mainSolver, genTrees, filterFun.map(_.toSet), firstOnly, timeoutMs)
val solutions = synth.synthesizeAll(p)
-
// Simplify expressions
val simplifiers = List[Expr => Expr](
simplifyTautologies(uninterpretedZ3)(_),
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 0739733ea0cbdefbcd0769e8e693fc5a454575e3..895ec71c44dea208d6b82f1fb818b951c748a29e 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -13,10 +13,11 @@ import java.io.File
import collection.mutable.PriorityQueue
class Synthesizer(val r: Reporter,
- val solvers: List[Solver],
+ solver: Solver,
generateDerivationTrees: Boolean,
filterFuns: Option[Set[String]],
- firstOnly: Boolean) {
+ firstOnly: Boolean,
+ timeoutMs: Option[Long]) {
import r.{error,warning,info,fatalError}
@@ -28,27 +29,36 @@ class Synthesizer(val r: Reporter,
val workList = new PriorityQueue[Task]()
val rootTask = new RootTask(this, p)
- val giveUpComplexity = new TaskComplexity(null) {
- override def value = 100000
- }
-
workList += rootTask
+ val ts = System.currentTimeMillis
+ def timeoutExpired(): Boolean = {
+ timeoutMs match {
+ case Some(t) if (System.currentTimeMillis-ts)/1000 > t => true
+ case _ => false
+ }
+ }
+
+ val worstSolution = Solution.choose(p)
+ def bestSolutionSoFar(): Solution= rootTask.solution.getOrElse(worstSolution)
+
while (!workList.isEmpty && !(firstOnly && rootTask.solution.isDefined)) {
val task = workList.dequeue()
- if (task.complexity > giveUpComplexity) {
- // This task is too complicated, we give up with a choose solution
- val solution = Solution.choose(task.problem)
- task.solution = Some(solution)
- task.parent.partlySolvedBy(task, solution)
- } else {
+ // Check if solving this task has the slightest chance of improving the
+ // current solution
+ if (task.minSolutionComplexity < bestSolutionSoFar().complexity) {
val subProblems = task.run
for (p <- subProblems; r <- rules) yield {
workList += new Task(this, task, p, r)
}
}
+
+ if (timeoutExpired()) {
+ warning("Timeout reached")
+ workList.clear()
+ }
}
if (generateDerivationTrees) {
@@ -57,30 +67,25 @@ class Synthesizer(val r: Reporter,
derivationCounter += 1
}
- rootTask.solution.getOrElse(Solution.none)
+ bestSolutionSoFar()
}
def solveSAT(phi: Expr): (Option[Boolean], Map[Identifier, Expr]) = {
- for (s <- solvers) {
- s.solveOrGetCounterexample(Not(phi)) match {
- case (Some(true), _) =>
- return (Some(false), Map())
- case (Some(false), model) =>
- return (Some(true), model)
- case _ =>
- }
+ solver.solveOrGetCounterexample(Not(phi)) match {
+ case (Some(true), _) =>
+ (Some(false), Map())
+ case (Some(false), model) =>
+ (Some(true), model)
+ case (None, _) =>
+ println("WOOPS: failure on "+phi)
+ (None, Map())
}
- (None, Map())
}
val rules = Rules.all(this) ++ Heuristics.all(this)
import purescala.Trees._
def synthesizeAll(program: Program): List[(Choose, Solution)] = {
-
- solvers.foreach(_.setProgram(program))
-
-
def noop(u:Expr, u2: Expr) = u
var solutions = List[(Choose, Solution)]()
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index c1c5bdb694b6de1a3e78792b2ddeb5e3a01c4684..4db32fd42102b16880e5ea13fd15c7620bde00c1 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -6,9 +6,15 @@ class Task(synth: Synthesizer,
val problem: Problem,
val rule: Rule) extends Ordered[Task] {
- val complexity: TaskComplexity = new TaskComplexity(this)
+ def compare(that: Task) = {
+ val cproblem = -(this.problem.complexity compare that.problem.complexity) // problem DESC
- def compare(that: Task) = that.complexity compare this.complexity // sort by complexity ASC
+ if (cproblem == 0) {
+ this.rule.priority-that.rule.priority
+ } else {
+ cproblem
+ }
+ }
var subProblems: List[Problem] = Nil
var onSuccess: List[Solution] => Solution = _
@@ -64,7 +70,7 @@ class Task(synth: Synthesizer,
}
}
- lazy val minSolutionCost: Cost = rule.cost + parent.minSolutionCost
+ lazy val minSolutionComplexity: FixedSolutionComplexity = new FixedSolutionComplexity(rule.cost+parent.minSolutionComplexity.value)
override def toString = "Applying "+rule+" on "+problem
}
@@ -72,7 +78,7 @@ class Task(synth: Synthesizer,
class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, problem, null) {
var solver: Option[Task] = None
- override lazy val minSolutionCost = 0
+ override lazy val minSolutionComplexity = new FixedSolutionComplexity(0)
override def partlySolvedBy(t: Task, s: Solution) {
if (isBetterSolutionThan(s, solution)) {