diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index c60c0ca4d6b3d4afe4ecdab4171c088131817c62..b62d73254fc0f13b32d463f78498943b5b0eda0e 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 767f7584d5922ff5acbbe091a37e80017e38c223..7cedb5d0207e1fd01f591e09ccd621cb2b7a93d5 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 cdc4dcab6b2b4c50069c8347488d13211a5dc0f6..30e19b2efed7bd26d2fac900b66cc8666144b98c 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 12cad391a745e6f9bc3aec2b4aff54ceefc5cee5..0000000000000000000000000000000000000000
--- 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 0000000000000000000000000000000000000000..6699bc080167b435a854733214d0dd19ce1385d5
--- /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 0000000000000000000000000000000000000000..959f564527048e6896c646cd76f693c721fd8346
--- /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 6e628ecffd37a795b1c63912f31c0c38d624bba1..30c04b2f5f3eaaabcde5f3765c7000597fccbd3e 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
-
 }