From 8af26bbf67b6b441e143e878507e3267890e740d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 19 Nov 2012 14:04:16 +0100
Subject: [PATCH] Fix compilation and various things
---
.../scala/leon/synthesis/DerivationTree.scala | 4 ++--
src/main/scala/leon/synthesis/Task.scala | 17 +++++++++++------
2 files changed, 13 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/synthesis/DerivationTree.scala b/src/main/scala/leon/synthesis/DerivationTree.scala
index c409f4020..eae0104f4 100644
--- a/src/main/scala/leon/synthesis/DerivationTree.scala
+++ b/src/main/scala/leon/synthesis/DerivationTree.scala
@@ -37,7 +37,7 @@ class DerivationTree(root: RootTask) {
res append " "+node+" [ label = <<TABLE BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"><TR><TD BORDER=\"0\">"+t.rule+"</TD></TR><TR><TD BGCOLOR=\"indianred1\">"+escapeHTML(t.problem.toString)+"</TD></TR><TR><TD BGCOLOR=\"greenyellow\">"+escapeHTML(t.solution.map(_.toString).getOrElse("?"))+"</TD></TR></TABLE>> shape = \"none\" ];\n"
- for (st <- t.steps.flatMap(_.subSolvers.values)) {
+ for (st <- t.solver.map(_.allSteps).flatten.flatMap(_.subSolvers.values)) {
res.append(" "+taskName(st)+" -> "+node+"\n")
printTask(st)
}
@@ -45,7 +45,7 @@ class DerivationTree(root: RootTask) {
}
- root.solver.foreach(printTask)
+ root.solverTask.foreach(printTask)
res append "}\n"
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 97b4a9b03..2e565bbad 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -25,6 +25,8 @@ class Task(synth: Synthesizer,
}
var solution: Option[Solution] = None
+ var solver: Option[RuleApplication] = None
+
var alternatives = Set[RuleApplication]()
var minComplexity: AbsSolComplexity = new FixedSolComplexity(0)
@@ -66,9 +68,12 @@ class Task(synth: Synthesizer,
} else {
onSuccess(solutions) match {
case (s, true) =>
- solution = Some(s)
+ if (isBetterSolutionThan(s, solution)) {
+ solution = Some(s)
+ solver = Some(this)
- parent.partlySolvedBy(Task.this, solution.get)
+ parent.partlySolvedBy(Task.this, s)
+ }
case _ =>
// solution is there, but it is incomplete (precondition not strongest)
//parent.partlySolvedBy(this, Solution.choose(problem))
@@ -117,18 +122,18 @@ class Task(synth: Synthesizer,
}
class RootTask(synth: Synthesizer, problem: Problem) extends Task(synth, null, problem, null) {
- var solver: Option[Task] = None
+ var solverTask: Option[Task] = None
override def run() = {
List(problem)
}
- override def isSolvedFor(problem: Problem) = solver.isDefined
+ override def isSolvedFor(problem: Problem) = solverTask.isDefined
override def partlySolvedBy(t: Task, s: Solution) {
if (isBetterSolutionThan(s, solution)) {
- solution = Some(s)
- solver = Some(t)
+ solution = Some(s)
+ solverTask = Some(t)
}
}
}
--
GitLab