diff --git a/src/main/scala/leon/evaluators/AbstractEvaluator.scala b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
index 2b8baa99424dbd7de9d4d2c4d87c82293e4de2b1..0befea52604aa86c60a2c3820a9abce0bdc9f513 100644
--- a/src/main/scala/leon/evaluators/AbstractEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AbstractEvaluator.scala
@@ -59,7 +59,7 @@ class AbstractEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvalu
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..41cff9a053040d9ce4254a679f711d95760ccb0f 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -46,6 +46,48 @@ 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 */
+ 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 {
+ case Left(m) => eval(expr, m)
+ case Right(errorMessage) =>
+ val m = mapping.filter{ case (k, v) => purescala.ExprOps.isValue(v) }.toMap
+ eval(expr, m) match {
+ case res @ evaluators.EvaluationResults.Successful(result) => res
+ case _ => evaluators.EvaluationResults.EvaluatorError(errorMessage)
+ }
+ })
+ }
+
+ /** 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] = {
+ var f= mapping.toSet
+ var mBuilder = collection.mutable.ListBuffer[(Identifier, Value)]()
+ 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/EvaluatorContexts.scala b/src/main/scala/leon/evaluators/EvaluatorContexts.scala
index 859e960d5d7aadbc63de656fd3c340fbc60b30f1..b5d3b4b5fd04db0e9118a653c058d04304c5d63e 100644
--- a/src/main/scala/leon/evaluators/EvaluatorContexts.scala
+++ b/src/main/scala/leon/evaluators/EvaluatorContexts.scala
@@ -15,16 +15,34 @@ trait RecContext[RC <: RecContext[RC]] {
def newVars(news: Map[Identifier, Expr]): RC
def withNewVar(id: Identifier, v: Expr): RC = {
+ if(!purescala.ExprOps.isValue(v)) {
+ println(s"Trying to add $id -> $v in context butnot a value")
+ println(Thread.currentThread().getStackTrace.map(_.toString).mkString("\n"))
+ System.exit(0)
+ }
newVars(mappings + (id -> v))
}
def withNewVars(news: Map[Identifier, Expr]): RC = {
+ if(news.exists{ case (k, v) => !purescala.ExprOps.isValue(v) }) {
+ println(s"Trying to add $news in context but not a value")
+ println(Thread.currentThread().getStackTrace.map(_.toString).mkString("\n"))
+ System.exit(0)
+ }
newVars(mappings ++ news)
}
}
case class DefaultRecContext(mappings: Map[Identifier, Expr]) extends RecContext[DefaultRecContext] {
def newVars(news: Map[Identifier, Expr]) = copy(news)
+
+ mappings.find{ case (k, v) => !purescala.ExprOps.isValue(v) } match {
+ case None =>
+ case Some(a) =>
+ println(s"Trying to add $mappings in context but $a has not a value as second argument (of type ${a._2.getType}) and class ${a._2.getClass} because ${purescala.ExprOps.msgs}")
+ println(Thread.currentThread().getStackTrace.map(_.toString).mkString("\n"))
+ System.exit(0)
+ }
}
class GlobalContext(val model: Model, val maxSteps: Int, val check: Boolean) {
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 f715bf109d598abcbb860021b1c73b131a23e58a..6cc0a39bd8b354c0aa263c9031875fafddc28aab 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,29 @@ 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
+ (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..cd0da333bcfd1882d3360fd769e6f7f49584eef0 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -64,9 +64,9 @@ 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 {
+ evaluator.evalEnvExpr(e, env).result match {
case Some(BooleanLiteral(b)) => b
case _ => true
}
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index 35a6986864dde1a97fdca214536dac6a21b52c57..92664547e33e73ccce08544a235249b5c0856d0a 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.evalEnvExpr(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 0ffdbc7692a0e0766345cbc9c105ad92bdc2b0bb..31731dca30d02281fae6883f139b29dbd96f18d9 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -107,7 +107,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
((p.as zip i.ins).toMap, p.pc.toClause)
}
- evaluator.eval(cond, mapping) match {
+ evaluator.evalEnvExpr(cond, mapping) match {
case EvaluationResults.Successful(BooleanLiteral(true)) => true
case _ => false
}
@@ -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/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 933ae752b19eff0ff816718ef7e6c4ee79560f22..e4e5192bc96b99bcfb2f28272665329ffc37a612 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -453,11 +453,11 @@ abstract class CEGISLike(name: String) extends Rule(name) {
timers.testForProgram.start()
val res = ex match {
case InExample(ins) =>
- evaluator.eval(cnstr, p.as.zip(ins).toMap ++ p.pc.bindings)
+ evaluator.evalEnvExpr(cnstr, p.as.zip(ins).toMap ++ p.pc.bindings)
case InOutExample(ins, outs) =>
val eq = equality(innerSol, tupleWrap(outs))
- evaluator.eval(eq, p.as.zip(ins).toMap ++ p.pc.bindings)
+ evaluator.evalEnvExpr(eq, p.as.zip(ins).toMap ++ p.pc.bindings)
}
timers.testForProgram.stop()
diff --git a/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala b/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
index 4463e6818b2b7b102cf404bd80ca794d9b96c3c7..ba3cb368510f2fd79c811766c57f55d71d1c4d71 100644
--- a/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
+++ b/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
@@ -67,7 +67,7 @@ case object IntroduceRecCalls extends NormalizingRule("Introduce rec. calls") {
val evaluator = new NoChooseEvaluator(hctx, hctx.program)
def mapExample(ex: Example): List[Example] = {
- val results = calls map (evaluator.eval(_, p.as.zip(ex.ins).toMap).result)
+ val results = calls map (evaluator.evalEnvExpr(_, p.as.zip(ex.ins)).result)
if (results forall (_.isDefined)) List({
val extra = results map (_.get)
ex match {
diff --git a/src/test/scala/leon/test/helpers/WithLikelyEq.scala b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
index 9836fc151c7218e61f53cf7e3cff74da5ffc719a..21a97ec48ff9a5926d3e2ebfe50eeac044ab8716 100644
--- a/src/test/scala/leon/test/helpers/WithLikelyEq.scala
+++ b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
@@ -45,9 +45,8 @@ trait WithLikelyEq {
cartesianProduct(allValues).foreach { vs =>
val m = (freeVars zip vs).toMap
-
val doTest = pre.map { p =>
- evaluator.eval(p, m).result match {
+ evaluator.evalEnvExpr(p, m).result match {
case Some(BooleanLiteral(b)) => b
case _ => fail("Precondition is not a boolean expression")
}