diff --git a/project/Build.scala b/project/Build.scala
index 1d9e5787079bdc800c0fb84c0a383ce9242630ea..5adc5a3b2e85fe55bff012340b5a34de9750188d 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -48,7 +48,7 @@ object Leon extends Build {
val sourceGen = {
sourceGenerators in Compile += Def.task {
- val libFiles = (file("library") ** "*.scala").getPaths.mkString("List(\"", "\", \"", "\")")
+ val libFiles = ((baseDirectory.value / "library") ** "*.scala").getPaths.mkString("List(\"", "\", \"", "\")")
val build = (sourceManaged in Compile).value / "leon" / "Build.scala";
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 9cc1baf3b8fb50b564cf38fc3cc88a3496b8ed88..5d97ff9891c62b61f8fc0827b5f25036fc7f14b7 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -169,8 +169,10 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
|$e"""
}
case LetDef(fd,body) =>
- p"""|$fd
- |$body"""
+ optB {
+ p"""|$fd
+ |$body"""
+ }
case Require(pre, body) =>
p"""|require($pre)
@@ -475,6 +477,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
def requiresBraces(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
case (pa: PrettyPrintable, _) => pa.printRequiresBraces(within)
case (_, None) => false
+ case (_: LetDef, Some(_: FunDef)) => true
case (_: Require, Some(_: Ensuring)) => false
case (_: Require, _) => true
case (_: Assert, Some(_: Definition)) => true
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 36c52c05935e82fa9a5674ab105a3b86c457c2b1..4bca1518def1b35d63ab6ff5d3bfeb67bd084efa 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -435,7 +435,7 @@ object TreeOps {
case TupleSelect(LetTuple(ids, v, b), ts) =>
Some(LetTuple(ids, v, TupleSelect(b, ts)))
- case IfExpr(c, thenn, elze) if (thenn == elze) =>
+ case IfExpr(c, thenn, elze) if (thenn == elze) && !containsChoose(e) =>
Some(thenn)
case IfExpr(c, BooleanLiteral(true), BooleanLiteral(false)) =>
@@ -1943,7 +1943,44 @@ object TreeOps {
def postMapOnFunDef(repl : Expr => Option[Expr], applyRec : Boolean = false )(funDef : FunDef) : FunDef = {
applyOnFunDef(postMap(repl, applyRec))(funDef)
}
+
+ /**
+ * Used to lift closures introduced by synthesis. Closures already define all
+ * the necessary information as arguments, no need to close them.
+ */
+ def liftClosures(e: Expr): (Set[FunDef], Expr) = {
+ var fds: Set[FunDef] = Set()
+
+ val res = postMap{
+ case LetDef(fd, b) =>
+ fds += fd
+ Some(b)
+ case _ =>
+ None
+ }(e)
+
+ (fds, res)
+ }
+ def preTraversalWithParent(f: (Expr, Option[Tree]) => Unit, initParent: Option[Tree] = None)(e: Expr): Unit = {
+ val rec = preTraversalWithParent(f, Some(e)) _
+
+ f(e, initParent)
+
+ e match {
+ case u @ UnaryOperator(e, builder) =>
+ rec(e)
+
+ case b @ BinaryOperator(e1, e2, builder) =>
+ rec(e1)
+ rec(e2)
+
+ case n @ NAryOperator(es, builder) =>
+ es.foreach(rec)
+
+ case t: Terminal =>
+ }
+ }
/**
* Deprecated API
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index 4874fa838a6a4e6a65189315cfa15f8b99f09c32..26d1229f45c62c52e39c02d194df733852092035 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -46,8 +46,7 @@ class FileInterface(reporter: Reporter) {
}
}
- def substitute(str: String, fromTree: Tree, toTree: Tree): String = {
-
+ def substitute(str: String, fromTree: Tree, printer: (Int) => String): String = {
fromTree.getPos match {
case rp: RangePosition =>
val from = rp.pointFrom
@@ -61,16 +60,24 @@ class FileInterface(reporter: Reporter) {
val indent = lineChars.takeWhile(_ == ' ').size
- val p = new ScalaPrinter(PrinterOptions())
- p.pp(toTree)(PrinterContext(toTree, Some(fromTree), indent/2, p))
+ val res = printer(indent/2)
- before + "{" + p.toString + "}" + after
+ before + res + after
case p =>
sys.error("Substitution requires RangePos on the input tree: "+fromTree +": "+fromTree.getClass+" GOT" +p)
}
}
+
+ def substitute(str: String, fromTree: Tree, toTree: Tree): String = {
+ substitute(str, fromTree, (indent: Int) => {
+ val p = new ScalaPrinter(PrinterOptions())
+ p.pp(toTree)(PrinterContext(toTree, None, indent, p))
+ p.toString
+ })
+ }
+
def readFile(file: File): String = {
scala.io.Source.fromFile(file).mkString
}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 1de672ad9355eef54aacef3d6ffb4c330f735429..65edb8ff8b23a44ed7810b48666d8a8f14c299a4 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -12,21 +12,25 @@ import purescala.ScopeSimplifier
import solvers.z3._
import solvers._
+import leon.utils.Simplifiers
+
// Defines a synthesis solution of the form:
// ⟨ P | T ⟩
class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr) {
override def toString = "⟨ "+pre+" | "+defs.mkString(" ")+" "+term+" ⟩"
- def toExpr = {
- val result = if (pre == BooleanLiteral(true)) {
+ def guardedTerm = {
+ if (pre == BooleanLiteral(true)) {
term
} else if (pre == BooleanLiteral(false)) {
Error("Impossible program").setType(term.getType)
} else {
IfExpr(pre, term, Error("Precondition failed").setType(term.getType))
}
+ }
- defs.foldLeft(result){ case (t, fd) => LetDef(fd, t) }
+ def toExpr = {
+ defs.foldLeft(guardedTerm){ case (t, fd) => LetDef(fd, t) }
}
// Projects a solution (ignore several output variables)
@@ -48,35 +52,8 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr) {
}
- def fullTerm =
- defs.foldLeft(term){ case (t, fd) => LetDef(fd, t) }
-
def toSimplifiedExpr(ctx: LeonContext, p: Program): Expr = {
- val uninterpretedZ3 = SolverFactory(() => new UninterpretedZ3Solver(ctx, p))
-
- val simplifiers = List[Expr => Expr](
- simplifyTautologies(uninterpretedZ3)(_),
- simplifyLets _,
- decomposeIfs _,
- matchToIfThenElse _,
- simplifyPaths(uninterpretedZ3)(_),
- patternMatchReconstruction _,
- rewriteTuples _,
- evalGround(ctx, p),
- normalizeExpression _
- )
-
- val simple = { expr: Expr =>
- simplifiers.foldLeft(expr){ case (x, sim) =>
- sim(x)
- }
- }
-
- // Simplify first using stable simplifiers
- val s = fixpoint(simple, 5)(toExpr)
-
- // Clean up ids/names
- (new ScopeSimplifier).transform(s)
+ Simplifiers.bestEffort(ctx, p)(toExpr)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 7a6c7f0b943fa8e1ceed38e62d857dac8f767aa9..7ebe6c9cb05ee004ac62092b8b947b5c55acb067 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -466,8 +466,8 @@ case object CEGIS extends Rule("CEGIS") {
var unrolings = 0
val maxUnrolings = 3
- val exSolverTo = 3000L
- val cexSolverTo = 3000L
+ val exSolverTo = 2000L
+ val cexSolverTo = 2000L
var baseExampleInputs: Seq[Seq[Expr]] = Seq()
diff --git a/src/main/scala/leon/utils/Simplifiers.scala b/src/main/scala/leon/utils/Simplifiers.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3fef391d759a24db824745b0953c1f03107ae88c
--- /dev/null
+++ b/src/main/scala/leon/utils/Simplifiers.scala
@@ -0,0 +1,40 @@
+package leon
+package utils
+
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.ScopeSimplifier
+import solvers.z3.UninterpretedZ3Solver
+import solvers._
+
+object Simplifiers {
+
+ def bestEffort(ctx: LeonContext, p: Program)(e: Expr): Expr = {
+ val uninterpretedZ3 = SolverFactory(() => new UninterpretedZ3Solver(ctx, p))
+
+ val simplifiers = List[Expr => Expr](
+ simplifyTautologies(uninterpretedZ3)(_),
+ simplifyLets _,
+ decomposeIfs _,
+ matchToIfThenElse _,
+ simplifyPaths(uninterpretedZ3)(_),
+ patternMatchReconstruction _,
+ rewriteTuples _,
+ evalGround(ctx, p),
+ normalizeExpression _
+ )
+
+ val simple = { expr: Expr =>
+ simplifiers.foldLeft(expr){ case (x, sim) =>
+ sim(x)
+ }
+ }
+
+ // Simplify first using stable simplifiers
+ val s = fixpoint(simple, 5)(e)
+
+ // Clean up ids/names
+ (new ScopeSimplifier).transform(s)
+ }
+}
diff --git a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
index 000977b687963f2e1e58e54c9a315e31140fc060..6b9bf910c29b17fd6be77920e29157087f528a44 100644
--- a/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
+++ b/src/test/scala/leon/test/synthesis/StablePrintingSuite.scala
@@ -6,8 +6,11 @@ package synthesis
import leon._
import leon.purescala.Definitions._
+import leon.purescala.Common._
import leon.purescala.Trees._
import leon.purescala.ScalaPrinter
+import leon.purescala.PrinterContext
+import leon.purescala.PrinterOptions
import leon.purescala.TreeOps._
import leon.solvers.z3._
import leon.solvers.Solver
@@ -75,6 +78,7 @@ class StablePrintingSuite extends LeonTestSuite {
for (e <- reporter.lastErrors) {
info(e)
}
+ info(e.getMessage)
fail("Compilation failed")
}
@@ -92,7 +96,13 @@ class StablePrintingSuite extends LeonTestSuite {
a.onSuccess(sub.map(Solution.choose(_))) match {
case Some(sol) =>
val result = sol.toSimplifiedExpr(ctx, pgm)
- val newContent = new FileInterface(ctx.reporter).substitute(j.content, ci.ch, result)
+
+ val newContent = new FileInterface(ctx.reporter).substitute(j.content, ci.ch, (indent: Int) => {
+ val p = new ScalaPrinter(PrinterOptions())
+ p.pp(result)(PrinterContext(result, Some(ci.fd), indent, p))
+ p.toString
+ })
+
workList push Job(newContent, (i to i+sub.size).toSet, a.toString :: j.rules)
case None =>
}