diff --git a/src/main/scala/inox/ast/Constructors.scala b/src/main/scala/inox/ast/Constructors.scala
index d351540c25e9b02504623e718df4a4bb7391a507..fed2d4ce1723c20f05a622c2bfe236533ae26ad3 100644
--- a/src/main/scala/inox/ast/Constructors.scala
+++ b/src/main/scala/inox/ast/Constructors.scala
@@ -301,8 +301,8 @@ trait Constructors {
case (_, IntegerLiteral(bi)) if bi == 0 => lhs
case (IntLiteral(0), _) => rhs
case (_, IntLiteral(0)) => lhs
- case (FractionalLiteral(n, d), _) if n == 0 => rhs
- case (_, FractionalLiteral(n, d)) if n == 0 => lhs
+ case (FractionLiteral(n, d), _) if n == 0 => rhs
+ case (_, FractionLiteral(n, d)) if n == 0 => lhs
case _ => Plus(lhs, rhs)
}
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index d7fab61eec1a2467e7af1393ee93c41059f3e076..b9b3e20067f53acdedace7eea6b634a3647eb01d 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -418,8 +418,8 @@ trait Definitions { self: Trees =>
lazy val body = fd.body map translated
lazy val precondition = fd.precondition map translated
lazy val precOrTrue = translated(fd.precOrTrue)
- lazy val postcondition = fd.postcondition map translated
- lazy val postOrTrue = translated(fd.postOrTrue)
+ lazy val postcondition = fd.postcondition map (p => translated(p).asInstanceOf[Lambda])
+ lazy val postOrTrue = translated(fd.postOrTrue).asInstanceOf[Lambda]
def hasImplementation = body.isDefined
def hasBody = hasImplementation
diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
index 9fdc9329dc280649cfd820d6edfe2f2428c71b23..dd88569e7469f58e288ef066ed009faab0e6fd87 100644
--- a/src/main/scala/inox/ast/ExprOps.scala
+++ b/src/main/scala/inox/ast/ExprOps.scala
@@ -146,10 +146,10 @@ trait ExprOps extends GenTreeOps {
}
/** Returns the postcondition of an expression wrapped in Option */
- def postconditionOf(expr: Expr): Option[Expr] = expr match {
- case Let(i, e, b) => postconditionOf(b).map(Let(i, e, _).copiedFrom(expr))
- case Ensuring(_, post) => Some(post)
- case _ => None
+ def postconditionOf(expr: Expr): Option[Lambda] = expr match {
+ case Let(i, e, b) => postconditionOf(b).map(l => l.copy(body = Let(i, e, l.body)).copiedFrom(expr))
+ case Ensuring(_, post: Lambda) => Some(post)
+ case _ => None
}
/** Returns a tuple of precondition, the raw body and the postcondition of an expression */
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index d5d21dfbc6230907f0fbbc1d2adfec9cbb5f5c6c..472d68a17a299fc64c82d69120da0b550a611d84 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -3,6 +3,8 @@
package inox
package ast
+import scala.collection.BitSet
+
/** Expression definitions for Pure Scala.
*
* If you are looking for things such as function or class definitions,
@@ -273,12 +275,14 @@ trait Expressions { self: Trees =>
case class UnapplyPattern(binder: Option[ValDef], id: Identifier, tps: Seq[Type], subPatterns: Seq[Pattern]) extends Pattern {
// Hacky, but ok
def optionType(implicit s: Symbols) = s.getFunction(id, tps).returnType.asInstanceOf[ClassType]
- def someType(implicit s: Symbols): ClassType = {
- val optionChildren = optionType.tcd.asInstanceOf[TypedAbstractClassDef].ccDescendants.sortBy(_.fields.size)
- val someTcd = optionChildren(1)
- ClassType(someTcd.id, someTcd.tps)
+ def optionChildren(implicit s: Symbols): (ClassType, ClassType) = {
+ val children = optionType.tcd.asInstanceOf[TypedAbstractClassDef].ccDescendants.sortBy(_.fields.size)
+ val Seq(noneType, someType) = children.map(_.toType)
+ (noneType, someType)
}
+ def noneType(implicit s: Symbols): ClassType = optionChildren(s)._1
+ def someType(implicit s: Symbols): ClassType = optionChildren(s)._2
def someValue(implicit s: Symbols): ValDef = someType.tcd.asInstanceOf[TypedCaseClassDef].fields.head
/** Construct a pattern matching against unapply(scrut) (as an if-expression)
@@ -357,14 +361,28 @@ trait Expressions { self: Trees =>
def getType(implicit s: Symbols): Type = CharType
}
- /** $encodingof a 32-bit integer literal */
- case class IntLiteral(value: Int) extends Literal[Int] {
- def getType(implicit s: Symbols): Type = Int32Type
- }
-
/** $encodingof a n-bit bitvector literal */
- case class BVLiteral(value: BigInt, size: Int) extends Literal[BigInt] {
+ case class BVLiteral(value: BitSet, size: Int) extends Literal[BitSet] {
def getType(implicit s: Symbols): Type = BVType(size)
+ def toBigInt: BigInt = {
+ val res = value.foldLeft(BigInt(0))((res, i) => res + BigInt(2).pow(i))
+ if (value(size)) BigInt(2).pow(size) - res else res
+ }
+ }
+
+ object BVLiteral {
+ def apply(bi: BigInt, size: Int): BVLiteral = BVLiteral(
+ (1 to size).foldLeft(BitSet.empty) { case (res, i) =>
+ if ((bi & BigInt(2).pow(i)) > 0) res + i else res
+ }, size)
+ }
+
+ object IntLiteral {
+ def apply(i: Int): BVLiteral = BVLiteral(BigInt(i), 32)
+ def unapply(e: Expr): Option[Int] = e match {
+ case b @ BVLiteral(_, 32) => Some(b.toBigInt.toInt)
+ case _ => None
+ }
}
/** $encodingof an infinite precision integer literal */
@@ -373,7 +391,7 @@ trait Expressions { self: Trees =>
}
/** $encodingof a fraction literal */
- case class FractionalLiteral(numerator: BigInt, denominator: BigInt) extends Literal[(BigInt, BigInt)] {
+ case class FractionLiteral(numerator: BigInt, denominator: BigInt) extends Literal[(BigInt, BigInt)] {
val value = (numerator, denominator)
def getType(implicit s: Symbols): Type = RealType
}
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index 39bb9eba37b37a37a3fd9560f26cf40eaf8359bf..979cffc572ec800ba60e138a945bc8ae2c593851 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -142,8 +142,9 @@ trait Printers { self: Trees =>
case StringBigLength(expr) => p"$expr.bigLength"
case IntLiteral(v) => p"$v"
+ case BVLiteral(bits, size) => p"x${(size to 1 by -1).map(i => if (bits(i)) "1" else "0")}"
case IntegerLiteral(v) => p"$v"
- case FractionalLiteral(n, d) =>
+ case FractionLiteral(n, d) =>
if (d == 1) p"$n"
else p"$n/$d"
case CharLiteral(v) => p"$v"
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 223d2627e4cd3fa7b7a88a5dae22b1bac6847a5b..19202719bfc7ffb22935d03379a5b7b27a1c2298 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -460,7 +460,7 @@ trait SymbolOps extends TreeOps { self: TypeOps =>
def simplestValue(tpe: Type): Expr = tpe match {
case StringType => StringLiteral("")
case Int32Type => IntLiteral(0)
- case RealType => FractionalLiteral(0, 1)
+ case RealType => FractionLiteral(0, 1)
case IntegerType => IntegerLiteral(0)
case CharType => CharLiteral('a')
case BooleanType => BooleanLiteral(false)
@@ -752,36 +752,36 @@ trait SymbolOps extends TreeOps { self: TypeOps =>
}
/**
- * Some helper methods for FractionalLiterals
+ * Some helper methods for FractionLiterals
*/
- def normalizeFraction(fl: FractionalLiteral) = {
- val FractionalLiteral(num, denom) = fl
+ def normalizeFraction(fl: FractionLiteral) = {
+ val FractionLiteral(num, denom) = fl
val modNum = if (num < 0) -num else num
val modDenom = if (denom < 0) -denom else denom
val divisor = modNum.gcd(modDenom)
val simpNum = num / divisor
val simpDenom = denom / divisor
if (simpDenom < 0)
- FractionalLiteral(-simpNum, -simpDenom)
+ FractionLiteral(-simpNum, -simpDenom)
else
- FractionalLiteral(simpNum, simpDenom)
+ FractionLiteral(simpNum, simpDenom)
}
- val realzero = FractionalLiteral(0, 1)
- def floor(fl: FractionalLiteral): FractionalLiteral = {
- val FractionalLiteral(n, d) = normalizeFraction(fl)
+ val realzero = FractionLiteral(0, 1)
+ def floor(fl: FractionLiteral): FractionLiteral = {
+ val FractionLiteral(n, d) = normalizeFraction(fl)
if (d == 0) throw new IllegalStateException("denominator zero")
if (n == 0) realzero
else if (n > 0) {
//perform integer division
- FractionalLiteral(n / d, 1)
+ FractionLiteral(n / d, 1)
} else {
//here the number is negative
if (n % d == 0)
- FractionalLiteral(n / d, 1)
+ FractionLiteral(n / d, 1)
else {
//perform integer division and subtract 1
- FractionalLiteral(n / d - 1, 1)
+ FractionLiteral(n / d - 1, 1)
}
}
}
@@ -991,7 +991,7 @@ trait SymbolOps extends TreeOps { self: TypeOps =>
case (IntLiteral(_), Int32Type) => true
case (IntegerLiteral(_), IntegerType) => true
case (CharLiteral(_), CharType) => true
- case (FractionalLiteral(_, _), RealType) => true
+ case (FractionLiteral(_, _), RealType) => true
case (BooleanLiteral(_), BooleanType) => true
case (UnitLiteral(), UnitType) => true
case (GenericValue(t, _), tp) => t == tp
diff --git a/src/main/scala/inox/evaluators/ContextualEvaluator.scala b/src/main/scala/inox/evaluators/ContextualEvaluator.scala
index 973483cae3813ef596c3a77689e112f3d962bfb9..fba8ac52dfc68456d48d78747636fe849ba2d15c 100644
--- a/src/main/scala/inox/evaluators/ContextualEvaluator.scala
+++ b/src/main/scala/inox/evaluators/ContextualEvaluator.scala
@@ -1,50 +1,51 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
+package inox
package evaluators
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Expressions._
-import purescala.Types._
-import solvers.Model
-import codegen.runtime.{LeonCodeGenRuntimeException, LeonCodeGenEvaluationException}
+trait ContextualEvaluator extends Evaluator {
+ val maxSteps: Int
+ import program._
+ import program.trees._
-abstract class ContextualEvaluator(ctx: LeonContext, prog: Program, val maxSteps: Int) extends Evaluator(ctx, prog) with CEvalHelpers {
+ trait RecContext[RC <: RecContext[RC]] {
+ def mappings: Map[ValDef, Expr]
+ def newVars(news: Map[ValDef, Expr]): RC
+ def withNewVar(vd: ValDef, expr: Expr): RC = newVars(mappings + (vd -> expr))
+ def withNewVars(news: Map[ValDef, Expr]): RC = newVars(mappings ++ news)
+ }
+
+ case class DefaultRecContext(mappings: Map[ValDef, Expr]) extends RecContext[DefaultRecContext] {
+ def newVars(news: Map[ValDef, Expr]) = copy(mappings = news)
+ }
- protected implicit val _ = ctx
+ class GlobalContext(val maxSteps: Int) {
+ var stepsLeft = maxSteps
+ }
type RC <: RecContext[RC]
type GC <: GlobalContext
- def initRC(mappings: Map[Identifier, Expr]): RC
- def initGC(model: solvers.Model, check: Boolean): GC
+ def initRC(mappings: Map[ValDef, Expr]): RC
+ def initGC: GC
- case class EvalError(msg : String) extends Exception {
+ case class EvalError(msg: String) extends Exception {
override def getMessage = msg + Option(super.getMessage).map("\n" + _).getOrElse("")
}
- case class RuntimeError(msg : String) extends Exception
+ case class RuntimeError(msg: String) extends Exception
case class QuantificationError(msg: String) extends Exception
- // Used by leon-web, please do not delete
- var lastGC: Option[GC] = None
-
- def eval(ex: Expr, model: Model) = {
+ def eval(ex: Expr, model: Map[ValDef, Expr]) = {
try {
- lastGC = Some(initGC(model, check = true))
ctx.timers.evaluators.recursive.runtime.start()
- EvaluationResults.Successful(e(ex)(initRC(model.toMap), lastGC.get))
+ EvaluationResults.Successful(e(ex)(initRC(model), initGC))
} catch {
case EvalError(msg) =>
EvaluationResults.EvaluatorError(msg)
- case ee: LeonCodeGenEvaluationException =>
- EvaluationResults.EvaluatorError(ee.getMessage)
case so: StackOverflowError =>
EvaluationResults.RuntimeError("Stack overflow")
case e @ RuntimeError(msg) =>
EvaluationResults.RuntimeError(msg)
- case re: LeonCodeGenRuntimeException =>
- EvaluationResults.RuntimeError(re.getMessage)
case jre: java.lang.RuntimeException =>
EvaluationResults.RuntimeError(jre.getMessage)
} finally {
@@ -54,68 +55,17 @@ abstract class ContextualEvaluator(ctx: LeonContext, prog: Program, val maxSteps
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} of type ${tree.getType}."
-
+ def typeErrorMsg(tree: Expr, expected: Type): String = s"Type error : expected ${expected.asString}, found ${tree.asString} of type ${tree.getType}."
}
-private[evaluators] trait CEvalHelpers {
- this: ContextualEvaluator =>
-
- /* This is an effort to generalize forall to non-det. solvers
- def forallInstantiations(gctx:GC, fargs: Seq[ValDef], conj: Expr) = {
-
- val henkinModel: PartialModel = gctx.model match {
- case hm: PartialModel => 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)
- }
- }*/
-
-
+trait HasDefaultRecContext extends ContextualEvaluator {
+ import program.trees._
+ type RC = DefaultRecContext
+ def initRC(mappings: Map[ValDef, Expr]) = DefaultRecContext(mappings)
+}
+trait HasDefaultGlobalContext extends ContextualEvaluator {
+ type GC = GlobalContext
+ def initGC = new GlobalContext(maxSteps)
}
+
diff --git a/src/main/scala/inox/evaluators/EvaluatorContexts.scala b/src/main/scala/inox/evaluators/EvaluatorContexts.scala
deleted file mode 100644
index 859e960d5d7aadbc63de656fd3c340fbc60b30f1..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/evaluators/EvaluatorContexts.scala
+++ /dev/null
@@ -1,44 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package evaluators
-
-import purescala.Common.Identifier
-import leon.purescala.Expressions.{Lambda, Expr}
-import solvers.Model
-
-import scala.collection.mutable.{Map => MutableMap}
-
-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, val check: Boolean) {
- var stepsLeft = maxSteps
-
- val lambdas: MutableMap[Lambda, Lambda] = MutableMap.empty
-}
-
-trait HasDefaultRecContext extends ContextualEvaluator {
- type RC = DefaultRecContext
- def initRC(mappings: Map[Identifier, Expr]) = DefaultRecContext(mappings)
-}
-
-trait HasDefaultGlobalContext extends ContextualEvaluator {
- def initGC(model: solvers.Model, check: Boolean) = new GlobalContext(model, this.maxSteps, check)
- type GC = GlobalContext
-}
\ No newline at end of file
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
index 6838efe26ee3d36b88b8a28cef7d38c3819ce43a..d1eba7f1ed700c4d8c38fee825f566c158f5ee37 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -1,109 +1,31 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
+package inox
package evaluators
-import purescala.Quantification._
-import purescala.Constructors._
-import purescala.ExprOps._
-import purescala.Expressions.Pattern
-import purescala.Extractors._
-import purescala.TypeOps.isSubtypeOf
-import purescala.Types._
-import purescala.Common._
-import purescala.Expressions._
-import purescala.Definitions._
-import solvers.TimeoutableSolverFactory
-import solvers.{PartialModel, SolverFactory}
-import purescala.DefOps
-import solvers.{PartialModel, Model, SolverFactory, SolverContext}
-import solvers.unrolling.UnrollingProcedure
-import scala.collection.mutable.{Map => MutableMap}
-import scala.concurrent.duration._
-import org.apache.commons.lang3.StringEscapeUtils
-import leon.purescala.TypeOps
-
-abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: EvaluationBank, maxSteps: Int)
- extends ContextualEvaluator(ctx, prog, maxSteps)
- with DeterministicEvaluator {
-
- def this(ctx: LeonContext, prog: Program, maxSteps: Int) =
- this(ctx, prog, new EvaluationBank, maxSteps)
+import scala.collection.BitSet
+
+trait RecursiveEvaluator
+ extends ContextualEvaluator
+ with DeterministicEvaluator
+ with SolvingEvaluator {
+
+ import program._
+ import program.trees._
+ import program.symbols._
+ import program.trees.exprOps._
val name = "evaluator"
- val description = "Recursive interpreter for PureScala expressions"
-
- lazy val scalaEv = new ScalacEvaluator(this, ctx, prog)
-
- protected val clpCache = MutableMap[(Choose, Seq[Expr]), Expr]()
- protected var frlCache = Map[(Forall, Seq[Expr]), Expr]()
-
- private var evaluationFailsOnChoose = false
- /** Sets the flag if when encountering a Choose, it should fail instead of solving it. */
- def setEvaluationFailOnChoose(b: Boolean) = { this.evaluationFailsOnChoose = b; this }
-
- protected[evaluators] object SpecializedFunctionInvocation {
- def unapply(expr: Expr)(implicit rctx: RC, gctx: GC): Option[Expr] = expr match {
- case FunctionInvocation(TypedFunDef(fd, Nil), Seq(input)) if fd == program.library.escape.get =>
- e(input) match {
- case StringLiteral(s) =>
- Some(StringLiteral(StringEscapeUtils.escapeJava(s)))
- case _ => throw EvalError(typeErrorMsg(input, StringType))
- }
-
- case FunctionInvocation(TypedFunDef(fd, Seq(ta, tb)), Seq(mp, inkv, betweenkv, fk, fv)) if fd == program.library.mapMkString.get =>
- println("invkv")
- val inkv_str = e(inkv) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(inkv, StringType)) }
- println(s"invkv_str = $inkv_str")
- val betweenkv_str = e(betweenkv) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(betweenkv, StringType)) }
- println(s"betweenkv_str = $betweenkv_str")
- val mp_map = e(mp) match { case FiniteMap(theMap, keyType, valueType) => theMap case _ => throw EvalError(typeErrorMsg(mp, MapType(ta, tb))) }
- println(s"mp_map = $mp_map")
-
- val res = mp_map.map{ case (k, v) =>
- (e(application(fk, Seq(k))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(k, StringType)) }) +
- inkv_str +
- (v match {
- case CaseClass(some, Seq(v)) if some == program.library.Some.get.typed(Seq(tb)) =>
- (e(application(fv, Seq(v))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(k, StringType)) })
- case CaseClass(t, _) if TypeOps.isSubtypeOf(t, tb) =>
- (e(application(fv, Seq(v))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(k, StringType)) })
- case _ => throw EvalError(typeErrorMsg(v, program.library.Some.get.typed(Seq(tb))))
- })}.toList.sorted.mkString(betweenkv_str)
-
- Some(StringLiteral(res))
-
- case FunctionInvocation(TypedFunDef(fd, Seq(ta)), Seq(mp, inf, f)) if fd == program.library.setMkString.get =>
- val inf_str = e(inf) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(inf, StringType)) }
- val mp_set = e(mp) match { case FiniteSet(elems, valueType) => elems case _ => throw EvalError(typeErrorMsg(mp, SetType(ta))) }
-
- val res = mp_set.map{ case v =>
- e(application(f, Seq(v))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(v, StringType)) } }.toList.sorted.mkString(inf_str)
-
- Some(StringLiteral(res))
-
- case FunctionInvocation(TypedFunDef(fd, Seq(ta)), Seq(mp, inf, f)) if fd == program.library.bagMkString.get =>
- val inf_str = e(inf) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(inf, StringType)) }
- val mp_bag = e(mp) match { case FiniteBag(elems, valueType) => elems case _ => throw EvalError(typeErrorMsg(mp, SetType(ta))) }
-
- val res = mp_bag.flatMap{ case (k, v) =>
- val fk = (e(application(f, Seq(k))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(k, StringType)) })
- val times = (e(v)) match { case InfiniteIntegerLiteral(i) => i case _ => throw EvalError(typeErrorMsg(k, IntegerType)) }
- List.range(1, times.toString.toInt).map(_ => fk)
- }.toList.sorted.mkString(inf_str)
-
- Some(StringLiteral(res))
- case _ => None
- }
- }
-
+ val description = "Recursive interpreter for Inox expressions"
+
+ private def shift(b: BitSet, size: Int, i: Int): BitSet =
+ b.map(_ + i).filter(bit => bit >= 1 && bit <= size)
+
protected[evaluators] def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
- case Variable(id) =>
- rctx.mappings.get(id) match {
- case Some(v) =>
- v
- case None =>
- throw EvalError("No value for identifier " + id.asString + " in mapping " + rctx.mappings)
+ case v: Variable =>
+ rctx.mappings.get(v.toVal) match {
+ case Some(v) => v
+ case None => throw EvalError("No value for variable " + v.asString + " in mapping " + rctx.mappings)
}
case Application(caller, args) =>
@@ -112,10 +34,6 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
val newArgs = args.map(e)
val mapping = l.paramSubst(newArgs)
e(body)(rctx.withNewVars(mapping), gctx)
- case FiniteLambda(mapping, dflt, _) =>
- mapping.find { case (pargs, res) =>
- (args zip pargs).forall(p => e(Equals(p._1, p._2)) == BooleanLiteral(true))
- }.map(_._2).getOrElse(dflt)
case f =>
throw EvalError("Cannot apply non-lambda function " + f.asString)
}
@@ -150,32 +68,19 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
case _ => throw EvalError(typeErrorMsg(first, BooleanType))
}
- case FunctionInvocation(TypedFunDef(fd, Seq(tp)), Seq(set)) if fd == program.library.setToList.get =>
- val els = e(set) match {
- case FiniteSet(els, _) => els
- case _ => throw EvalError(typeErrorMsg(set, SetType(tp)))
- }
- 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 SpecializedFunctionInvocation(result) => result
-
- case FunctionInvocation(tfd, args) =>
+ case FunctionInvocation(id, tps, args) =>
if (gctx.stepsLeft < 0) {
throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
}
gctx.stepsLeft -= 1
+ val tfd = getFunction(id, tps)
val evArgs = args map e
- //println(s"calling ${tfd.id} with $evArgs")
-
// build a mapping for the function...
val frame = rctx.withNewVars(tfd.paramSubst(evArgs))
- if(tfd.hasPrecondition) {
+ if (tfd.hasPrecondition) {
e(tfd.precondition.get)(frame, gctx) match {
case BooleanLiteral(true) =>
case BooleanLiteral(false) =>
@@ -185,18 +90,18 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
}
}
- val callResult = if (tfd.fd.annotations("extern") && ctx.classDir.isDefined) {
- scalaEv.call(tfd, evArgs)
- } else {
- if(!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) {
- throw EvalError("Evaluation of function with unknown implementation." + expr)
- }
+ // @nv TODO: choose evaluation
- val body = tfd.body.getOrElse(rctx.mappings(tfd.id))
- e(body)(frame, gctx)
+ /* @nv TODO: should we do this differently?? lambdas??
+ if (!tfd.hasBody && !rctx.mappings.isDefinedAt(tfd.id)) {
+ throw EvalError("Evaluation of function with unknown implementation." + expr)
}
+ */
- //println(s"Gave $callResult")
+ val callResult: Expr = tfd.body match {
+ case Some(body) => e(body)(frame, gctx)
+ case None => onSpecInvocation(tfd.postOrTrue)
+ }
tfd.postcondition match {
case Some(post) =>
@@ -210,25 +115,31 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
callResult
- case And(args) if args.isEmpty => BooleanLiteral(true)
+ case And(Seq(e1, e2)) =>
+ (e(e1), e(e2)) match {
+ case (BooleanLiteral(b1), BooleanLiteral(b2)) => BooleanLiteral(b1 && b2)
+ case (BVLiteral(i1, s1), BVLiteral(i2, s2)) if s1 == s2 => BVLiteral(i1 & i2, s1)
+ case (le, re) => throw EvalError("Unexpected operation: (" + le.asString + ") && (" + re.asString + ")")
+ }
+
case And(args) =>
- e(args.head) match {
- case BooleanLiteral(false) => BooleanLiteral(false)
- case BooleanLiteral(true) => e(andJoin(args.tail))
- case other => throw EvalError(typeErrorMsg(other, BooleanType))
+ e(And(args.head, e(And(args.tail))))
+
+ case Or(Seq(e1, e2)) =>
+ (e(e1), e(e2)) match {
+ case (BooleanLiteral(b1), BooleanLiteral(b2)) => BooleanLiteral(b1 || b2)
+ case (BVLiteral(i1, s1), BVLiteral(i2, s2)) if s1 == s2 => BVLiteral(i1 | i2, s1)
+ case (le, re) => throw EvalError("Unexpected operation: (" + le.asString + ") || (" + re.asString + ")")
}
- case Or(args) if args.isEmpty => BooleanLiteral(false)
case Or(args) =>
- e(args.head) match {
- case BooleanLiteral(true) => BooleanLiteral(true)
- case BooleanLiteral(false) => e(orJoin(args.tail))
- case other => throw EvalError(typeErrorMsg(other, BooleanType))
- }
+ e(Or(args.head, e(Or(args.tail))))
case Not(arg) =>
e(arg) match {
case BooleanLiteral(v) => BooleanLiteral(!v)
+ case BVLiteral(bs, s) =>
+ BVLiteral(BitSet.empty ++ (1 to s).flatMap(i => if (bs(i)) None else Some(i)), s)
case other => throw EvalError(typeErrorMsg(other, BooleanType))
}
@@ -244,24 +155,32 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
val rv = e(re)
(lv,rv) match {
- case (FiniteSet(el1, _),FiniteSet(el2, _)) => BooleanLiteral(el1 == el2)
- case (FiniteBag(el1, _),FiniteBag(el2, _)) => BooleanLiteral(el1 == el2)
- case (FiniteMap(el1, _, _),FiniteMap(el2, _, _)) => BooleanLiteral(el1.toSet == el2.toSet)
- case (FiniteLambda(m1, d1, _), FiniteLambda(m2, d2, _)) => BooleanLiteral(m1.toSet == m2.toSet && d1 == d2)
+ case (FiniteSet(el1, _),FiniteSet(el2, _)) =>
+ BooleanLiteral(el1.toSet == el2.toSet)
+ case (FiniteBag(el1, _),FiniteBag(el2, _)) =>
+ BooleanLiteral(el1.toMap == el2.toMap)
+ case (FiniteMap(el1, dflt1, _),FiniteMap(el2, dflt2, _)) =>
+ BooleanLiteral(el1.toMap == el2.toMap && dflt1 == dflt2)
+ case (l1: Lambda, l2: Lambda) =>
+ val (nl1, subst1) = normalizeStructure(l1)
+ val (nl2, subst2) = normalizeStructure(l2)
+ BooleanLiteral(nl1 == nl2 && subst1.keys.toSet == subst2.keys.toSet && {
+ subst1.forall { case (k, v) => e(Equals(v, subst2(k))) match {
+ case BooleanLiteral(res) => res
+ case e => throw EvalError(typeErrorMsg(e, BooleanType))
+ }}
+ })
case _ => BooleanLiteral(lv == rv)
}
case CaseClass(cct, args) =>
val cc = CaseClass(cct, args.map(e))
- val check = bank.invariantCheck(cc)
- if (check.isFailure) {
- throw RuntimeError("ADT invariant violation for " + cct.classDef.id.asString + " reached in evaluation.: " + cct.invariant.get.asString)
- } else if (check.isRequired) {
- e(FunctionInvocation(cct.invariant.get, Seq(cc))) match {
- case BooleanLiteral(success) =>
- bank.invariantResult(cc, success)
- if (!success)
- throw RuntimeError("ADT invariant violation for " + cct.classDef.id.asString + " reached in evaluation.: " + cct.invariant.get.asString)
+ cct.tcd.invariant.foreach { tfd =>
+ val v = Variable(FreshIdentifier("x", true), cct)
+ e(tfd.applied(Seq(v)))(rctx.withNewVar(v.toVal, cc), gctx) match {
+ case BooleanLiteral(true) =>
+ case BooleanLiteral(false) =>
+ throw RuntimeError("ADT invariant violation for " + cc.asString)
case other =>
throw RuntimeError(typeErrorMsg(other, BooleanType))
}
@@ -281,226 +200,197 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
BooleanLiteral(isSubtypeOf(le.getType, ct))
case CaseClassSelector(ct1, expr, sel) =>
- val le = e(expr)
- le match {
- case CaseClass(ct2, args) if ct1 == ct2 => args(ct1.classDef.selectorID2Index(sel))
- case _ => throw EvalError(typeErrorMsg(le, ct1))
+ e(expr) match {
+ case CaseClass(ct2, args) if ct1 == ct2 => args(ct1.tcd.cd match {
+ case ccd: CaseClassDef => ccd.selectorID2Index(sel)
+ case _ => throw RuntimeError("Unexpected case class type")
+ })
+ case le => throw EvalError(typeErrorMsg(le, ct1))
}
case Plus(l,r) =>
(e(l), e(r)) match {
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 + i2)
- case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ case (BVLiteral(i1, s1), BVLiteral(i2, s2)) if s1 == s2 => BVLiteral(
+ (1 to s1).foldLeft((BitSet.empty, false)) { case ((res, carry), i) =>
+ val (b1, b2) = (i1(i), i2(i))
+ val nextCarry = (b1 && b2) || (b1 && carry) || (b2 && carry)
+ val ri = b1 ^ b2 ^ carry
+ (if (ri) res + i else res, nextCarry)
+ }._1, s1)
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) => IntegerLiteral(i1 + i2)
+ case (FractionLiteral(ln, ld), FractionLiteral(rn, rd)) =>
+ normalizeFraction(FractionLiteral(ln * rd + rn * ld, ld * rd))
+ case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") + (" + re.asString + ")")
}
case Minus(l,r) =>
(e(l), e(r)) match {
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 - i2)
- case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
- }
-
- case RealPlus(l, r) =>
- (e(l), e(r)) match {
- case (FractionalLiteral(ln, ld), FractionalLiteral(rn, rd)) =>
- normalizeFraction(FractionalLiteral(ln * rd + rn * ld, ld * rd))
- case (le, re) => throw EvalError(typeErrorMsg(le, RealType))
+ case (b1: BVLiteral, b2: BVLiteral) => e(Plus(b1, UMinus(b2)))
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) => IntegerLiteral(i1 - i2)
+ case (FractionLiteral(ln, ld), FractionLiteral(rn, rd)) =>
+ normalizeFraction(FractionLiteral(ln * rd - rn * ld, ld * rd))
+ case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") - (" + re.asString + ")")
}
- case RealMinus(l,r) =>
- e(RealPlus(l, RealUMinus(r)))
-
case StringConcat(l, r) =>
(e(l), e(r)) match {
case (StringLiteral(i1), StringLiteral(i2)) => StringLiteral(i1 + i2)
case (le,re) => throw EvalError(typeErrorMsg(le, StringType))
}
+
case StringLength(a) => e(a) match {
case StringLiteral(a) => IntLiteral(a.length)
case res => throw EvalError(typeErrorMsg(res, Int32Type))
}
+
case StringBigLength(a) => e(a) match {
- case StringLiteral(a) => InfiniteIntegerLiteral(a.length)
+ case StringLiteral(a) => IntegerLiteral(a.length)
case res => throw EvalError(typeErrorMsg(res, IntegerType))
}
+
case SubString(a, start, end) => (e(a), e(start), e(end)) match {
case (StringLiteral(a), IntLiteral(b), IntLiteral(c)) =>
StringLiteral(a.substring(b, c))
case res => throw EvalError(typeErrorMsg(res._1, StringType))
}
+
case BigSubString(a, start, end) => (e(a), e(start), e(end)) match {
- case (StringLiteral(a), InfiniteIntegerLiteral(b), InfiniteIntegerLiteral(c)) =>
+ case (StringLiteral(a), IntegerLiteral(b), IntegerLiteral(c)) =>
StringLiteral(a.substring(b.toInt, c.toInt))
case res => throw EvalError(typeErrorMsg(res._1, StringType))
}
+
case Int32ToString(a) => e(a) match {
case IntLiteral(i) => StringLiteral(i.toString)
case res => throw EvalError(typeErrorMsg(res, Int32Type))
}
+
case CharToString(a) =>
e(a) match {
case CharLiteral(i) => StringLiteral(i.toString)
case res => throw EvalError(typeErrorMsg(res, CharType))
}
+
case IntegerToString(a) => e(a) match {
- case InfiniteIntegerLiteral(i) => StringLiteral(i.toString)
+ case IntegerLiteral(i) => StringLiteral(i.toString)
case res => throw EvalError(typeErrorMsg(res, IntegerType))
}
+
case BooleanToString(a) => e(a) match {
case BooleanLiteral(i) => StringLiteral(i.toString)
case res => throw EvalError(typeErrorMsg(res, BooleanType))
}
+
case RealToString(a) => e(a) match {
- case FractionalLiteral(n, d) => StringLiteral(n.toString + "/" + d.toString)
+ case FractionLiteral(n, d) => StringLiteral(n.toString + "/" + d.toString)
case res => throw EvalError(typeErrorMsg(res, RealType))
}
- case BVPlus(l,r) =>
- (e(l), e(r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 + i2)
- case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
- }
-
- case BVMinus(l,r) =>
- (e(l), e(r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 - i2)
- case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
- }
-
case UMinus(ex) =>
e(ex) match {
- case InfiniteIntegerLiteral(i) => InfiniteIntegerLiteral(-i)
- case re => throw EvalError(typeErrorMsg(re, IntegerType))
- }
-
- case BVUMinus(ex) =>
- e(ex) match {
- case IntLiteral(i) => IntLiteral(-i)
- case re => throw EvalError(typeErrorMsg(re, Int32Type))
- }
-
- case RealUMinus(ex) =>
- e(ex) match {
- case FractionalLiteral(n, d) => FractionalLiteral(-n, d)
- case re => throw EvalError(typeErrorMsg(re, RealType))
- }
-
-
- case BVNot(ex) =>
- e(ex) match {
- case IntLiteral(i) => IntLiteral(~i)
- case re => throw EvalError(typeErrorMsg(re, Int32Type))
+ case BVLiteral(b, s) =>
+ BVLiteral((1 to s).foldLeft((BitSet.empty, false)) { case ((res, seen1), i) =>
+ if (b(i) && seen1) (res + i, true)
+ else if (!seen1) (res, seen1)
+ else (if (!b(i)) res + i else res, seen1)
+ }._1, s)
+ case IntegerLiteral(i) => IntegerLiteral(-i)
+ case FractionLiteral(n, d) => FractionLiteral(-n, d)
+ case re => throw EvalError("Unexpected operation: -(" + re.asString + ")")
}
case Times(l,r) =>
(e(l), e(r)) match {
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 * i2)
- case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ case (BVLiteral(i1, s1), BVLiteral(i2, s2)) if s1 == s2 =>
+ BVLiteral(i1.foldLeft(BitSet.empty) { case (res, i) =>
+ res ++ shift(i2, s2, i)
+ }, s1)
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) => IntegerLiteral(i1 * i2)
+ case (FractionLiteral(ln, ld), FractionLiteral(rn, rd)) =>
+ normalizeFraction(FractionLiteral((ln * rn), (ld * rd)))
+ case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") * (" + re.asString + ")")
}
case Division(l,r) =>
(e(l), e(r)) match {
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) =>
- if(i2 != BigInt(0)) InfiniteIntegerLiteral(i1 / i2) else throw RuntimeError("Division by 0.")
- case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ case (b1 @ BVLiteral(_, s1), b2 @ BVLiteral(_, s2)) if s1 == s2 =>
+ val bi2 = b2.toBigInt
+ if (bi2 != 0) BVLiteral(b1.toBigInt / bi2, s1) else throw RuntimeError("Division by 0.")
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) =>
+ if(i2 != BigInt(0)) IntegerLiteral(i1 / i2) else throw RuntimeError("Division by 0.")
+ case (FractionLiteral(ln, ld), FractionLiteral(rn, rd)) =>
+ if (rn != 0)
+ normalizeFraction(FractionLiteral(ln * rd, ld * rn))
+ else throw RuntimeError("Division by 0.")
+ case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") / (" + re.asString + ")")
}
case Remainder(l,r) =>
(e(l), e(r)) match {
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) =>
- if(i2 != BigInt(0)) InfiniteIntegerLiteral(i1 % i2) else throw RuntimeError("Remainder of division by 0.")
- case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ case (b1 @ BVLiteral(_, s1), b2 @ BVLiteral(_, s2)) if s1 == s2 =>
+ val bi2 = b2.toBigInt
+ if (bi2 != 0) BVLiteral(b1.toBigInt % bi2, s1) else throw RuntimeError("Division by 0.")
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) =>
+ if(i2 != BigInt(0)) IntegerLiteral(i1 % i2) else throw RuntimeError("Remainder of division by 0.")
+ case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") rem (" + re.asString + ")")
}
+
case Modulo(l,r) =>
(e(l), e(r)) match {
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) =>
+ case (b1 @ BVLiteral(_, s1), b2 @ BVLiteral(_, s2)) if s1 == s2 =>
+ val bi2 = b2.toBigInt
+ if (bi2 < 0)
+ BVLiteral(b1.toBigInt mod (-bi2), s1)
+ else if (bi2 != 0)
+ BVLiteral(b1.toBigInt mod bi2, s1)
+ else
+ throw RuntimeError("Modulo of division by 0.")
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) =>
if(i2 < 0)
- InfiniteIntegerLiteral(i1 mod (-i2))
+ IntegerLiteral(i1 mod (-i2))
else if(i2 != BigInt(0))
- InfiniteIntegerLiteral(i1 mod i2)
+ IntegerLiteral(i1 mod i2)
else
throw RuntimeError("Modulo of division by 0.")
- case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
- }
-
- case BVTimes(l,r) =>
- (e(l), e(r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 * i2)
- case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
- }
-
- case BVDivision(l,r) =>
- (e(l), e(r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) =>
- if(i2 != 0) IntLiteral(i1 / i2) else throw RuntimeError("Division by 0.")
- case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
- }
-
- case BVRemainder(l,r) =>
- (e(l), e(r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) =>
- if(i2 != 0) IntLiteral(i1 % i2) else throw RuntimeError("Remainder of division by 0.")
- case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
- }
-
- case RealTimes(l,r) =>
- (e(l), e(r)) match {
- case (FractionalLiteral(ln, ld), FractionalLiteral(rn, rd)) =>
- normalizeFraction(FractionalLiteral((ln * rn), (ld * rd)))
- case (le,re) => throw EvalError(typeErrorMsg(le, RealType))
- }
-
- case RealDivision(l,r) =>
- (e(l), e(r)) match {
- case (FractionalLiteral(ln, ld), FractionalLiteral(rn, rd)) =>
- if (rn != 0)
- normalizeFraction(FractionalLiteral(ln * rd, ld * rn))
- else throw RuntimeError("Division by 0.")
- case (le,re) => throw EvalError(typeErrorMsg(le, RealType))
- }
-
-
- case BVAnd(l,r) =>
- (e(l), e(r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 & i2)
- case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
- }
-
- case BVOr(l,r) =>
- (e(l), e(r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 | i2)
- case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") % (" + re.asString + ")")
}
case BVXOr(l,r) =>
(e(l), e(r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 ^ i2)
- case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ case (BVLiteral(i1, s1), BVLiteral(i2, s2)) if s1 == s2 => BVLiteral(i1 ^ i2, s1)
+ case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") ^ (" + re.asString + ")")
}
case BVShiftLeft(l,r) =>
(e(l), e(r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 << i2)
- case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ case (BVLiteral(i1, s1), b2 @ BVLiteral(_, s2)) if s1 == s2 =>
+ BVLiteral(shift(i1, s1, b2.toBigInt.toInt), s1)
+ case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") << (" + re.asString + ")")
}
case BVAShiftRight(l,r) =>
(e(l), e(r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 >> i2)
- case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ case (BVLiteral(i1, s1), b2 @ BVLiteral(_, s2)) if s1 == s2 =>
+ val shiftCount = b2.toBigInt.toInt
+ val shifted = shift(i1, s1, -shiftCount)
+ BVLiteral(if (i1(s1)) shifted ++ ((s1 - shiftCount) to s1) else shifted, s1)
+ case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") >> (" + re.asString + ")")
}
case BVLShiftRight(l,r) =>
(e(l), e(r)) match {
- case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 >>> i2)
- case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ case (BVLiteral(i1, s1), b2 @ BVLiteral(_, s2)) if s1 == s2 =>
+ BVLiteral(shift(i1, s1, -b2.toBigInt.toInt), s1)
+ case (le,re) => throw EvalError("Unexpected operation: (" + le.asString + ") >>> (" + re.asString + ")")
}
case LessThan(l,r) =>
(e(l), e(r)) 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))
+ case (b1 @ BVLiteral(_, s1), b2 @ BVLiteral(_, s2)) if s1 == s2 =>
+ BooleanLiteral(b1.toBigInt < b2.toBigInt)
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) => BooleanLiteral(i1 < i2)
+ case (a @ FractionLiteral(_, _), b @ FractionLiteral(_, _)) =>
+ val FractionLiteral(n, _) = e(Minus(a, b))
BooleanLiteral(n < 0)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 < c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
@@ -508,10 +398,11 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
case GreaterThan(l,r) =>
(e(l), e(r)) 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))
+ case (b1 @ BVLiteral(_, s1), b2 @ BVLiteral(_, s2)) if s1 == s2 =>
+ BooleanLiteral(b1.toBigInt > b2.toBigInt)
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) => BooleanLiteral(i1 > i2)
+ case (a @ FractionLiteral(_, _), b @ FractionLiteral(_, _)) =>
+ val FractionLiteral(n, _) = e(Minus(a, b))
BooleanLiteral(n > 0)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 > c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
@@ -519,10 +410,11 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
case LessEquals(l,r) =>
(e(l), e(r)) 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))
+ case (b1 @ BVLiteral(_, s1), b2 @ BVLiteral(_, s2)) if s1 == s2 =>
+ BooleanLiteral(b1.toBigInt <= b2.toBigInt)
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) => BooleanLiteral(i1 <= i2)
+ case (a @ FractionLiteral(_, _), b @ FractionLiteral(_, _)) =>
+ val FractionLiteral(n, _) = e(Minus(a, b))
BooleanLiteral(n <= 0)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 <= c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
@@ -530,10 +422,11 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
case GreaterEquals(l,r) =>
(e(l), e(r)) 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))
+ case (b1 @ BVLiteral(_, s1), b2 @ BVLiteral(_, s2)) if s1 == s2 =>
+ BooleanLiteral(b1.toBigInt >= b2.toBigInt)
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) => BooleanLiteral(i1 >= i2)
+ case (a @ FractionLiteral(_, _), b @ FractionLiteral(_, _)) =>
+ val FractionLiteral(n, _) = e(Minus(a, b))
BooleanLiteral(n >= 0)
case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 >= c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
@@ -541,7 +434,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
case SetAdd(s1, elem) =>
(e(s1), e(elem)) match {
- case (FiniteSet(els1, tpe), evElem) => FiniteSet(els1 + evElem, tpe)
+ case (FiniteSet(els1, tpe), evElem) => FiniteSet((els1 :+ evElem).distinct, tpe)
case (le, re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
@@ -559,7 +452,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
case SetDifference(s1,s2) =>
(e(s1), e(s2)) match {
- case (FiniteSet(els1, tpe), FiniteSet(els2, _)) => FiniteSet(els1 -- els2, tpe)
+ case (FiniteSet(els1, tpe), FiniteSet(els2, _)) => FiniteSet((els1.toSet -- els2).toSeq, tpe)
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
@@ -569,273 +462,101 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
}
case SubsetOf(s1,s2) => (e(s1), e(s2)) match {
- case (FiniteSet(els1, _),FiniteSet(els2, _)) => BooleanLiteral(els1.subsetOf(els2))
+ case (FiniteSet(els1, _),FiniteSet(els2, _)) => BooleanLiteral(els1.toSet.subsetOf(els2.toSet))
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
case SetCardinality(s) =>
val sr = e(s)
sr match {
- case FiniteSet(els, _) => InfiniteIntegerLiteral(els.size)
+ case FiniteSet(els, _) => IntegerLiteral(els.size)
case _ => throw EvalError(typeErrorMsg(sr, SetType(Untyped)))
}
case f @ FiniteSet(els, base) =>
- FiniteSet(els.map(e), base)
+ FiniteSet(els.map(e).distinct, base)
case BagAdd(bag, elem) => (e(bag), e(elem)) match {
- case (FiniteBag(els, tpe), evElem) => FiniteBag(els + (evElem -> (els.get(evElem) match {
- case Some(InfiniteIntegerLiteral(i)) => InfiniteIntegerLiteral(i + 1)
- case Some(i) => throw EvalError(typeErrorMsg(i, IntegerType))
- case None => InfiniteIntegerLiteral(1)
- })), tpe)
+ case (FiniteBag(els, tpe), evElem) =>
+ val (matching, rest) = els.partition(_._1 == evElem)
+ FiniteBag(rest :+ (evElem -> matching.lastOption.map {
+ case (_, IntegerLiteral(i)) => IntegerLiteral(i + 1)
+ case (_, e) => throw EvalError(typeErrorMsg(e, IntegerType))
+ }.getOrElse(IntegerLiteral(1))), tpe)
case (le, re) => throw EvalError(typeErrorMsg(le, bag.getType))
}
case MultiplicityInBag(elem, bag) => (e(elem), e(bag)) match {
- case (evElem, FiniteBag(els, tpe)) => els.getOrElse(evElem, InfiniteIntegerLiteral(0))
+ case (evElem, FiniteBag(els, tpe)) =>
+ els.collect { case (k,v) if k == evElem => v }.lastOption.getOrElse(IntegerLiteral(0))
case (le, re) => throw EvalError(typeErrorMsg(re, bag.getType))
}
case BagIntersection(b1, b2) => (e(b1), e(b2)) match {
- case (FiniteBag(els1, tpe), FiniteBag(els2, _)) => FiniteBag(els1.flatMap { case (k, v) =>
- val i = (v, els2.getOrElse(k, InfiniteIntegerLiteral(0))) match {
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => i1 min i2
- case (le, re) => throw EvalError(typeErrorMsg(le, IntegerType))
- }
+ case (FiniteBag(els1, tpe), FiniteBag(els2, _)) =>
+ val map2 = els2.toMap
+ FiniteBag(els1.flatMap { case (k, v) =>
+ val i = (v, map2.getOrElse(k, IntegerLiteral(0))) match {
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) => i1 min i2
+ case (le, re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ }
- if (i <= 0) None else Some(k -> InfiniteIntegerLiteral(i))
- }, tpe)
+ if (i <= 0) None else Some(k -> IntegerLiteral(i))
+ }, tpe)
case (le, re) => throw EvalError(typeErrorMsg(le, b1.getType))
}
case BagUnion(b1, b2) => (e(b1), e(b2)) match {
- case (FiniteBag(els1, tpe), FiniteBag(els2, _)) => FiniteBag((els1.keys ++ els2.keys).toSet.map { (k: Expr) =>
- k -> ((els1.getOrElse(k, InfiniteIntegerLiteral(0)), els2.getOrElse(k, InfiniteIntegerLiteral(0))) match {
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 + i2)
- case (le, re) => throw EvalError(typeErrorMsg(le, IntegerType))
- })
- }.toMap, tpe)
+ case (FiniteBag(els1, tpe), FiniteBag(els2, _)) =>
+ val (map1, map2) = (els1.toMap, els2.toMap)
+ FiniteBag((map1.keys ++ map2.keys).toSet.map { (k: Expr) =>
+ k -> ((map1.getOrElse(k, IntegerLiteral(0)), map2.getOrElse(k, IntegerLiteral(0))) match {
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) => IntegerLiteral(i1 + i2)
+ case (le, re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ })
+ }.toSeq, tpe)
case (le, re) => throw EvalError(typeErrorMsg(le, b1.getType))
}
case BagDifference(b1, b2) => (e(b1), e(b2)) match {
- case (FiniteBag(els1, tpe), FiniteBag(els2, _)) => FiniteBag(els1.flatMap { case (k, v) =>
- val i = (v, els2.getOrElse(k, InfiniteIntegerLiteral(0))) match {
- case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => i1 - i2
- case (le, re) => throw EvalError(typeErrorMsg(le, IntegerType))
- }
+ case (FiniteBag(els1, tpe), FiniteBag(els2, _)) =>
+ val map2 = els2.toMap
+ FiniteBag(els1.flatMap { case (k, v) =>
+ val i = (v, map2.getOrElse(k, IntegerLiteral(0))) match {
+ case (IntegerLiteral(i1), IntegerLiteral(i2)) => i1 - i2
+ case (le, re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ }
- if (i <= 0) None else Some(k -> InfiniteIntegerLiteral(i))
- }, tpe)
+ if (i <= 0) None else Some(k -> IntegerLiteral(i))
+ }, tpe)
case (le, re) => throw EvalError(typeErrorMsg(le, b1.getType))
}
case FiniteBag(els, base) =>
- FiniteBag(els.map{ case (k, v) => (e(k), e(v)) }, base)
+ // we use toMap.toSeq to reduce dupplicate keys
+ FiniteBag(els.map { case (k, v) => (e(k), e(v)) }.toMap.toSeq, base)
case l @ Lambda(_, _) =>
- val mapping = variablesOf(l).map(id => id -> e(Variable(id))).toMap
- replaceFromIDs(mapping, l).asInstanceOf[Lambda]
-
- case FiniteLambda(mapping, dflt, tpe) =>
- FiniteLambda(mapping.map(p => p._1.map(e) -> e(p._2)), e(dflt), tpe)
-
- case f @ Forall(fargs, body) =>
+ val mapping = variablesOf(l).map(v => v -> e(v)).toMap
+ replaceFromSymbols(mapping, l).asInstanceOf[Lambda]
- implicit val debugSection = utils.DebugSectionVerification
+ case f: Forall => onForallInvocation(f)
- ctx.reporter.debug("Executing forall: " + f.asString)
-
- val mapping = variablesOf(f).map(id => id -> rctx.mappings(id)).toMap
- val context = mapping.toSeq.sortBy(_._1.uniqueName).map(_._2)
-
- frlCache.getOrElse((f, context), {
- val tStart = System.currentTimeMillis
-
- val newOptions = Seq(
- LeonOption(UnrollingProcedure.optFeelingLucky)(false),
- LeonOption(UnrollingProcedure.optSilentErrors)(true),
- LeonOption(UnrollingProcedure.optCheckModels)(true)
- )
-
- val newCtx = ctx.copy(options = ctx.options.filterNot { opt =>
- newOptions.exists(no => opt.optionDef == no.optionDef)
- } ++ newOptions)
-
- val sctx = SolverContext(newCtx, bank)
- val solverf = SolverFactory.getFromSettings(sctx, program).withTimeout(1.second)
- val solver = solverf.getNewSolver()
-
- try {
- val cnstr = Not(replaceFromIDs(mapping, body))
- solver.assertCnstr(cnstr)
-
- gctx.model match {
- case pm: PartialModel =>
- val quantifiers = fargs.map(_.id).toSet
- val quorums = extractQuorums(body, quantifiers)
-
- val domainCnstr = orJoin(quorums.map { quorum =>
- val quantifierDomains = quorum.flatMap { case (path, caller, args) =>
- val domain = pm.domains.get(e(caller))
- args.zipWithIndex.flatMap {
- case (Variable(id),idx) if quantifiers(id) =>
- Some(id -> domain.map(cargs => path -> cargs(idx)))
- case _ => None
- }
- }
-
- val domainMap = quantifierDomains.groupBy(_._1).mapValues(_.map(_._2).flatten)
- andJoin(domainMap.toSeq.map { case (id, dom) =>
- orJoin(dom.toSeq.map { case (path, value) =>
- // @nv: Equality with variable is ok, see [[leon.codegen.runtime.Monitor]]
- path and Equals(Variable(id), value)
- })
- })
- })
-
- solver.assertCnstr(domainCnstr)
-
- case _ =>
- }
-
- solver.check match {
- case Some(negRes) =>
- val total = System.currentTimeMillis-tStart
- val res = BooleanLiteral(!negRes)
- ctx.reporter.debug("Verification took "+total+"ms")
- ctx.reporter.debug("Finished forall evaluation with: "+res)
-
- frlCache += (f, context) -> res
- res
- case _ =>
- throw RuntimeError("Timeout exceeded")
- }
- } catch {
- case e: Throwable =>
- throw EvalError("Runtime verification of forall failed: "+e.getMessage)
- } finally {
- solverf.reclaim(solver)
- solverf.shutdown()
- }
- })
-
- case ArrayLength(a) =>
- val FiniteArray(_, _, IntLiteral(length)) = e(a)
- IntLiteral(length)
-
- case ArrayUpdated(a, i, v) =>
- val ra = e(a)
- val ri = e(i)
- val rv = e(v)
-
- val IntLiteral(index) = ri
- val FiniteArray(elems, default, length) = ra
- val ArrayType(tp) = ra.getType
- finiteArray(elems.updated(index, rv), default map { (_, length) }, tp)
-
- case ArraySelect(a, i) =>
- val IntLiteral(index) = e(i)
- val FiniteArray(elems, default, _) = e(a)
- try {
- elems.get(index).orElse(default).get
- } catch {
- case e : IndexOutOfBoundsException => throw RuntimeError(e.getMessage)
- }
-
- case f @ FiniteArray(elems, default, length) =>
- val ArrayType(tp) = f.getType
- finiteArray(
- elems.map(el => (el._1, e(el._2))),
- default.map{ d => (e(d), e(length)) },
- tp
- )
-
- case f @ FiniteMap(ss, kT, vT) =>
- FiniteMap(ss.map{ case (k, v) => (e(k), e(v)) }, kT, vT)
+ case f @ FiniteMap(ss, dflt, vT) =>
+ // we use toMap.toSeq to reduce dupplicate keys
+ FiniteMap(ss.map{ case (k, v) => (e(k), e(v)) }.toMap.toSeq, e(dflt), vT)
case g @ MapApply(m,k) => (e(m), e(k)) match {
case (FiniteMap(ss, _, _), e) =>
- ss.getOrElse(e, throw RuntimeError("Key not found: " + e.asString))
+ ss.toMap.getOrElse(e, throw RuntimeError("Key not found: " + e.asString))
case (l,r) =>
throw EvalError(typeErrorMsg(l, MapType(r.getType, g.getType)))
}
- case u @ MapUnion(m1,m2) => (e(m1), e(m2)) match {
- case (f1@FiniteMap(ss1, _, _), FiniteMap(ss2, _, _)) =>
- val newSs = ss1 ++ ss2
- val MapType(kT, vT) = u.getType
- FiniteMap(newSs, kT, vT)
- case (l, r) =>
- throw EvalError(typeErrorMsg(l, m1.getType))
- }
-
- case i @ MapIsDefinedAt(m,k) => (e(m), e(k)) match {
- case (FiniteMap(ss, _, _), e) => BooleanLiteral(ss.contains(e))
- case (l, r) => throw EvalError(typeErrorMsg(l, m.getType))
- }
-
- case p : Passes =>
- e(p.asConstraint)
-
- case choose: Choose =>
- if(evaluationFailsOnChoose) {
- throw EvalError("Evaluator set to not solve choose constructs")
- }
-
- implicit val debugSection = utils.DebugSectionSynthesis
-
- val p = synthesis.Problem.fromSpec(choose.pred)
-
- ctx.reporter.debug("Executing choose!")
-
- val ins = p.as.map(rctx.mappings(_))
-
- clpCache.getOrElse((choose, ins), {
- val tStart = System.currentTimeMillis
-
- val sctx = SolverContext(ctx, bank)
- val solverf = SolverFactory.getFromSettings(sctx, program).withTimeout(1.seconds)
- val solver = solverf.getNewSolver()
-
- try {
- val cnstr = p.pc withBindings p.as.map(id => id -> rctx.mappings(id)) and p.phi
- solver.assertCnstr(cnstr)
-
- 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)
-
- clpCache += (choose, ins) -> leonRes
- leonRes
- case Some(false) =>
- throw RuntimeError("Constraint is UNSAT")
- case _ =>
- throw RuntimeError("Timeout exceeded")
- }
- } catch {
- case e: Throwable =>
- throw EvalError("Runtime synthesis of choose failed: "+e.getMessage)
- } finally {
- solverf.reclaim(solver)
- solverf.shutdown()
- }
- })
-
case MatchExpr(scrut, cases) =>
val rscrut = e(scrut)
cases.toStream.map(c => matchesCase(rscrut, c)).find(_.nonEmpty) match {
@@ -845,21 +566,17 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
throw RuntimeError("MatchError: "+rscrut.asString+" did not match any of the cases:\n"+cases)
}
- case synthesis.utils.MutableExpr(ex) =>
- e(ex)
-
case gl: GenericValue => gl
- case fl : FractionalLiteral => normalizeFraction(fl)
+ case fl : FractionLiteral => normalizeFraction(fl)
case l : Literal[_] => l
case other =>
throw EvalError("Unhandled case in Evaluator : [" + other.getClass + "] " + other.asString)
}
- def matchesCase(scrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Option[(MatchCase, Map[Identifier, Expr])] = {
- import purescala.TypeOps.isSubtypeOf
+ def matchesCase(scrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Option[(MatchCase, Map[ValDef, Expr])] = {
- def matchesPattern(pat: Pattern, expr: Expr): Option[Map[Identifier, Expr]] = (pat, expr) match {
+ def matchesPattern(pat: Pattern, expr: Expr): Option[Map[ValDef, Expr]] = (pat, expr) match {
case (InstanceOfPattern(ob, pct), e) =>
if (isSubtypeOf(e.getType, pct)) {
Some(obind(ob, e))
@@ -880,11 +597,14 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
} else {
None
}
- case (up @ UnapplyPattern(ob, _, subs), scrut) =>
- e(functionInvocation(up.unapplyFun.fd, Seq(scrut))) match {
- case CaseClass(CaseClassType(cd, _), Seq()) if cd == program.library.None.get =>
+ case (up @ UnapplyPattern(ob, id, tps, subs), scrut) =>
+ val tfd = getFunction(id, tps)
+ val (noneType, someType) = up.optionChildren
+
+ e(FunctionInvocation(id, tps, Seq(scrut))) match {
+ case CaseClass(`noneType`, Seq()) =>
None
- case CaseClass(CaseClassType(cd, _), Seq(arg)) if cd == program.library.Some.get =>
+ case CaseClass(`someType`, Seq(arg)) =>
val res = subs zip unwrapTuple(arg, subs.size) map {
case (s,a) => matchesPattern(s,a)
}
@@ -894,7 +614,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
None
}
case other =>
- throw EvalError(typeErrorMsg(other, up.unapplyFun.returnType))
+ throw EvalError(typeErrorMsg(other, tfd.returnType))
}
case (TuplePattern(ob, subs), Tuple(args)) =>
if (subs.size == args.size) {
@@ -912,8 +632,8 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
case _ => None
}
- def obind(ob: Option[Identifier], e: Expr): Map[Identifier, Expr] = {
- Map[Identifier, Expr]() ++ ob.map(id => id -> e)
+ def obind(ovd: Option[ValDef], e: Expr): Map[ValDef, Expr] = {
+ ovd.map(vd => vd -> e).toMap
}
caze match {
diff --git a/src/main/scala/inox/evaluators/SolvingEvaluator.scala b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
index 9b5aee6aeb2cd97ce74c1f7f0439ccec02b0a124..267328f68f2a14e886d11f8071889840f7821d30 100644
--- a/src/main/scala/inox/evaluators/SolvingEvaluator.scala
+++ b/src/main/scala/inox/evaluators/SolvingEvaluator.scala
@@ -8,6 +8,9 @@ import solvers._
import scala.collection.mutable.{Map => MutableMap}
trait SolvingEvaluator extends Evaluator {
+ import program._
+ import program.trees._
+ import program.symbols._
object optForallCache extends InoxOptionDef[MutableMap[program.trees.Forall, Boolean]] {
val parser = { (_: String) => throw FatalError("Unparsable option \"bankOption\"") }
@@ -18,34 +21,25 @@ trait SolvingEvaluator extends Evaluator {
}
def getSolver(opts: InoxOption[Any]*): Solver { val program: SolvingEvaluator.this.program.type }
-}
-
-trait SolvingEvalInterface {
- val program: Program
- import program._
- import program.trees._
- import program.symbols._
-
- val evaluator: DeterministicEvaluator with SolvingEvaluator { val program: SolvingEvalInterface.this.program.type }
private val specCache: MutableMap[Expr, Expr] = MutableMap.empty
private val forallCache: MutableMap[Forall, Expr] = MutableMap.empty
- def onSpecInvocation(specs: Expr): Expr = specCache.getOrElseUpdate(specs, {
- val Seq(free) = exprOps.variablesOf(specs).toSeq
+ def onSpecInvocation(specs: Lambda): Expr = specCache.getOrElseUpdate(specs, {
+ val Lambda(Seq(vd), body) = specs
val timer = ctx.timers.evaluators.specs.start()
- val solver = evaluator.getSolver(evaluator.options.options.collect {
- case o @ InoxOption(opt, _) if opt == evaluator.optForallCache => o
+ val solver = getSolver(options.options.collect {
+ case o @ InoxOption(opt, _) if opt == optForallCache => o
}.toSeq : _*)
- solver.assertCnstr(specs)
+ solver.assertCnstr(body)
val res = solver.check(model = true)
timer.stop()
res match {
case solver.Model(model) =>
- valuateWithModel(model)(free.toVal)
+ valuateWithModel(model)(vd)
case _ =>
throw new RuntimeException("Failed to evaluate specs " + specs.asString)
@@ -53,17 +47,17 @@ trait SolvingEvalInterface {
})
def onForallInvocation(forall: Forall): Expr = {
- val cache = evaluator.options.findOption(evaluator.optForallCache).getOrElse {
+ val cache = options.findOption(optForallCache).getOrElse {
throw new RuntimeException("Couldn't find evaluator's forall cache")
}
BooleanLiteral(cache.getOrElse(forall, {
val timer = ctx.timers.evaluators.forall.start()
- val solver = evaluator.getSolver(
+ val solver = getSolver(
InoxOption(optSilentErrors)(true),
InoxOption(optCheckModels)(false),
- InoxOption(evaluator.optForallCache)(cache)
+ InoxOption(optForallCache)(cache)
)
solver.assertCnstr(Not(forall.body))
@@ -77,7 +71,7 @@ trait SolvingEvalInterface {
case solver.Model(model) =>
cache(forall) = false
- evaluator.eval(Not(forall.body), model) match {
+ eval(Not(forall.body), model) match {
case EvaluationResults.Successful(BooleanLiteral(true)) => false
case _ => throw new RuntimeException("Forall model check failed")
}
@@ -88,3 +82,4 @@ trait SolvingEvalInterface {
}))
}
}
+