From 2d495c3f56c704aabe7e44cd71988aea6bb13746 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 24 Oct 2012 16:48:02 +0200
Subject: [PATCH] Fix derivation generations, genreate dot files
---
.../scala/leon/synthesis/Synthesizer.scala | 31 +++++++++++++------
src/main/scala/leon/synthesis/Task.scala | 2 +-
testcases/synthesis/Spt.scala | 2 ++
3 files changed, 24 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index daebf0f41..b754201f2 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -14,14 +14,19 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
import r.{error,warning,info,fatalError}
private[this] var solution: Option[Solution] = None
+ private[this] var derivationTree: DerivationTree = _
+
+ var derivationCounter = 1;
def synthesize(p: Problem, rules: List[Rule]): Solution = {
val workList = new PriorityQueue[Task]()
val rootTask = new RootTask(this, p)
+
workList += rootTask
solution = None
+ derivationTree = new DerivationTree(rootTask)
while (!workList.isEmpty && solution.isEmpty) {
val task = workList.dequeue()
@@ -48,9 +53,25 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
}
}
+
+ derivationTree.toDotFile("derivation"+derivationCounter+".dot")
+ derivationCounter += 1
+
solution.getOrElse(Solution.none)
}
+ def onTaskSucceeded(task: Task, solution: Solution) {
+ info(" => Solved "+task.problem+" ⊢ "+solution)
+ derivationTree.recordSolutionFor(task, solution)
+
+ if (task.parent eq null) {
+ info(" SUCCESS!")
+ this.solution = Some(solution)
+ } else {
+ task.parent.subSucceeded(task.problem, solution)
+ }
+ }
+
def solveSAT(phi: Expr): (Option[Boolean], Map[Identifier, Expr]) = {
for (s <- solvers) {
s.solveOrGetCounterexample(Not(phi)) match {
@@ -64,16 +85,6 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
(None, Map())
}
- def onTaskSucceeded(task: Task, solution: Solution) {
- info(" => Solved "+task.problem+" ⊢ "+solution)
- if (task.parent eq null) {
- info(" SUCCESS!")
- this.solution = Some(solution)
- } else {
- task.parent.subSucceeded(task.problem, solution)
- }
- }
-
def synthesizeAll(program: Program) = {
import purescala.Trees._
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 73858e295..d73a7f58a 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -29,7 +29,7 @@ class DecomposedTask(synth: Synthesizer,
def subTasks = subProblems.map(new Task(synth, this, _, score))
- var subSolutions = Map[Problem, Solution]()
+ var subSolutions = Map[Problem, Solution]()
def isSuccess = subProblems.isEmpty
diff --git a/testcases/synthesis/Spt.scala b/testcases/synthesis/Spt.scala
index 3a797a9b1..99cc01287 100644
--- a/testcases/synthesis/Spt.scala
+++ b/testcases/synthesis/Spt.scala
@@ -15,6 +15,8 @@ object SynthesisProceduresToolkit {
def e6(a: Nat, b: Nat): (Nat, NatList) = choose( (x: Nat, y: NatList) => a == Succ(b))
+ def e7(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = choose( (x1 : Nat, x2 : NatList, x3 : Nat, x4 : NatList) => Cons(Succ(x1), x2) == a1 && Succ(x1) != a2 && a3 == Cons(x3, Cons(x3, x4)) || (a1 == a3 && x1 == x3))
+
abstract class Nat
case class Z() extends Nat
case class Succ(n: Nat) extends Nat
--
GitLab