From e21eea0f5b8a7901247ac38d294b331c374ae59f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 19 Oct 2012 17:55:14 +0200
Subject: [PATCH] This may work
---
src/main/scala/leon/synthesis/Problem.scala | 2 +-
src/main/scala/leon/synthesis/Solution.scala | 5 ++---
.../scala/leon/synthesis/Synthesizer.scala | 19 +++++++++++++++++--
3 files changed, 20 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index b62d73254..8571c7648 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -6,6 +6,6 @@ import leon.purescala.Common._
// Defines a synthesis triple of the form:
// ⟦ as ⟨ phi ⟩ xs ⟧
-case class Problem(as: Set[Identifier], phi: Expr, xs: Set[Identifier]) {
+case class Problem(as: List[Identifier], phi: Expr, xs: List[Identifier]) {
override def toString = "⟦ "+as.mkString(";")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 30e19b2ef..f59c8b693 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -1,7 +1,7 @@
package leon
package synthesis
-import leon.purescala.Trees.Expr
+import leon.purescala.Trees._
// Defines a synthesis solution of the form:
// ⟨ P | T ⟩
@@ -10,6 +10,5 @@ case class Solution(pre: Expr, term: Expr) {
}
object Solution {
- def fromProblem(p: Problem): Solution =
- null
+ def choose(p: Problem): Solution = Solution(BooleanLiteral(true), Choose(p.xs, p.phi))
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 6699bc080..ba4c3c4f1 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -26,9 +26,24 @@ class Synthesizer(rules: List[Rule]) {
task.subProblems match {
case Nil =>
- task.onSuccess()
+ throw new Exception("Such tasks shouldbe handled immediately")
case subProblems =>
- workList ++= subProblems.flatMap(applyRules(_, task))
+ for (sp <- subProblems) {
+ val alternatives = applyRules(sp, task)
+
+ alternatives.find(_.isSuccess) match {
+ case Some(ss) =>
+ ss.onSuccess()
+ case None =>
+ workList ++= alternatives
+ }
+
+ // We are stuck
+ if (alternatives.isEmpty) {
+ // I give up
+ task.onSuccess(sp, Solution.choose(sp))
+ }
+ }
}
}
--
GitLab