From 2be74176c66e081a9f30775b92ef49de218173a2 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 14 Nov 2012 20:17:29 +0100
Subject: [PATCH] With --firstonly we stop as soon as possible, and stop
propagating choose() down in the tree
---
.../scala/leon/synthesis/Heuristics.scala | 2 +-
.../scala/leon/synthesis/Synthesizer.scala | 30 +++++++++++++++----
src/main/scala/leon/synthesis/Task.scala | 18 +++++------
3 files changed, 33 insertions(+), 17 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 2a221536f..ea24005d6 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -10,7 +10,7 @@ import purescala.Definitions._
object Heuristics {
def all = Set[Synthesizer => Rule](
- new IntInduction(_),
+ //new IntInduction(_),
new OptimisticInjection(_),
new ADTInduction(_)
)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index a811fe6b7..b7c3e1fed 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -51,13 +51,33 @@ class Synthesizer(val reporter: Reporter,
}
}
- while (!workList.isEmpty && !(firstOnly && rootTask.solution.isDefined)) {
+ while (!workList.isEmpty) {
val task = workList.dequeue()
- val subProblems = task.run()
-
- if (task.minComplexity <= bestSolutionSoFar.complexity) {
- addProblems(task, subProblems)
+ val prefix = "[%-20s] ".format(Option(task.rule).map(_.toString).getOrElse("root"))
+
+ if (!(firstOnly && (task.parent ne null) && task.parent.isSolved)) {
+ val subProblems = task.run()
+
+ if (task.minComplexity <= bestSolutionSoFar.complexity) {
+ if (task.solution.isDefined || !subProblems.isEmpty) {
+ if (task.solution.isDefined) {
+ info(prefix+"Got: "+task.problem)
+ info(prefix+"Solved with: "+task.solution.get)
+ } else {
+ info(prefix+"Got: "+task.problem)
+ info(prefix+"Decomposed into:")
+ for(p <- subProblems) {
+ info(prefix+" - "+p)
+ }
+ }
+ }
+ addProblems(task, subProblems)
+ } else {
+ info(prefix+"Skip (worse): "+task.problem)
+ }
+ } else {
+ info(prefix+"Skip (done): "+task.problem)
}
if (timeoutExpired()) {
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index c35e2bb24..4bf92ad33 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -24,6 +24,7 @@ class Task(synth: Synthesizer,
}
}
+
var solution: Option[Solution] = None
var minComplexity: AbsSolComplexity = new FixedSolComplexity(0)
@@ -39,6 +40,8 @@ class Task(synth: Synthesizer,
def currentStep = steps.head
+ def isSolved: Boolean = parent.isSolved || (nextSteps.isEmpty && (currentStep.subSolutions.size == currentStep.subProblems.size))
+
def partlySolvedBy(t: Task, s: Solution) {
if (isBetterSolutionThan(s, currentStep.subSolutions.get(t.problem))) {
currentStep.subSolutions += t.problem -> s
@@ -62,7 +65,7 @@ class Task(synth: Synthesizer,
parent.partlySolvedBy(this, solution.get)
case _ =>
// solution is there, but it is incomplete (precondition not strongest)
- parent.partlySolvedBy(this, Solution.choose(problem))
+ //parent.partlySolvedBy(this, Solution.choose(problem))
}
}
}
@@ -75,7 +78,7 @@ class Task(synth: Synthesizer,
if (currentStep.failures.size == synth.rules.size) {
// We might want to report unsolved instead of solvedByChoose, depending
// on the cases
- parent.partlySolvedBy(this, Solution.choose(problem))
+ //parent.partlySolvedBy(this, Solution.choose(problem))
}
}
@@ -86,9 +89,6 @@ class Task(synth: Synthesizer,
this.solution = Some(solution)
parent.partlySolvedBy(this, solution)
- val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
- synth.reporter.info(prefix+"Got: "+problem)
- synth.reporter.info(prefix+"Solved with: "+solution)
Nil
case RuleMultiSteps(subProblems, interSteps, onSuccess) =>
@@ -102,12 +102,6 @@ class Task(synth: Synthesizer,
val simplestSubSolutions = interSteps.foldLeft(subProblems.map(Solution.basic(_))){ (sols, step) => step(sols).map(Solution.basic(_)) }
val simplestSolution = onSuccess(simplestSubSolutions)._1
minComplexity = new FixedSolComplexity(parent.minComplexity.value + simplestSolution.complexity.value)
- val prefix = "[%-20s] ".format(Option(rule).map(_.toString).getOrElse("root"))
- synth.reporter.info(prefix+"Got: "+problem)
- synth.reporter.info(prefix+"Decomposed into:")
- for(p <- subProblems) {
- synth.reporter.info(prefix+" - "+p)
- }
subProblems
@@ -127,6 +121,8 @@ class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, p
List(problem)
}
+ override def isSolved = solver.isDefined
+
override def partlySolvedBy(t: Task, s: Solution) {
if (isBetterSolutionThan(s, solution)) {
solution = Some(s)
--
GitLab