From 45f42fc33a2e4deb3081d9ad3de974e7112edad1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 4 May 2012 04:34:31 +0000
Subject: [PATCH] cleaner (and more correct) separation of array operation
---
src/main/scala/leon/ArrayTransformation.scala | 2 +-
src/main/scala/leon/Evaluator.scala | 10 +++---
src/main/scala/leon/FairZ3Solver.scala | 32 ++++++++++++-------
.../scala/leon/purescala/PrettyPrinter.scala | 5 +++
src/main/scala/leon/purescala/Trees.scala | 2 ++
testcases/regression/valid/Array3.scala | 12 ++++---
6 files changed, 39 insertions(+), 24 deletions(-)
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 95e8719b1..dd1fee89e 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -25,7 +25,7 @@ object ArrayTransformation extends Pass {
case fill@ArrayFill(length, default) => {
var rLength = transform(length)
val rDefault = transform(default)
- val rFill = ArrayFill(length, default).setType(fill.getType)
+ val rFill = ArrayMake(rDefault).setType(fill.getType)
Tuple(Seq(rFill, length)).setType(TupleType(Seq(fill.getType, Int32Type)))
}
case sel@ArraySelect(a, i) => {
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index 6f72611ce..47337af61 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -248,11 +248,9 @@ object Evaluator {
case i @ IntLiteral(_) => i
case b @ BooleanLiteral(_) => b
- case f @ ArrayFill(length, default) => {
- val rLength = rec(ctx, length)
+ case f @ ArrayMake(default) => {
val rDefault = rec(ctx, default)
- assert(rLength.isInstanceOf[IntLiteral])
- ArrayFill(rLength, rDefault)
+ ArrayMake(rDefault)
}
case ArrayUpdated(a, i, v) => {
val ra = rec(ctx, a)
@@ -266,7 +264,7 @@ object Evaluator {
var ra = rec(ctx, a)
var found = false
var result: Option[Expr] = None
- while(!ra.isInstanceOf[ArrayFill] && !found) {
+ while(!ra.isInstanceOf[ArrayMake] && !found) {
val ArrayUpdated(ra2, IntLiteral(i), v) = ra
if(index == i) {
result = Some(v)
@@ -277,7 +275,7 @@ object Evaluator {
}
result match {
case Some(r) => r
- case None => ra.asInstanceOf[ArrayFill].defaultValue
+ case None => ra.asInstanceOf[ArrayMake].defaultValue
}
}
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 7a21e9ab2..3ab173b7d 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -525,14 +525,11 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
reporter.info(" - Initial unrolling...")
val (clauses, guards) = unrollingBank.initialUnrolling(expandedVC)
- //for(clause <- clauses) {
- //println("we're getting a new clause " + clause)
- // z3.assertCnstr(toZ3Formula(z3, clause).get)
- //}
+ for(clause <- clauses) {
+ Logger.debug("we're getting a new clause " + clause, 4, "z3solver")
+ }
- //println("The blocking guards: " + guards)
val cc = toZ3Formula(z3, And(clauses)).get
- // println("CC : " + cc)
z3.assertCnstr(cc)
// these are the optional sequence of assumption literals
@@ -573,6 +570,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
(a, m, Seq.empty[Z3AST])
}
reporter.info(" - Finished search with blocked literals")
+ Logger.debug("The blocking guards are: " + blockingSet.mkString(", "), 4, "z3solver")
// if (Settings.useCores)
// reporter.info(" - Core is : " + core)
@@ -747,16 +745,13 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
reporter.info(" - more unrollings")
for((id,polarity) <- toReleaseAsPairs) {
val (newClauses,newBlockers) = unrollingBank.unlock(id, !polarity)
- //println("Unlocked : " + (id, !polarity))
for(clause <- newClauses) {
- //println("we're getting a new clause " + clause)
- // z3.assertCnstr(toZ3Formula(z3, clause).get)
+ Logger.debug("we're getting a new clause " + clause, 4, "z3solver")
}
for(ncl <- newClauses) {
z3.assertCnstr(toZ3Formula(z3, ncl).get)
}
- //z3.assertCnstr(toZ3Formula(z3, And(newClauses)).get)
blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
}
reporter.info(" - finished unrolling")
@@ -1055,8 +1050,8 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
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 ArrayType(base) = fill.getType
+ case a@ArrayMake(default) => {
+ val ArrayType(base) = a.getType
z3.mkConstArray(typeToSort(base), rec(default))
}
case ArraySelect(ar, index) => {
@@ -1122,6 +1117,19 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
(if (elems.isEmpty) EmptySet(dt) else FiniteSet(elems.toSeq)).setType(expType.get)
}
}
+ case Some(ArrayType(dt)) =>
+ model.getArrayValue(t) match {
+ case None => throw new CantTranslateException(t)
+ case Some((map, elseValue)) =>
+ map.foldLeft(ArrayMake(rec(elseValue, Some(dt))): Expr) {
+ case (acc, (key, value)) => ArrayUpdated(acc, rec(key, Some(Int32Type)), rec(value, Some(dt)))
+ }
+ }
+ case Some(TupleType(tpes)) => {
+ val Z3AppAST(decl, args) = z3.getASTKind(t)
+ val rargs = args.zip(tpes).map(p => rec(p._1, Some(p._2)))
+ Tuple(rargs)
+ }
case other =>
z3.getASTKind(t) match {
case Z3AppAST(decl, args) => {
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 848c1dad3..b0b0bba08 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -260,6 +260,11 @@ object PrettyPrinter {
pp(v, sb, lvl)
sb.append(")#" + fill.getType)
}
+ case am@ArrayMake(v) => {
+ sb.append("Array.make(")
+ pp(v, sb, lvl)
+ sb.append(")")
+ }
case sel@ArraySelect(ar, i) => {
pp(ar, sb, lvl)
sb.append("(")
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index b308dbf53..030845358 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -381,6 +381,7 @@ object Trees {
/* Array operations */
case class ArrayFill(length: Expr, defaultValue: Expr) extends Expr
+ case class ArrayMake(defaultValue: Expr) extends Expr
case class ArraySelect(array: Expr, index: Expr) extends Expr
//the difference between ArrayUpdate and ArrayUpdated is that the former has a side effect while the latter is the function variant
//ArrayUpdate should be eliminated soon in the analysis while ArrayUpdated is keep all the way to the backend
@@ -423,6 +424,7 @@ object Trees {
case Assignment(id, e) => Some((e, Assignment(id, _)))
case TupleSelect(t, i) => Some((t, TupleSelect(_, i)))
case ArrayLength(a) => Some((a, ArrayLength))
+ case ArrayMake(t) => Some((t, ArrayMake))
case e@Epsilon(t) => Some((t, (expr: Expr) => Epsilon(expr).setType(e.getType).setPosInfo(e)))
case _ => None
}
diff --git a/testcases/regression/valid/Array3.scala b/testcases/regression/valid/Array3.scala
index d51894c36..bbb1845b8 100644
--- a/testcases/regression/valid/Array3.scala
+++ b/testcases/regression/valid/Array3.scala
@@ -1,14 +1,16 @@
-object Array1 {
+import leon.Utils._
+
+object Array3 {
def foo(): Int = {
- val a = Array.fill(5)(0)
+ val a = Array.fill(5)(3)
var i = 0
var sum = 0
- while(i < a.length) {
+ (while(i < a.length) {
sum = sum + a(i)
i = i + 1
- }
+ }) invariant(i >= 0)
sum
- } ensuring(_ == 0)
+ } ensuring(_ == 15)
}
--
GitLab