From 176b5e7a4c97ddf3f455710a9bb0247971b03c8f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 3 May 2012 16:17:24 +0200
Subject: [PATCH] convert array to pair of array and length
---
src/main/scala/leon/ArrayTransformation.scala | 6 ++---
src/main/scala/leon/FairZ3Solver.scala | 22 +++++++++++++++++++
.../leon/ImperativeCodeElimination.scala | 2 --
3 files changed, 25 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 5f72d96a6..9c5bf63c0 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -48,9 +48,9 @@ object ArrayTransformation extends Pass {
//val Tuple(Seq(Variable(id), length)) = ar
IfExpr(
And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
- Assignment(id, Tuple(Seq(ArrayUpdated(array, i, v), length)).setType(TupleType(Seq(array.getType, Int32Type)))),
- Error("Array out of bound access").setType(UnitType)
- ).setType(UnitType)
+ Block(Seq(Assignment(id, Tuple(Seq(ArrayUpdated(array, i, v), length)).setType(TupleType(Seq(array.getType, Int32Type))))), IntLiteral(0)),
+ Error("Array out of bound access").setType(Int32Type)
+ ).setType(Int32Type)
}
case Let(i, v, b) => {
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 919b5b4f9..7a21e9ab2 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -59,6 +59,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
fallbackSorts = Map.empty
mapSorts = Map.empty
+ arraySorts = Map.empty
funSorts = Map.empty
funDomainConstructors = Map.empty
funDomainSelectors = Map.empty
@@ -97,6 +98,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
private var boolSort: Z3Sort = null
private var setSorts: Map[TypeTree, Z3Sort] = Map.empty
private var mapSorts: Map[TypeTree, Z3Sort] = Map.empty
+ private var arraySorts: Map[TypeTree, Z3Sort] = Map.empty
protected[leon] var funSorts: Map[TypeTree, Z3Sort] = Map.empty
protected[leon] var funDomainConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
@@ -386,6 +388,16 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
ms
}
}
+ case at @ ArrayType(base) => arraySorts.get(at) match {
+ case Some(s) => s
+ case None => {
+ val fromSort = typeToSort(Int32Type)
+ val toSort = typeToSort(base)
+ val as = z3.mkArraySort(fromSort, toSort)
+ arraySorts += (at -> as)
+ as
+ }
+ }
case ft @ FunctionType(fts, tt) => funSorts.get(ft) match {
case Some(s) => s
case None => {
@@ -1043,6 +1055,16 @@ 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
+ z3.mkConstArray(typeToSort(base), rec(default))
+ }
+ case ArraySelect(ar, index) => {
+ z3.mkSelect(rec(ar), rec(index))
+ }
+ case ArrayUpdated(ar, index, newVal) => {
+ z3.mkStore(rec(ar), rec(index), rec(newVal))
+ }
case AnonymousFunctionInvocation(id, args) => id.getType match {
case ft @ FunctionType(fts, tt) => {
val consFD = funDomainConstructors(ft)
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index eb139f824..131418c69 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -15,11 +15,9 @@ object ImperativeCodeElimination extends Pass {
def apply(pgm: Program): Program = {
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => fd.body.map(body => {
- Logger.debug("Transforming to functional code the following function:\n" + fd, 5, "imperative")
parent = fd
val (res, scope, _) = toFunction(body)
fd.body = Some(scope(res))
- Logger.debug("Resulting functional code is:\n" + fd, 5, "imperative")
}))
pgm
}
--
GitLab