From 15c7f84426916464288398aadf7ed7e1213563aa Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Thu, 18 Sep 2014 11:44:41 +0200
Subject: [PATCH] Allow symbolic/partial evaluation of tests
This is necessary to allow expressions in tests, such as List.::
---
.../scala/leon/evaluators/RecursiveEvaluator.scala | 4 +++-
src/main/scala/leon/synthesis/Problem.scala | 14 ++++++++++++--
2 files changed, 15 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 2274336b9..18dbe6ced 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -71,8 +71,10 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
case Variable(id) =>
rctx.mappings.get(id) match {
- case Some(v) =>
+ case Some(v) if (v != expr) =>
e(v)
+ case Some(v) =>
+ v
case None =>
throw EvalError("No value for identifier " + id.name + " in mapping.")
}
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index b56974ffc..82b02486f 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -79,10 +79,20 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
case _ => Nil
}
+ val evaluator = new DefaultEvaluator(sctx.context, sctx.program)
+
val testClusters = collect[Map[Identifier, Expr]] {
case FunctionInvocation(tfd, List(in, out, FiniteMap(inouts))) if tfd.id.name == "passes" =>
val infos = extractIds(Tuple(Seq(in, out)))
- val exs = inouts.map{ case (i, o) => Tuple(Seq(i, o)) }
+ val exs = inouts.map{ case (i, o) =>
+ val test = Tuple(Seq(i, o))
+ val ids = variablesOf(test)
+ evaluator.eval(test, ids.map { (i: Identifier) => i -> i.toVariable }.toMap) match {
+ case EvaluationResults.Successful(res) => res
+ case _ =>
+ test
+ }
+ }
// Check whether we can extract all ids from example
val results = exs.collect { case e if infos.forall(_._2.isDefinedAt(e)) =>
@@ -147,7 +157,7 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
object Problem {
def fromChoose(ch: Choose, pc: Expr = BooleanLiteral(true)): Problem = {
val xs = ch.vars
- val phi = ch.pred
+ val phi = simplifyLets(ch.pred)
val as = (variablesOf(And(pc, phi))--xs).toList
Problem(as, pc, phi, xs)
--
GitLab