From 862613e1fc9b34da4ab5a5d5a9b31e64b5c0819f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 2 Nov 2012 16:36:20 +0100
Subject: [PATCH] This tends to guarantee termination, better handling of
giveups
---
.../scala/leon/synthesis/Heuristics.scala | 2 +-
src/main/scala/leon/synthesis/Rules.scala | 9 +------
.../scala/leon/synthesis/Synthesizer.scala | 18 ++++++++++---
src/main/scala/leon/synthesis/Task.scala | 27 +++++++++++++++++--
4 files changed, 41 insertions(+), 15 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index c1ad89415..f96ecacbf 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, 50) {
+class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 8, 100) {
def applyOn(task: Task): RuleResult = {
val p = task.problem
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 7210ef271..51e1c02ea 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -17,8 +17,7 @@ object Rules {
new CaseSplit(synth),
new UnusedInput(synth),
new UnconstrainedOutput(synth),
- new Assert(synth),
- new GiveUp(synth)
+ new Assert(synth)
)
}
@@ -276,9 +275,3 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 20, 0) {
}
}
-class GiveUp(synth: Synthesizer) extends Rule("GiveUp", synth, -100000, 100) {
- def applyOn(task: Task): RuleResult = {
- RuleSuccess(Solution.choose(task.problem))
- }
-}
-
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index d18bd0cb1..0739733ea 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -28,16 +28,26 @@ 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
while (!workList.isEmpty && !(firstOnly && rootTask.solution.isDefined)) {
val task = workList.dequeue()
- val subProblems = task.run
-
- for (p <- subProblems; r <- rules) yield {
- workList += new Task(this, task, p, r)
+ 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 {
+ val subProblems = task.run
+
+ for (p <- subProblems; r <- rules) yield {
+ workList += new Task(this, task, p, r)
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index fd4e8a2c9..c1c5bdb69 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -2,7 +2,7 @@ package leon
package synthesis
class Task(synth: Synthesizer,
- parent: Task,
+ val parent: Task,
val problem: Problem,
val rule: Rule) extends Ordered[Task] {
@@ -34,6 +34,17 @@ class Task(synth: Synthesizer,
}
}
+ var failures = Set[Rule]()
+ def unsolvedBy(t: Task) {
+ failures += t.rule
+
+ if (failures.size == synth.rules.size) {
+ // We might want to report unsolved instead of solvedByChoose, depending
+ // on the cases
+ parent.partlySolvedBy(this, Solution.choose(problem))
+ }
+ }
+
def run: List[Problem] = {
rule.applyOn(this) match {
case RuleSuccess(solution) =>
@@ -48,6 +59,7 @@ class Task(synth: Synthesizer,
subProblems
case RuleInapplicable =>
+ parent.unsolvedBy(this)
Nil
}
}
@@ -62,13 +74,24 @@ class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, p
override lazy val minSolutionCost = 0
- override def partlySolvedBy(t: Task, s: Solution) = {
+ override def partlySolvedBy(t: Task, s: Solution) {
if (isBetterSolutionThan(s, solution)) {
solution = Some(s)
solver = Some(t)
}
}
+ override def unsolvedBy(t: Task) {
+ failures += t.rule
+
+ if (failures.size == synth.rules.size) {
+ // We might want to report unsolved instead of solvedByChoose, depending
+ // on the cases
+ solution = Some(Solution.choose(problem))
+ solver = None
+ }
+ }
+
override def run: List[Problem] = {
List(problem)
}
--
GitLab