From ac306f8f4c7c1f6a75b05143dc9ecef91bdce4f1 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 10 Nov 2015 13:46:17 +0100
Subject: [PATCH] Refactor Evaluators. Introduce NDEvaluator trait and
StreamEvaluator
EvaluationResults.Result is now polymorphic
Refactor evaluator contexts
Refactor evaluator hierarchy
Make tests up to date
---
.../scala/leon/codegen/CompilationUnit.scala | 12 +-
.../scala/leon/datagen/VanuatooDataGen.scala | 2 +-
.../leon/evaluators/AngelicEvaluator.scala | 26 +
.../leon/evaluators/CodeGenEvaluator.scala | 3 +-
.../leon/evaluators/ContextualEvaluator.scala | 114 ++++
.../leon/evaluators/DefaultEvaluator.scala | 21 +-
.../scala/leon/evaluators/DualEvaluator.scala | 11 +-
.../leon/evaluators/EvaluationResults.scala | 6 +-
.../scala/leon/evaluators/Evaluator.scala | 20 +-
.../leon/evaluators/EvaluatorContexts.scala | 39 ++
.../leon/evaluators/RecursiveEvaluator.scala | 179 ++----
.../leon/evaluators/ScalacEvaluator.scala | 45 +-
.../leon/evaluators/StreamEvaluator.scala | 591 ++++++++++++++++++
.../leon/evaluators/TracingEvaluator.scala | 5 +-
.../scala/leon/purescala/Definitions.scala | 1 +
.../scala/leon/purescala/Extractors.scala | 12 +-
.../scala/leon/repair/RepairNDEvaluator.scala | 2 +-
.../leon/repair/RepairTrackingEvaluator.scala | 9 +-
src/main/scala/leon/repair/rules/Focus.scala | 4 +-
.../scala/leon/solvers/EvaluatingSolver.scala | 2 +-
.../leon/synthesis/ConversionPhase.scala | 5 +-
.../leon/synthesis/LinearEquations.scala | 2 +-
.../leon/synthesis/rules/CEGISLike.scala | 5 +-
src/main/scala/leon/utils/SeqUtils.scala | 45 ++
.../evaluators/EvaluatorSuite.scala | 5 +-
.../purescala/CallGraphSuite.scala | 4 +-
.../integration/purescala/DataGenSuite.scala | 3 -
.../integration/purescala/DefOpsSuite.scala | 2 -
.../solvers/EnumerationSolverSuite.scala | 1 -
.../solvers/FairZ3SolverTests.scala | 2 -
.../solvers/ModelEnumerationSuite.scala | 2 +-
.../integration/solvers/SolversSuite.scala | 2 +-
.../solvers/TimeoutSolverSuite.scala | 1 -
.../solvers/UnrollingSolverSuite.scala | 2 -
src/test/scala/leon/test/LeonTestSuite.scala | 4 -
.../leon/unit/evaluators/EvaluatorSuite.scala | 22 +-
36 files changed, 942 insertions(+), 269 deletions(-)
create mode 100644 src/main/scala/leon/evaluators/AngelicEvaluator.scala
create mode 100644 src/main/scala/leon/evaluators/ContextualEvaluator.scala
create mode 100644 src/main/scala/leon/evaluators/EvaluatorContexts.scala
create mode 100644 src/main/scala/leon/evaluators/StreamEvaluator.scala
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 69f95f455..36ad6a2a2 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -505,13 +505,11 @@ class CompilationUnit(val ctx: LeonContext,
for {
ch <- u.classHierarchies
c <- ch
- } {
- c match {
- case acd: AbstractClassDef =>
- compileAbstractClassDef(acd)
- case ccd: CaseClassDef =>
- compileCaseClassDef(ccd)
- }
+ } c match {
+ case acd: AbstractClassDef =>
+ compileAbstractClassDef(acd)
+ case ccd: CaseClassDef =>
+ compileCaseClassDef(ccd)
}
for (m <- u.modules) compileModule(m)
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index e68e21f01..1a4792442 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -222,7 +222,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
(AnyPattern[Expr, TypeTree](), false)
}
- type InstrumentedResult = (EvaluationResults.Result, Option[vanuatoo.Pattern[Expr, TypeTree]])
+ type InstrumentedResult = (EvaluationResults.Result[Expr], Option[vanuatoo.Pattern[Expr, TypeTree]])
def compile(expression: Expr, argorder: Seq[Identifier]) : Option[Expr=>InstrumentedResult] = {
import leon.codegen.runtime.LeonCodeGenRuntimeException
diff --git a/src/main/scala/leon/evaluators/AngelicEvaluator.scala b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
new file mode 100644
index 000000000..c1374b54f
--- /dev/null
+++ b/src/main/scala/leon/evaluators/AngelicEvaluator.scala
@@ -0,0 +1,26 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package evaluators
+
+import leon.solvers.Model
+import purescala.Definitions.Program
+import purescala.Expressions.Expr
+import EvaluationResults._
+
+class AngelicEvaluator(ctx: LeonContext, prog: Program, underlying: NDEvaluator)
+ extends Evaluator(ctx, prog)
+ with DeterministicEvaluator
+{
+ val description: String = "angelic evaluator"
+ val name: String = "Interpreter that returns the first solution of a non-deterministic program"
+
+ 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/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index 36cd9da0c..a32bce7e5 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -6,12 +6,11 @@ package evaluators
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.Quantification._
import codegen.CompilationUnit
import codegen.CodeGenParams
-class CodeGenEvaluator(ctx: LeonContext, val unit : CompilationUnit) extends Evaluator(ctx, unit.program) {
+class CodeGenEvaluator(ctx: LeonContext, val unit : CompilationUnit) extends Evaluator(ctx, unit.program) with DeterministicEvaluator {
val name = "codegen-eval"
val description = "Evaluator for PureScala expressions based on compilation to JVM"
diff --git a/src/main/scala/leon/evaluators/ContextualEvaluator.scala b/src/main/scala/leon/evaluators/ContextualEvaluator.scala
new file mode 100644
index 000000000..59e46a658
--- /dev/null
+++ b/src/main/scala/leon/evaluators/ContextualEvaluator.scala
@@ -0,0 +1,114 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package evaluators
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.Constructors._
+import purescala.ExprOps._
+import purescala.Quantification._
+import solvers.{HenkinModel, Model}
+
+abstract class ContextualEvaluator(ctx: LeonContext, prog: Program, val maxSteps: Int) extends Evaluator(ctx, prog) with CEvalHelpers {
+
+ protected implicit val _ = ctx
+
+ type RC <: RecContext[RC]
+ type GC <: GlobalContext
+
+ def initRC(mappings: Map[Identifier, Expr]): RC
+ def initGC(model: solvers.Model): GC
+
+ case class EvalError(msg : String) extends Exception
+ case class RuntimeError(msg : String) extends Exception
+
+ // Used by leon-web, please do not delete
+ var lastGC: Option[GC] = None
+
+ def eval(ex: Expr, model: Model) = {
+ try {
+ lastGC = Some(initGC(model))
+ ctx.timers.evaluators.recursive.runtime.start()
+ EvaluationResults.Successful(e(ex)(initRC(model.toMap), lastGC.get))
+ } catch {
+ case so: StackOverflowError =>
+ EvaluationResults.EvaluatorError("Stack overflow")
+ case EvalError(msg) =>
+ EvaluationResults.EvaluatorError(msg)
+ case e @ RuntimeError(msg) =>
+ EvaluationResults.RuntimeError(msg)
+ case jre: java.lang.RuntimeException =>
+ EvaluationResults.RuntimeError(jre.getMessage)
+ } finally {
+ ctx.timers.evaluators.recursive.runtime.stop()
+ }
+ }
+
+ protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): Value
+
+ def typeErrorMsg(tree : Expr, expected : TypeTree) : String = s"Type error : expected ${expected.asString}, found ${tree.asString}."
+
+}
+
+private[evaluators] trait CEvalHelpers {
+ this: ContextualEvaluator =>
+
+ def forallInstantiations(gctx:GC, fargs: Seq[ValDef], conj: Expr) = {
+
+ val henkinModel: HenkinModel = gctx.model match {
+ case hm: HenkinModel => hm
+ case _ => throw EvalError("Can't evaluate foralls without henkin model")
+ }
+
+ val vars = variablesOf(conj)
+ val args = fargs.map(_.id).filter(vars)
+ val quantified = args.toSet
+
+ val matcherQuorums = extractQuorums(conj, quantified)
+
+ matcherQuorums.flatMap { quorum =>
+ var mappings: Seq[(Identifier, Int, Int)] = Seq.empty
+ var constraints: Seq[(Expr, Int, Int)] = Seq.empty
+
+ for (((expr, args), qidx) <- quorum.zipWithIndex) {
+ val (qmappings, qconstraints) = args.zipWithIndex.partition {
+ case (Variable(id), aidx) => quantified(id)
+ case _ => false
+ }
+
+ mappings ++= qmappings.map(p => (p._1.asInstanceOf[Variable].id, qidx, p._2))
+ constraints ++= qconstraints.map(p => (p._1, qidx, p._2))
+ }
+
+ var equalities: Seq[((Int, Int), (Int, Int))] = Seq.empty
+ val mapping = for ((id, es) <- mappings.groupBy(_._1)) yield {
+ val base :: others = es.toList.map(p => (p._2, p._3))
+ equalities ++= others.map(p => base -> p)
+ (id -> base)
+ }
+
+ val argSets = quorum.foldLeft[List[Seq[Seq[Expr]]]](List(Seq.empty)) {
+ case (acc, (expr, _)) => acc.flatMap(s => henkinModel.domain(expr).map(d => s :+ d))
+ }
+
+ argSets.map { args =>
+ val argMap: Map[(Int, Int), Expr] = args.zipWithIndex.flatMap {
+ case (a, qidx) => a.zipWithIndex.map { case (e, aidx) => (qidx, aidx) -> e }
+ }.toMap
+
+ val map = mapping.map { case (id, key) => id -> argMap(key) }
+ val enabler = andJoin(constraints.map {
+ case (e, qidx, aidx) => Equals(e, argMap(qidx -> aidx))
+ } ++ equalities.map {
+ case (k1, k2) => Equals(argMap(k1), argMap(k2))
+ })
+
+ (enabler, map)
+ }
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index d732d48c0..5c951eedc 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -1,21 +1,8 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
package leon
package evaluators
-import purescala.Common._
-import purescala.Expressions._
-import purescala.Definitions._
-import purescala.Quantification._
-
-class DefaultEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluator(ctx, prog, 50000) {
- type RC = DefaultRecContext
- type GC = GlobalContext
-
- def initRC(mappings: Map[Identifier, Expr]) = DefaultRecContext(mappings)
- def initGC(model: solvers.Model) = new GlobalContext(model)
+import purescala.Definitions.Program
- case class DefaultRecContext(mappings: Map[Identifier, Expr]) extends RecContext {
- def newVars(news: Map[Identifier, Expr]) = copy(news)
- }
-}
+class DefaultEvaluator(ctx: LeonContext, prog: Program)
+ extends RecursiveEvaluator(ctx, prog, 5000)
+ with DefaultContexts
\ No newline at end of file
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
index cd843fbb1..05f60fd27 100644
--- a/src/main/scala/leon/evaluators/DualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -6,19 +6,20 @@ package evaluators
import purescala.Common._
import purescala.Expressions._
import purescala.Definitions._
-import purescala.Quantification._
import purescala.Types._
import codegen._
class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams) extends RecursiveEvaluator(ctx, prog, params.maxFunctionInvocations) {
- type RC = DefaultRecContext
+
+ type RC = DualRecContext
type GC = GlobalContext
+ def initGC(model: solvers.Model) = new GlobalContext(model, this.maxSteps)
+
implicit val debugSection = utils.DebugSectionEvaluation
- def initRC(mappings: Map[Identifier, Expr]) = DefaultRecContext(mappings)
- def initGC(model: solvers.Model) = new GlobalContext(model)
+ def initRC(mappings: Map[Identifier, Expr]): RC = DualRecContext(mappings)
var monitor = new runtime.LeonCodeGenRuntimeMonitor(params.maxFunctionInvocations)
@@ -26,7 +27,7 @@ class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams) exte
val isCompiled = prog.definedFunctions.toSet
- case class DefaultRecContext(mappings: Map[Identifier, Expr], needJVMRef: Boolean = false) extends RecContext {
+ case class DualRecContext(mappings: Map[Identifier, Expr], needJVMRef: Boolean = false) extends RecContext[DualRecContext] {
def newVars(news: Map[Identifier, Expr]) = copy(news)
}
diff --git a/src/main/scala/leon/evaluators/EvaluationResults.scala b/src/main/scala/leon/evaluators/EvaluationResults.scala
index e37c61e3b..b9cbecdde 100644
--- a/src/main/scala/leon/evaluators/EvaluationResults.scala
+++ b/src/main/scala/leon/evaluators/EvaluationResults.scala
@@ -3,14 +3,12 @@
package leon
package evaluators
-import purescala.Expressions.Expr
-
object EvaluationResults {
/** Possible results of expression evaluation. */
- sealed abstract class Result(val result : Option[Expr])
+ sealed abstract class Result[+A](val result : Option[A])
/** Represents an evaluation that successfully derived the result `value`. */
- case class Successful(value : Expr) extends Result(Some(value))
+ case class Successful[A](value : A) extends Result(Some(value))
/** Represents an evaluation that led to an error (in the program). */
case class RuntimeError(message : String) extends Result(None)
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index 9d14bd3df..9843da81d 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -6,14 +6,18 @@ package evaluators
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.Quantification._
-import purescala.ExprOps._
import solvers.Model
abstract class Evaluator(val context: LeonContext, val program: Program) extends LeonComponent {
- type EvaluationResult = EvaluationResults.Result
+ /** The type of value that this [[Evaluator]] calculates
+ * Typically, it will be [[Expr]] for deterministic evaluators, and
+ * [[Stream[Expr]]] for non-deterministic ones.
+ */
+ type Value
+
+ type EvaluationResult = EvaluationResults.Result[Value]
/** Evaluates an expression, using [[Model.mapping]] as a valuation function for the free variables. */
def eval(expr: Expr, model: Model) : EvaluationResult
@@ -29,7 +33,8 @@ abstract class Evaluator(val context: LeonContext, val program: Program) extends
/** Compiles an expression into a function, where the arguments are the free variables in the expression.
* `argorder` specifies in which order the arguments should be passed.
* The default implementation uses the evaluation function each time, but evaluators are free
- * to (and encouraged to) apply any specialization. */
+ * to (and encouraged to) apply any specialization.
+ */
def compile(expr: Expr, args: Seq[Identifier]) : Option[Model => EvaluationResult] = Some(
(model: Model) => if(args.exists(arg => !model.isDefinedAt(arg))) {
EvaluationResults.EvaluatorError("Wrong number of arguments for evaluation.")
@@ -39,3 +44,10 @@ 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/EvaluatorContexts.scala b/src/main/scala/leon/evaluators/EvaluatorContexts.scala
new file mode 100644
index 000000000..776e389dd
--- /dev/null
+++ b/src/main/scala/leon/evaluators/EvaluatorContexts.scala
@@ -0,0 +1,39 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package evaluators
+
+import purescala.Common.Identifier
+import purescala.Expressions.Expr
+import solvers.Model
+
+trait RecContext[RC <: RecContext[RC]] {
+ def mappings: Map[Identifier, Expr]
+
+ def newVars(news: Map[Identifier, Expr]): RC
+
+ def withNewVar(id: Identifier, v: Expr): RC = {
+ newVars(mappings + (id -> v))
+ }
+
+ def withNewVars(news: Map[Identifier, Expr]): RC = {
+ newVars(mappings ++ news)
+ }
+}
+
+case class DefaultRecContext(mappings: Map[Identifier, Expr]) extends RecContext[DefaultRecContext] {
+ def newVars(news: Map[Identifier, Expr]) = copy(news)
+}
+
+class GlobalContext(val model: Model, val maxSteps: Int) {
+ var stepsLeft = maxSteps
+}
+
+protected[evaluators] trait DefaultContexts extends ContextualEvaluator {
+
+ final type RC = DefaultRecContext
+ final type GC = GlobalContext
+
+ def initRC(mappings: Map[Identifier, Expr]) = DefaultRecContext(mappings)
+ def initGC(model: solvers.Model) = new GlobalContext(model, this.maxSteps)
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index fccda2aea..d1392d498 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -3,78 +3,28 @@
package leon
package evaluators
+import leon.purescala.Constructors._
+import leon.purescala.ExprOps._
+import leon.purescala.Expressions.Pattern
+import leon.purescala.Extractors._
+import leon.purescala.Quantification._
+import leon.purescala.TypeOps._
+import leon.purescala.Types._
+import leon.solvers.{SolverFactory, HenkinModel}
import purescala.Common._
-import purescala.Definitions._
-import purescala.ExprOps._
import purescala.Expressions._
-import purescala.Types._
-import purescala.TypeOps.isSubtypeOf
-import purescala.Constructors._
-import purescala.Extractors._
-import purescala.Quantification._
-import solvers.{Model, HenkinModel}
-import solvers.SolverFactory
-
-abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int) extends Evaluator(ctx, prog) {
- val name = "evaluator"
- val description = "Recursive interpreter for PureScala expressions"
-
- private implicit val _ = ctx
-
- type RC <: RecContext
- type GC <: GlobalContext
-
- case class EvalError(msg : String) extends Exception
- case class RuntimeError(msg : String) extends Exception
-
- val scalaEv = new ScalacEvaluator(this, ctx, prog)
-
- trait RecContext {
- def mappings: Map[Identifier, Expr]
-
- def newVars(news: Map[Identifier, Expr]): RC
-
- def withNewVar(id: Identifier, v: Expr): RC = {
- newVars(mappings + (id -> v))
- }
+import purescala.Definitions._
- def withNewVars(news: Map[Identifier, Expr]): RC = {
- newVars(mappings ++ news)
- }
- }
+abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int)
+ extends ContextualEvaluator(ctx, prog, maxSteps)
+ with DeterministicEvaluator {
- class GlobalContext(val model: Model) {
- def maxSteps = RecursiveEvaluator.this.maxSteps
+ val name = "evaluator"
+ val description = "Recursive interpreter for PureScala expressions"
- var stepsLeft = maxSteps
- }
+ lazy val scalaEv = new ScalacEvaluator(this, ctx, prog)
- def initRC(mappings: Map[Identifier, Expr]): RC
- def initGC(model: Model): GC
-
- // Used by leon-web, please do not delete
- var lastGC: Option[GC] = None
-
- private[this] var clpCache = Map[(Choose, Seq[Expr]), Expr]()
-
- def eval(ex: Expr, model: Model) = {
- try {
- lastGC = Some(initGC(model))
- ctx.timers.evaluators.recursive.runtime.start()
- EvaluationResults.Successful(e(ex)(initRC(model.toMap), lastGC.get))
- } catch {
- case so: StackOverflowError =>
- EvaluationResults.EvaluatorError("Stack overflow")
- case EvalError(msg) =>
- EvaluationResults.EvaluatorError(msg)
- case e @ RuntimeError(msg) =>
- EvaluationResults.RuntimeError(msg)
- case jre: java.lang.RuntimeException =>
- EvaluationResults.RuntimeError(jre.getMessage)
- } finally {
- ctx.timers.evaluators.recursive.runtime.stop()
- }
- }
+ protected var clpCache = Map[(Choose, Seq[Expr]), Expr]()
protected def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
case Variable(id) =>
@@ -195,9 +145,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
callResult
- case And(args) if args.isEmpty =>
- BooleanLiteral(true)
-
+ case And(args) if args.isEmpty => BooleanLiteral(true)
case And(args) =>
e(args.head) match {
case BooleanLiteral(false) => BooleanLiteral(false)
@@ -220,9 +168,10 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
}
case Implies(l,r) =>
- (e(l), e(r)) match {
- case (BooleanLiteral(b1),BooleanLiteral(b2)) => BooleanLiteral(!b1 || b2)
- case (le, re) => throw EvalError(typeErrorMsg(le, BooleanType))
+ e(l) match {
+ case BooleanLiteral(false) => BooleanLiteral(true)
+ case BooleanLiteral(true) => e(r)
+ case le => throw EvalError(typeErrorMsg(le, BooleanType))
}
case Equals(le,re) =>
@@ -273,7 +222,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case RealPlus(l, r) =>
(e(l), e(r)) match {
case (FractionalLiteral(ln, ld), FractionalLiteral(rn, rd)) =>
- normalizeFraction(FractionalLiteral((ln * rd + rn * ld), (ld * rd)))
+ normalizeFraction(FractionalLiteral(ln * rd + rn * ld, ld * rd))
case (le, re) => throw EvalError(typeErrorMsg(le, RealType))
}
@@ -379,7 +328,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (FractionalLiteral(ln, ld), FractionalLiteral(rn, rd)) =>
if (rn != 0)
- normalizeFraction(FractionalLiteral((ln * rd), (ld * rn)))
+ normalizeFraction(FractionalLiteral(ln * rd, ld * rn))
else throw RuntimeError("Division by 0.")
case (le,re) => throw EvalError(typeErrorMsg(le, RealType))
}
@@ -426,8 +375,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 < i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 < i2)
case (a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) =>
- val FractionalLiteral(n, _) = e(RealMinus(a, b))
- BooleanLiteral(n < 0)
+ val FractionalLiteral(n, _) = e(RealMinus(a, b))
+ BooleanLiteral(n < 0)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 < c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -437,8 +386,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 > i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 > i2)
case (a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) =>
- val FractionalLiteral(n, _) = e(RealMinus(a, b))
- BooleanLiteral(n > 0)
+ val FractionalLiteral(n, _) = e(RealMinus(a, b))
+ BooleanLiteral(n > 0)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 > c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -448,8 +397,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 <= i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 <= i2)
case (a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) =>
- val FractionalLiteral(n, _) = e(RealMinus(a, b))
- BooleanLiteral(n <= 0)
+ val FractionalLiteral(n, _) = e(RealMinus(a, b))
+ BooleanLiteral(n <= 0)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 <= c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -459,8 +408,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 >= i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 >= i2)
case (a @ FractionalLiteral(_, _), b @ FractionalLiteral(_, _)) =>
- val FractionalLiteral(n, _) = e(RealMinus(a, b))
- BooleanLiteral(n >= 0)
+ val FractionalLiteral(n, _) = e(RealMinus(a, b))
+ BooleanLiteral(n >= 0)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 >= c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -475,21 +424,19 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case SetIntersection(s1,s2) =>
(e(s1), e(s2)) match {
- case (f @ FiniteSet(els1, _), FiniteSet(els2, _)) => {
+ case (f @ FiniteSet(els1, _), FiniteSet(els2, _)) =>
val newElems = els1 intersect els2
val SetType(tpe) = f.getType
FiniteSet(newElems, tpe)
- }
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
case SetDifference(s1,s2) =>
(e(s1), e(s2)) match {
- case (f @ FiniteSet(els1, _),FiniteSet(els2, _)) => {
+ case (f @ FiniteSet(els1, _),FiniteSet(els2, _)) =>
val SetType(tpe) = f.getType
val newElems = els1 -- els2
FiniteSet(newElems, tpe)
- }
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
@@ -520,59 +467,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
PartialLambda(mapping.map(p => p._1.map(e) -> e(p._2)), tpe)
case f @ Forall(fargs, TopLevelAnds(conjuncts)) =>
- val henkinModel: HenkinModel = gctx.model match {
- case hm: HenkinModel => hm
- case _ => throw EvalError("Can't evaluate foralls without henkin model")
- }
-
e(andJoin(for (conj <- conjuncts) yield {
- val vars = variablesOf(conj)
- val args = fargs.map(_.id).filter(vars)
- val quantified = args.toSet
-
- val matcherQuorums = extractQuorums(conj, quantified)
-
- val instantiations = matcherQuorums.flatMap { quorum =>
- var mappings: Seq[(Identifier, Int, Int)] = Seq.empty
- var constraints: Seq[(Expr, Int, Int)] = Seq.empty
-
- for (((expr, args), qidx) <- quorum.zipWithIndex) {
- val (qmappings, qconstraints) = args.zipWithIndex.partition {
- case (Variable(id),aidx) => quantified(id)
- case _ => false
- }
-
- mappings ++= qmappings.map(p => (p._1.asInstanceOf[Variable].id, qidx, p._2))
- constraints ++= qconstraints.map(p => (p._1, qidx, p._2))
- }
-
- var equalities: Seq[((Int, Int), (Int, Int))] = Seq.empty
- val mapping = for ((id, es) <- mappings.groupBy(_._1)) yield {
- val base :: others = es.toList.map(p => (p._2, p._3))
- equalities ++= others.map(p => base -> p)
- (id -> base)
- }
-
- val argSets = quorum.foldLeft[List[Seq[Seq[Expr]]]](List(Seq.empty)) {
- case (acc, (expr, _)) => acc.flatMap(s => henkinModel.domain(expr).map(d => s :+ d))
- }
-
- argSets.map { args =>
- val argMap: Map[(Int, Int), Expr] = args.zipWithIndex.flatMap {
- case (a, qidx) => a.zipWithIndex.map { case (e, aidx) => (qidx, aidx) -> e }
- }.toMap
-
- val map = mapping.map { case (id, key) => id -> argMap(key) }
- val enabler = andJoin(constraints.map {
- case (e, qidx, aidx) => Equals(e, argMap(qidx -> aidx))
- } ++ equalities.map {
- case (k1, k2) => Equals(argMap(k1), argMap(k2))
- })
-
- (enabler, map)
- }
- }
-
+ val instantiations = forallInstantiations(gctx, fargs, conj)
e(andJoin(instantiations.map { case (enabler, mapping) =>
e(Implies(enabler, conj))(rctx.withNewVars(mapping), gctx)
}))
@@ -631,9 +527,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (l, r) => throw EvalError(typeErrorMsg(l, m.getType))
}
- case gv: GenericValue =>
- gv
-
case p : Passes =>
e(p.asConstraint)
@@ -702,6 +595,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
throw RuntimeError("MatchError: "+rscrut.asString+" did not match any of the cases")
}
+ case gl: GenericValue => gl
case fl : FractionalLiteral => normalizeFraction(fl)
case l : Literal[_] => l
@@ -784,6 +678,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
}
}
- def typeErrorMsg(tree : Expr, expected : TypeTree) : String = s"Type error : expected ${expected.asString}, found ${tree.asString}."
+
}
+
diff --git a/src/main/scala/leon/evaluators/ScalacEvaluator.scala b/src/main/scala/leon/evaluators/ScalacEvaluator.scala
index 7c4d8ee92..63bb9f6fa 100644
--- a/src/main/scala/leon/evaluators/ScalacEvaluator.scala
+++ b/src/main/scala/leon/evaluators/ScalacEvaluator.scala
@@ -11,13 +11,8 @@ import purescala.Expressions._
import purescala.Types._
import java.io.File
-import java.nio.file.Files
-import java.net.{URL, URLClassLoader}
-import java.lang.reflect.{Constructor, Method}
-
-import frontends.scalac.FullScalaCompiler
-
-import scala.tools.nsc.{Settings=>NSCSettings,CompilerCommand}
+import java.net.URLClassLoader
+import java.lang.reflect.Constructor
/**
* Call scalac-compiled functions from within Leon
@@ -25,7 +20,7 @@ import scala.tools.nsc.{Settings=>NSCSettings,CompilerCommand}
* Known limitations:
* - Multiple argument lists
*/
-class ScalacEvaluator(ev: Evaluator, ctx: LeonContext, pgm: Program) extends LeonComponent {
+class ScalacEvaluator(ev: DeterministicEvaluator, ctx: LeonContext, pgm: Program) extends LeonComponent {
implicit val _: Program = pgm
val name = "Evaluator of external functions"
@@ -300,11 +295,11 @@ class ScalacEvaluator(ev: Evaluator, ctx: LeonContext, pgm: Program) extends Leo
/**
* Black magic here we come!
*/
- import org.objectweb.asm.ClassReader;
- import org.objectweb.asm.ClassWriter;
- import org.objectweb.asm.ClassVisitor;
- import org.objectweb.asm.MethodVisitor;
- import org.objectweb.asm.Opcodes;
+ import org.objectweb.asm.ClassReader
+ import org.objectweb.asm.ClassWriter
+ import org.objectweb.asm.ClassVisitor
+ import org.objectweb.asm.MethodVisitor
+ import org.objectweb.asm.Opcodes
class InterceptingClassLoader(p: ClassLoader) extends ClassLoader(p) {
import java.io._
@@ -320,24 +315,24 @@ class ScalacEvaluator(ev: Evaluator, ctx: LeonContext, pgm: Program) extends Leo
if (!(toInstrument contains name)) {
super.loadClass(name, resolve)
} else {
- val bs = new ByteArrayOutputStream();
- val is = getResourceAsStream(name.replace('.', '/') + ".class");
- val buf = new Array[Byte](512);
- var len = is.read(buf);
+ val bs = new ByteArrayOutputStream()
+ val is = getResourceAsStream(name.replace('.', '/') + ".class")
+ val buf = new Array[Byte](512)
+ var len = is.read(buf)
while (len > 0) {
- bs.write(buf, 0, len);
+ bs.write(buf, 0, len)
len = is.read(buf)
}
// Transform bytecode
- val cr = new ClassReader(bs.toByteArray());
- val cw = new ClassWriter(cr, ClassWriter.COMPUTE_FRAMES);
- val cv = new LeonCallsClassVisitor(cw, name, toInstrument(name));
- cr.accept(cv, 0);
+ val cr = new ClassReader(bs.toByteArray())
+ val cw = new ClassWriter(cr, ClassWriter.COMPUTE_FRAMES)
+ val cv = new LeonCallsClassVisitor(cw, name, toInstrument(name))
+ cr.accept(cv, 0)
- val res = cw.toByteArray();
+ val res = cw.toByteArray()
- defineClass(name, res, 0, res.length);
+ defineClass(name, res, 0, res.length)
}
}
}
@@ -451,7 +446,7 @@ class ScalacEvaluator(ev: Evaluator, ctx: LeonContext, pgm: Program) extends Leo
unbox(fd.returnType)
mv.visitInsn(returnOpCode(fd.returnType))
- mv.visitEnd();
+ mv.visitEnd()
}
}
}
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
new file mode 100644
index 000000000..5b387368b
--- /dev/null
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -0,0 +1,591 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package evaluators
+
+import purescala.Constructors._
+import purescala.ExprOps._
+import purescala.Extractors._
+import purescala.TypeOps._
+import purescala.Types._
+import purescala.Common.Identifier
+import purescala.Definitions.{TypedFunDef, Program}
+import purescala.Expressions._
+
+import leon.solvers.SolverFactory
+import leon.utils.StreamUtils.cartesianProduct
+
+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"
+
+ case class NDValue(tp: TypeTree) extends Expr with Terminal {
+ val getType = tp
+ }
+
+ protected[evaluators] def e(expr: Expr)(implicit rctx: RC, gctx: GC): Stream[Expr] = expr match {
+ case Variable(id) =>
+ rctx.mappings.get(id).toStream
+
+ case Application(caller, args) =>
+ for {
+ cl <- e(caller).distinct
+ newArgs <- cartesianProduct(args map e).distinct
+ res <- cl match {
+ case l @ Lambda(params, body) =>
+ val mapping = l.paramSubst(newArgs)
+ e(body)(rctx.withNewVars(mapping), gctx).distinct
+ case PartialLambda(mapping, _) =>
+ mapping.collectFirst {
+ case (pargs, res) if (newArgs zip pargs).forall { case (f, r) => f == r } =>
+ res
+ }.toStream
+ case _ =>
+ Stream()
+ }
+ } yield res
+
+ case Let(i,v,b) =>
+ for {
+ ev <- e(v).distinct
+ eb <- e(b)(rctx.withNewVar(i, ev), gctx).distinct
+ } yield eb
+
+ case Assert(cond, oerr, body) =>
+ e(IfExpr(Not(cond), Error(expr.getType, oerr.getOrElse("Assertion failed @"+expr.getPos)), body))
+
+ case en@Ensuring(body, post) =>
+ if ( exists{
+ case Hole(_,_) => true
+ case WithOracle(_,_) => true
+ case _ => false
+ }(en)) {
+ import synthesis.ConversionPhase.convert
+ e(convert(en, ctx))
+ } else {
+ e(en.toAssert)
+ }
+
+ case Error(tpe, desc) =>
+ Stream()
+
+ case NDValue(tp) =>
+ import grammars.ValueGrammar
+ ValueGrammar.getProductions(tp).toStream.map{ g => g.builder(Seq())}
+
+ case IfExpr(cond, thenn, elze) =>
+ e(cond).distinct.flatMap {
+ case BooleanLiteral(true) => e(thenn)
+ case BooleanLiteral(false) => e(elze)
+ case other => Stream()
+ }.distinct
+
+ case FunctionInvocation(TypedFunDef(fd, Seq(tp)), Seq(set)) if fd == program.library.setToList.get =>
+ val cons = program.library.Cons.get
+ val nil = CaseClass(CaseClassType(program.library.Nil.get, Seq(tp)), Seq())
+ def mkCons(h: Expr, t: Expr) = CaseClass(CaseClassType(cons, Seq(tp)), Seq(h,t))
+ e(set).distinct.collect {
+ case FiniteSet(els, _) =>
+ els.foldRight(nil)(mkCons)
+ }.distinct
+
+ case FunctionInvocation(tfd, args) =>
+ if (gctx.stepsLeft < 0) {
+ return Stream()
+ }
+ gctx.stepsLeft -= 1
+
+ for {
+ evArgs <- cartesianProduct(args map e).distinct
+ // build a mapping for the function...
+ frame = rctx.withNewVars(tfd.paramSubst(evArgs))
+ BooleanLiteral(true) <- e(tfd.precOrTrue)(frame, gctx).distinct
+ body <- tfd.body.orElse(rctx.mappings.get(tfd.id)).toStream
+ callResult <- e(body)(frame, gctx).distinct
+ BooleanLiteral(true) <- e(application(tfd.postOrTrue, Seq(callResult)))(frame, gctx).distinct
+ } yield callResult
+
+ case And(args) if args.isEmpty =>
+ Stream(BooleanLiteral(true))
+ case And(args) =>
+ e(args.head).distinct.flatMap {
+ case BooleanLiteral(false) => Stream(BooleanLiteral(false))
+ case BooleanLiteral(true) => e(andJoin(args.tail))
+ case other => Stream()
+ }
+
+ case Or(args) if args.isEmpty =>
+ Stream(BooleanLiteral(false))
+ case Or(args) =>
+ e(args.head).distinct.flatMap {
+ case BooleanLiteral(true) => Stream(BooleanLiteral(true))
+ case BooleanLiteral(false) => e(orJoin(args.tail))
+ case other => Stream()
+ }
+
+ case Implies(lhs, rhs) =>
+ e(Or(Not(lhs), rhs))
+
+ case l @ Lambda(_, _) =>
+ val (nl, structSubst) = normalizeStructure(l)
+ val mapping = variablesOf(l).map(id =>
+ structSubst(id) -> (e(Variable(id)) match {
+ case Stream(v) => v
+ case _ => return Stream()
+ })
+ ).toMap
+ Stream(replaceFromIDs(mapping, nl))
+
+ case PartialLambda(mapping, tpe) =>
+ def solveOne(pair: (Seq[Expr], Expr)) = {
+ val (args, res) = pair
+ for {
+ as <- cartesianProduct(args map e)
+ r <- e(res)
+ } yield as -> r
+ }
+ cartesianProduct(mapping map solveOne) map (PartialLambda(_, tpe))
+
+ case f @ Forall(fargs, TopLevelAnds(conjuncts)) =>
+
+ def solveOne(conj: Expr) = {
+ val instantiations = forallInstantiations(gctx, fargs, conj)
+ for {
+ es <- cartesianProduct(instantiations.map { case (enabler, mapping) =>
+ e(Implies(enabler, conj))(rctx.withNewVars(mapping), gctx)
+ })
+ res <- e(andJoin(es))
+ } yield res
+ }
+
+ for {
+ conj <- cartesianProduct(conjuncts map solveOne)
+ res <- e(andJoin(conj))
+ } yield res
+
+ case p : Passes =>
+ e(p.asConstraint)
+
+ case choose: Choose =>
+
+ // TODO add memoization
+ implicit val debugSection = utils.DebugSectionSynthesis
+
+ val p = synthesis.Problem.fromSpec(choose.pred)
+
+ ctx.reporter.debug("Executing choose!")
+
+ val tStart = System.currentTimeMillis
+
+ val solverf = SolverFactory.getFromSettings(ctx, program)
+ val solver = solverf.getNewSolver()
+
+ try {
+ val eqs = p.as.map {
+ case id =>
+ Equals(Variable(id), rctx.mappings(id))
+ }
+
+ val cnstr = andJoin(eqs ::: p.pc :: p.phi :: Nil)
+ solver.assertCnstr(cnstr)
+
+ def getSolution = try {
+ solver.check match {
+ case Some(true) =>
+ val model = solver.getModel
+
+ val valModel = valuateWithModel(model) _
+
+ 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)
+
+ Some(leonRes)
+ case _ =>
+ None
+ }
+ } catch {
+ case _: Throwable => None
+ }
+
+ Stream.iterate(getSolution)(prev => {
+ val ensureDistinct = Not(Equals(tupleWrap(p.xs.map{ _.toVariable}), prev.get))
+ solver.assertCnstr(ensureDistinct)
+ 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()
+ }
+
+ case MatchExpr(scrut, cases) =>
+
+ def matchesCase(scrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Stream[(MatchCase, Map[Identifier, Expr])] = {
+ import purescala.TypeOps.isSubtypeOf
+
+ def matchesPattern(pat: Pattern, expr: Expr): Stream[Map[Identifier, Expr]] = (pat, expr) match {
+ case (InstanceOfPattern(ob, pct), e) =>
+ (if (isSubtypeOf(e.getType, pct)) {
+ Some(obind(ob, e))
+ } else {
+ None
+ }).toStream
+ case (WildcardPattern(ob), e) =>
+ Stream(obind(ob, e))
+
+ case (CaseClassPattern(ob, pct, subs), CaseClass(ct, args)) =>
+ if (pct == ct) {
+ val subMaps = (subs zip args).map{ case (s, a) => matchesPattern(s, a) }
+ cartesianProduct(subMaps).map( _.flatten.toMap ++ obind(ob, expr))
+ } else {
+ Stream()
+ }
+ case (up @ UnapplyPattern(ob, _, subs), scrut) =>
+ e(FunctionInvocation(up.unapplyFun, Seq(scrut))) flatMap {
+ case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.Nil.get =>
+ None
+ case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Cons.get =>
+ val subMaps = subs zip unwrapTuple(arg, up.unapplyFun.returnType.isInstanceOf[TupleType]) map {
+ case (s,a) => matchesPattern(s,a)
+ }
+ cartesianProduct(subMaps).map( _.flatten.toMap ++ obind(ob, expr))
+ case other =>
+ None
+ }
+ case (TuplePattern(ob, subs), Tuple(args)) =>
+ if (subs.size == args.size) {
+ val subMaps = (subs zip args).map { case (s, a) => matchesPattern(s, a) }
+ cartesianProduct(subMaps).map(_.flatten.toMap ++ obind(ob, expr))
+ } else Stream()
+ case (LiteralPattern(ob, l1) , l2 : Literal[_]) if l1 == l2 =>
+ Stream(obind(ob,l1))
+ case _ => Stream()
+ }
+
+ def obind(ob: Option[Identifier], e: Expr): Map[Identifier, Expr] = {
+ Map[Identifier, Expr]() ++ ob.map(id => id -> e)
+ }
+
+ caze match {
+ case SimpleCase(p, rhs) =>
+ matchesPattern(p, scrut).map(r =>
+ (caze, r)
+ )
+
+ case GuardedCase(p, g, rhs) =>
+ for {
+ r <- matchesPattern(p, scrut)
+ BooleanLiteral(true) <- e(g)(rctx.withNewVars(r), gctx)
+ } yield (caze, r)
+ }
+ }
+
+ for {
+ rscrut <- e(scrut)
+ cs <- cases.toStream.map(c => matchesCase(rscrut, c)).find(_.nonEmpty).toStream
+ (c, mp) <- cs
+ res <- e(c.rhs)(rctx.withNewVars(mp), gctx)
+ } yield res
+
+ case Operator(es, _) =>
+ cartesianProduct(es map e) flatMap { es =>
+ try {
+ Some(step(expr, es))
+ } catch {
+ case _: RuntimeError =>
+ // EvalErrors stop the computation alltogether
+ None
+ }
+ }
+
+ case other =>
+ context.reporter.error(other.getPos, "Error: don't know how to handle " + other.asString + " in Evaluator ("+other.getClass+").")
+ Stream()
+ }
+
+
+ protected def step(expr: Expr, subs: Seq[Expr])(implicit rctx: RC, gctx: GC): Expr = (expr, subs) match {
+ case (Tuple(_), ts) =>
+ Tuple(ts)
+
+ case (TupleSelect(_, i), rs) =>
+ rs(i - 1)
+
+ case (Assert(_, oerr, _), Seq(BooleanLiteral(cond), body)) =>
+ if (cond) body
+ else throw RuntimeError(oerr.getOrElse("Assertion failed @" + expr.getPos))
+
+ case (Error(_, desc), _) =>
+ throw RuntimeError("Error reached in evaluation: " + desc)
+
+ case (FunctionInvocation(TypedFunDef(fd, Seq(tp)), _), Seq(FiniteSet(els, _))) if fd == program.library.setToList.get =>
+ val cons = program.library.Cons.get
+ val nil = CaseClass(CaseClassType(program.library.Nil.get, Seq(tp)), Seq())
+ def mkCons(h: Expr, t: Expr) = CaseClass(CaseClassType(cons, Seq(tp)), Seq(h, t))
+ els.foldRight(nil)(mkCons)
+
+ case (Not(_), Seq(BooleanLiteral(arg))) =>
+ BooleanLiteral(!arg)
+
+ case (Implies(_, _) Seq (BooleanLiteral(b1), BooleanLiteral(b2))) =>
+ BooleanLiteral(!b1 || b2)
+
+ case (Equals(_, _), Seq(lv, rv)) =>
+ (lv, rv) match {
+ case (FiniteSet(el1, _), FiniteSet(el2, _)) => BooleanLiteral(el1 == el2)
+ case (FiniteMap(el1, _, _), FiniteMap(el2, _, _)) => BooleanLiteral(el1.toSet == el2.toSet)
+ case (PartialLambda(m1, _), PartialLambda(m2, _)) => BooleanLiteral(m1.toSet == m2.toSet)
+ case _ => BooleanLiteral(lv == rv)
+ }
+
+ case (CaseClass(cd, _), args) =>
+ CaseClass(cd, args)
+
+ case (AsInstanceOf(_, ct), Seq(ce)) =>
+ if (isSubtypeOf(ce.getType, ct)) {
+ ce
+ } else {
+ throw RuntimeError("Cast error: cannot cast " + ce.asString + " to " + ct.asString)
+ }
+
+ case (IsInstanceOf(_, ct), Seq(ce)) =>
+ BooleanLiteral(isSubtypeOf(ce.getType, ct))
+
+ case (CaseClassSelector(ct1, _, sel), Seq(CaseClass(ct2, args))) if ct1 == ct2 =>
+ args(ct1.classDef.selectorID2Index(sel))
+
+ case (Plus(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
+ InfiniteIntegerLiteral(i1 + i2)
+
+ case (Minus(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
+ InfiniteIntegerLiteral(i1 - i2)
+
+ case (Times(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
+ InfiniteIntegerLiteral(i1 * i2)
+
+ case (Division(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
+ if (i2 != BigInt(0)) InfiniteIntegerLiteral(i1 / i2)
+ else throw RuntimeError("Division by 0.")
+
+ case (Remainder(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
+ if (i2 != BigInt(0)) InfiniteIntegerLiteral(i1 % i2)
+ else throw RuntimeError("Remainder of division by 0.")
+
+ case (Modulo(_, _), Seq(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2))) =>
+ if (i2 < 0)
+ InfiniteIntegerLiteral(i1 mod (-i2))
+ else if (i2 != BigInt(0))
+ InfiniteIntegerLiteral(i1 mod i2)
+ 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))
+
+ case (RealMinus(_, _), Seq(FractionalLiteral(ln, ld), FractionalLiteral(rn, rd))) =>
+ normalizeFraction(FractionalLiteral(ln * rd - rn * ld, ld * rd))
+
+ case (RealTimes(_, _), Seq(FractionalLiteral(ln, ld), FractionalLiteral(rn, rd))) =>
+ normalizeFraction(FractionalLiteral(ln * rn, ld * rd))
+
+ case (RealDivision(_, _), Seq(FractionalLiteral(ln, ld), FractionalLiteral(rn, rd))) =>
+ if (rn != 0) normalizeFraction(FractionalLiteral(ln * rd, ld * rn))
+ else throw RuntimeError("Division by 0.")
+
+ case (BVPlus(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
+ IntLiteral(i1 + i2)
+
+ case (BVMinus(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
+ IntLiteral(i1 - i2)
+
+ case (BVUMinus(_), Seq(IntLiteral(i))) =>
+ IntLiteral(-i)
+
+ case (RealUMinus(_), Seq(FractionalLiteral(n, d))) =>
+ FractionalLiteral(-n, d)
+
+ case (BVNot(_), Seq(IntLiteral(i))) =>
+ IntLiteral(~i)
+
+ case (BVTimes(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
+ IntLiteral(i1 * i2)
+
+ case (BVDivision(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
+ if (i2 != 0) IntLiteral(i1 / i2)
+ else throw RuntimeError("Division by 0.")
+
+ case (BVRemainder(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
+ if (i2 != 0) IntLiteral(i1 % i2)
+ else throw RuntimeError("Remainder of division by 0.")
+
+ case (BVAnd(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
+ IntLiteral(i1 & i2)
+
+ case (BVOr(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
+ IntLiteral(i1 | i2)
+
+ case (BVXOr(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
+ IntLiteral(i1 ^ i2)
+
+ case (BVShiftLeft(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
+ IntLiteral(i1 << i2)
+
+ case (BVAShiftRight(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
+ IntLiteral(i1 >> i2)
+
+ case (BVLShiftRight(_, _), Seq(IntLiteral(i1), IntLiteral(i2))) =>
+ IntLiteral(i1 >>> i2)
+
+ case (LessThan(_, _), Seq(el, er)) =>
+ (el, er) match {
+ case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 < i2)
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 < i2)
+ case (a@FractionalLiteral(_, _), b@FractionalLiteral(_, _)) =>
+ val FractionalLiteral(n, _) = e(RealMinus(a, b)).head
+ BooleanLiteral(n < 0)
+ case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 < c2)
+ case (le, re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ }
+
+ case (GreaterThan(_, _), Seq(el, er)) =>
+ (el, er) match {
+ case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 > i2)
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 > i2)
+ case (a@FractionalLiteral(_, _), b@FractionalLiteral(_, _)) =>
+ val FractionalLiteral(n, _) = e(RealMinus(a, b)).head
+ BooleanLiteral(n > 0)
+ case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 > c2)
+ case (le, re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ }
+
+ case (LessEquals(_, _), Seq(el, er)) =>
+ (el, er) match {
+ case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 <= i2)
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 <= i2)
+ case (a@FractionalLiteral(_, _), b@FractionalLiteral(_, _)) =>
+ val FractionalLiteral(n, _) = e(RealMinus(a, b)).head
+ BooleanLiteral(n <= 0)
+ case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 <= c2)
+ case (le, re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ }
+
+ case (GreaterEquals(_, _), Seq(el, er)) =>
+ (el, er) match {
+ case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 >= i2)
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 >= i2)
+ case (a@FractionalLiteral(_, _), b@FractionalLiteral(_, _)) =>
+ val FractionalLiteral(n, _) = e(RealMinus(a, b)).head
+ BooleanLiteral(n >= 0)
+ case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 >= c2)
+ case (le, re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ }
+
+ case (IsTyped(su@SetUnion(s1, s2), tpe), Seq(
+ IsTyped(FiniteSet(els1, _), SetType(tpe1)),
+ IsTyped(FiniteSet(els2, _), SetType(tpe2))
+ )) =>
+ FiniteSet(
+ els1 ++ els2,
+ leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(su, tpe)))
+ )
+
+ case (IsTyped(su@SetIntersection(s1, s2), tpe), Seq(
+ IsTyped(FiniteSet(els1, _), SetType(tpe1)),
+ IsTyped(FiniteSet(els2, _), SetType(tpe2))
+ )) =>
+ FiniteSet(
+ els1 & els2,
+ leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(su, tpe)))
+ )
+
+ case (IsTyped(su@SetDifference(s1, s2), tpe), Seq(
+ IsTyped(FiniteSet(els1, _), SetType(tpe1)),
+ IsTyped(FiniteSet(els2, _), SetType(tpe2))
+ )) =>
+ FiniteSet(
+ els1 -- els2,
+ leastUpperBound(tpe1, tpe2).getOrElse(throw EvalError(typeErrorMsg(su, tpe)))
+ )
+
+ case (ElementOfSet(_, _), Seq(e, FiniteSet(els, _))) =>
+ BooleanLiteral(els.contains(e))
+
+ case (SubsetOf(_, _), Seq(FiniteSet(els1, _), FiniteSet(els2, _))) =>
+ BooleanLiteral(els1.subsetOf(els2))
+
+ case (SetCardinality(_), Seq(FiniteSet(els, _))) =>
+ IntLiteral(els.size)
+
+ case (FiniteSet(_, base), els) =>
+ FiniteSet(els.toSet, base)
+
+ case (ArrayLength(_), Seq(FiniteArray(_, _, IntLiteral(length)))) =>
+ IntLiteral(length)
+
+ case (ArrayUpdated(_, _, _), Seq(
+ IsTyped(FiniteArray(elems, default, length), ArrayType(tp)),
+ IntLiteral(i),
+ v
+ )) =>
+ finiteArray(elems.updated(i, v), default map {(_, length)}, tp)
+
+ case (ArraySelect(_, _), Seq(fa@FiniteArray(elems, default, IntLiteral(length)), IntLiteral(index))) =>
+ elems
+ .get(index)
+ .orElse(if (index >= 0 && index < length) default else None)
+ .getOrElse(throw RuntimeError(s"Array out of bounds error during evaluation:\n array = $fa, index = $index"))
+
+ case (fa@FiniteArray(_, _, _), subs) =>
+ val Operator(_, builder) = fa
+ builder(subs)
+
+ case (fm@FiniteMap(_, _, _), subs) =>
+ val Operator(_, builder) = fm
+ builder(subs)
+
+ case (g@MapApply(_, _), Seq(FiniteMap(m, _, _), k)) =>
+ m.getOrElse(k, throw RuntimeError("Key not found: " + k.asString))
+
+ case (u@IsTyped(MapUnion(_, _), MapType(kT, vT)), Seq(FiniteMap(m1, _, _), FiniteMap(m2, _, _))) =>
+ FiniteMap(m1 ++ m2, kT, vT)
+
+ case (i@MapIsDefinedAt(_, _), Seq(FiniteMap(elems, _, _), k)) =>
+ BooleanLiteral(elems.contains(k))
+
+ case (gv: GenericValue, Seq()) =>
+ gv
+
+ case (fl: FractionalLiteral, Seq()) =>
+ normalizeFraction(fl)
+
+ case (l: Literal[_], Seq()) =>
+ 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/evaluators/TracingEvaluator.scala b/src/main/scala/leon/evaluators/TracingEvaluator.scala
index ec977763f..ad2d5723e 100644
--- a/src/main/scala/leon/evaluators/TracingEvaluator.scala
+++ b/src/main/scala/leon/evaluators/TracingEvaluator.scala
@@ -6,7 +6,6 @@ package evaluators
import purescala.Common._
import purescala.Expressions._
import purescala.Definitions._
-import purescala.Quantification._
import purescala.Types._
class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) extends RecursiveEvaluator(ctx, prog, maxSteps) {
@@ -17,9 +16,9 @@ class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) ex
def initGC(model: solvers.Model) = new TracingGlobalContext(Nil, model)
- class TracingGlobalContext(var values: List[(Tree, Expr)], model: solvers.Model) extends GlobalContext(model)
+ class TracingGlobalContext(var values: List[(Tree, Expr)], model: solvers.Model) extends GlobalContext(model, maxSteps)
- case class TracingRecContext(mappings: Map[Identifier, Expr], tracingFrames: Int) extends RecContext {
+ case class TracingRecContext(mappings: Map[Identifier, Expr], tracingFrames: Int) extends RecContext[TracingRecContext] {
def newVars(news: Map[Identifier, Expr]) = copy(mappings = news)
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index cc1b716fe..103ed1bee 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -543,6 +543,7 @@ object Definitions {
def precondition = fd.precondition map cached
def precOrTrue = cached(fd.precOrTrue)
def postcondition = fd.postcondition map cached
+ def postOrTrue = cached(fd.postOrTrue)
def hasImplementation = body.isDefined
def hasBody = hasImplementation
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index c8cf8f118..7f7359795 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -47,7 +47,7 @@ object Extractors {
val builder = (as: Seq[Expr]) => {
def rec(kvs: Seq[Expr]): Seq[(Seq[Expr], Expr)] = kvs match {
case seq if seq.size >= sze =>
- val ((args :+ res), rest) = seq.splitAt(sze)
+ val (args :+ res, rest) = seq.splitAt(sze)
(args -> res) +: rec(rest)
case Seq() => Seq.empty
case _ => sys.error("unexpected number of key/value expressions")
@@ -195,10 +195,7 @@ object Extractors {
{ case Seq(c, t, e) => IfExpr(c, t, e) }
))
case MatchExpr(scrut, cases) => Some((
- scrut +: cases.flatMap {
- case SimpleCase(_, e) => Seq(e)
- case GuardedCase(_, e1, e2) => Seq(e1, e2)
- },
+ scrut +: cases.flatMap { _.expressions },
(es: Seq[Expr]) => {
var i = 1
val newcases = for (caze <- cases) yield caze match {
@@ -210,9 +207,8 @@ object Extractors {
}
))
case Passes(in, out, cases) => Some((
- in +: out +: cases.flatMap {
- _.expressions
- }, {
+ in +: out +: cases.flatMap { _.expressions },
+ {
case Seq(in, out, es@_*) => {
var i = 0
val newcases = for (caze <- cases) yield caze match {
diff --git a/src/main/scala/leon/repair/RepairNDEvaluator.scala b/src/main/scala/leon/repair/RepairNDEvaluator.scala
index d3e0df174..e9d63b1b9 100644
--- a/src/main/scala/leon/repair/RepairNDEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairNDEvaluator.scala
@@ -16,7 +16,7 @@ import scala.util.Try
// If a function invocation fails or violates a postcondition for cond,
// it backtracks and gets executed again for !cond
class RepairNDEvaluator(ctx: LeonContext, prog: Program, fd : FunDef, cond: Expr) extends DefaultEvaluator(ctx, prog) {
-
+
override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
case FunctionInvocation(tfd, args) if tfd.fd == fd =>
diff --git a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
index 664b9e3b2..2846bc484 100644
--- a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
@@ -8,9 +8,8 @@ import leon.purescala.Common._
import leon.purescala.Expressions._
import leon.purescala.Types._
import leon.purescala.Definitions._
-import leon.purescala.Quantification._
import leon.LeonContext
-import leon.evaluators.RecursiveEvaluator
+import leon.evaluators._
/**
* This evaluator tracks all dependencies between function calls (.fullCallGraph)
@@ -20,9 +19,9 @@ import leon.evaluators.RecursiveEvaluator
class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluator(ctx, prog, 50000) {
type RC = CollectingRecContext
type GC = GlobalContext
-
+
def initRC(mappings: Map[Identifier, Expr]) = CollectingRecContext(mappings, None)
- def initGC(model: leon.solvers.Model) = new GlobalContext(model)
+ def initGC(model: leon.solvers.Model) = new GlobalContext(model, maxSteps)
type FI = (FunDef, Seq[Expr])
@@ -46,7 +45,7 @@ class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends Recursive
private def registerFailed (fi : FI) = fiStatus_ update (fi, false)
def fiStatus = fiStatus_.toMap.withDefaultValue(false)
- case class CollectingRecContext(mappings: Map[Identifier, Expr], lastFI : Option[FI]) extends RecContext {
+ case class CollectingRecContext(mappings: Map[Identifier, Expr], lastFI : Option[FI]) extends RecContext[CollectingRecContext] {
def newVars(news: Map[Identifier, Expr]) = copy(news, lastFI)
def withLastFI(fi : FI) = copy(lastFI = Some(fi))
}
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/main/scala/leon/solvers/EvaluatingSolver.scala b/src/main/scala/leon/solvers/EvaluatingSolver.scala
index 3463235c9..75dcb5631 100644
--- a/src/main/scala/leon/solvers/EvaluatingSolver.scala
+++ b/src/main/scala/leon/solvers/EvaluatingSolver.scala
@@ -10,7 +10,7 @@ trait EvaluatingSolver extends Solver {
val useCodeGen: Boolean
- lazy val evaluator: Evaluator =
+ lazy val evaluator: DeterministicEvaluator =
if (useCodeGen) {
new CodeGenEvaluator(context, program)
} else {
diff --git a/src/main/scala/leon/synthesis/ConversionPhase.scala b/src/main/scala/leon/synthesis/ConversionPhase.scala
index 366037b2a..d5f4e842f 100644
--- a/src/main/scala/leon/synthesis/ConversionPhase.scala
+++ b/src/main/scala/leon/synthesis/ConversionPhase.scala
@@ -64,7 +64,7 @@ object ConversionPhase extends UnitPhase[Program] {
*
* def foo(a: T) = {
* require(..a..)
- * ???
+ * _
* } ensuring { res =>
* post(res)
* }
@@ -75,8 +75,9 @@ object ConversionPhase extends UnitPhase[Program] {
* require(..a..)
* choose(x => post(x))
* }
+ * (in practice, there will be no pre-and postcondition)
*
- * 4) Functions that have only a choose as body gets their spec from the choose.
+ * 4) Functions that have only a choose as body gets their spec from the choose.
*
* def foo(a: T) = {
* choose(x => post(a, x))
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index f68fea066..da0f91810 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -74,7 +74,7 @@ object LinearEquations {
var i = 0
while(i < sols.size) {
// seriously ???
- K(i+j+1)(j) = evaluator.eval(sols(i)).asInstanceOf[EvaluationResults.Successful].value.asInstanceOf[InfiniteIntegerLiteral].value
+ K(i+j+1)(j) = evaluator.eval(sols(i)).asInstanceOf[EvaluationResults.Successful[Expr]].value.asInstanceOf[InfiniteIntegerLiteral].value
i += 1
}
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index eb9169244..5d06aa76a 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -20,7 +20,6 @@ import scala.collection.mutable.{HashMap=>MutableMap, ArrayBuffer}
import evaluators._
import datagen._
-import leon.utils._
import codegen.CodeGenParams
abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
@@ -380,7 +379,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
private val innerPhi = outerExprToInnerExpr(p.phi)
private var programCTree: Program = _
- private var tester: (Example, Set[Identifier]) => EvaluationResults.Result = _
+ private var tester: (Example, Set[Identifier]) => EvaluationResults.Result[Expr] = _
private def setCExpr(cTreeInfo: (Expr, Seq[FunDef])): Unit = {
val (cTree, newFds) = cTreeInfo
@@ -392,7 +391,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
//println(programCTree.asString)
//println(".. "*30)
-// val evaluator = new DualEvaluator(sctx.context, programCTree, CodeGenParams.default)
+ //val evaluator = new DualEvaluator(sctx.context, programCTree, CodeGenParams.default)
val evaluator = new DefaultEvaluator(sctx.context, programCTree)
tester =
diff --git a/src/main/scala/leon/utils/SeqUtils.scala b/src/main/scala/leon/utils/SeqUtils.scala
index 5a5e2dff3..002f2ebed 100644
--- a/src/main/scala/leon/utils/SeqUtils.scala
+++ b/src/main/scala/leon/utils/SeqUtils.scala
@@ -2,6 +2,7 @@
package leon.utils
+import scala.collection.SeqView
import scala.collection.mutable.ArrayBuffer
object SeqUtils {
@@ -42,3 +43,47 @@ object SeqUtils {
}
}
}
+
+class CartesianView[+A](views: Seq[SeqView[A, Seq[A]]]) extends SeqView[Seq[A], Seq[Seq[A]]] {
+ override protected def underlying: Seq[Seq[A]] = SeqUtils.cartesianProduct(views)
+
+ override def length: Int = views.map{ _.size }.product
+
+ override def apply(idx: Int): Seq[A] = {
+ if (idx < 0 || idx >= length) throw new IndexOutOfBoundsException
+ var c = idx
+ for (v <- views) yield {
+ val ic = c % v.size
+ c /= v.size
+ v(ic)
+ }
+ }
+
+ override def iterator: Iterator[Seq[A]] = new Iterator[Seq[A]] {
+ // It's unfortunate, but we have to use streams to memoize
+ private val streams = views.map { _.toStream }
+ private val current = streams.toArray
+
+ // We take a note if there exists an empty view to begin with
+ // (which means the whole iterator is empty)
+ private val empty = streams exists { _.isEmpty }
+
+ override def hasNext: Boolean = !empty && current.exists { _.nonEmpty }
+
+ override def next(): Seq[A] = {
+ if (!hasNext) throw new NoSuchElementException("next on empty iterator")
+ // Propagate curry
+ for (i <- (0 to streams.size).takeWhile(current(_).isEmpty)) {
+ current(i) = streams(i)
+ }
+
+ val ret = current map { _.head }
+
+ for (i <- (0 to streams.size)) {
+ current(i) = current(i).tail
+ }
+
+ ret
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
index 810d9d40e..82c419b04 100644
--- a/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/EvaluatorSuite.scala
@@ -5,7 +5,7 @@ package leon.integration.evaluators
import leon._
import leon.test._
import leon.test.helpers._
-import leon.evaluators._
+import leon.evaluators.{Evaluator => _, DeterministicEvaluator => Evaluator, _}
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Expressions._
@@ -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/integration/purescala/CallGraphSuite.scala b/src/test/scala/leon/integration/purescala/CallGraphSuite.scala
index 7c47baa4b..636cd4f40 100644
--- a/src/test/scala/leon/integration/purescala/CallGraphSuite.scala
+++ b/src/test/scala/leon/integration/purescala/CallGraphSuite.scala
@@ -4,9 +4,7 @@ package leon.integration.purescala
import leon.test._
-import leon._
-import leon.purescala.Definitions._
-import leon.utils._
+import leon.purescala.Definitions.Program
class CallGraphSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL {
diff --git a/src/test/scala/leon/integration/purescala/DataGenSuite.scala b/src/test/scala/leon/integration/purescala/DataGenSuite.scala
index 3a2eaf24f..b1acfd74c 100644
--- a/src/test/scala/leon/integration/purescala/DataGenSuite.scala
+++ b/src/test/scala/leon/integration/purescala/DataGenSuite.scala
@@ -3,12 +3,9 @@
package leon.integration.purescala
import leon.test._
-import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
-import leon.frontends.scalac.ExtractionPhase
import leon.purescala.Common._
import leon.purescala.Expressions._
-import leon.purescala.Definitions._
import leon.purescala.Types._
import leon.datagen._
diff --git a/src/test/scala/leon/integration/purescala/DefOpsSuite.scala b/src/test/scala/leon/integration/purescala/DefOpsSuite.scala
index 3df239fb1..c7aad05c6 100644
--- a/src/test/scala/leon/integration/purescala/DefOpsSuite.scala
+++ b/src/test/scala/leon/integration/purescala/DefOpsSuite.scala
@@ -4,10 +4,8 @@ package leon.integration.purescala
import leon.test._
-import leon._
import leon.purescala.Definitions._
import leon.purescala.DefOps._
-import leon.utils._
class DefOpsSuite extends LeonTestSuiteWithProgram {
diff --git a/src/test/scala/leon/integration/solvers/EnumerationSolverSuite.scala b/src/test/scala/leon/integration/solvers/EnumerationSolverSuite.scala
index 593245826..89031230b 100644
--- a/src/test/scala/leon/integration/solvers/EnumerationSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/EnumerationSolverSuite.scala
@@ -2,7 +2,6 @@
package leon.integration.solvers
-import leon.test._
import leon.solvers._
import leon.purescala.Common._
import leon.purescala.Definitions._
diff --git a/src/test/scala/leon/integration/solvers/FairZ3SolverTests.scala b/src/test/scala/leon/integration/solvers/FairZ3SolverTests.scala
index f89ecfd13..b08e7f916 100644
--- a/src/test/scala/leon/integration/solvers/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/integration/solvers/FairZ3SolverTests.scala
@@ -2,14 +2,12 @@
package leon.integration.solvers
-import leon.test._
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Expressions._
import leon.purescala.Types._
import leon.LeonContext
-import leon.solvers._
import leon.solvers.z3._
class FairZ3SolverTests extends LeonSolverSuite {
diff --git a/src/test/scala/leon/integration/solvers/ModelEnumerationSuite.scala b/src/test/scala/leon/integration/solvers/ModelEnumerationSuite.scala
index 38553d171..3b405720a 100644
--- a/src/test/scala/leon/integration/solvers/ModelEnumerationSuite.scala
+++ b/src/test/scala/leon/integration/solvers/ModelEnumerationSuite.scala
@@ -12,7 +12,7 @@ import leon.purescala.Common._
import leon.evaluators._
import leon.purescala.Expressions._
-class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
+class ModelEnumerationSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
val sources = List(
"""|import leon.lang._
|import leon.annotation._
diff --git a/src/test/scala/leon/integration/solvers/SolversSuite.scala b/src/test/scala/leon/integration/solvers/SolversSuite.scala
index 40fd07357..0e75e922c 100644
--- a/src/test/scala/leon/integration/solvers/SolversSuite.scala
+++ b/src/test/scala/leon/integration/solvers/SolversSuite.scala
@@ -84,7 +84,7 @@ class SolversSuite extends LeonTestSuiteWithProgram {
fail("Constraint "+cnstr.asString+" is unsat!?")
}
} finally {
- solver.free
+ solver.free()
}
}
diff --git a/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala b/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala
index cce647cc1..4ee340988 100644
--- a/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala
@@ -4,7 +4,6 @@ package leon.integration.solvers
import leon._
import leon.test._
-import leon.utils.Interruptible
import leon.solvers._
import leon.purescala.Common._
import leon.purescala.Definitions._
diff --git a/src/test/scala/leon/integration/solvers/UnrollingSolverSuite.scala b/src/test/scala/leon/integration/solvers/UnrollingSolverSuite.scala
index d9e4d8bb9..b3c0f82f2 100644
--- a/src/test/scala/leon/integration/solvers/UnrollingSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/UnrollingSolverSuite.scala
@@ -2,13 +2,11 @@
package leon.integration.solvers
-import leon.test._
import leon.LeonContext
import leon.purescala.Expressions._
import leon.purescala.Types._
import leon.purescala.Common._
import leon.purescala.Definitions._
-import leon.solvers._
import leon.solvers.z3._
import leon.solvers.combinators._
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
index 4c459cf6b..18bd8fc14 100644
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -3,10 +3,6 @@
package leon.test
import leon._
-import leon.purescala.Definitions.Program
-import leon.LeonContext
-import leon.utils._
-import leon.frontends.scalac.ExtractionPhase
import org.scalatest._
import org.scalatest.exceptions.TestFailedException
diff --git a/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
index 4d97487f6..4002a0af0 100644
--- a/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/unit/evaluators/EvaluatorSuite.scala
@@ -1,40 +1,36 @@
/* Copyright 2009-2015 EPFL, Lausanne */
-package leon.unit.allEvaluators
+package leon.unit.evaluators
import leon._
import leon.test._
import leon.evaluators._
-import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
-import leon.frontends.scalac.ExtractionPhase
-
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Expressions._
-import leon.purescala.DefOps._
import leon.purescala.Types._
import leon.purescala.Extractors._
import leon.purescala.Constructors._
-import leon.codegen._
class EvaluatorSuite extends LeonTestSuite with helpers.ExpressionsDSL {
implicit val pgm = Program.empty
- def normalEvaluators(implicit ctx: LeonContext, pgm: Program): List[Evaluator] = {
+ 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))
)
}
- def codegenEvaluators(implicit ctx: LeonContext, pgm: Program): List[Evaluator] = {
+ def codegenEvaluators(implicit ctx: LeonContext, pgm: Program): List[DeterministicEvaluator] = {
List(
new CodeGenEvaluator(ctx, pgm)
)
}
- def allEvaluators(implicit ctx: LeonContext, pgm: Program): List[Evaluator] = {
+ def allEvaluators(implicit ctx: LeonContext, pgm: Program): List[DeterministicEvaluator] = {
normalEvaluators ++ codegenEvaluators
}
@@ -275,7 +271,7 @@ class EvaluatorSuite extends LeonTestSuite with helpers.ExpressionsDSL {
def success: Expr = res
}
- case class Success(expr: Expr, env: Map[Identifier, Expr], evaluator: Evaluator, res: Expr) extends EvalDSL {
+ case class Success(expr: Expr, env: Map[Identifier, Expr], evaluator: DeterministicEvaluator, res: Expr) extends EvalDSL {
override def failed = {
fail(s"Evaluation of '$expr' with '$evaluator' (and env $env) should have failed")
}
@@ -285,7 +281,7 @@ class EvaluatorSuite extends LeonTestSuite with helpers.ExpressionsDSL {
}
}
- case class Failed(expr: Expr, env: Map[Identifier, Expr], evaluator: Evaluator, err: String) extends EvalDSL {
+ case class Failed(expr: Expr, env: Map[Identifier, Expr], evaluator: DeterministicEvaluator, err: String) extends EvalDSL {
override def success = {
fail(s"Evaluation of '$expr' with '$evaluator' (and env $env) should have succeeded but failed with $err")
}
@@ -295,7 +291,7 @@ class EvaluatorSuite extends LeonTestSuite with helpers.ExpressionsDSL {
def ===(res: Expr) = success
}
- def eval(e: Evaluator, toEval: Expr, env: Map[Identifier, Expr] = Map()): EvalDSL = {
+ def eval(e: DeterministicEvaluator, toEval: Expr, env: Map[Identifier, Expr] = Map()): EvalDSL = {
e.eval(toEval, env) match {
case EvaluationResults.Successful(res) => Success(toEval, env, e, res)
case EvaluationResults.RuntimeError(err) => Failed(toEval, env, e, err)
--
GitLab