From 7366462beeb70f568fc68e4668469a1a03245f22 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Wed, 27 Jan 2016 16:31:26 +0100
Subject: [PATCH] Homomorphic to work on lambdas + tests. Ability to keep
abstract term on the RHS of examples without trivially evaluating the choose
construct.
---
.../leon/evaluators/RecursiveEvaluator.scala | 7 +++++
src/main/scala/leon/purescala/ExprOps.scala | 7 +++++
.../scala/leon/synthesis/ExamplesFinder.scala | 5 +++-
.../leon/synthesis/rules/StringRender.scala | 6 +++--
.../integration/purescala/ExprOpsSuite.scala | 26 +++++++++++++++----
5 files changed, 43 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index b57383e8b..62e69fa62 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -28,6 +28,10 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
lazy val scalaEv = new ScalacEvaluator(this, ctx, prog)
protected var clpCache = Map[(Choose, Seq[Expr]), Expr]()
+
+ private var evaluationFailsOnChoose = false
+ /** Sets the flag if when encountering a Choose, it should fail instead of solving it. */
+ def setEvaluationFailOnChoose(b: Boolean) = { this.evaluationFailsOnChoose = b; this }
protected[evaluators] def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
case Variable(id) =>
@@ -577,6 +581,9 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
e(p.asConstraint)
case choose: Choose =>
+ if(evaluationFailsOnChoose) {
+ throw EvalError("Evaluator set to not solve choose constructs")
+ }
implicit val debugSection = utils.DebugSectionSynthesis
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index c651d3880..e03ac549e 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1560,6 +1560,8 @@ object ExprOps {
}
implicit class AugmentedContext(c: Option[Map[Identifier, Identifier]]) {
def &&(other: => Option[Map[Identifier, Identifier]]) = mergeContexts(c, other)
+ def --(other: Seq[Identifier]) =
+ c.map(_ -- other)
}
implicit class AugmentedBooleant(c: Boolean) {
def &&(other: => Option[Map[Identifier, Identifier]]) = if(c) other else None
@@ -1685,6 +1687,11 @@ object ExprOps {
// TODO: Seems a lot is missing, like Literals
+ case (Lambda(defs, body), Lambda(defs2, body2)) =>
+ // We remove variables introduced by lambdas.
+ (isHomo(body, body2) &&
+ (defs zip defs2).mergeall{ case (ValDef(a1, _), ValDef(a2, _)) => Option(Map(a1 -> a2)) }
+ ) -- (defs.map(_.id))
case Same(Operator(es1, _), Operator(es2, _)) =>
(es1.size == es2.size) &&
(es1 zip es2).mergeall{ case (e1, e2) => isHomo(e1, e2) }
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 0110f7128..1fa660b55 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -27,8 +27,11 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
val reporter = ctx.reporter
private var keepAbstractExamples = false
-
+ /** If true, will not evaluate examples to check them. */
def setKeepAbstractExamples(b: Boolean) = { this.keepAbstractExamples = b; this}
+ /** Sets if evalution of the result of tests should stop on choose statements.
+ * Useful for programming by Example */
+ def setEvaluationFailOnChoose(b: Boolean) = { evaluator.setEvaluationFailOnChoose(b); this }
def extractFromFunDef(fd: FunDef, partition: Boolean): ExamplesBank = fd.postcondition match {
case Some(Lambda(Seq(ValDef(id, _)), post)) =>
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index b3172538e..cce501ac1 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -176,7 +176,7 @@ case object StringRender extends Rule("StringRender") {
case Some(equations) =>
gatherEquations(q, acc ++= equations)
case None =>
- hctx.reporter.info("Could not extract equations from ["+sfget+"] == ["+rhsget+"]")
+ hctx.reporter.info("Could not extract equations from ["+sfget+"] == ["+rhsget+"]\n coming from ... == " + rhExpr)
None
}
case _ =>
@@ -547,7 +547,9 @@ case object StringRender extends Rule("StringRender") {
case List(IsTyped(v, StringType)) =>
val description = "Creates a standard string conversion function"
- val examplesFinder = new ExamplesFinder(hctx.context, hctx.program).setKeepAbstractExamples(true)
+ val examplesFinder = new ExamplesFinder(hctx.context, hctx.program)
+ .setKeepAbstractExamples(true)
+ .setEvaluationFailOnChoose(true)
val examples = examplesFinder.extractFromProblem(p)
val abstractStringConverters: StringConverters =
diff --git a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
index 2512f87ce..b8c0dbd8a 100644
--- a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
+++ b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
@@ -7,6 +7,7 @@ import leon.test._
import leon.purescala.Constructors._
import leon.purescala.Expressions._
import leon.purescala.ExprOps._
+import leon.purescala.Definitions._
import leon.purescala.Common._
class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL {
@@ -106,12 +107,27 @@ class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL
import leon.purescala.ExprOps.canBeHomomorphic
import leon.purescala.Types._
import leon.purescala.Definitions._
- val d = FreshIdentifier("x", IntegerType)
- val e = FreshIdentifier("y", IntegerType)
- assert(canBeHomomorphic(Variable(d), Variable(e)).isEmpty)
- val l1 = Lambda(Seq(ValDef(d)), Variable(d))
- val l2 = Lambda(Seq(ValDef(e)), Variable(e))
+ val d = FreshIdentifier("d", IntegerType)
+ val x = FreshIdentifier("x", IntegerType)
+ val y = FreshIdentifier("y", IntegerType)
+ assert(canBeHomomorphic(Variable(d), Variable(x)).isEmpty)
+ val l1 = Lambda(Seq(ValDef(x)), Variable(x))
+ val l2 = Lambda(Seq(ValDef(y)), Variable(y))
assert(canBeHomomorphic(l1, l2).nonEmpty)
+ val fType = FunctionType(Seq(IntegerType), IntegerType)
+ val f = FreshIdentifier("f",
+ FunctionType(Seq(IntegerType, fType, fType), IntegerType))
+ val farg1 = FreshIdentifier("arg1", IntegerType)
+ val farg2 = FreshIdentifier("arg2", fType)
+ val farg3 = FreshIdentifier("arg3", fType)
+
+ val fdef = new FunDef(f, Seq(), Seq(ValDef(farg1), ValDef(farg2), ValDef(farg3)), IntegerType)
+
+ // Captured variables should be silent, even if they share the same identifier in two places of the code.
+ assert(canBeHomomorphic(
+ FunctionInvocation(fdef.typed, Seq(Variable(d), l1, l2)),
+ FunctionInvocation(fdef.typed, Seq(Variable(d), l1, l1))).nonEmpty)
+
}
}
--
GitLab