From 764e9ca0fbe224b19a3d71cbecbebeabe4259545 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 9 May 2012 22:48:27 +0000
Subject: [PATCH] using FiniteArray to represent models containing array
---
src/main/scala/leon/Evaluator.scala | 35 +++++++------------
src/main/scala/leon/FairZ3Solver.scala | 15 +++++---
.../scala/leon/purescala/PrettyPrinter.scala | 3 ++
src/main/scala/leon/purescala/Trees.scala | 2 ++
4 files changed, 28 insertions(+), 27 deletions(-)
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index c26d7ca3d..d9a0733ec 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 90f95153e..8ec0984ee 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 cd3df3797..f03c624af 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 11adb22fc..1c015cfe6 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))
--
GitLab