diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c60c0ca4d6b3d4afe4ecdab4171c088131817c62
--- /dev/null
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -0,0 +1,4 @@
+package leon
+package synthesis
+
+case class Problem();
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
new file mode 100644
index 0000000000000000000000000000000000000000..767f7584d5922ff5acbbe091a37e80017e38c223
--- /dev/null
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -0,0 +1,11 @@
+package leon
+package synthesis
+
+/** AST definitions for Pure Scala. */
+object Rules {
+
+  abstract class Rule {
+    def isApplicable(p: Problem): Option[Step];
+  }
+
+}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cdc4dcab6b2b4c50069c8347488d13211a5dc0f6
--- /dev/null
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -0,0 +1,4 @@
+package leon
+package synthesis
+
+case class Solution();
diff --git a/src/main/scala/leon/synthesis/Step.scala b/src/main/scala/leon/synthesis/Step.scala
new file mode 100644
index 0000000000000000000000000000000000000000..12cad391a745e6f9bc3aec2b4aff54ceefc5cee5
--- /dev/null
+++ b/src/main/scala/leon/synthesis/Step.scala
@@ -0,0 +1,4 @@
+package leon
+package synthesis
+
+case class Step(subProblems: List[Problem], construct: List[Solution] => Solution, score: Score);
diff --git a/src/main/scala/leon/synthesis/package.scala b/src/main/scala/leon/synthesis/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6e628ecffd37a795b1c63912f31c0c38d624bba1
--- /dev/null
+++ b/src/main/scala/leon/synthesis/package.scala
@@ -0,0 +1,6 @@
+package leon
+
+package object synthesis {
+  type Score = Int
+
+}