From ea95a62f98d1439777f95395d4fce73191f18d9b Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 19 Oct 2012 16:29:10 +0200
Subject: [PATCH] This is madness
---
src/main/scala/leon/synthesis/Problem.scala | 9 +++-
src/main/scala/leon/synthesis/Rules.scala | 9 +---
src/main/scala/leon/synthesis/Solution.scala | 13 +++++-
src/main/scala/leon/synthesis/Step.scala | 4 --
.../scala/leon/synthesis/Synthesizer.scala | 39 +++++++++++++++++
src/main/scala/leon/synthesis/Task.scala | 43 +++++++++++++++++++
src/main/scala/leon/synthesis/package.scala | 1 -
7 files changed, 104 insertions(+), 14 deletions(-)
delete mode 100644 src/main/scala/leon/synthesis/Step.scala
create mode 100644 src/main/scala/leon/synthesis/Synthesizer.scala
create mode 100644 src/main/scala/leon/synthesis/Task.scala
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index c60c0ca4d..b62d73254 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -1,4 +1,11 @@
package leon
package synthesis
-case class Problem();
+import leon.purescala.Trees._
+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]) {
+ override def toString = "⟦ "+as.mkString(";")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
+}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 767f7584d..7cedb5d02 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -1,11 +1,6 @@
package leon
package synthesis
-/** AST definitions for Pure Scala. */
-object Rules {
-
- abstract class Rule {
- def isApplicable(p: Problem): Option[Step];
- }
-
+abstract class Rule(val name: String) {
+ def isApplicable(p: Problem, parent: Task): List[Task]
}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index cdc4dcab6..30e19b2ef 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -1,4 +1,15 @@
package leon
package synthesis
-case class Solution();
+import leon.purescala.Trees.Expr
+
+// Defines a synthesis solution of the form:
+// ⟨ P | T ⟩
+case class Solution(pre: Expr, term: Expr) {
+ override def toString = "⟨ "+pre+" | "+term+" ⟩"
+}
+
+object Solution {
+ def fromProblem(p: Problem): Solution =
+ null
+}
diff --git a/src/main/scala/leon/synthesis/Step.scala b/src/main/scala/leon/synthesis/Step.scala
deleted file mode 100644
index 12cad391a..000000000
--- a/src/main/scala/leon/synthesis/Step.scala
+++ /dev/null
@@ -1,4 +0,0 @@
-package leon
-package synthesis
-
-case class Step(subProblems: List[Problem], construct: List[Solution] => Solution, score: Score);
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
new file mode 100644
index 000000000..6699bc080
--- /dev/null
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -0,0 +1,39 @@
+package leon
+package synthesis
+
+import collection.mutable.PriorityQueue
+
+class Synthesizer(rules: List[Rule]) {
+ def applyRules(p: Problem, parent: Task): List[Task] = {
+ rules.flatMap(_.isApplicable(p, parent))
+ }
+
+ def synthesize(p: Problem): Solution = {
+ val workList = new PriorityQueue[Task]()
+
+ var solution: Solution = null
+
+ val rootTask = new RootTask(p) {
+ override def notifyParent(s: Solution) {
+ solution = s
+ }
+ }
+
+ workList += rootTask
+
+ while (!workList.isEmpty) {
+ val task = workList.dequeue()
+
+ task.subProblems match {
+ case Nil =>
+ task.onSuccess()
+ case subProblems =>
+ workList ++= subProblems.flatMap(applyRules(_, task))
+ }
+
+ }
+
+ solution
+ }
+}
+
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
new file mode 100644
index 000000000..959f56452
--- /dev/null
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -0,0 +1,43 @@
+package leon
+package synthesis
+
+class Task(
+ val parent: Task,
+ val problem: Problem,
+ val subProblems: List[Problem],
+ val construct: List[Solution] => Solution,
+ val score: Score
+ ) extends Ordered[Task] {
+
+ var subSolutions = Map[Problem, Solution]()
+
+ def compare(that: Task) = this.score - that.score
+
+ def isSuccess = subProblems.isEmpty
+
+ def onSuccess() {
+ assert(isSuccess)
+ notifyParent(construct(Nil))
+ }
+
+ def onSuccess(p: Problem, s: Solution) {
+ assert(subProblems contains p)
+ assert(!(subSolutions contains p))
+
+ subSolutions += p -> s
+
+ if (subSolutions.size == subProblems.size) {
+ notifyParent(construct(subProblems map subSolutions))
+ }
+ }
+
+ def notifyParent(solution: Solution) {
+ parent.onSuccess(problem, solution)
+ }
+}
+
+class RootTask(p: Problem) extends Task(null, p, List(p), xs => xs.head, 0) {
+ override def notifyParent(solution: Solution) {
+ sys.error("You need to extend this!")
+ }
+}
diff --git a/src/main/scala/leon/synthesis/package.scala b/src/main/scala/leon/synthesis/package.scala
index 6e628ecff..30c04b2f5 100644
--- a/src/main/scala/leon/synthesis/package.scala
+++ b/src/main/scala/leon/synthesis/package.scala
@@ -2,5 +2,4 @@ package leon
package object synthesis {
type Score = Int
-
}
--
GitLab