From de8b1242ab1c8ea7f3a814166d8211d7cda542ae Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 18 Nov 2015 08:56:46 +0100
Subject: [PATCH] Evaluator improvements
NDEvaluator now a trait
(Previous) NDEvaluator -> StreamEvaluator
AngelicEvaluator is parametrized to the underlying evaluator
Fix Choose and Minus in StreamEvaluator
---
.../leon/evaluators/AngelicEvaluator.scala | 19 ++++--
.../scala/leon/evaluators/Evaluator.scala | 4 ++
...DEvaluator.scala => StreamEvaluator.scala} | 68 ++++++++++---------
src/main/scala/leon/repair/rules/Focus.scala | 4 +-
.../evaluators/EvaluatorSuite.scala | 3 +-
.../leon/unit/evaluators/EvaluatorSuite.scala | 3 +-
6 files changed, 57 insertions(+), 44 deletions(-)
rename src/main/scala/leon/evaluators/{NDEvaluator.scala => StreamEvaluator.scala} (93%)
diff --git a/src/main/scala/leon/evaluators/AngelicEvaluator.scala b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
index 30926b890..c1374b54f 100644
--- a/src/main/scala/leon/evaluators/AngelicEvaluator.scala
+++ b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
@@ -3,19 +3,24 @@
package leon
package evaluators
+import leon.solvers.Model
import purescala.Definitions.Program
import purescala.Expressions.Expr
+import EvaluationResults._
-class AngelicEvaluator(ctx: LeonContext, prog: Program)
- extends ContextualEvaluator(ctx, prog, 50000)
+class AngelicEvaluator(ctx: LeonContext, prog: Program, underlying: NDEvaluator)
+ extends Evaluator(ctx, prog)
with DeterministicEvaluator
- with DefaultContexts
{
- private val underlying = new NDEvaluator(ctx, prog)
-
val description: String = "angelic evaluator"
val name: String = "Interpreter that returns the first solution of a non-deterministic program"
- protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr =
- underlying.e(expr)(rctx, gctx).headOption.getOrElse(throw RuntimeError("No solution!"))
+ def eval(expr: Expr, model: Model): EvaluationResult = underlying.eval(expr, model) match {
+ case Successful(Stream(h, _*)) =>
+ Successful(h)
+ case Successful(Stream()) =>
+ RuntimeError("Underlying ND-evaluator returned no solution")
+ case other@(RuntimeError(_) | EvaluatorError(_)) =>
+ other.asInstanceOf[Result[Nothing]]
+ }
}
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index 609afd792..9843da81d 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -46,4 +46,8 @@ abstract class Evaluator(val context: LeonContext, val program: Program) extends
trait DeterministicEvaluator extends Evaluator {
type Value = Expr
+}
+
+trait NDEvaluator extends Evaluator {
+ type Value = Stream[Expr]
}
\ No newline at end of file
diff --git a/src/main/scala/leon/evaluators/NDEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
similarity index 93%
rename from src/main/scala/leon/evaluators/NDEvaluator.scala
rename to src/main/scala/leon/evaluators/StreamEvaluator.scala
index 1937d46f7..5b387368b 100644
--- a/src/main/scala/leon/evaluators/NDEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -15,16 +15,15 @@ import purescala.Expressions._
import leon.solvers.SolverFactory
import leon.utils.StreamUtils.cartesianProduct
-class NDEvaluator(ctx: LeonContext, prog: Program)
+class StreamEvaluator(ctx: LeonContext, prog: Program)
extends ContextualEvaluator(ctx, prog, 50000)
+ with NDEvaluator
with DefaultContexts
{
val name = "ND-evaluator"
val description = "Non-deterministic interpreter for Leon programs that returns a Stream of solutions"
- type Value = Stream[Expr]
-
case class NDValue(tp: TypeTree) extends Expr with Terminal {
val getType = tp
}
@@ -155,11 +154,7 @@ class NDEvaluator(ctx: LeonContext, prog: Program)
case f @ Forall(fargs, TopLevelAnds(conjuncts)) =>
def solveOne(conj: Expr) = {
- val instantiations = try {
- forallInstantiations(gctx, fargs, conj)
- } catch {
- case _: EvalError => Seq()
- }
+ val instantiations = forallInstantiations(gctx, fargs, conj)
for {
es <- cartesianProduct(instantiations.map { case (enabler, mapping) =>
e(Implies(enabler, conj))(rctx.withNewVars(mapping), gctx)
@@ -199,39 +194,46 @@ class NDEvaluator(ctx: LeonContext, prog: Program)
val cnstr = andJoin(eqs ::: p.pc :: p.phi :: Nil)
solver.assertCnstr(cnstr)
- def getSolution = solver.check match {
- case Some(true) =>
- val model = solver.getModel
+ def getSolution = try {
+ solver.check match {
+ case Some(true) =>
+ val model = solver.getModel
- val valModel = valuateWithModel(model) _
+ val valModel = valuateWithModel(model) _
- val res = p.xs.map(valModel)
- val leonRes = tupleWrap(res)
- val total = System.currentTimeMillis-tStart
+ val res = p.xs.map(valModel)
+ val leonRes = tupleWrap(res)
+ val total = System.currentTimeMillis - tStart
- ctx.reporter.debug("Synthesis took "+total+"ms")
- ctx.reporter.debug("Finished synthesis with "+leonRes.asString)
+ ctx.reporter.debug("Synthesis took " + total + "ms")
+ ctx.reporter.debug("Finished synthesis with " + leonRes.asString)
- Some(leonRes)
- case _ =>
- None
+ Some(leonRes)
+ case _ =>
+ None
+ }
+ } catch {
+ case _: Throwable => None
}
Stream.iterate(getSolution)(prev => {
- val ensureDistinct = Not(Equals(p.xs.head.toVariable, prev.get))
+ val ensureDistinct = Not(Equals(tupleWrap(p.xs.map{ _.toVariable}), prev.get))
solver.assertCnstr(ensureDistinct)
- getSolution
+ val sol = getSolution
+ // Clean up when the stream ends
+ if (sol.isEmpty) {
+ solverf.reclaim(solver)
+ solverf.shutdown()
+ }
+ sol
}).takeWhile(_.isDefined).map(_.get)
-
} catch {
case e: Throwable =>
+ solverf.reclaim(solver)
+ solverf.shutdown()
Stream()
- } finally {
- solverf.reclaim(solver)
- solverf.shutdown()
}
-
case MatchExpr(scrut, cases) =>
def matchesCase(scrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Stream[(MatchCase, Map[Identifier, Expr])] = {
@@ -306,7 +308,8 @@ class NDEvaluator(ctx: LeonContext, prog: Program)
try {
Some(step(expr, es))
} catch {
- case _: EvalError | _: RuntimeError =>
+ case _: RuntimeError =>
+ // EvalErrors stop the computation alltogether
None
}
}
@@ -370,7 +373,7 @@ class NDEvaluator(ctx: LeonContext, prog: Program)
case (Plus(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
InfiniteIntegerLiteral(i1 + i2)
- case (Minus(_, _) Seq (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
+ case (Minus(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
InfiniteIntegerLiteral(i1 - i2)
case (Times(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
@@ -392,6 +395,9 @@ class NDEvaluator(ctx: LeonContext, prog: Program)
else
throw RuntimeError("Modulo of division by 0.")
+ case (UMinus(_), Seq(InfiniteIntegerLiteral(i))) =>
+ InfiniteIntegerLiteral(-i)
+
case (RealPlus(_, _), Seq(FractionalLiteral(ln, ld), FractionalLiteral(rn, rd))) =>
normalizeFraction(FractionalLiteral(ln * rd + rn * ld, ld * rd))
@@ -411,9 +417,6 @@ class NDEvaluator(ctx: LeonContext, prog: Program)
case (BVMinus(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
IntLiteral(i1 - i2)
- case (UMinus(_), Seq(InfiniteIntegerLiteral(i))) =>
- InfiniteIntegerLiteral(-i)
-
case (BVUMinus(_), Seq(IntLiteral(i))) =>
IntLiteral(-i)
@@ -578,6 +581,7 @@ class NDEvaluator(ctx: LeonContext, prog: Program)
l
case (other, _) =>
+ context.reporter.error(other.getPos, "Error: don't know how to handle " + other.asString + " in Evaluator ("+other.getClass+").")
throw EvalError("Unhandled case in Evaluator: " + other.asString)
}
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index 8c1694dbd..d6b4d874f 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -75,9 +75,7 @@ case object Focus extends PreprocessingRule("Focus") {
val fdSpec = {
val id = FreshIdentifier("res", fd.returnType)
- Let(id, fd.body.get,
- fd.postcondition.map(l => application(l, Seq(id.toVariable))).getOrElse(BooleanLiteral(true))
- )
+ Let(id, fd.body.get, application(fd.postOrTrue, Seq(id.toVariable)))
}
val TopLevelAnds(clauses) = p.ws
diff --git a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
index 1643e4800..82c419b04 100644
--- a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
@@ -205,7 +205,8 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
def normalEvaluators(implicit ctx: LeonContext, pgm: Program): List[Evaluator] = {
List(
- new DefaultEvaluator(ctx, pgm)
+ new DefaultEvaluator(ctx, pgm),
+ new AngelicEvaluator(ctx, pgm, new StreamEvaluator(ctx, pgm))
)
}
diff --git a/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
index 6c614a562..4002a0af0 100644
--- a/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
@@ -19,7 +19,8 @@ class EvaluatorSuite extends LeonTestSuite with helpers.ExpressionsDSL {
def normalEvaluators(implicit ctx: LeonContext, pgm: Program): List[DeterministicEvaluator] = {
List(
- new DefaultEvaluator(ctx, pgm)
+ new DefaultEvaluator(ctx, pgm),
+ new AngelicEvaluator(ctx, pgm, new StreamEvaluator(ctx, pgm))
)
}
--
GitLab