diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala index c26d7ca3d404774908fc3e1d80ad01cd04921546..d9a0733ecd0863cec8562e71f9c63e1822e5d0e2 100644 --- a/src/main/scala/leon/Evaluator.scala +++ b/src/main/scala/leon/Evaluator.scala @@ -85,7 +85,9 @@ object Evaluator { if(fd.hasPrecondition) { rec(frame, matchToIfThenElse(fd.precondition.get)) match { case BooleanLiteral(true) => ; - case BooleanLiteral(false) => throw RuntimeErrorEx("Precondition violation for " + fd.id.name + " reached in evaluation.") + case BooleanLiteral(false) => { + throw RuntimeErrorEx("Precondition violation for " + fd.id.name + " reached in evaluation.: " + fd.precondition.get) + } case other => throw TypeErrorEx(TypeError(other, BooleanType)) } } @@ -260,39 +262,28 @@ object Evaluator { case f @ ArrayFill(length, default) => { val rDefault = rec(ctx, default) val rLength = rec(ctx, length) - ArrayFill(rLength, rDefault) + val IntLiteral(iLength) = rLength + FiniteArray((1 to iLength).map(_ => rDefault).toSeq) } case ArrayLength(a) => { var ra = rec(ctx, a) - while(!ra.isInstanceOf[ArrayFill]) + while(!ra.isInstanceOf[FiniteArray]) ra = ra.asInstanceOf[ArrayUpdated].array - ra.asInstanceOf[ArrayFill].length + IntLiteral(ra.asInstanceOf[FiniteArray].exprs.size) } case ArrayUpdated(a, i, v) => { val ra = rec(ctx, a) val ri = rec(ctx, i) - assert(ri.isInstanceOf[IntLiteral]) val rv = rec(ctx, v) - ArrayUpdated(ra, ri, rv) + + val IntLiteral(index) = ri + val FiniteArray(exprs) = ra + FiniteArray(exprs.updated(index, rv)) } case ArraySelect(a, i) => { val IntLiteral(index) = rec(ctx, i) - var ra = rec(ctx, a) - var found = false - var result: Option[Expr] = None - while(!ra.isInstanceOf[ArrayFill] && !found) { - val ArrayUpdated(ra2, IntLiteral(i), v) = ra - if(index == i) { - result = Some(v) - found = true - } else { - ra = ra2 - } - } - result match { - case Some(r) => r - case None => ra.asInstanceOf[ArrayFill].defaultValue - } + val FiniteArray(exprs) = rec(ctx, a) + exprs(index) } case f @ FiniteMap(ss) => FiniteMap(ss.map(rec(ctx,_)).distinct.asInstanceOf[Seq[SingletonMap]]).setType(f.getType) diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala index 90f95153ed7ef925a98c0ca3ec0a234a606cb9d0..8ec0984ee1994371ad95a95b7367887c923d2ff5 100644 --- a/src/main/scala/leon/FairZ3Solver.scala +++ b/src/main/scala/leon/FairZ3Solver.scala @@ -1187,13 +1187,18 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S case Some(ArrayType(dt)) => { val Z3AppAST(decl, args) = z3.getASTKind(t) assert(args.size == 2) - val length = rec(args(1), Some(Int32Type)) + val IntLiteral(length) = rec(args(1), Some(Int32Type)) val array = model.getArrayValue(args(0)) match { case None => throw new CantTranslateException(t) - case Some((map, elseValue)) => - map.foldLeft(ArrayFill(length, rec(elseValue, Some(dt))): Expr) { - case (acc, (key, value)) => ArrayUpdated(acc, rec(key, Some(Int32Type)), rec(value, Some(dt))) - } + case Some((map, elseValue)) => { + val exprs = map.foldLeft((1 to length).map(_ => rec(elseValue, Some(dt))).toSeq)((acc, p) => { + val IntLiteral(index) = rec(p._1, Some(Int32Type)) + if(index >= 0 && index < length) + acc.updated(index, rec(p._2, Some(dt))) + else acc + }) + FiniteArray(exprs) + } } array } diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala index cd3df37975b52e4893c04f37e57d1b9640720bc9..f03c624af8acddea63ad6c68f993446ffb3cda92 100644 --- a/src/main/scala/leon/purescala/PrettyPrinter.scala +++ b/src/main/scala/leon/purescala/PrettyPrinter.scala @@ -286,6 +286,9 @@ object PrettyPrinter { pp(v, sb, lvl) sb.append(")") } + case FiniteArray(exprs) => { + ppNary(sb, exprs, "Array(", ", ", ")", lvl) + } case Distinct(exprs) => { var nsb = sb diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala index 11adb22fc3d44b26805ec98d7fa80056c196662b..1c015cfe6e1127a178746786d2fe7678c6b30c4d 100644 --- a/src/main/scala/leon/purescala/Trees.scala +++ b/src/main/scala/leon/purescala/Trees.scala @@ -398,6 +398,7 @@ object Trees { case class ArrayLength(array: Expr) extends Expr with FixedType { val fixedType = Int32Type } + case class FiniteArray(exprs: Seq[Expr]) extends Expr /* List operations */ case class NilList(baseType: TypeTree) extends Expr with Terminal @@ -489,6 +490,7 @@ object Trees { case FiniteMultiset(args) => Some((args, FiniteMultiset)) case ArrayUpdate(t1, t2, t3) => Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdate(as(0), as(1), as(2)))) 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, FiniteArray)) case Distinct(args) => Some((args, Distinct)) case Block(args, rest) => Some((args :+ rest, exprs => Block(exprs.init, exprs.last))) case Tuple(args) => Some((args, Tuple))