From 605a8155234654cc6976efb48e1f080df52aedcc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Thu, 21 Apr 2016 10:26:05 +0200
Subject: [PATCH] Factorized env function.
---
src/main/scala/leon/evaluators/Evaluator.scala | 14 ++++++++++++--
.../scala/leon/test/helpers/WithLikelyEq.scala | 4 ++--
2 files changed, 14 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index 41cff9a05..c924e8bb5 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -51,7 +51,7 @@ trait DeterministicEvaluator extends Evaluator {
final def evalEnvExpr(expr: Expr, mapping: Iterable[(Identifier, Expr)]) : EvaluationResult = {
if(mapping.forall{ case (key, value) => purescala.ExprOps.isValue(value) }) {
eval(expr, mapping.toMap)
- } else (evalEnv(mapping) match {
+ } else (_evalEnv(mapping) match {
case Left(m) => eval(expr, m)
case Right(errorMessage) =>
val m = mapping.filter{ case (k, v) => purescala.ExprOps.isValue(v) }.toMap
@@ -62,9 +62,19 @@ trait DeterministicEvaluator extends Evaluator {
})
}
+ /** Returns an evaluated environment. If it fails, removes all non-values from the environment. */
+ def evalEnv(mapping: Iterable[(Identifier, Expr)]): Map[Identifier, Value] = {
+ if(mapping.forall{ case (key, value) => purescala.ExprOps.isValue(value) }) {
+ mapping.toMap
+ } else (_evalEnv(mapping) match {
+ case Left(m) => m
+ case Right(msg) => mapping.filter(x => purescala.ExprOps.isValue(x._2)).toMap
+ })
+ }
+
/** From a not yet well evaluated context with dependencies between variables, returns a head where all exprs are values (as a Left())
* If this does not succeed, it provides an error message as Right()*/
- private def evalEnv(mapping: Iterable[(Identifier, Expr)]): Either[Map[Identifier, Value], String] = {
+ private def _evalEnv(mapping: Iterable[(Identifier, Expr)]): Either[Map[Identifier, Value], String] = {
var f= mapping.toSet
var mBuilder = collection.mutable.ListBuffer[(Identifier, Value)]()
var changed = true
diff --git a/src/test/scala/leon/test/helpers/WithLikelyEq.scala b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
index 21a97ec48..f121f4553 100644
--- a/src/test/scala/leon/test/helpers/WithLikelyEq.scala
+++ b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
@@ -44,9 +44,9 @@ trait WithLikelyEq {
val allValues = freeVars.map(id => values.get(id).map(Seq(_)).getOrElse(typesValues(id.getType)))
cartesianProduct(allValues).foreach { vs =>
- val m = (freeVars zip vs).toMap
+ val m = evaluator.evalEnv(freeVars zip vs)
val doTest = pre.map { p =>
- evaluator.evalEnvExpr(p, m).result match {
+ evaluator.eval(p, m).result match {
case Some(BooleanLiteral(b)) => b
case _ => fail("Precondition is not a boolean expression")
}
--
GitLab