From fa07882851e7a3a59eb428ae724a3b5be542ff54 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Tue, 21 May 2013 23:43:06 +0200
Subject: [PATCH] Implement solver support for FiniteArray
---
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 0b29dd89c..1a94e295f 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -522,6 +522,14 @@ trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
val res = getLength(ar)
res
}
+
+ case arr @ FiniteArray(exprs) => {
+ val ArrayType(innerType) = arr.getType
+ val arrayType = arr.getType
+ val a: Expr = ArrayFill(IntLiteral(exprs.length), simplestValue(innerType)).setType(arrayType)
+ val u = exprs.zipWithIndex.foldLeft(a)((array, expI) => ArrayUpdated(array, IntLiteral(expI._2), expI._1).setType(arrayType))
+ rec(u)
+ }
case Distinct(exs) => z3.mkDistinct(exs.map(rec(_)): _*)
case _ => {
--
GitLab