From 30f322e621441ca22dcd9d03dd5d1efc2a97a4ab Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 11 May 2015 16:05:51 +0200
Subject: [PATCH] Encode/Decode chars properly in SMT solvers
---
.../scala/leon/solvers/smtlib/SMTLIBSolver.scala | 6 ++++--
.../scala/leon/solvers/smtlib/SMTLIBZ3Target.scala | 14 ++++++++++----
.../scala/leon/solvers/z3/AbstractZ3Solver.scala | 2 ++
3 files changed, 16 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 5106a6049..77bbb3441 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -217,7 +217,10 @@ abstract class SMTLIBSolver(val context: LeonContext,
protected def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match {
case SetType(base) =>
- require(r.default == BooleanLiteral(false), "Co-finite sets are not supported.")
+ if (r.default != BooleanLiteral(false)) {
+ reporter.warning("Co-finite sets are not supported.")
+ throw new IllegalArgumentException
+ }
require(r.keyTpe == base, s"Type error in solver model, expected $base, found ${r.keyTpe}")
finiteSet(r.elems.keySet, base)
@@ -499,7 +502,6 @@ abstract class SMTLIBSolver(val context: LeonContext,
case IntLiteral(i) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(i))
case CharLiteral(c) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(c.toInt))
case BooleanLiteral(v) => Core.BoolConst(v)
- case StringLiteral(s) => SString(s)
case Let(b,d,e) =>
val id = id2sym(b)
val value = toSMT(d)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 5e5926f49..d7565c8d5 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -10,6 +10,7 @@ import Definitions.Program
import Expressions._
import Extractors._
import Types._
+import Constructors._
import ExprOps.simplestValue
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
@@ -76,7 +77,7 @@ class SMTLIBZ3Target(context: LeonContext, program: Program) extends SMTLIBSolve
case (QualifiedIdentifier(ExtendedIdentifier(SSymbol("as-array"), k: SSymbol), _), tpe) =>
if (letDefs contains k) {
// Need to recover value form function model
- fromRawArray(extractRawArray(letDefs(k)), tpe)
+ fromRawArray(extractRawArray(letDefs(k), tpe), tpe)
} else {
unsupported(" as-array on non-function or unknown symbol "+k)
}
@@ -151,10 +152,15 @@ class SMTLIBZ3Target(context: LeonContext, program: Program) extends SMTLIBSolve
super.toSMT(e)
}
- def extractRawArray(s: DefineFun)(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): RawArrayValue = s match {
+ def extractRawArray(s: DefineFun, tpe: TypeTree)(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): RawArrayValue = s match {
case DefineFun(SMTFunDef(a, Seq(SortedVar(arg, akind)), rkind, body)) =>
- val argTpe = sorts.toA(akind)
- val retTpe = sorts.toA(rkind)
+ val (argTpe, retTpe) = tpe match {
+ case SetType(base) => (base, BooleanType)
+ case ArrayType(base) => (Int32Type, base)
+ case FunctionType(args, ret) => (tupleTypeWrap(args), ret)
+ case RawArrayType(from, to) => (from, to)
+ case _ => unsupported("Unsupported type for (un)packing into raw arrays: "+tpe +" (got kinds "+akind+" -> "+rkind+")")
+ }
def extractCases(e: Term): (Map[Expr, Expr], Expr) = e match {
case ITE(SMTEquals(SimpleSymbol(`arg`), k), v, e) =>
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index f2303d699..c2aea200c 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -413,6 +413,7 @@ trait AbstractZ3Solver
declareADTSort(act)
}
+
case cct: CaseClassType =>
sorts.toZ3OrCompute(cct) {
declareADTSort(cct)
@@ -560,6 +561,7 @@ trait AbstractZ3Solver
case Not(e) => z3.mkNot(rec(e))
case IntLiteral(v) => z3.mkInt(v, typeToSort(Int32Type))
case InfiniteIntegerLiteral(v) => z3.mkNumeral(v.toString, typeToSort(IntegerType))
+ case CharLiteral(c) => z3.mkInt(c, typeToSort(Int32Type))
case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
case UnitLiteral() => unitValue
case Equals(l, r) => z3.mkEq(rec( l ), rec( r ) )
--
GitLab