diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 72d87cec11eade2afab25312c5438725a461073c..b76d05c6064b7c5f33760e6e7cc58429403ad38e 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -68,6 +68,16 @@ object PrettyPrinter {
private def pp(tree: Expr, sb: StringBuffer, lvl: Int): StringBuffer = tree match {
case Variable(id) => sb.append(id)
case DeBruijnIndex(idx) => sb.append("_" + idx)
+ case LetTuple(bs,d,e) => {
+ //pp(e, pp(d, sb.append("(let (" + b + " := "), lvl).append(") in "), lvl).append(")")
+ sb.append("(let (" + bs.mkString(",") + " := ");
+ pp(d, sb, lvl)
+ sb.append(") in\n")
+ ind(sb, lvl+1)
+ pp(e, sb, lvl+1)
+ sb.append(")")
+ sb
+ }
case Let(b,d,e) => {
//pp(e, pp(d, sb.append("(let (" + b + " := "), lvl).append(") in "), lvl).append(")")
sb.append("(let (" + b + " := ");
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index e32b3dd7a888b3cc04dbb9ab43e3ff7823d74777..259ce7911c506e0b9f9f801c0d8d09f2542f4cfe 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -59,12 +59,12 @@ object Trees {
setType(et)
}
- //case class LetTuple(binders: Seq[Identifier], value: Expr, body: Expr) extends Expr {
- // binders.foreach(_.markAsLetBinder)
- // val et = body.getType
- // if(et != Untyped)
- // setType(et)
- //}
+ case class LetTuple(binders: Seq[Identifier], value: Expr, body: Expr) extends Expr {
+ binders.foreach(_.markAsLetBinder)
+ val et = body.getType
+ if(et != Untyped)
+ setType(et)
+ }
case class LetDef(value: FunDef, body: Expr) extends Expr {
val et = body.getType
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index b9dc74af176689e0a534bb6c753051781ac06a87..83ed51723781298115c03088ac2370a0ce938c37 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -1,11 +1,57 @@
package leon
package synthesis
+import purescala.Trees._
+
object Rules {
- def all = List()
+ def all = List(
+ OnePoint
+ )
}
abstract class Rule(val name: String) {
def isApplicable(p: Problem, parent: Task): List[Task]
}
+
+object OnePoint extends Rule("One-point") {
+ def isApplicable(p: Problem, parent: Task): List[Task] = {
+
+ p.phi match {
+ case And(exprs) =>
+ val candidates = exprs.collect {
+ case eq @ Equals(Variable(x), e) if (p.xs contains x) && !(variablesOf(e) contains x) =>
+ (x, e, eq)
+ case eq @ Equals(e, Variable(x)) if (p.xs contains x) && !(variablesOf(e) contains x) =>
+ (x, e, eq)
+ }
+
+ if (!candidates.isEmpty) {
+ val (x, e, eq) = candidates.head
+
+ val others = exprs.filter(_ != eq)
+ val oxs = p.xs.filter(_ != x)
+
+ val newProblem = Problem(p.as, replace(Map(Variable(x) -> e), And(others)), oxs)
+
+ val onSuccess: List[Solution] => Solution = {
+ case List(Solution(pre, term)) =>
+ if (oxs.isEmpty) {
+ Solution(pre, e)
+ } else {
+ Solution(pre, LetTuple(oxs, term, replace(Map(Variable(x) -> e), Tuple(p.xs.map(Variable(_))))) )
+ }
+ case _ => Solution.none
+ }
+
+ List(new Task(parent, p, List(newProblem), onSuccess, 100))
+ } else {
+ Nil
+ }
+
+
+ case _ =>
+ Nil
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index f59c8b693e0b1fd17f482d551e3eb3c9f15dedda..8346a9a60f95474f0e4a325687aec390cbc5ed6a 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -11,4 +11,6 @@ case class Solution(pre: Expr, term: Expr) {
object Solution {
def choose(p: Problem): Solution = Solution(BooleanLiteral(true), Choose(p.xs, p.phi))
+
+ def none: Solution = throw new Exception("Unexpected failure to construct solution")
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index ab5f75432c13de551f0eb0ba525a8f10516314c1..94fa516d58868b2fcf050fe2c08c63e130711691 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -38,7 +38,7 @@ class Synthesizer(rules: List[Rule]) {
alternatives.find(_.isSuccess) match {
case Some(ss) =>
- ss.onSuccess()
+ ss.succeeded()
case None =>
workList ++= alternatives
}
@@ -46,7 +46,7 @@ class Synthesizer(rules: List[Rule]) {
// We are stuck
if (alternatives.isEmpty) {
// I give up
- task.onSuccess(sp, Solution.choose(sp))
+ task.subSucceeded(sp, Solution.choose(sp))
}
}
}
@@ -65,9 +65,9 @@ class Synthesizer(rules: List[Rule]) {
import purescala.Trees._
import purescala.TypeTrees._
- val aID = FreshIdentifier("a").setType(Int32Type)
- val a = Variable(aID)
- val p = Problem(Nil, And(GreaterThan(a, IntLiteral(2)), Equals(a, IntLiteral(3))), List(aID))
+ val x = Variable(FreshIdentifier("x").setType(Int32Type))
+ val y = Variable(FreshIdentifier("y").setType(Int32Type))
+ val p = Problem(Nil, And(GreaterThan(x, y), Equals(x, IntLiteral(3))), List(x.id, y.id))
synthesize(p)
}
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 69a3232808e305ca445aebee1fb220fa3a6c53c2..2b8d6ad8862a03e688157f27759aae17ca976631 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -5,7 +5,7 @@ class Task(
val parent: Task,
val problem: Problem,
val subProblems: List[Problem],
- val construct: List[Solution] => Solution,
+ val onSuccess: List[Solution] => Solution,
val score: Score
) extends Ordered[Task] {
@@ -15,12 +15,12 @@ class Task(
def isSuccess = subProblems.isEmpty
- def onSuccess() {
+ def succeeded() {
assert(isSuccess)
- notifyParent(construct(Nil))
+ notifyParent(onSuccess(Nil))
}
- def onSuccess(p: Problem, s: Solution) {
+ def subSucceeded(p: Problem, s: Solution) {
assert(subProblems contains p)
assert(!(subSolutions contains p))
@@ -28,16 +28,16 @@ class Task(
if (subSolutions.size == subProblems.size) {
- val solution = construct(subProblems map subSolutions)
+ val solution = onSuccess(subProblems map subSolutions)
- println(": "+problem+" ⊢ "+solution)
+ println("Found solution to: "+problem+" ⊢ "+solution)
notifyParent(solution)
}
}
def notifyParent(solution: Solution) {
- parent.onSuccess(problem, solution)
+ parent.subSucceeded(problem, solution)
}
}