diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala index b7c3e1feddb15eac004b4d1dbae134777a008a62..63db3ca0a70d718ae6aacd84b7c449d29efa866b 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 4bf92ad330cc6a2e1243a25eaae353ceb132a4d4..a9d18d5b5d10aa90e16d623b674bdd75c88548a7 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)) {