From 6a949b5f0ec6387230f5518a0b7d73622ce6f1a6 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 18 May 2016 17:01:09 +0200
Subject: [PATCH] NativeZ3 handles bags natively
---
.../purescala/DefinitionTransformer.scala | 2 -
.../leon/solvers/smtlib/SMTLIBZ3Target.scala | 3 ++
.../leon/solvers/z3/AbstractZ3Solver.scala | 42 ++++++++++++++++++-
.../leon/solvers/z3/Z3UnrollingSolver.scala | 3 +-
4 files changed, 45 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/purescala/DefinitionTransformer.scala b/src/main/scala/leon/purescala/DefinitionTransformer.scala
index 6dfea1dbe..b71e5d819 100644
--- a/src/main/scala/leon/purescala/DefinitionTransformer.scala
+++ b/src/main/scala/leon/purescala/DefinitionTransformer.scala
@@ -27,10 +27,8 @@ class DefinitionTransformer(
super.transform(transformType(tpe).getOrElse(tpe))
}
-
final override def transform(id: Identifier): Identifier = transformId(id, false)
-
def transformExpr(e: Expr)(implicit bindings: Map[Identifier, Identifier]): Option[Expr] = None
final override def transform(e: Expr)(implicit bindings: Map[Identifier, Identifier]): Expr = {
transformExpr(e) match {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 52894a29c..eb55f9b60 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -154,6 +154,9 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
ArrayMap(plus, toSMT(b1), toSMT(b2))
case BagIntersection(b1, b2) =>
+ toSMT(BagDifference(b1, BagDifference(b1, b2)))
+
+ case BagDifference(b1, b2) =>
val abs = SortedSymbol("abs", List(IntegerType).map(declareSort), declareSort(IntegerType))
val plus = SortedSymbol("+", List(IntegerType, IntegerType).map(declareSort), declareSort(IntegerType))
val minus = SortedSymbol("-", List(IntegerType, IntegerType).map(declareSort), declareSort(IntegerType))
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 0eff41ea6..644b91dd1 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -223,6 +223,9 @@ trait AbstractZ3Solver extends Z3Solver {
case tt @ MapType(fromType, toType) =>
typeToSort(RawArrayType(fromType, library.optionType(toType)))
+ case tt @ BagType(base) =>
+ typeToSort(RawArrayType(base, IntegerType))
+
case rat @ RawArrayType(from, to) =>
sorts.cached(rat) {
val fromSort = typeToSort(from)
@@ -473,6 +476,35 @@ trait AbstractZ3Solver extends Z3Solver {
case SetDifference(s1, s2) => z3.mkSetDifference(rec(s1), rec(s2))
case f @ FiniteSet(elems, base) => elems.foldLeft(z3.mkEmptySet(typeToSort(base)))((ast, el) => z3.mkSetAdd(ast, rec(el)))
+ case fb @ FiniteBag(elems, base) =>
+ typeToSort(fb.getType)
+ toSMT(RawArrayValue(base, elems, InfiniteIntegerLiteral(0)))
+
+ case BagAdd(b, e) =>
+ val bag = rec(b)
+ val elem = rec(e)
+ z3.mkStore(bag, elem, z3.mkAdd(z3.mkSelect(bag, elem), rec(InfiniteIntegerLiteral(1))))
+
+ case MultiplicityInBag(e, b) =>
+ z3.mkSelect(rec(b), rec(e))
+
+ case BagUnion(b1, b2) =>
+ val plus = z3.getFuncDecl(OpAdd, typeToSort(IntegerType), typeToSort(IntegerType))
+ z3.mkArrayMap(plus, rec(b1), rec(b2))
+
+ case BagIntersection(b1, b2) =>
+ rec(BagDifference(b1, BagDifference(b1, b2)))
+
+ case BagDifference(b1, b2) =>
+ val abs = z3.getFuncDecl(OpAbs, typeToSort(IntegerType))
+ val plus = z3.getFuncDecl(OpAdd, typeToSort(IntegerType), typeToSort(IntegerType))
+ val minus = z3.getFuncDecl(OpSub, typeToSort(IntegerType), typeToSort(IntegerType))
+ val div = z3.getFuncDecl(OpDiv, typeToSort(IntegerType), typeToSort(IntegerType))
+
+ val all2 = z3.mkArrayConst(typeToSort(IntegerType), z3.mkInt(2))
+ val withNeg = z3.mkArrayMap(minus, rec(b1), rec(b2))
+ z3.mkArrayMap(div, z3.mkArrayMap(plus, withNeg, z3.mkArrayMap(abs, withNeg)), all2)
+
case RawArrayValue(keyTpe, elems, default) =>
val ar = z3.mkConstArray(typeToSort(keyTpe), rec(default))
@@ -670,7 +702,7 @@ trait AbstractZ3Solver extends Z3Solver {
// We expect a RawArrayValue with keys in from and values in Option[to],
// with default value == None
if (r.default.getType != library.noneType(to)) {
- unsupported(r, "Solver returned a co-finite set which is not supported.")
+ unsupported(r, "Solver returned a co-finite map which is not supported.")
}
require(r.keyTpe == from, s"Type error in solver model, expected ${from.asString}, found ${r.keyTpe.asString}")
@@ -682,6 +714,14 @@ trait AbstractZ3Solver extends Z3Solver {
FiniteMap(elems, from, to)
}
+ case BagType(base) =>
+ val r @ RawArrayValue(_, elems, default) = rec(t, RawArrayType(base, IntegerType))
+ if (default != InfiniteIntegerLiteral(0)) {
+ unsupported(r, "Solver returned a co-finite bag which is not supported.")
+ }
+
+ FiniteBag(elems, base)
+
case tpe @ SetType(dt) =>
model.getSetValue(t) match {
case None => unsound(t, "invalid set AST")
diff --git a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
index ce224e8dc..c367f8f3c 100644
--- a/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
@@ -11,6 +11,5 @@ import theories._
class Z3UnrollingSolver(context: SolverContext, program: Program, underlying: Z3Solver)
extends UnrollingSolver(context, program, underlying,
- new StringEncoder(context.context, program) >>
- new BagEncoder(context.context, program))
+ new StringEncoder(context.context, program)
with Z3Solver
--
GitLab