diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index f4537232707462e9dd8b0c313abac19d1c64724a..b540a483c2cc1c2c3be0cfe8f280e58d7828c4d1 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -18,12 +18,11 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
this(ctx, CompilationUnit.compileProgram(prog).get) // this .get is dubious...
}
-
def eval(expression : Expr, mapping : Map[Identifier,Expr]) : EvaluationResult = {
// ctx.reporter.warning("Using `eval` in CodeGenEvaluator is discouraged. Use `compile` whenever applicable.")
val toPairs = mapping.toSeq
- compile(expression, toPairs.map(_._1)).map(e => e(toPairs.map(_._2))).getOrElse(EvaluationError("Couldn't compile expression."))
+ compile(expression, toPairs.map(_._1)).map(e => e(toPairs.map(_._2))).getOrElse(EvaluationResults.EvaluatorError("Couldn't compile expression."))
}
override def compile(expression : Expr, argorder : Seq[Identifier]) : Option[Seq[Expr]=>EvaluationResult] = {
@@ -35,19 +34,19 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
Some((args : Seq[Expr]) => {
try {
- EvaluationSuccessful(ce.eval(args))
+ EvaluationResults.Successful(ce.eval(args))
} catch {
case e : ArithmeticException =>
- EvaluationFailure(e.getMessage)
+ EvaluationResults.RuntimeError(e.getMessage)
case e : ArrayIndexOutOfBoundsException =>
- EvaluationFailure(e.getMessage)
+ EvaluationResults.RuntimeError(e.getMessage)
case e : LeonCodeGenRuntimeException =>
- EvaluationFailure(e.getMessage)
+ EvaluationResults.RuntimeError(e.getMessage)
case e : LeonCodeGenEvaluationException =>
- EvaluationError(e.getMessage)
+ EvaluationResults.EvaluatorError(e.getMessage)
}
})
} catch {
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index 47d86be95e018c115f226d36334df54e9f5ce982..a1f66ae1c8d65367e307a25e9bb553dc74f5e01a 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -19,7 +19,7 @@ class DefaultEvaluator(ctx : LeonContext, prog : Program) extends Evaluator(ctx,
private val maxSteps = 50000
- def eval(expression: Expr, mapping : Map[Identifier,Expr]) : EvaluationResult = {
+ def eval(expression: Expr, mapping : Map[Identifier,Expr]) : EvaluationResults.Result = {
var left: Int = maxSteps
def rec(ctx: Map[Identifier,Expr], expr: Expr) : Expr = if(left <= 0) {
@@ -299,11 +299,14 @@ class DefaultEvaluator(ctx : LeonContext, prog : Program) extends Evaluator(ctx,
}
try {
- EvaluationSuccessful(rec(mapping, expression))
+ EvaluationResults.Successful(rec(mapping, expression))
} catch {
- case so: StackOverflowError => EvaluationError("Stack overflow")
- case EvalError(msg) => EvaluationError(msg)
- case RuntimeError(msg) => EvaluationFailure(msg)
+ case so: StackOverflowError =>
+ EvaluationResults.EvaluatorError("Stack overflow")
+ case EvalError(msg) =>
+ EvaluationResults.EvaluatorError(msg)
+ case RuntimeError(msg) =>
+ EvaluationResults.RuntimeError(msg)
}
}
diff --git a/src/main/scala/leon/evaluators/EvaluationResults.scala b/src/main/scala/leon/evaluators/EvaluationResults.scala
new file mode 100644
index 0000000000000000000000000000000000000000..598121fd0ccf0c963d204c2df0dbc26f42f6a041
--- /dev/null
+++ b/src/main/scala/leon/evaluators/EvaluationResults.scala
@@ -0,0 +1,18 @@
+package leon
+package evaluators
+
+import purescala.Trees.Expr
+
+object EvaluationResults {
+ /** Possible results of expression evaluation. */
+ sealed abstract class Result(val result : Option[Expr])
+
+ /** Represents an evaluation that successfully derived the result `value`. */
+ case class Successful(value : Expr) extends Result(Some(value))
+
+ /** Represents an evaluation that led to an error (in the program). */
+ case class RuntimeError(message : String) extends Result(None)
+
+ /** Represents an evaluation that failed (in the evaluator). */
+ case class EvaluatorError(message : String) extends Result(None)
+}
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index 7beda070f28ce84795afb44691e2e124f08906f8..a54e406e37ff561f42ac668e7837cd80a7ac0b32 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -7,6 +7,8 @@ import purescala.Trees._
abstract class Evaluator(val context : LeonContext, val program : Program) extends LeonComponent {
+ type EvaluationResult = EvaluationResults.Result
+
/** Evaluates an expression, using `mapping` as a valuation function for the free variables. */
def eval(expr : Expr, mapping : Map[Identifier,Expr]) : EvaluationResult
@@ -19,7 +21,7 @@ abstract class Evaluator(val context : LeonContext, val program : Program) exten
* to (and encouraged to) apply any specialization. */
def compile(expr : Expr, argorder : Seq[Identifier]) : Option[Seq[Expr]=>EvaluationResult] = Some(
(args : Seq[Expr]) => if(args.size != argorder.size) {
- EvaluationError("Wrong number of arguments for evaluation.")
+ EvaluationResults.EvaluatorError("Wrong number of arguments for evaluation.")
} else {
val mapping = argorder.zip(args).toMap
eval(expr, mapping)
@@ -27,14 +29,3 @@ abstract class Evaluator(val context : LeonContext, val program : Program) exten
)
}
-/** Possible results of expression evaluation. */
-sealed abstract class EvaluationResult(val result : Option[Expr])
-
-/** Represents an evaluation that successfully derived the result `value`. */
-case class EvaluationSuccessful(value : Expr) extends EvaluationResult(Some(value))
-
-/** Represents an evaluation that led to an error (in the program). */
-case class EvaluationFailure(message : String) extends EvaluationResult(None)
-
-/** Represents an evaluation that failed (in the evaluator). */
-case class EvaluationError(message : String) extends EvaluationResult(None)
diff --git a/src/main/scala/leon/solvers/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
index c793d37f853829a684b86197955a5bc53f68e0c1..3ba1a3fa4d55a8605eb6ffca9523bd438ccba882 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -117,24 +117,24 @@ class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extend
val evalResult = evaluator.eval(expression, var2val)
evalResult match {
- case EvaluationSuccessful(BooleanLiteral(true)) => {
+ case EvaluationResults.Successful(BooleanLiteral(true)) => {
//continue trying
}
- case EvaluationSuccessful(BooleanLiteral(false)) => {
+ case EvaluationResults.Successful(BooleanLiteral(false)) => {
reporter.info("Found counter example to formula: " + var2val)
result = Some(false)
stop = true
}
- case EvaluationFailure(_) => {
+ case EvaluationResults.RuntimeError(_) => {
reporter.info("Input leads to runtime error: " + var2val)
result = Some(false)
stop = true
}
// otherwise, simply continue with another assignement
- case EvaluationError(_) => ;
+ case EvaluationResults.EvaluatorError(_) => ;
}
iteration += 1
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 448f42c252342fb887e4ed5172d38db916ca4886..59da550254ff6dcb8945788ed64fc306d3c8b176 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -172,19 +172,19 @@ class FairZ3Solver(context : LeonContext)
val evalResult = evaluator.eval(formula, asMap)
evalResult match {
- case EvaluationSuccessful(BooleanLiteral(true)) =>
+ case EvaluationResults.Successful(BooleanLiteral(true)) =>
reporter.info("- Model validated.")
(true, asMap)
- case EvaluationSuccessful(BooleanLiteral(false)) =>
+ case EvaluationResults.Successful(BooleanLiteral(false)) =>
reporter.info("- Invalid model.")
(false, asMap)
- case EvaluationFailure(msg) =>
+ case EvaluationResults.RuntimeError(msg) =>
reporter.info("- Model leads to runtime error.")
(false, asMap)
- case EvaluationError(msg) =>
+ case EvaluationResults.EvaluatorError(msg) =>
reporter.warning("Something went wrong. While evaluating the model, we got this : " + msg)
(false, asMap)
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index abb79d0ecf6430541e0220ed9364337b9e10215c..44963afa412544673afd06df24ad7db35c1a2545 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -94,7 +94,7 @@ class FunctionTemplate private(
val leonArgs = ga.map(_.get).force
val invocation = FunctionInvocation(funDef, leonArgs)
solver.getEvaluator.eval(invocation) match {
- case EvaluationSuccessful(result) =>
+ case EvaluationResults.Successful(result) =>
val z3Invocation = z3.mkApp(solver.functionDefToDecl(funDef), args: _*)
val z3Value = solver.toZ3Formula(result).get
val asZ3 = z3.mkEq(z3Invocation, z3Value)
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index 1465ea919f33ec86e31693c37f54de84b99b8cb8..e86ecf4171489323f10b349c024b223c301337a2 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -76,7 +76,7 @@ object LinearEquations {
var i = 0
while(i < sols.size) {
// seriously ???
- K(i+j+1)(j) = evaluator.eval(sols(i)).asInstanceOf[EvaluationSuccessful].value.asInstanceOf[IntLiteral].value
+ K(i+j+1)(j) = evaluator.eval(sols(i)).asInstanceOf[EvaluationResults.Successful].value.asInstanceOf[IntLiteral].value
i += 1
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 41527707f3150f6b2fb6bba0705b9deb37337a42..623c870c64b83d39c774032c8893e98b8865fc28 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -161,6 +161,8 @@ case object CEGIS extends Rule("CEGIS") {
private var cChildren: Map[Identifier, Set[Identifier]] = Map().withDefaultValue(Set())
+ type EvaluationResult = EvaluationResults.Result
+
private var triedCompilation = false
private var progEvaluator: Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = None
@@ -181,14 +183,14 @@ case object CEGIS extends Rule("CEGIS") {
val evalResult = progEvaluator.get.apply(bssValues, ins)
evalResult match {
- case EvaluationSuccessful(res) =>
+ case EvaluationResults.Successful(res) =>
res == BooleanLiteral(true)
- case EvaluationError(err) =>
+ case EvaluationResults.RuntimeError(err) =>
sctx.reporter.error("Error testing CE: "+err)
true
- case EvaluationFailure(err) =>
+ case EvaluationResults.EvaluatorError(err) =>
sctx.reporter.error("Error testing CE: "+err)
true
}
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 4fe7228d15a3ad68d671507d8735eb94b3c7b1d1..ce625a75e379b7ce0bdbd715be48ab80bdb5e3cc 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -60,14 +60,16 @@ class EvaluatorsTests extends FunSuite {
}
private def checkCompSuccess(evaluator : Evaluator, in : Expr) : Expr = {
+ import EvaluationResults._
+
evaluator.eval(in) match {
- case EvaluationFailure(msg) =>
+ case RuntimeError(msg) =>
throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have succeeded, but it failed (%s).".format(in, evaluator.name, msg))
- case EvaluationError(msg) =>
+ case EvaluatorError(msg) =>
throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have succeeded, but the evaluator had an internal error (%s).".format(in, evaluator.name, msg))
- case EvaluationSuccessful(result) =>
+ case Successful(result) =>
result
}
}
@@ -129,27 +131,31 @@ class EvaluatorsTests extends FunSuite {
}
private def checkError(evaluator : Evaluator, in : Expr) {
+ import EvaluationResults._
+
evaluator.eval(in) match {
- case EvaluationError(msg) =>
+ case EvaluatorError(msg) =>
throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have failed, but it produced an internal error (%s).".format(in, evaluator.name, msg))
- case EvaluationSuccessful(result) =>
+ case Successful(result) =>
throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have failed, but it produced the result '%s' instead.".format(in, evaluator.name, result))
- case EvaluationFailure(_) =>
+ case RuntimeError(_) =>
// that's the desired outcome
}
}
private def checkEvaluatorError(evaluator : Evaluator, in : Expr) {
+ import EvaluationResults._
+
evaluator.eval(in) match {
- case EvaluationFailure(msg) =>
+ case RuntimeError(msg) =>
throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have produced an internal error, but it failed instead (%s).".format(in, evaluator.name, msg))
- case EvaluationSuccessful(result) =>
+ case Successful(result) =>
throw new AssertionError("Evaluation of '%s' with evaluator '%s' should have produced an internal error, but it produced the result '%s' instead.".format(in, evaluator.name, result))
- case EvaluationError(_) =>
+ case EvaluatorError(_) =>
// that's the desired outcome
}
}
diff --git a/src/test/scala/leon/test/purescala/LikelyEq.scala b/src/test/scala/leon/test/purescala/LikelyEq.scala
index f1a6e971b5e2958bd742e76f23c5e1420ace3b59..84744ee62252c16c352a8c8fe109b0794f338f5c 100644
--- a/src/test/scala/leon/test/purescala/LikelyEq.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEq.scala
@@ -32,9 +32,9 @@ object LikelyEq {
compare: (Expr, Expr) => Boolean = (e1, e2) => e1 == e2,
defaultMap: Map[Identifier, Expr] = Map()): Boolean = {
if(vs.isEmpty) {
- val ndm = defaultMap.map { case (id, expr) => (id, evaluator.eval(expr).asInstanceOf[EvaluationSuccessful].value) } //TODO: not quite sure why I need to do this...
+ val ndm = defaultMap.map { case (id, expr) => (id, evaluator.eval(expr).asInstanceOf[EvaluationResults.Successful].value) } //TODO: not quite sure why I need to do this...
(evaluator.eval(e1, ndm), evaluator.eval(e2, defaultMap)) match {
- case (EvaluationSuccessful(v1), EvaluationSuccessful(v2)) => compare(v1, v2)
+ case (EvaluationResults.Successful(v1), EvaluationResults.Successful(v2)) => compare(v1, v2)
case (err1, err2) => sys.error("evaluation could not complete, got: (" + err1 + ", " + err2 + ")")
}
} else {
@@ -49,14 +49,14 @@ object LikelyEq {
val ne1 = replace(m, e1)
val ne2 = replace(m, e2)
val npre = replace(m, pre)
- val ndm = defaultMap.map{ case (id, expr) => (id, evaluator.eval(expr, m.map{case (Variable(id), t) => (id, t)}).asInstanceOf[EvaluationSuccessful].value) }
+ val ndm = defaultMap.map{ case (id, expr) => (id, evaluator.eval(expr, m.map{case (Variable(id), t) => (id, t)}).asInstanceOf[EvaluationResults.Successful].value) }
evaluator.eval(npre, ndm) match {
- case EvaluationSuccessful(BooleanLiteral(false)) =>
- case EvaluationSuccessful(BooleanLiteral(true)) =>
+ case EvaluationResults.Successful(BooleanLiteral(false)) =>
+ case EvaluationResults.Successful(BooleanLiteral(true)) =>
val ev1 = evaluator.eval(ne1, ndm)
val ev2 = evaluator.eval(ne2, ndm)
(ev1, ev2) match {
- case (EvaluationSuccessful(v1), EvaluationSuccessful(v2)) => if(!compare(v1, v2)) isEq = false
+ case (EvaluationResults.Successful(v1), EvaluationResults.Successful(v2)) => if(!compare(v1, v2)) isEq = false
case (err1, err2) => sys.error("evaluation could not complete, got: (" + err1 + ", " + err2 + ")")
}
case err => sys.error("evaluation of precondition could not complete, got: " + err)