From 373c4aba199175a5c1e54de66d418a8c475e7357 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 4 Feb 2015 20:39:38 +0100
Subject: [PATCH] Refactor FiniteArray to an implicit representation
FiniteArray now takes an Expr for the length, a default
Expr, and a Map of defined Expr for some of its elements.
Adapt the rest of Leon to the new trees.
The PrettyPrinter tries to be a little bit smart about
how to print the array, only printing a few elements when the
array gets too big. The regression test produces an
huge array counter-example that used to lead to a crash of
Leon with the previous implementation of Array (fully represented
in memory).
---
.../scala/leon/codegen/CodeGeneration.scala | 7 +--
.../scala/leon/codegen/CompilationUnit.scala | 4 +-
.../leon/evaluators/RecursiveEvaluator.scala | 28 ++++++------
.../frontends/scalac/CodeExtraction.scala | 2 +-
.../scala/leon/purescala/Extractors.scala | 21 +++++++--
.../scala/leon/purescala/PrettyPrinter.scala | 32 ++++++++++++--
.../scala/leon/purescala/ScalaPrinter.scala | 28 +++++++++++-
src/main/scala/leon/purescala/TreeOps.scala | 2 +-
src/main/scala/leon/purescala/Trees.scala | 12 +++++-
.../solvers/smtlib/SMTLIBCVC4Target.scala | 4 +-
.../leon/solvers/smtlib/SMTLIBTarget.scala | 12 +++++-
.../leon/solvers/smtlib/SMTLIBZ3Target.scala | 7 +--
.../leon/solvers/z3/AbstractZ3Solver.scala | 30 ++++++-------
.../verification/VerificationReport.scala | 1 -
.../purescala/invalid/BigArray.scala | 11 +++++
.../evaluators/DefaultEvaluatorTests.scala | 43 +++++++++++++++++++
16 files changed, 185 insertions(+), 59 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/BigArray.scala
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index f83c724db..ff969c68b 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -650,8 +650,9 @@ trait CodeGeneration {
ch << storeInstr
//returns targetArray
- case a @ FiniteArray(es) =>
- ch << Ldc(es.size)
+ case a @ FiniteArray(elems, default, length) =>
+ val IntLiteral(l) = length
+ ch << Ldc(l)
val storeInstr = a.getType match {
case ArrayType(CharType) => ch << NewArray.primitive("T_CHAR"); CASTORE
case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
@@ -659,7 +660,7 @@ trait CodeGeneration {
case ArrayType(other) => ch << NewArray(typeToJVM(other)); AASTORE
case other => throw CompilationException("Cannot compile finite array expression whose type is %s.".format(other))
}
- for((e,i) <- es.zipWithIndex) {
+ for((i, e) <- elems) {
ch << DUP << Ldc(i)
mkExpr(e, ch)
ch << storeInstr
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 20e41e421..64851adca 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -146,8 +146,8 @@ class CompilationUnit(val ctx: LeonContext,
// For now, we only treat boolean arrays separately.
// We have a use for these, mind you.
- case f @ FiniteArray(exprs) if f.getType == ArrayType(BooleanType) =>
- exprs.map(e => exprToJVM(e).asInstanceOf[java.lang.Boolean].booleanValue).toArray
+ //case f @ FiniteArray(exprs) if f.getType == ArrayType(BooleanType) =>
+ // exprs.map(e => exprToJVM(e).asInstanceOf[java.lang.Boolean].booleanValue).toArray
case s @ FiniteSet(els) =>
val s = new leon.codegen.runtime.Set()
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 6eb4323b4..fa0148b5d 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -336,17 +336,9 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case u @ UnitLiteral() => u
case l @ Lambda(_, _) => l
- case f @ ArrayFill(length, default) =>
- val rDefault = e(default)
- val rLength = e(length)
- val IntLiteral(iLength) = rLength
- FiniteArray((1 to iLength).map(_ => rDefault).toSeq).setType(ArrayType(rDefault.getType))
-
case ArrayLength(a) =>
- var ra = e(a)
- while(!ra.isInstanceOf[FiniteArray])
- ra = ra.asInstanceOf[ArrayUpdated].array
- IntLiteral(ra.asInstanceOf[FiniteArray].exprs.size)
+ var FiniteArray(elems, default, IntLiteral(length)) = e(a)
+ IntLiteral(length)
case ArrayUpdated(a, i, v) =>
val ra = e(a)
@@ -354,20 +346,24 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val rv = e(v)
val IntLiteral(index) = ri
- val FiniteArray(exprs) = ra
- FiniteArray(exprs.updated(index, rv)).setType(ra.getType)
+ val FiniteArray(elems, default, length) = ra
+ FiniteArray(elems.updated(index, rv), default, length).setType(ra.getType)
case ArraySelect(a, i) =>
val IntLiteral(index) = e(i)
- val FiniteArray(exprs) = e(a)
+ val FiniteArray(elems, default, length) = e(a)
try {
- exprs(index)
+ elems.get(index).orElse(default).get
} catch {
case e : IndexOutOfBoundsException => throw RuntimeError(e.getMessage)
}
- case FiniteArray(exprs) =>
- FiniteArray(exprs.map(ex => e(ex))).setType(expr.getType)
+ case FiniteArray(elems, default, length) =>
+ FiniteArray(
+ elems.map(el => (el._1, e(el._2))),
+ default.map(e),
+ e(length)
+ ).setType(expr.getType)
case f @ FiniteMap(ss) => FiniteMap(ss.map{ case (k, v) => (e(k), e(v)) }.distinct).setType(f.getType)
case g @ MapGet(m,k) => (e(m), e(k)) match {
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index bbfffc373..254fd8f57 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1365,7 +1365,7 @@ trait CodeExtraction extends ASTExtractors {
val underlying = extractType(baseType)
val lengthRec = extractTree(length)
val defaultValueRec = extractTree(defaultValue)
- ArrayFill(lengthRec, defaultValueRec)
+ FiniteArray(Map(), Some(defaultValueRec), lengthRec).setType(ArrayType(underlying))
case ExIfThenElse(t1,t2,t3) =>
val r1 = extractTree(t1)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index a5c591bdd..d8ba07c13 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -65,7 +65,6 @@ object Extractors {
case MapUnion(t1,t2) => Some((t1,t2,MapUnion))
case MapDifference(t1,t2) => Some((t1,t2,MapDifference))
case MapIsDefinedAt(t1,t2) => Some((t1,t2, MapIsDefinedAt))
- case ArrayFill(t1, t2) => Some((t1, t2, ArrayFill))
case ArraySelect(t1, t2) => Some((t1, t2, ArraySelect))
case Let(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => Let(binders, e, b)))
case LetTuple(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => LetTuple(binders, e, b)))
@@ -120,10 +119,24 @@ object Extractors {
}
case FiniteMultiset(args) => Some((args, FiniteMultiset))
case ArrayUpdated(t1, t2, t3) => Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdated(as(0), as(1), as(2))))
- case FiniteArray(args) => Some((args, { (as: Seq[Expr]) =>
- val tpe = leastUpperBound(as.map(_.getType)).map(ArrayType(_)).getOrElse(expr.getType)
- FiniteArray(as).setType(tpe)
+ case FiniteArray(elems, default, length) => {
+ val fixedElems: Seq[(Int, Expr)] = elems.toSeq
+ val all: Seq[Expr] = fixedElems.map(_._2) ++ default ++ Seq(length)
+ Some((all, (as: Seq[Expr]) => {
+ val tpe = leastUpperBound(as.map(_.getType))
+ .map(ArrayType(_))
+ .getOrElse(expr.getType)
+ val (newElems, newDefault, newSize) = default match {
+ case None => (as.init, None, as.last)
+ case Some(_) => (as.init.init, Some(as.init.last), as.last)
+ }
+ FiniteArray(
+ fixedElems.zip(newElems).map(p => (p._1._1, p._2)).toMap,
+ newDefault,
+ newSize).setType(tpe)
}))
+ }
+
case Tuple(args) => Some((args, Tuple))
case IfExpr(cond, thenn, elze) => Some((Seq(cond, thenn, elze), (as: Seq[Expr]) => IfExpr(as(0), as(1), as(2))))
case MatchLike(scrut, cases, builder) => Some((
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index de7052e22..43d98b758 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -13,7 +13,7 @@ import utils._
import java.lang.StringBuffer
import PrinterHelpers._
-import TreeOps.{isStringLiteral, isListLiteral}
+import TreeOps.{isStringLiteral, isListLiteral, simplestValue}
import TypeTreeOps.leastUpperBound
import synthesis.Witnesses._
@@ -374,10 +374,36 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case MapGet(m,k) => p"$m($k)"
case MapIsDefinedAt(m,k) => p"$m.isDefinedAt($k)"
case ArrayLength(a) => p"$a.length"
- case ArrayFill(size, v) => p"Array.fill($size)($v)"
case ArraySelect(a, i) => p"$a($i)"
case ArrayUpdated(a, i, v) => p"$a.updated($i, $v)"
- case FiniteArray(exprs) => p"Array($exprs)"
+ case a@FiniteArray(es, d, s) => {
+ val ArrayType(underlying) = a.getType
+ val default = d.getOrElse(simplestValue(underlying))
+ def ppBigArray(): Unit = {
+ if(es.isEmpty) {
+ p"Array($default, $default, $default, ..., $default) (of size $s)"
+ } else {
+ p"Array(_) (of size $s)"
+ }
+ }
+ s match {
+ case IntLiteral(length) => {
+ if(es.size == length) {
+ val orderedElements = es.toSeq.sortWith((e1, e2) => e1._1 < e2._1)
+ p"Array($orderedElements)"
+ } else if(length < 10) {
+ val elems = (0 until length).map(i =>
+ es.find(el => el._1 == i).map(el => el._2).getOrElse(d.get)
+ )
+ p"Array($elems)"
+ } else {
+ ppBigArray()
+ }
+ }
+ case _ => ppBigArray()
+ }
+ }
+
case Not(expr) => p"\u00AC$expr"
case ValDef(id, tpe) => p"${typed(id)}"
case This(_) => p"this"
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index d9fd8e296..82ddb9cb8 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -49,7 +49,33 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
case SetDifference(l,r) => p"$l -- $r"
case SetIntersection(l,r) => p"$l & $r"
case SetCardinality(s) => p"$s.size"
- case FiniteArray(exprs) => p"Array($exprs)"
+
+ case a@FiniteArray(elems, oDef, size) => {
+ import TreeOps._
+ val ArrayType(underlying) = a.getType
+ val default = oDef.getOrElse(simplestValue(underlying))
+ size match {
+ case IntLiteral(s) => {
+ val explicitArray = Array.fill(s)(default)
+ for((id, el) <- elems)
+ explicitArray(id) = el
+ val lit = explicitArray.toList
+ p"Array($lit)"
+ }
+ case size => {
+ p"""|{
+ | val tmp = Array.fill($size)($default)
+ |"""
+ for((id, el) <- elems)
+ p""""| tmp($id) = $el
+ |"""
+ p"""| tmp
+ |}"""
+
+ }
+ }
+ }
+
case Not(expr) => p"!$expr"
case _ =>
super.pp(tree)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 801469a6b..2789fb43a 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1016,7 +1016,7 @@ object TreeOps {
case SetType(baseType) => FiniteSet(Set()).setType(tpe)
case MapType(fromType, toType) => FiniteMap(Seq()).setType(tpe)
case TupleType(tpes) => Tuple(tpes.map(simplestValue))
- case ArrayType(tpe) => ArrayFill(IntLiteral(0), simplestValue(tpe))
+ case ArrayType(tpe) => FiniteArray(Map(), Some(simplestValue(tpe)), IntLiteral(0)).setType(ArrayType(tpe))
case act @ AbstractClassType(acd, tpe) =>
val children = acd.knownChildren
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 052dd2305..89a23828b 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -430,8 +430,8 @@ object Trees {
val getType = BooleanType
}
- /* Array operations */
+ /* Array operations */
case class ArraySelect(array: Expr, index: Expr) extends Expr {
def getType = array.getType match {
case ArrayType(base) =>
@@ -454,7 +454,15 @@ object Trees {
val getType = Int32Type
}
- case class FiniteArray(exprs: Seq[Expr]) extends Expr with MutableTyped
+ case class FiniteArray(elems: Map[Int, Expr], default: Option[Expr], length: Expr) extends Expr with MutableTyped
+
+ object FiniteArray {
+ def apply(elems: Seq[Expr]): FiniteArray = {
+ val res = FiniteArray(elems.zipWithIndex.map(_.swap).toMap, None, IntLiteral(elems.size))
+ elems.headOption.foreach(e => res.setType(ArrayType(e.getType)))
+ res
+ }
+ }
/* Special trees */
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 074fffce4..796b49647 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -98,13 +98,13 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
}
override def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]) = e match {
- case a @ FiniteArray(elems) =>
+ case a @ FiniteArray(elems, default, size) =>
val tpe @ ArrayType(base) = normalizeType(a.getType)
declareSort(tpe)
var ar: Term = declareVariable(FreshIdentifier("arrayconst").setType(RawArrayType(Int32Type, base)))
- for ((e, i) <- elems.zipWithIndex) {
+ for ((i, e) <- elems) {
ar = FunctionApplication(SSymbol("store"), Seq(ar, toSMT(IntLiteral(i)), toSMT(e)))
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index eb59fd5b9..4d222d4f7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -526,9 +526,17 @@ trait SMTLIBTarget {
val IntLiteral(size) = fromSMT(args(0), Int32Type)
val RawArrayValue(_, elems, default) = fromSMT(args(1), RawArrayType(Int32Type, at.base))
- val entries = for (i <- 0 to size-1) yield elems.getOrElse(IntLiteral(i), default)
+ if(size > 10) {
+ val definedElements = elems.collect{
+ case (IntLiteral(i), value) => (i, value)
+ }.toMap
+ FiniteArray(definedElements, Some(default), IntLiteral(size)).setType(at)
- FiniteArray(entries).setType(at)
+ } else {
+ val entries = for (i <- 0 to size-1) yield elems.getOrElse(IntLiteral(i), default)
+
+ FiniteArray(entries).setType(at)
+ }
case t =>
unsupported("Woot? structural type that is non-structural: "+t)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 91e205c6a..7206a276c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -85,14 +85,15 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
}
override def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]): Term = e match {
- case a @ FiniteArray(elems) =>
+ case a @ FiniteArray(elems, oDef, size) =>
val tpe @ ArrayType(base) = normalizeType(a.getType)
declareSort(tpe)
+ val default: Expr = oDef.getOrElse(simplestValue(base))
- var ar: Term = ArrayConst(declareSort(RawArrayType(Int32Type, base)), toSMT(simplestValue(base)))
+ var ar: Term = ArrayConst(declareSort(RawArrayType(Int32Type, base)), toSMT(default))
- for ((e, i) <- elems.zipWithIndex) {
+ for ((i, e) <- elems) {
ar = ArraysEx.Store(ar, toSMT(IntLiteral(i)), toSMT(e))
}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 02b6683c4..03201a3eb 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -633,14 +633,6 @@ trait AbstractZ3Solver
case MapType(ft, tt) => z3.mkDistinct(z3.mkSelect(rec(m), rec(k)), mapRangeNoneConstructors(tt)())
case errorType => scala.sys.error("Unexpected type for map: " + (ex, errorType))
}
- case fill @ ArrayFill(length, default) =>
- val at @ ArrayType(base) = fill.getType
- typeToSort(at)
- val meta = arrayMetaDecls(normalizeType(at))
-
- val ar = z3.mkConstArray(typeToSort(Int32Type), rec(default))
- val res = meta.cons(ar, rec(length))
- res
case ArraySelect(a, index) =>
typeToSort(a.getType)
@@ -665,13 +657,17 @@ trait AbstractZ3Solver
val res = meta.length(ar)
res
- case arr @ FiniteArray(exprs) => {
- val ArrayType(innerType) = arr.getType
- val arrayType = arr.getType
- val a: Expr = ArrayFill(IntLiteral(exprs.length), simplestValue(innerType))
- val u = exprs.zipWithIndex.foldLeft(a)((array, expI) => ArrayUpdated(array, IntLiteral(expI._2), expI._1))
- rec(u)
- }
+ case arr @ FiniteArray(elems, oDefault, length) =>
+ val at @ ArrayType(base) = arr.getType
+ typeToSort(at)
+ val meta = arrayMetaDecls(normalizeType(at))
+
+ val default = oDefault.getOrElse(simplestValue(base))
+
+ val ar = z3.mkConstArray(typeToSort(base), rec(default))
+ val u = elems.foldLeft(ar)((array, el) =>
+ z3.mkStore(array, rec(IntLiteral(el._1)), rec(el._2)))
+ meta.cons(u, rec(length))
case gv @ GenericValue(tp, id) =>
z3.mkApp(genericValueToDecl(gv))
@@ -739,9 +735,7 @@ trait AbstractZ3Solver
(index -> rec(v))
}
- FiniteArray(for (i <- 1 to length) yield {
- valuesMap.getOrElse(i, elseValue)
- }).setType(at)
+ FiniteArray(valuesMap, Some(elseValue), IntLiteral(length)).setType(at)
}
case LeonType(tpe @ MapType(kt, vt)) =>
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index bec5a07bf..1b39389f6 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -4,7 +4,6 @@ package leon
package verification
import purescala.Definitions.FunDef
-import purescala.ScalaPrinter
class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
import scala.math.Ordering.Implicits._
diff --git a/src/test/resources/regression/verification/purescala/invalid/BigArray.scala b/src/test/resources/regression/verification/purescala/invalid/BigArray.scala
new file mode 100644
index 000000000..f75e88970
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/BigArray.scala
@@ -0,0 +1,11 @@
+import leon.annotation._
+import leon.lang._
+
+object BigArray {
+
+ def big(a: Array[Int]): Int = {
+ require(a.length >= 10 && a(7) == 42)
+ a.length
+ } ensuring(_ <= 1000000000)
+
+}
diff --git a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
index 8b0946d8b..0dd8fe1d3 100644
--- a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
+++ b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
@@ -103,4 +103,47 @@ class DefaultEvaluatorTests extends leon.test.LeonTestSuite {
defaultEvaluator.eval(Let(id, IntLiteral(42), Variable(id))),
IntLiteral(42))
}
+
+
+ test("eval literal array ops") {
+ expectSuccessful(
+ defaultEvaluator.eval(FiniteArray(Map(), Some(IntLiteral(12)), IntLiteral(7)).setType(ArrayType(Int32Type))),
+ FiniteArray(Map(), Some(IntLiteral(12)), IntLiteral(7)))
+ expectSuccessful(
+ defaultEvaluator.eval(
+ ArrayLength(FiniteArray(Map(), Some(IntLiteral(12)), IntLiteral(7)).setType(ArrayType(Int32Type)))),
+ IntLiteral(7))
+ expectSuccessful(
+ defaultEvaluator.eval(ArraySelect(
+ FiniteArray(Seq(IntLiteral(2), IntLiteral(4), IntLiteral(7))),
+ IntLiteral(1))),
+ IntLiteral(4))
+ expectSuccessful(
+ defaultEvaluator.eval(
+ ArrayUpdated(
+ FiniteArray(Seq(IntLiteral(2), IntLiteral(4), IntLiteral(7))),
+ IntLiteral(1),
+ IntLiteral(42))),
+ FiniteArray(Seq(IntLiteral(2), IntLiteral(42), IntLiteral(7))))
+ }
+
+ test("eval variable length of array") {
+ val id = FreshIdentifier("id").setType(Int32Type)
+ expectSuccessful(
+ defaultEvaluator.eval(
+ ArrayLength(
+ FiniteArray(Map(), Some(IntLiteral(12)), Variable(id))
+ .setType(ArrayType(Int32Type))),
+ Map(id -> IntLiteral(27))),
+ IntLiteral(27))
+ }
+
+ test("eval variable default value of array") {
+ val id = FreshIdentifier("id").setType(Int32Type)
+ expectSuccessful(
+ defaultEvaluator.eval(
+ FiniteArray(Map(), Some(Variable(id)), IntLiteral(7)).setType(ArrayType(Int32Type)),
+ Map(id -> IntLiteral(27))),
+ FiniteArray(Map(), Some(IntLiteral(27)), IntLiteral(7)))
+ }
}
--
GitLab