From b32249281c2a68e025b1833b49b8b6d47fa7a569 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Wed, 27 Apr 2016 15:32:35 +0200
Subject: [PATCH] Now deterministic eval by default check if the model is
ground, else evaluate it.
---
src/main/scala/leon/evaluators/Evaluator.scala | 10 +++++-----
src/main/scala/leon/repair/rules/Focus.scala | 2 +-
src/main/scala/leon/synthesis/ExamplesBank.scala | 2 +-
src/main/scala/leon/synthesis/ExamplesFinder.scala | 2 +-
src/main/scala/leon/synthesis/rules/CEGISLike.scala | 4 ++--
.../scala/leon/synthesis/rules/IntroduceRecCalls.scala | 2 +-
6 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index a4cb12831..c308c5e34 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)
@@ -48,14 +48,14 @@ 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 = {
+ override def eval(expr: Expr, mapping: Map[Identifier, Expr]) : EvaluationResult = {
if(mapping.forall{ case (key, value) => purescala.ExprOps.isValue(value) }) {
- eval(expr, mapping.toMap)
+ super.eval(expr, mapping.toMap)
} else (_evalEnv(mapping) match {
- case Left(m) => eval(expr, m)
+ case Left(m) => super.eval(expr, m)
case Right(errorMessage) =>
val m = mapping.filter{ case (k, v) => purescala.ExprOps.isValue(v) }.toMap
- eval(expr, m) match {
+ super.eval(expr, m) match {
case res @ evaluators.EvaluationResults.Successful(result) => res
case _ => evaluators.EvaluationResults.EvaluatorError(errorMessage)
}
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index bdeff6255..a881953bb 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -66,7 +66,7 @@ case object Focus extends PreprocessingRule("Focus") {
def existsFailing(e: Expr, env: Map[Identifier, Expr], evaluator: DeterministicEvaluator): Boolean = {
p.eb.invalids.exists { ex =>
- evaluator.evalEnvExpr(e, (p.as zip ex.ins).toMap ++ env).result match {
+ evaluator.eval(e, (p.as zip ex.ins).toMap ++ 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 92664547e..6cababe39 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -184,7 +184,7 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
/** Filter inputs through expr which is an expression evaluating to a boolean */
def filterIns(expr: Expr): QualifiedExamplesBank = {
filterIns(m =>
- hctx.defaultEvaluator.evalEnvExpr(expr, m)
+ hctx.defaultEvaluator.eval(expr, m)
.result == Some(BooleanLiteral(true)))
}
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 31731dca3..915384f1a 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.evalEnvExpr(cond, mapping) match {
+ evaluator.eval(cond, mapping) match {
case EvaluationResults.Successful(BooleanLiteral(true)) => true
case _ => false
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index e4e5192bc..933ae752b 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.evalEnvExpr(cnstr, p.as.zip(ins).toMap ++ p.pc.bindings)
+ evaluator.eval(cnstr, p.as.zip(ins).toMap ++ p.pc.bindings)
case InOutExample(ins, outs) =>
val eq = equality(innerSol, tupleWrap(outs))
- evaluator.evalEnvExpr(eq, p.as.zip(ins).toMap ++ p.pc.bindings)
+ evaluator.eval(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 ba3cb3685..4463e6818 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.evalEnvExpr(_, p.as.zip(ex.ins)).result)
+ val results = calls map (evaluator.eval(_, p.as.zip(ex.ins).toMap).result)
if (results forall (_.isDefined)) List({
val extra = results map (_.get)
ex match {
--
GitLab