diff --git a/src/main/scala/leon/evaluators/AbstractEvaluator.scala b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
index 5caec3ee8a3f585ba8a61981c1cd783e01f52e92..2e0a7a2bb1959f720e62ab47f4c6783436e4d28b 100644
--- a/src/main/scala/leon/evaluators/AbstractEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
@@ -61,7 +61,7 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
var evaluateCaseClassSelector = true
protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): (Expr, Expr) = {
- implicit def aToC: AbstractEvaluator.this.underlying.RC = DefaultRecContext(rctx.mappings)
+ implicit def aToC: AbstractEvaluator.this.underlying.RC = DefaultRecContext(rctx.mappings.filter{ case (k, v) => ExprOps.isValue(v) })
expr match {
case Variable(id) =>
(rctx.mappings.get(id), rctx.mappingsAbstract.get(id)) match {
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index a15febb65c31129db2d5ee37da88cd148dce3806..c308c5e347e859bc192833bf015e4c2013dc26b9 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -25,7 +25,7 @@ abstract class Evaluator(val context: LeonContext, val program: Program) extends
/** Evaluates an expression given a simple model (assumes expr is quantifier-free).
* Mainly useful for compatibility reasons.
*/
- final def eval(expr: Expr, mapping: Map[Identifier, Expr]) : EvaluationResult = eval(expr, new Model(mapping))
+ def eval(expr: Expr, mapping: Map[Identifier, Expr]) : EvaluationResult = eval(expr, new Model(mapping))
/** Evaluates a ground expression. */
final def eval(expr: Expr) : EvaluationResult = eval(expr, Model.empty)
@@ -46,6 +46,59 @@ abstract class Evaluator(val context: LeonContext, val program: Program) extends
trait DeterministicEvaluator extends Evaluator {
type Value = Expr
+
+ /**Evaluates the environment first, resolving non-cyclic dependencies, and then evaluate the expression */
+ override def eval(expr: Expr, mapping: Map[Identifier, Expr]) : EvaluationResult = {
+ if(mapping.forall{ case (key, value) => purescala.ExprOps.isValue(value) }) {
+ super.eval(expr, mapping.toMap)
+ } else (_evalEnv(mapping) match {
+ case Left(m) => super.eval(expr, m)
+ case Right(errorMessage) =>
+ val m = mapping.filter{ case (k, v) => purescala.ExprOps.isValue(v) }.toMap
+ super.eval(expr, m) match {
+ case res @ evaluators.EvaluationResults.Successful(result) => res
+ case _ => evaluators.EvaluationResults.EvaluatorError(errorMessage)
+ }
+ })
+ }
+
+ /** 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] = {
+ val (evaled, nonevaled) = mapping.partition{ case (id, expr) => purescala.ExprOps.isValue(expr)}
+ var f= nonevaled.toSet
+ var mBuilder = collection.mutable.ListBuffer[(Identifier, Value)]() ++= evaled
+ var changed = true
+ while(f.nonEmpty && changed) {
+ changed = false
+ for((i, v) <- f) {
+ eval(v, mBuilder.toMap).result match {
+ case None =>
+ case Some(e) =>
+ changed = true
+ mBuilder += ((i -> e))
+ f -= ((i, v))
+ }
+ }
+ }
+ if(!changed) {
+ val str = "In the context " + mapping + ",\n" +
+ (for((i, v) <- f) yield {
+ s"eval(${v}) returned the error: " + eval(v, mBuilder.toMap)
+ }).mkString("\n")
+ Right(str)
+ } else Left(mBuilder.toMap)
+ }
}
trait NDEvaluator extends Evaluator {
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index cfb45f73350de39cf208441d324a85f0b9b363b9..10351213546db205fc52e1fc83d817315de81119 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -39,8 +39,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
protected[evaluators] def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
case Variable(id) =>
rctx.mappings.get(id) match {
- case Some(v) if v != expr =>
- e(v)
case Some(v) =>
v
case None =>
@@ -213,7 +211,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case CaseClass(cct, args) =>
val cc = CaseClass(cct, args.map(e))
if (cct.classDef.hasInvariant) {
- e(FunctionInvocation(cct.invariant.get, Seq(cc))) match {
+ val i = FreshIdentifier("i", cct)
+ e(FunctionInvocation(cct.invariant.get, Seq(Variable(i))))(rctx.withNewVar(i, cc), gctx) match {
case BooleanLiteral(true) =>
case BooleanLiteral(false) =>
throw RuntimeError("ADT invariant violation for " + cct.classDef.id.asString + " reached in evaluation.: " + cct.invariant.get.asString)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index fb7cb0742ed74430e628c70b3f0a5ff5b7fa9f19..f3a9a94caaabf7e5d2c104439f041de680c54f53 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -2136,9 +2136,17 @@ object ExprOps extends GenTreeOps[Expr] {
case _ =>
fun
}
+ var msgs: String = ""
+ implicit class BooleanAdder(b: Boolean) {
+ def <(msg: String) = {if(!b) msgs += msg; b}
+ }
/** Returns true if expr is a value of type t */
def isValueOfType(e: Expr, t: TypeTree): Boolean = {
+ def unWrapSome(s: Expr) = s match {
+ case CaseClass(_, Seq(a)) => a
+ case _ => s
+ }
(e, t) match {
case (StringLiteral(_), StringType) => true
case (IntLiteral(_), Int32Type) => true
@@ -2154,25 +2162,30 @@ object ExprOps extends GenTreeOps[Expr] {
tbase == base &&
(elems forall isValue)
case (FiniteMap(elems, tk, tv), MapType(from, to)) =>
- tk == from && tv == to &&
- (elems forall (kv => isValueOfType(kv._1, from) && isValueOfType(kv._2, to) ))
+ (tk == from) < s"$tk not equal to $from" && (tv == to) < s"$tv not equal to $to" &&
+ (elems forall (kv => isValueOfType(kv._1, from) < s"${kv._1} not a value of type ${from}" && isValueOfType(unWrapSome(kv._2), to) < s"${unWrapSome(kv._2)} not a value of type ${to}" ))
case (NonemptyArray(elems, defaultValues), ArrayType(base)) =>
elems.values forall (x => isValueOfType(x, base))
case (EmptyArray(tpe), ArrayType(base)) =>
tpe == base
case (CaseClass(ct, args), ct2@AbstractClassType(classDef, tps)) =>
- TypeOps.isSubtypeOf(ct, ct2) &&
- ((args zip ct.fieldsTypes) forall (argstyped => isValueOfType(argstyped._1, argstyped._2)))
+ TypeOps.isSubtypeOf(ct, ct2) < s"$ct not a subtype of $ct2" &&
+ ((args zip ct.fieldsTypes) forall (argstyped => isValueOfType(argstyped._1, argstyped._2) < s"${argstyped._1} not a value of type ${argstyped._2}" ))
case (CaseClass(ct, args), ct2@CaseClassType(classDef, tps)) =>
- ct == ct2 &&
+ (ct == ct2) < s"$ct not equal to $ct2" &&
((args zip ct.fieldsTypes) forall (argstyped => isValueOfType(argstyped._1, argstyped._2)))
+ case (FiniteLambda(mapping, default, tpe), exTpe@FunctionType(ins, out)) =>
+ tpe == exTpe
case (Lambda(valdefs, body), FunctionType(ins, out)) =>
- (valdefs zip ins forall (vdin => vdin._1.getType == vdin._2)) &&
- body.getType == out
+ variablesOf(e).isEmpty &&
+ (valdefs zip ins forall (vdin => (vdin._1.getType == vdin._2) < s"${vdin._1.getType} is not equal to ${vdin._2}")) &&
+ (body.getType == out) < s"${body.getType} is not equal to ${out}"
+ case (FiniteBag(elements, fbtpe), BagType(tpe)) =>
+ fbtpe == tpe && elements.forall{ case (key, value) => isValueOfType(key, tpe) && isValueOfType(value, IntegerType) }
case _ => false
}
}
-
+
/** Returns true if expr is a value. Stronger than isGround */
val isValue = (e: Expr) => isValueOfType(e, e.getType)
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index c9f86a404bac39d3cd5bfec8b16e6d48eba2d968..2488aec8cebdd6de10d070800a4991df2e9894ba 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -8,8 +8,7 @@ import leon.LeonContext
import leon.evaluators
import leon.utils.StreamUtils
import leon.purescala.Quantification._
-import leon.utils.DebugSectionSynthesis
-import leon.utils.DebugSectionVerification
+import leon.utils.DebugSectionEvaluation
import purescala.Definitions.Program
import purescala.Expressions._
import purescala.Types.StringType
@@ -121,7 +120,7 @@ class SelfPrettyPrinter {
case Some(StringLiteral(res)) if res != "" =>
res
case res =>
- ctx.reporter.debug("not a string literal " + res)
+ ctx.reporter.debug("not a string literal " + result)
orElse
}
} catch {
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index 512fb0afdbfa4fe99c517ca18d822e33b6293f19..a881953bb9354472703660cae8bacbb542e67596 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -64,7 +64,7 @@ case object Focus extends PreprocessingRule("Focus") {
soFar
}
- def existsFailing(e: Expr, env: Map[Identifier, Expr], evaluator: Evaluator): Boolean = {
+ def existsFailing(e: Expr, env: Map[Identifier, Expr], evaluator: DeterministicEvaluator): Boolean = {
p.eb.invalids.exists { ex =>
evaluator.eval(e, (p.as zip ex.ins).toMap ++ env).result match {
case Some(BooleanLiteral(b)) => b
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index 403fb08fd20c9297b91cd6294cfc4a707e7ad40a..b7aa7dc664c80941d8fcd23e7e5f807aead28174 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
@@ -210,7 +210,11 @@ trait AbstractUnrollingSolver[T]
private def validateModel(model: Model, assumptions: Seq[Expr], silenceErrors: Boolean): Boolean = {
val expr = andJoin(assumptions ++ constraints)
- evaluator.eval(expr, model) match {
+ val newExpr = model.toSeq.foldLeft(expr){
+ case (e, (k, v)) => let(k, v, e)
+ }
+
+ evaluator.eval(newExpr) match {
case EvaluationResults.Successful(BooleanLiteral(true)) =>
reporter.debug("- Model validated.")
true
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index 35a6986864dde1a97fdca214536dac6a21b52c57..6cababe398c6159ec4e5cce721b795a751825bda 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -181,9 +181,11 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
QualifiedExamplesBank(nas, xs, eb mapIns { (in: Seq[Expr]) => List(toKeep.map(in)) })
}
- /** Filter inputs throught expr which is an expression evaluating to a boolean */
+ /** Filter inputs through expr which is an expression evaluating to a boolean */
def filterIns(expr: Expr): QualifiedExamplesBank = {
- filterIns(m => hctx.defaultEvaluator.eval(expr, m).result == Some(BooleanLiteral(true)))
+ filterIns(m =>
+ hctx.defaultEvaluator.eval(expr, m)
+ .result == Some(BooleanLiteral(true)))
}
/** Filters inputs through the predicate pred, with an assignment of input variables to expressions. */
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index a20b37a100caf2ca0bfed6c8bcf7813c01149e88..52756108c029ff7fcad5d0f2a0e6aaceb3d6770c 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -143,8 +143,8 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
val ids = variablesOf(test)
// Test could contain expressions, we evaluate
- evaluator.eval(test, ids.map { (i: Identifier) => i -> i.toVariable }.toMap) match {
- case EvaluationResults.Successful(res) => res
+ abstractEvaluator.eval(test, Model.empty) match {
+ case EvaluationResults.Successful((res, _)) => res
case _ => test
}
}
diff --git a/src/test/scala/leon/test/helpers/WithLikelyEq.scala b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
index 9836fc151c7218e61f53cf7e3cff74da5ffc719a..f121f4553809fd7ae5b9e93d15bb1b5b7d3b2de0 100644
--- a/src/test/scala/leon/test/helpers/WithLikelyEq.scala
+++ b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
@@ -44,8 +44,7 @@ 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.eval(p, m).result match {
case Some(BooleanLiteral(b)) => b