diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala index cb945337d6b18320c0e8ecfaea24810e86f6b4ea..ba8ec79c42f157b67381e56eb16611bad3af23e8 100644 --- a/src/main/scala/leon/synthesis/Synthesizer.scala +++ b/src/main/scala/leon/synthesis/Synthesizer.scala @@ -52,7 +52,11 @@ class Synthesizer(val reporter: Reporter, while (!workList.isEmpty && !(firstOnly && rootTask.solution.isDefined)) { val task = workList.dequeue() - task.run() + val subProblems = task.run() + + if (task.minComplexity <= bestSolutionSoFar.complexity) { + addProblems(task, subProblems) + } if (timeoutExpired()) { warning("Timeout reached") diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala index a1632ec339bacfb5b6cf22dfa63824afb42c93ab..ed3bd980d09ba83c4bb668bf61bfbdf2a3b41622 100644 --- a/src/main/scala/leon/synthesis/Task.scala +++ b/src/main/scala/leon/synthesis/Task.scala @@ -25,6 +25,7 @@ class Task(synth: Synthesizer, } var solution: Option[Solution] = None + var minComplexity: AbsSolComplexity = new FixedSolComplexity(0) class TaskStep(val subProblems: List[Problem]) { var subSolutions = Map[Problem, Solution]() @@ -71,7 +72,7 @@ class Task(synth: Synthesizer, } } - def run() { + def run(): List[Problem] = { rule.applyOn(this) match { case RuleSuccess(solution) => // Solved @@ -81,12 +82,19 @@ class Task(synth: Synthesizer, val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root")) println(prefix+"Got: "+problem) println(prefix+"Solved with: "+solution) + Nil case RuleMultiSteps(subProblems, interSteps, onSuccess) => this.steps = new TaskStep(subProblems) :: Nil this.nextSteps = interSteps this.onSuccess = onSuccess + // Compute simplest solution possible to evaluate whether this rule is worth it + // To each problem we assign the most basic solution, fold on all inner + // steps, and then reconstruct final solution + val simplestSubSolutions = interSteps.foldLeft(subProblems.map(Solution.basic(_))){ (sols, step) => step(sols).map(Solution.basic(_)) } + val simplestSolution = onSuccess(simplestSubSolutions) + minComplexity = new FixedSolComplexity(parent.minComplexity.value + simplestSolution.complexity.value) val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root")) println(prefix+"Got: "+problem) println(prefix+"Decomposed into:") @@ -94,10 +102,11 @@ class Task(synth: Synthesizer, println(prefix+" - "+p) } - synth.addProblems(this, subProblems) + subProblems case RuleInapplicable => parent.unsolvedBy(this) + Nil } } @@ -107,8 +116,8 @@ class Task(synth: Synthesizer, class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, problem, null) { var solver: Option[Task] = None - override def run() { - synth.addProblems(this, List(problem)) + override def run() = { + List(problem) } override def partlySolvedBy(t: Task, s: Solution) {