From 730c2fabb07f3ae00ff87a370635670c08875846 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 14 Nov 2012 21:49:19 +0100
Subject: [PATCH] More precise isSolved
---
src/main/scala/leon/synthesis/Synthesizer.scala | 6 +-----
src/main/scala/leon/synthesis/Task.scala | 4 ++--
2 files changed, 3 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index b7c3e1fed..63db3ca0a 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -56,7 +56,7 @@ class Synthesizer(val reporter: Reporter,
val prefix = "[%-20s] ".format(Option(task.rule).map(_.toString).getOrElse("root"))
- if (!(firstOnly && (task.parent ne null) && task.parent.isSolved)) {
+ if (!(firstOnly && (task.parent ne null) && task.parent.isSolved(task.problem))) {
val subProblems = task.run()
if (task.minComplexity <= bestSolutionSoFar.complexity) {
@@ -73,11 +73,7 @@ class Synthesizer(val reporter: Reporter,
}
}
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 4bf92ad33..a9d18d5b5 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -40,7 +40,7 @@ class Task(synth: Synthesizer,
def currentStep = steps.head
- def isSolved: Boolean = parent.isSolved || (nextSteps.isEmpty && (currentStep.subSolutions.size == currentStep.subProblems.size))
+ def isSolved(problem: Problem): Boolean = parent.isSolved(this.problem) || (currentStep.subSolutions contains problem)
def partlySolvedBy(t: Task, s: Solution) {
if (isBetterSolutionThan(s, currentStep.subSolutions.get(t.problem))) {
@@ -121,7 +121,7 @@ class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, p
List(problem)
}
- override def isSolved = solver.isDefined
+ override def isSolved(problem: Problem) = solver.isDefined
override def partlySolvedBy(t: Task, s: Solution) {
if (isBetterSolutionThan(s, solution)) {
--
GitLab