From 3e99e54d4057b3ce116c914de0e6baec19426dc5 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 6 Jun 2016 18:44:01 +0200
Subject: [PATCH] array encoded with raw array operations
---
src/main/scala/leon/solvers/RawArray.scala | 36 +++++++++++++
.../leon/solvers/smtlib/SMTLIBTarget.scala | 6 +++
.../leon/solvers/theories/ArrayEncoder.scala | 50 +++++++++----------
.../leon/solvers/z3/AbstractZ3Solver.scala | 5 ++
.../purescala/valid/ADTWithArray1.scala | 14 ++++++
.../purescala/valid/ADTWithArray2.scala | 14 ++++++
6 files changed, 98 insertions(+), 27 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/valid/ADTWithArray1.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/ADTWithArray2.scala
diff --git a/src/main/scala/leon/solvers/RawArray.scala b/src/main/scala/leon/solvers/RawArray.scala
index 59b11894d..cfad13b80 100644
--- a/src/main/scala/leon/solvers/RawArray.scala
+++ b/src/main/scala/leon/solvers/RawArray.scala
@@ -6,6 +6,8 @@ package solvers
import purescala.Types._
import purescala.Expressions._
import purescala.Extractors._
+import purescala.{PrettyPrintable, PrinterContext}
+import purescala.PrinterHelpers._
// Corresponds to a complete map (SMT Array), not a Leon/Scala array
// Only used within solvers or SMT for encoding purposes
@@ -29,3 +31,37 @@ case class RawArrayValue(keyTpe: TypeTree, elems: Map[Expr, Expr], default: Expr
s"RawArray[${keyTpe.asString}]($elemsString, default = ${default.asString})"
}
}
+
+case class RawArraySelect(array: Expr, index: Expr) extends Expr with Extractable with PrettyPrintable {
+
+ override def extract: Option[(Seq[Expr], (Seq[Expr]) => Expr)] =
+ Some((Seq(array, index), es => RawArraySelect(es(0), es(1))))
+
+ val getType = array.getType.asInstanceOf[RawArrayType].to
+
+ override def asString(implicit ctx: LeonContext) = {
+ s"$array($index)"
+ }
+
+ override def printWith(implicit pctx: PrinterContext) = {
+ p"$array($index)"
+ }
+
+}
+
+case class RawArrayUpdated(array: Expr, index: Expr, newValue: Expr) extends Expr with Extractable with PrettyPrintable {
+
+ val getType = array.getType
+
+ override def extract: Option[(Seq[Expr], (Seq[Expr]) => Expr)] =
+ Some((Seq(array, index, newValue), es => RawArrayUpdated(es(0), es(1), es(2))))
+
+ override def asString(implicit ctx: LeonContext) = {
+ s"$array($index) = $newValue"
+ }
+
+ override def printWith(implicit pctx: PrinterContext) = {
+ p"$array($index) = $newValue"
+ }
+
+}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 77ed0a9c8..bb576468c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -438,6 +438,11 @@ trait SMTLIBTarget extends Interruptible {
FunctionApplication(selector, Seq(toSMT(a)))
+ case al @ RawArraySelect(a, i) =>
+ ArraysEx.Select(toSMT(a), toSMT(i))
+ case al @ RawArrayUpdated(a, i, e) =>
+ ArraysEx.Store(toSMT(a), toSMT(i), toSMT(e))
+
case al @ ArraySelect(a, i) =>
val tpe = normalizeType(a.getType)
@@ -445,6 +450,7 @@ trait SMTLIBTarget extends Interruptible {
ArraysEx.Select(scontent, toSMT(i))
+
case al @ ArrayUpdated(a, i, e) =>
val tpe = normalizeType(a.getType)
diff --git a/src/main/scala/leon/solvers/theories/ArrayEncoder.scala b/src/main/scala/leon/solvers/theories/ArrayEncoder.scala
index fd12709f6..a1bf0e4c3 100644
--- a/src/main/scala/leon/solvers/theories/ArrayEncoder.scala
+++ b/src/main/scala/leon/solvers/theories/ArrayEncoder.scala
@@ -6,8 +6,11 @@ package theories
import purescala.Common._
import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Extractors._
import purescala.Constructors._
import purescala.Types._
+import purescala.Types._
import purescala.Definitions._
import leon.utils.Bijection
import leon.purescala.TypeOps
@@ -15,7 +18,7 @@ import leon.purescala.TypeOps
class ArrayEncoder(ctx: LeonContext, p: Program) extends TheoryEncoder {
private val arrayTypeParam = TypeParameter.fresh("A")
- val ArrayCaseClass = new CaseClassDef(FreshIdentifier("Array"), Seq(TypeParameterDef(arrayTypeParam)), None, false)
+ val ArrayCaseClass = new CaseClassDef(FreshIdentifier("InternalArray"), Seq(TypeParameterDef(arrayTypeParam)), None, false)
val rawArrayField = FreshIdentifier("raw", RawArrayType(Int32Type, arrayTypeParam))
val lengthField = FreshIdentifier("length", Int32Type)
ArrayCaseClass.setFields(Seq(ValDef(rawArrayField), ValDef(lengthField)))
@@ -60,36 +63,32 @@ class ArrayEncoder(ctx: LeonContext, p: Program) extends TheoryEncoder {
val ra = transform(a)
Some(CaseClassSelector(ra.getType.asInstanceOf[CaseClassType], ra, lengthField))
- //case al @ ArraySelect(a, i) =>
- // val tpe = normalizeType(a.getType)
-
- // val scontent = FunctionApplication(selectors.toB((tpe, 1)), Seq(toSMT(a)))
-
- // ArraysEx.Select(scontent, toSMT(i))
-
- //case al @ ArrayUpdated(a, i, e) =>
- // val tpe = normalizeType(a.getType)
+ case al @ ArraySelect(a, i) =>
+ val ra = transform(a)
+ val ri = transform(i)
+ val raw = CaseClassSelector(ra.getType.asInstanceOf[CaseClassType], ra, rawArrayField)
+ Some(RawArraySelect(raw, ri))
- // val sa = toSMT(a)
- // val ssize = FunctionApplication(selectors.toB((tpe, 0)), Seq(sa))
- // val scontent = FunctionApplication(selectors.toB((tpe, 1)), Seq(sa))
+ case al @ ArrayUpdated(a, i, e) =>
+ val ra = transform(a)
+ val ri = transform(i)
+ val re = transform(e)
- // val newcontent = ArraysEx.Store(scontent, toSMT(i), toSMT(e))
+ val length = CaseClassSelector(ra.getType.asInstanceOf[CaseClassType], ra, lengthField)
+ val raw = CaseClassSelector(ra.getType.asInstanceOf[CaseClassType], ra, rawArrayField)
- // val constructor = constructors.toB(tpe)
- // FunctionApplication(constructor, Seq(ssize, newcontent))
+ Some(CaseClass(ra.getType.asInstanceOf[CaseClassType], Seq(RawArrayUpdated(raw, ri, re), length)))
- //case a @ FiniteArray(elems, oDef, size) =>
- // val tpe @ ArrayType(to) = normalizeType(a.getType)
- // declareSort(tpe)
+ case a @ FiniteArray(elems, oDef, size) =>
- // val default: Expr = oDef.getOrElse(simplestValue(to))
+ val tpe @ ArrayType(to) = a.getType
+ val default: Expr = transform(oDef.getOrElse(simplestValue(to)))
- // val arr = toSMT(RawArrayValue(Int32Type, elems.map {
- // case (k, v) => IntLiteral(k) -> v
- // }, default))
+ val raw = RawArrayValue(Int32Type, elems.map {
+ case (k, v) => IntLiteral(k) -> transform(v)
+ }, default)
+ Some(CaseClass(ArrayCaseClass.typed(Seq(to)), Seq(raw, transform(size))))
- // FunctionApplication(constructors.toB(tpe), List(toSMT(size), arr))
case _ => None
}
@@ -123,11 +122,8 @@ class ArrayEncoder(ctx: LeonContext, p: Program) extends TheoryEncoder {
override def transformExpr(e: Expr)(implicit binders: Map[Identifier, Identifier]): Option[Expr] = e match {
case cc @ CaseClass(cct, args) if cct.classDef == ArrayCaseClass =>
- println("Hey there!")
val Seq(rawArray, length) = args
- println(args)
val leonArray = fromRaw(rawArray, length)
- println(leonArray)
Some(leonArray)
// Some(StringLiteral(convertToString(cc)).copiedFrom(cc))
//case FunctionInvocation(SizeI, Seq(a)) =>
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 99567a865..15b654e7f 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -417,6 +417,11 @@ trait AbstractZ3Solver extends Z3Solver {
val tester = testers.toB(cct)
tester(rec(e))
+ case al @ RawArraySelect(a, i) =>
+ z3.mkSelect(rec(a), rec(i))
+ case al @ RawArrayUpdated(a, i, e) =>
+ z3.mkStore(rec(a), rec(i), rec(e))
+
case al @ ArraySelect(a, i) =>
val tpe = normalizeType(a.getType)
diff --git a/src/test/resources/regression/verification/purescala/valid/ADTWithArray1.scala b/src/test/resources/regression/verification/purescala/valid/ADTWithArray1.scala
new file mode 100644
index 000000000..62eeb2b10
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/ADTWithArray1.scala
@@ -0,0 +1,14 @@
+import leon.collection._
+
+object ADTWithArray1 {
+
+ case class A1(x: Int)
+
+ case class B(t: Array[A1])
+
+ def test(b: B): A1 = {
+ require(b.t.length > 0 && b.t(0).x > 0)
+ b.t(0)
+ } ensuring(a => a.x >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/ADTWithArray2.scala b/src/test/resources/regression/verification/purescala/valid/ADTWithArray2.scala
new file mode 100644
index 000000000..89a89a3f9
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/ADTWithArray2.scala
@@ -0,0 +1,14 @@
+import leon.collection._
+
+object ADTWithArray2 {
+
+ case class A1(x: Int)
+
+ case class B(t: Array[A1])
+
+ def test(b: B): Int = {
+ require(b.t.length > 2)
+ b.t.length
+ } ensuring(a => a > 0)
+
+}
--
GitLab