From 8ca74bdc27d7aa9f4c77897086b0e1ead3579392 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 6 Jul 2015 15:54:39 +0200
Subject: [PATCH] Fix handling of holes, and multiple-variables chooses
---
.../scala/leon/purescala/Constructors.scala | 4 ++-
.../solvers/templates/TemplateGenerator.scala | 18 ++++++++----
.../scala/leon/synthesis/ConvertHoles.scala | 29 ++++++++++++-------
.../regression/synthesis/Misc/HolesBug.scala | 16 ++++++++++
.../synthesis/SynthesisRegressionSuite.scala | 4 +++
5 files changed, 54 insertions(+), 17 deletions(-)
create mode 100644 src/test/resources/regression/synthesis/Misc/HolesBug.scala
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index aceebf495..148f8d051 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -68,7 +68,7 @@ object Constructors {
/** Will instantiate the type parameters of the function according to argument types */
def functionInvocation(fd : FunDef, args : Seq[Expr]) = {
- require(fd.params.length == args.length)
+ require(fd.params.length == args.length, "Invoking function with incorrect number of arguments")
val formalType = tupleTypeWrap(fd.params map { _.getType })
val actualType = tupleTypeWrap(args map { _.getType })
@@ -234,6 +234,8 @@ object Constructors {
def application(fn: Expr, realArgs: Seq[Expr]) = fn match {
case Lambda(formalArgs, body) =>
+ assert(realArgs.size == formalArgs.size, "Invoking lambda with incorrect number of arguments")
+
var defs: Seq[(Identifier, Expr)] = Seq()
val subst = formalArgs.zip(realArgs).map {
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index fc0826dbb..0ee3997c6 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -244,11 +244,19 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
}
}
- case c @ Choose(cond) =>
- val cid = FreshIdentifier("choose", c.getType, true)
- storeExpr(cid)
- storeGuarded(pathVar, application(cond, Seq(Variable(cid))))
- Variable(cid)
+ case c @ Choose(Lambda(params, cond)) =>
+
+ val cs = params.map(_.id.freshen.toVariable)
+
+ for (c <- cs) {
+ storeExpr(c.id)
+ }
+
+ val freshMap = (params.map(_.id) zip cs).toMap
+
+ storeGuarded(pathVar, replaceFromIDs(freshMap, cond))
+
+ tupleWrap(cs)
case l @ Lambda(args, body) =>
val idArgs : Seq[Identifier] = lambdaArgs(l)
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 3d9183a7b..4c27e9b96 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -64,26 +64,33 @@ object ConvertHoles extends LeonPhase[Program, Program] {
None
}(body)
- val asChoose = if (holes.nonEmpty) {
+ if (holes.nonEmpty) {
val cids: List[Identifier] = holes.map(_.freshen)
- val pred = post match {
- case Some(post) =>
- replaceFromIDs((holes zip cids.map(_.toVariable)).toMap, post)
- case None =>
+ val hToFresh = (holes zip cids.map(_.toVariable)).toMap
+
+ val spec = post match {
+ case Some(post: Lambda) =>
+ val asLet = letTuple(post.args.map(_.id), withoutHoles, post.body)
+
+ Lambda(cids.map(ValDef(_)), replaceFromIDs(hToFresh, asLet))
+
+ case _ =>
Lambda(cids.map(ValDef(_)), BooleanLiteral(true))
}
- letTuple(holes, Choose(pred), withoutHoles)
+ val choose = Choose(spec)
+
+ val valuations = letTuple(holes, choose, withoutHoles)
+
+ withPostcondition(withPrecondition(valuations, pre), post)
+
+ } else {
+ e
}
- else withoutHoles
- withPostcondition(withPrecondition(asChoose, pre), post)
-
case None => e
}
-
-
}
diff --git a/src/test/resources/regression/synthesis/Misc/HolesBug.scala b/src/test/resources/regression/synthesis/Misc/HolesBug.scala
new file mode 100644
index 000000000..47db91b99
--- /dev/null
+++ b/src/test/resources/regression/synthesis/Misc/HolesBug.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object HolesBug {
+ def plop(a: BigInt, b: BigInt): BigInt = {
+ if (a < b) {
+ ???[BigInt]
+ } else {
+ ???[BigInt]
+ }
+ } ensuring { res =>
+ res > 0
+ }
+}
+
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 35513481a..255781935 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -64,6 +64,10 @@ class SynthesisRegressionSuite extends LeonTestSuite {
testSynthesis("List", f, 200)
}
+ forEachFileIn("regression/synthesis/Misc/") { f =>
+ testSynthesis("Miscellaneous", f, 1000)
+ }
+
forEachFileIn("regression/synthesis/Holes/") { f =>
testSynthesis("Holes", f, 1000)
}
--
GitLab