diff --git a/library/lang/string/String.scala b/library/lang/string/String.scala
deleted file mode 100644
index 0a3e72bd1a6f234a79eba234a646b2c0844ecfaf..0000000000000000000000000000000000000000
--- a/library/lang/string/String.scala
+++ /dev/null
@@ -1,28 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.lang.string
-
-import leon.annotation._
-import leon.collection._
-
-@library
-case class String(chars: List[Char]) {
- def +(that: String): String = {
- String(this.chars ++ that.chars)
- }
-
- def size = chars.size
-
- def length = size
-
- @ignore
- override def toString = {
-
- "\""+charsToString(chars)+"\""
- }
- @ignore
- def charsToString(chars: List[Char]): java.lang.String = chars match {
- case Cons(h, t) => h + charsToString(t)
- case Nil() => ""
- }
-}
diff --git a/library/lang/string/package.scala b/library/lang/string/package.scala
deleted file mode 100644
index d931debe7c587f966aadd30b2860b1793c6ad431..0000000000000000000000000000000000000000
--- a/library/lang/string/package.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.lang
-
-import leon.annotation._
-import leon.collection._
-import scala.language.implicitConversions
-
-import scala.collection.immutable.{List => ScalaList}
-
-package object string {
- /*@ignore
- implicit def strToStr(s: java.lang.String): leon.lang.string.String = {
- String(listToList(s.toList))
- }*/
-
- @ignore
- def listToList[A](s: ScalaList[A]): List[A] = s match {
- case scala.::(h, t) =>
- Cons(h, listToList(t))
- case _ =>
- Nil[A]()
- }
-}
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 93c8c6d021233a6c5968d7de9a78b7c3d135ced1..26f976c095489f22cbc97dd9ee810d1d71ef9f99 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -177,6 +177,9 @@ class CompilationUnit(val ctx: LeonContext,
case FractionalLiteral(n, d) =>
new runtime.Rational(n.toString, d.toString)
+
+ case StringLiteral(v) =>
+ new java.lang.String(v)
case GenericValue(tp, id) =>
e
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 8b4846a3394c3c3ddd2326d24d23ce95e68f6b05..b82dc6a0f256fec3c3cf733addad76f899456f4a 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -58,6 +58,8 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
def stringConstructor(s: String) = strings(s)
+ lazy val stubValues = ints.values ++ bigInts.values ++ booleans.values ++ chars.values ++ rationals.values ++ strings.values
+
def cPattern(c: Constructor[Expr, TypeTree], args: Seq[VPattern[Expr, TypeTree]]) = {
ConstructorPattern[Expr, TypeTree](c, args)
}
@@ -307,7 +309,6 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
None
})
- val stubValues = ints.values ++ bigInts.values ++ booleans.values ++ chars.values ++ rationals.values
val gen = new StubGenerator[Expr, TypeTree](stubValues.toSeq,
Some(getConstructors _),
treatEmptyStubsAsChildless = true)
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index d9fd1d1d6696991909ffd5cd9b1f2e95590db7a4..4b89493e10d94d16fe355f9e63bc2e9f44f3714d 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -84,6 +84,10 @@ object Definitions {
def lookupAll(name: String) = DefOps.searchWithin(name, this)
def lookup(name: String) = lookupAll(name).headOption
+
+ def lookupCaseClass(name: String) = lookupAll(name).collect{ case c: CaseClassDef => c }.headOption
+ def lookupAbstractClass(name: String) = lookupAll(name).collect{ case c: AbstractClassDef => c }.headOption
+ def lookupFunDef(name: String) = lookupAll(name).collect{ case c: FunDef => c }.headOption
}
object Program {
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index ae93221bfe8313cf8cef20ed084d559a2a472133..13e4efbef15d754765776de6153c9f5a8b65c6c8 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -584,7 +584,7 @@ object Expressions {
/** $encodingof `lhs.length` for strings */
case class StringLength(expr: Expr) extends Expr {
val getType = {
- if (expr.getType == StringType) StringType
+ if (expr.getType == StringType) Int32Type
else Untyped
}
}
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index 35e4d1f61b7213bba3121d1fd4926d054075b717..aa4c204d00187ab211a7164a45ae41d8d77d8f8f 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -18,7 +18,6 @@ import purescala.Types._
import purescala.Common._
import purescala.Expressions._
import purescala.Definitions._
-import purescala.SelfPrettyPrinter
import leon.solvers.{ HenkinModel, Model, SolverFactory }
import leon.LeonContext
import leon.evaluators
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index f59087beed61b5cf9ca9c9b1eac46ce3a7cdcbb6..6b2d4272b37b4a06ba2731c5049bcc043b87c927 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -156,6 +156,8 @@ object SolverFactory {
SolverFactory(() => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
} else if(names contains "smt-z3") {
SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+ } else if ((names contains "fairz3") && hasNativeZ3) {
+ SolverFactory(() => new UninterpretedZ3Solver(ctx, program) with TimeoutSolver)
} else {
ctx.reporter.fatalError("No SMT solver available: native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index f1cf73142d51debaeda0fc5064096e522f049955..87cc849b41d2507d7e0ca53a351b2f605d387b46 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -14,6 +14,7 @@ import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, Forall => SMTFor
import _root_.smtlib.parser.Commands._
import _root_.smtlib.interpreters.CVC4Interpreter
import _root_.smtlib.theories.experimental.Sets
+import _root_.smtlib.theories.experimental.Strings
trait SMTLIBCVC4Target extends SMTLIBTarget {
@@ -30,7 +31,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
tpe match {
case SetType(base) =>
Sets.SetSort(declareSort(base))
-
+ case StringType => Strings.StringSort()
case _ =>
super.declareSort(t)
}
@@ -109,6 +110,31 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
case FiniteSet(elems, _) => elems
}).toSet, base)
+ case (SString(v), Some(StringType)) =>
+ StringLiteral(v)
+
+ case (Strings.Length(a), _) =>
+ val aa = fromSMT(a)
+ StringLength(aa)
+
+ case (Strings.Concat(a, b, c @ _*), _) =>
+ val aa = fromSMT(a)
+ val bb = fromSMT(b)
+ (StringConcat(aa, bb) /: c.map(fromSMT(_))) {
+ case (s, cc) => StringConcat(s, cc)
+ }
+
+ case (Strings.Substring(s, start, offset), _) =>
+ val ss = fromSMT(s)
+ val tt = fromSMT(start)
+ val oo = fromSMT(offset)
+ oo match {
+ case Minus(otherEnd, `tt`) => SubString(ss, tt, otherEnd)
+ case _ => SubString(ss, tt, Plus(tt, oo))
+ }
+
+ case (Strings.At(a, b), _) => fromSMT(Strings.Substring(a, b, SNumeral(1)))
+
case _ =>
super.fromSMT(t, otpe)
}
@@ -138,7 +164,14 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
case SetDifference(a, b) => Sets.Setminus(toSMT(a), toSMT(b))
case SetUnion(a, b) => Sets.Union(toSMT(a), toSMT(b))
case SetIntersection(a, b) => Sets.Intersection(toSMT(a), toSMT(b))
-
+ case StringLiteral(v) =>
+ declareSort(StringType)
+ Strings.StringLit(v)
+ case StringLength(a) => Strings.Length(toSMT(a))
+ case StringConcat(a, b) => Strings.Concat(toSMT(a), toSMT(b))
+ case SubString(a, start, Plus(start2, length)) if start == start2 =>
+ Strings.Substring(toSMT(a),toSMT(start),toSMT(length))
+ case SubString(a, start, end) => Strings.Substring(toSMT(a),toSMT(start),toSMT(Minus(end, start)))
case _ =>
super.toSMT(e)
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index b97297fb000f12b11972c675535d35a522587703..47017bcf1471770f1b1e9fb574a81bed34f4c515 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -241,7 +241,6 @@ trait SMTLIBTarget extends Interruptible {
case RealType => Reals.RealSort()
case Int32Type => FixedSizeBitVectors.BitVectorSort(32)
case CharType => FixedSizeBitVectors.BitVectorSort(32)
- case StringType => Strings.StringSort()
case RawArrayType(from, to) =>
Sort(SMTIdentifier(SSymbol("Array")), Seq(declareSort(from), declareSort(to)))
@@ -379,9 +378,6 @@ trait SMTLIBTarget extends Interruptible {
case FractionalLiteral(n, d) => Reals.Div(Reals.NumeralLit(n), Reals.NumeralLit(d))
case CharLiteral(c) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(c.toInt))
case BooleanLiteral(v) => Core.BoolConst(v)
- case StringLiteral(v) =>
- declareSort(StringType)
- Strings.StringLit(v)
case Let(b, d, e) =>
val id = id2sym(b)
val value = toSMT(d)
@@ -613,12 +609,6 @@ trait SMTLIBTarget extends Interruptible {
case RealMinus(a, b) => Reals.Sub(toSMT(a), toSMT(b))
case RealTimes(a, b) => Reals.Mul(toSMT(a), toSMT(b))
case RealDivision(a, b) => Reals.Div(toSMT(a), toSMT(b))
-
- case StringLength(a) => Strings.Length(toSMT(a))
- case StringConcat(a, b) => Strings.Concat(toSMT(a), toSMT(b))
- case SubString(a, start, Plus(start2, length)) if start == start2 =>
- Strings.Substring(toSMT(a),toSMT(start),toSMT(length))
- case SubString(a, start, end) => Strings.Substring(toSMT(a),toSMT(start),toSMT(Minus(end, start)))
case And(sub) => Core.And(sub.map(toSMT): _*)
case Or(sub) => Core.Or(sub.map(toSMT): _*)
@@ -764,31 +754,6 @@ trait SMTLIBTarget extends Interruptible {
case (SNumeral(n), Some(RealType)) =>
FractionalLiteral(n, 1)
- case (SString(v), Some(StringType)) =>
- StringLiteral(v)
-
- case (Strings.Length(a), _) =>
- val aa = fromSMT(a)
- StringLength(aa)
-
- case (Strings.Concat(a, b, c @ _*), _) =>
- val aa = fromSMT(a)
- val bb = fromSMT(b)
- (StringConcat(aa, bb) /: c.map(fromSMT(_))) {
- case (s, cc) => StringConcat(s, cc)
- }
-
- case (Strings.Substring(s, start, offset), _) =>
- val ss = fromSMT(s)
- val tt = fromSMT(start)
- val oo = fromSMT(offset)
- oo match {
- case Minus(otherEnd, `tt`) => SubString(ss, tt, otherEnd)
- case _ => SubString(ss, tt, Plus(tt, oo))
- }
-
- case (Strings.At(a, b), _) => fromSMT(Strings.Substring(a, b, SNumeral(1)))
-
case (FunctionApplication(SimpleSymbol(SSymbol("ite")), Seq(cond, thenn, elze)), t) =>
IfExpr(
fromSMT(cond, Some(BooleanType)),
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index 86cf40f474e62859acfd1fe2c0953e588590d6df..32adcd50f32da267a2663128a3c05759a87be948 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -15,6 +15,8 @@ import _root_.smtlib.theories.Core.{Equals => _, _}
class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolver(context, program) with SMTLIBZ3Target {
+ def getProgram: Program = program
+
// EK: We use get-model instead in order to extract models for arrays
override def getModel: Model = {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 3d4a06a838a5057a693d85754bb5113e1ce7d0ae..1731b94ae5f4f91b87248deddc50db5339915552 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -8,15 +8,15 @@ import purescala.Common._
import purescala.Expressions._
import purescala.Constructors._
import purescala.Types._
-
+import purescala.Definitions._
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
import _root_.smtlib.interpreters.Z3Interpreter
import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
import _root_.smtlib.theories.ArraysEx
+import leon.solvers.z3.Z3StringConversion
-trait SMTLIBZ3Target extends SMTLIBTarget {
-
+trait SMTLIBZ3Target extends SMTLIBTarget with Z3StringConversion[Term] {
def targetName = "z3"
def interpreterOps(ctx: LeonContext) = {
@@ -40,11 +40,11 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
override protected def declareSort(t: TypeTree): Sort = {
val tpe = normalizeType(t)
sorts.cachedB(tpe) {
- tpe match {
+ convertType(tpe) match {
case SetType(base) =>
super.declareSort(BooleanType)
declareSetSort(base)
- case _ =>
+ case t =>
super.declareSort(t)
}
}
@@ -69,9 +69,13 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
Sort(SMTIdentifier(setSort.get), Seq(declareSort(of)))
}
- override protected def fromSMT(t: Term, otpe: Option[TypeTree] = None)
+ override protected def fromSMT(t: Term, expected_otpe: Option[TypeTree] = None)
(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): Expr = {
- (t, otpe) match {
+ val otpe = expected_otpe match {
+ case Some(StringType) => Some(listchar)
+ case _ => expected_otpe
+ }
+ val res = (t, otpe) match {
case (SimpleSymbol(s), Some(tp: TypeParameter)) =>
val n = s.name.split("!").toList.last
GenericValue(tp, n.toInt)
@@ -96,6 +100,16 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
case _ =>
super.fromSMT(t, otpe)
}
+ expected_otpe match {
+ case Some(StringType) =>
+ StringLiteral(convertToString(res)(program))
+ case _ => res
+ }
+ }
+
+ def convertToTarget(e: Expr)(implicit bindings: Map[Identifier, Term]): Term = toSMT(e)
+ def targetApplication(tfd: TypedFunDef, args: Seq[Term])(implicit bindings: Map[Identifier, Term]): Term = {
+ FunctionApplication(declareFunction(tfd), args)
}
override protected def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]): Term = e match {
@@ -132,6 +146,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
case SetIntersection(l, r) =>
ArrayMap(SSymbol("and"), toSMT(l), toSMT(r))
+ case StringConverted(result) => result
case _ =>
super.toSMT(e)
}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index f0b7d5f91a9f53f32dd6eb9590c988618f0536d4..ac1e8855a4a53ed5ef2f66c34d4b015d9a26ba3f 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -264,311 +264,322 @@ trait AbstractZ3Solver extends Solver {
case other =>
throw SolverUnsupportedError(other, this)
}
+
+
protected[leon] def toZ3Formula(expr: Expr, initialMap: Map[Identifier, Z3AST] = Map.empty): Z3AST = {
- var z3Vars: Map[Identifier,Z3AST] = if(initialMap.nonEmpty) {
+ implicit var z3Vars: Map[Identifier,Z3AST] = if(initialMap.nonEmpty) {
initialMap
} else {
// FIXME TODO pleeeeeeeease make this cleaner. Ie. decide what set of
// variable has to remain in a map etc.
variables.aToB.collect{ case (Variable(id), p2) => id -> p2 }
}
-
- def rec(ex: Expr): Z3AST = ex match {
-
- // TODO: Leave that as a specialization?
- case LetTuple(ids, e, b) => {
- z3Vars = z3Vars ++ ids.zipWithIndex.map { case (id, ix) =>
- val entry = id -> rec(tupleSelect(e, ix + 1, ids.size))
- entry
+ new Z3StringConversion[Z3AST] {
+ def getProgram = AbstractZ3Solver.this.program
+ def convertToTarget(e: Expr)(implicit bindings: Map[Identifier, Z3AST]): Z3AST = {
+ rec(e)
}
- val rb = rec(b)
- z3Vars = z3Vars -- ids
- rb
- }
-
- case p @ Passes(_, _, _) =>
- rec(p.asConstraint)
-
- case me @ MatchExpr(s, cs) =>
- rec(matchToIfThenElse(me))
-
- case Let(i, e, b) => {
- val re = rec(e)
- z3Vars = z3Vars + (i -> re)
- val rb = rec(b)
- z3Vars = z3Vars - i
- rb
- }
-
- case Waypoint(_, e, _) => rec(e)
- case a @ Assert(cond, err, body) =>
- rec(IfExpr(cond, body, Error(a.getType, err.getOrElse("Assertion failed")).setPos(a.getPos)).setPos(a.getPos))
-
- case e @ Error(tpe, _) => {
- val newAST = z3.mkFreshConst("errorValue", typeToSort(tpe))
- // Might introduce dupplicates (e), but no worries here
- variables += (e -> newAST)
- newAST
- }
- case v @ Variable(id) => z3Vars.get(id) match {
- case Some(ast) =>
- ast
- case None => {
- variables.getB(v) match {
- case Some(ast) =>
- ast
-
- case None =>
- val newAST = z3.mkFreshConst(id.uniqueName, typeToSort(v.getType))
- z3Vars = z3Vars + (id -> newAST)
- variables += (v -> newAST)
- newAST
- }
- }
- }
-
- case ite @ IfExpr(c, t, e) => z3.mkITE(rec(c), rec(t), rec(e))
- case And(exs) => z3.mkAnd(exs.map(rec): _*)
- case Or(exs) => z3.mkOr(exs.map(rec): _*)
- case Implies(l, r) => z3.mkImplies(rec(l), rec(r))
- case Not(Equals(l, r)) => z3.mkDistinct(rec(l), rec(r))
- 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 FractionalLiteral(n, d) => z3.mkNumeral(s"$n / $d", typeToSort(RealType))
- case CharLiteral(c) => z3.mkInt(c, typeToSort(CharType))
- case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
- case Equals(l, r) => z3.mkEq(rec( l ), rec( r ) )
- case Plus(l, r) => z3.mkAdd(rec(l), rec(r))
- case Minus(l, r) => z3.mkSub(rec(l), rec(r))
- case Times(l, r) => z3.mkMul(rec(l), rec(r))
- case Division(l, r) => {
- val rl = rec(l)
- val rr = rec(r)
- z3.mkITE(
- z3.mkGE(rl, z3.mkNumeral("0", typeToSort(IntegerType))),
- z3.mkDiv(rl, rr),
- z3.mkUnaryMinus(z3.mkDiv(z3.mkUnaryMinus(rl), rr))
- )
- }
- case Remainder(l, r) => {
- val q = rec(Division(l, r))
- z3.mkSub(rec(l), z3.mkMul(rec(r), q))
- }
- case Modulo(l, r) => {
- z3.mkMod(rec(l), rec(r))
- }
- case UMinus(e) => z3.mkUnaryMinus(rec(e))
-
- case RealPlus(l, r) => z3.mkAdd(rec(l), rec(r))
- case RealMinus(l, r) => z3.mkSub(rec(l), rec(r))
- case RealTimes(l, r) => z3.mkMul(rec(l), rec(r))
- case RealDivision(l, r) => z3.mkDiv(rec(l), rec(r))
- case RealUMinus(e) => z3.mkUnaryMinus(rec(e))
-
- case BVPlus(l, r) => z3.mkBVAdd(rec(l), rec(r))
- case BVMinus(l, r) => z3.mkBVSub(rec(l), rec(r))
- case BVTimes(l, r) => z3.mkBVMul(rec(l), rec(r))
- case BVDivision(l, r) => z3.mkBVSdiv(rec(l), rec(r))
- case BVRemainder(l, r) => z3.mkBVSrem(rec(l), rec(r))
- case BVUMinus(e) => z3.mkBVNeg(rec(e))
- case BVNot(e) => z3.mkBVNot(rec(e))
- case BVAnd(l, r) => z3.mkBVAnd(rec(l), rec(r))
- case BVOr(l, r) => z3.mkBVOr(rec(l), rec(r))
- case BVXOr(l, r) => z3.mkBVXor(rec(l), rec(r))
- case BVShiftLeft(l, r) => z3.mkBVShl(rec(l), rec(r))
- case BVAShiftRight(l, r) => z3.mkBVAshr(rec(l), rec(r))
- case BVLShiftRight(l, r) => z3.mkBVLshr(rec(l), rec(r))
- case LessThan(l, r) => l.getType match {
- case IntegerType => z3.mkLT(rec(l), rec(r))
- case RealType => z3.mkLT(rec(l), rec(r))
- case Int32Type => z3.mkBVSlt(rec(l), rec(r))
- case CharType => z3.mkBVSlt(rec(l), rec(r))
- }
- case LessEquals(l, r) => l.getType match {
- case IntegerType => z3.mkLE(rec(l), rec(r))
- case RealType => z3.mkLE(rec(l), rec(r))
- case Int32Type => z3.mkBVSle(rec(l), rec(r))
- case CharType => z3.mkBVSle(rec(l), rec(r))
- //case _ => throw new IllegalStateException(s"l: $l, Left type: ${l.getType} Expr: $ex")
- }
- case GreaterThan(l, r) => l.getType match {
- case IntegerType => z3.mkGT(rec(l), rec(r))
- case RealType => z3.mkGT(rec(l), rec(r))
- case Int32Type => z3.mkBVSgt(rec(l), rec(r))
- case CharType => z3.mkBVSgt(rec(l), rec(r))
- }
- case GreaterEquals(l, r) => l.getType match {
- case IntegerType => z3.mkGE(rec(l), rec(r))
- case RealType => z3.mkGE(rec(l), rec(r))
- case Int32Type => z3.mkBVSge(rec(l), rec(r))
- case CharType => z3.mkBVSge(rec(l), rec(r))
- }
-
- case u : UnitLiteral =>
- val tpe = normalizeType(u.getType)
- typeToSort(tpe)
- val constructor = constructors.toB(tpe)
- constructor()
-
- case t @ Tuple(es) =>
- val tpe = normalizeType(t.getType)
- typeToSort(tpe)
- val constructor = constructors.toB(tpe)
- constructor(es.map(rec): _*)
-
- case ts @ TupleSelect(t, i) =>
- val tpe = normalizeType(t.getType)
- typeToSort(tpe)
- val selector = selectors.toB((tpe, i-1))
- selector(rec(t))
-
- case c @ CaseClass(ct, args) =>
- typeToSort(ct) // Making sure the sort is defined
- val constructor = constructors.toB(ct)
- constructor(args.map(rec): _*)
-
- case c @ CaseClassSelector(cct, cc, sel) =>
- typeToSort(cct) // Making sure the sort is defined
- val selector = selectors.toB(cct, c.selectorIndex)
- selector(rec(cc))
-
- case AsInstanceOf(expr, ct) =>
- rec(expr)
-
- case IsInstanceOf(e, act: AbstractClassType) =>
- act.knownCCDescendants match {
- case Seq(cct) =>
- rec(IsInstanceOf(e, cct))
- case more =>
- val i = FreshIdentifier("e", act, alwaysShowUniqueID = true)
- rec(Let(i, e, orJoin(more map(IsInstanceOf(Variable(i), _)))))
+ def targetApplication(tfd: TypedFunDef, args: Seq[Z3AST])(implicit bindings: Map[Identifier, Z3AST]): Z3AST = {
+ z3.mkApp(functionDefToDecl(tfd), args: _*)
}
-
- case IsInstanceOf(e, cct: CaseClassType) =>
- typeToSort(cct) // Making sure the sort is defined
- val tester = testers.toB(cct)
- tester(rec(e))
-
- case al @ ArraySelect(a, i) =>
- val tpe = normalizeType(a.getType)
-
- val sa = rec(a)
- val content = selectors.toB((tpe, 1))(sa)
-
- z3.mkSelect(content, rec(i))
-
- case al @ ArrayUpdated(a, i, e) =>
- val tpe = normalizeType(a.getType)
-
- val sa = rec(a)
- val ssize = selectors.toB((tpe, 0))(sa)
- val scontent = selectors.toB((tpe, 1))(sa)
-
- val newcontent = z3.mkStore(scontent, rec(i), rec(e))
-
- val constructor = constructors.toB(tpe)
-
- constructor(ssize, newcontent)
-
- case al @ ArrayLength(a) =>
- val tpe = normalizeType(a.getType)
- val sa = rec(a)
- selectors.toB((tpe, 0))(sa)
-
- case arr @ FiniteArray(elems, oDefault, length) =>
- val at @ ArrayType(base) = normalizeType(arr.getType)
- typeToSort(at)
-
- val default = oDefault.getOrElse(simplestValue(base))
-
- val ar = rec(RawArrayValue(Int32Type, elems.map {
- case (i, e) => IntLiteral(i) -> e
- }, default))
-
- constructors.toB(at)(rec(length), ar)
-
- case f @ FunctionInvocation(tfd, args) =>
- z3.mkApp(functionDefToDecl(tfd), args.map(rec): _*)
-
- case fa @ Application(caller, args) =>
- val ft @ FunctionType(froms, to) = normalizeType(caller.getType)
- val funDecl = lambdas.cachedB(ft) {
- val sortSeq = (ft +: froms).map(tpe => typeToSort(tpe))
- val returnSort = typeToSort(to)
-
- val name = FreshIdentifier("dynLambda").uniqueName
- z3.mkFreshFuncDecl(name, sortSeq, returnSort)
- }
- z3.mkApp(funDecl, (caller +: args).map(rec): _*)
-
- case ElementOfSet(e, s) => z3.mkSetMember(rec(e), rec(s))
- case SubsetOf(s1, s2) => z3.mkSetSubset(rec(s1), rec(s2))
- case SetIntersection(s1, s2) => z3.mkSetIntersect(rec(s1), rec(s2))
- case SetUnion(s1, s2) => z3.mkSetUnion(rec(s1), rec(s2))
- 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 RawArrayValue(keyTpe, elems, default) =>
- val ar = z3.mkConstArray(typeToSort(keyTpe), rec(default))
-
- elems.foldLeft(ar) {
- case (array, (k, v)) => z3.mkStore(array, rec(k), rec(v))
- }
-
- /**
- * ===== Map operations =====
- */
- case m @ FiniteMap(elems, from, to) =>
- val MapType(_, t) = normalizeType(m.getType)
-
- rec(RawArrayValue(from, elems.map{
- case (k, v) => (k, CaseClass(library.someType(t), Seq(v)))
- }.toMap, CaseClass(library.noneType(t), Seq())))
-
- case MapApply(m, k) =>
- val mt @ MapType(_, t) = normalizeType(m.getType)
- typeToSort(mt)
-
- val el = z3.mkSelect(rec(m), rec(k))
-
- // Really ?!? We don't check that it is actually != None?
- selectors.toB(library.someType(t), 0)(el)
-
- case MapIsDefinedAt(m, k) =>
- val mt @ MapType(_, t) = normalizeType(m.getType)
- typeToSort(mt)
-
- val el = z3.mkSelect(rec(m), rec(k))
-
- testers.toB(library.someType(t))(el)
-
- case MapUnion(m1, FiniteMap(elems, _, _)) =>
- val mt @ MapType(_, t) = normalizeType(m1.getType)
- typeToSort(mt)
-
- elems.foldLeft(rec(m1)) { case (m, (k,v)) =>
- z3.mkStore(m, rec(k), rec(CaseClass(library.someType(t), Seq(v))))
+ def rec(ex: Expr): Z3AST = ex match {
+
+ // TODO: Leave that as a specialization?
+ case LetTuple(ids, e, b) => {
+ z3Vars = z3Vars ++ ids.zipWithIndex.map { case (id, ix) =>
+ val entry = id -> rec(tupleSelect(e, ix + 1, ids.size))
+ entry
+ }
+ val rb = rec(b)
+ z3Vars = z3Vars -- ids
+ rb
+ }
+
+ case p @ Passes(_, _, _) =>
+ rec(p.asConstraint)
+
+ case me @ MatchExpr(s, cs) =>
+ rec(matchToIfThenElse(me))
+
+ case Let(i, e, b) => {
+ val re = rec(e)
+ z3Vars = z3Vars + (i -> re)
+ val rb = rec(b)
+ z3Vars = z3Vars - i
+ rb
+ }
+
+ case Waypoint(_, e, _) => rec(e)
+ case a @ Assert(cond, err, body) =>
+ rec(IfExpr(cond, body, Error(a.getType, err.getOrElse("Assertion failed")).setPos(a.getPos)).setPos(a.getPos))
+
+ case e @ Error(tpe, _) => {
+ val newAST = z3.mkFreshConst("errorValue", typeToSort(tpe))
+ // Might introduce dupplicates (e), but no worries here
+ variables += (e -> newAST)
+ newAST
+ }
+ case v @ Variable(id) => z3Vars.get(id) match {
+ case Some(ast) =>
+ ast
+ case None => {
+ variables.getB(v) match {
+ case Some(ast) =>
+ ast
+
+ case None =>
+ val newAST = z3.mkFreshConst(id.uniqueName, typeToSort(v.getType))
+ z3Vars = z3Vars + (id -> newAST)
+ variables += (v -> newAST)
+ newAST
+ }
+ }
+ }
+
+ case ite @ IfExpr(c, t, e) => z3.mkITE(rec(c), rec(t), rec(e))
+ case And(exs) => z3.mkAnd(exs.map(rec): _*)
+ case Or(exs) => z3.mkOr(exs.map(rec): _*)
+ case Implies(l, r) => z3.mkImplies(rec(l), rec(r))
+ case Not(Equals(l, r)) => z3.mkDistinct(rec(l), rec(r))
+ 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 FractionalLiteral(n, d) => z3.mkNumeral(s"$n / $d", typeToSort(RealType))
+ case CharLiteral(c) => z3.mkInt(c, typeToSort(CharType))
+ case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
+ case Equals(l, r) => z3.mkEq(rec( l ), rec( r ) )
+ case Plus(l, r) => z3.mkAdd(rec(l), rec(r))
+ case Minus(l, r) => z3.mkSub(rec(l), rec(r))
+ case Times(l, r) => z3.mkMul(rec(l), rec(r))
+ case Division(l, r) => {
+ val rl = rec(l)
+ val rr = rec(r)
+ z3.mkITE(
+ z3.mkGE(rl, z3.mkNumeral("0", typeToSort(IntegerType))),
+ z3.mkDiv(rl, rr),
+ z3.mkUnaryMinus(z3.mkDiv(z3.mkUnaryMinus(rl), rr))
+ )
+ }
+ case Remainder(l, r) => {
+ val q = rec(Division(l, r))
+ z3.mkSub(rec(l), z3.mkMul(rec(r), q))
+ }
+ case Modulo(l, r) => {
+ z3.mkMod(rec(l), rec(r))
+ }
+ case UMinus(e) => z3.mkUnaryMinus(rec(e))
+
+ case RealPlus(l, r) => z3.mkAdd(rec(l), rec(r))
+ case RealMinus(l, r) => z3.mkSub(rec(l), rec(r))
+ case RealTimes(l, r) => z3.mkMul(rec(l), rec(r))
+ case RealDivision(l, r) => z3.mkDiv(rec(l), rec(r))
+ case RealUMinus(e) => z3.mkUnaryMinus(rec(e))
+
+ case BVPlus(l, r) => z3.mkBVAdd(rec(l), rec(r))
+ case BVMinus(l, r) => z3.mkBVSub(rec(l), rec(r))
+ case BVTimes(l, r) => z3.mkBVMul(rec(l), rec(r))
+ case BVDivision(l, r) => z3.mkBVSdiv(rec(l), rec(r))
+ case BVRemainder(l, r) => z3.mkBVSrem(rec(l), rec(r))
+ case BVUMinus(e) => z3.mkBVNeg(rec(e))
+ case BVNot(e) => z3.mkBVNot(rec(e))
+ case BVAnd(l, r) => z3.mkBVAnd(rec(l), rec(r))
+ case BVOr(l, r) => z3.mkBVOr(rec(l), rec(r))
+ case BVXOr(l, r) => z3.mkBVXor(rec(l), rec(r))
+ case BVShiftLeft(l, r) => z3.mkBVShl(rec(l), rec(r))
+ case BVAShiftRight(l, r) => z3.mkBVAshr(rec(l), rec(r))
+ case BVLShiftRight(l, r) => z3.mkBVLshr(rec(l), rec(r))
+ case LessThan(l, r) => l.getType match {
+ case IntegerType => z3.mkLT(rec(l), rec(r))
+ case RealType => z3.mkLT(rec(l), rec(r))
+ case Int32Type => z3.mkBVSlt(rec(l), rec(r))
+ case CharType => z3.mkBVSlt(rec(l), rec(r))
+ }
+ case LessEquals(l, r) => l.getType match {
+ case IntegerType => z3.mkLE(rec(l), rec(r))
+ case RealType => z3.mkLE(rec(l), rec(r))
+ case Int32Type => z3.mkBVSle(rec(l), rec(r))
+ case CharType => z3.mkBVSle(rec(l), rec(r))
+ //case _ => throw new IllegalStateException(s"l: $l, Left type: ${l.getType} Expr: $ex")
+ }
+ case GreaterThan(l, r) => l.getType match {
+ case IntegerType => z3.mkGT(rec(l), rec(r))
+ case RealType => z3.mkGT(rec(l), rec(r))
+ case Int32Type => z3.mkBVSgt(rec(l), rec(r))
+ case CharType => z3.mkBVSgt(rec(l), rec(r))
+ }
+ case GreaterEquals(l, r) => l.getType match {
+ case IntegerType => z3.mkGE(rec(l), rec(r))
+ case RealType => z3.mkGE(rec(l), rec(r))
+ case Int32Type => z3.mkBVSge(rec(l), rec(r))
+ case CharType => z3.mkBVSge(rec(l), rec(r))
+ }
+
+ case StringConverted(result) =>
+ result
+
+ case u : UnitLiteral =>
+ val tpe = normalizeType(u.getType)
+ typeToSort(tpe)
+ val constructor = constructors.toB(tpe)
+ constructor()
+
+ case t @ Tuple(es) =>
+ val tpe = normalizeType(t.getType)
+ typeToSort(tpe)
+ val constructor = constructors.toB(tpe)
+ constructor(es.map(rec): _*)
+
+ case ts @ TupleSelect(t, i) =>
+ val tpe = normalizeType(t.getType)
+ typeToSort(tpe)
+ val selector = selectors.toB((tpe, i-1))
+ selector(rec(t))
+
+ case c @ CaseClass(ct, args) =>
+ typeToSort(ct) // Making sure the sort is defined
+ val constructor = constructors.toB(ct)
+ constructor(args.map(rec): _*)
+
+ case c @ CaseClassSelector(cct, cc, sel) =>
+ typeToSort(cct) // Making sure the sort is defined
+ val selector = selectors.toB(cct, c.selectorIndex)
+ selector(rec(cc))
+
+ case AsInstanceOf(expr, ct) =>
+ rec(expr)
+
+ case IsInstanceOf(e, act: AbstractClassType) =>
+ act.knownCCDescendants match {
+ case Seq(cct) =>
+ rec(IsInstanceOf(e, cct))
+ case more =>
+ val i = FreshIdentifier("e", act, alwaysShowUniqueID = true)
+ rec(Let(i, e, orJoin(more map(IsInstanceOf(Variable(i), _)))))
+ }
+
+ case IsInstanceOf(e, cct: CaseClassType) =>
+ typeToSort(cct) // Making sure the sort is defined
+ val tester = testers.toB(cct)
+ tester(rec(e))
+
+ case al @ ArraySelect(a, i) =>
+ val tpe = normalizeType(a.getType)
+
+ val sa = rec(a)
+ val content = selectors.toB((tpe, 1))(sa)
+
+ z3.mkSelect(content, rec(i))
+
+ case al @ ArrayUpdated(a, i, e) =>
+ val tpe = normalizeType(a.getType)
+
+ val sa = rec(a)
+ val ssize = selectors.toB((tpe, 0))(sa)
+ val scontent = selectors.toB((tpe, 1))(sa)
+
+ val newcontent = z3.mkStore(scontent, rec(i), rec(e))
+
+ val constructor = constructors.toB(tpe)
+
+ constructor(ssize, newcontent)
+
+ case al @ ArrayLength(a) =>
+ val tpe = normalizeType(a.getType)
+ val sa = rec(a)
+ selectors.toB((tpe, 0))(sa)
+
+ case arr @ FiniteArray(elems, oDefault, length) =>
+ val at @ ArrayType(base) = normalizeType(arr.getType)
+ typeToSort(at)
+
+ val default = oDefault.getOrElse(simplestValue(base))
+
+ val ar = rec(RawArrayValue(Int32Type, elems.map {
+ case (i, e) => IntLiteral(i) -> e
+ }, default))
+
+ constructors.toB(at)(rec(length), ar)
+
+ case f @ FunctionInvocation(tfd, args) =>
+ z3.mkApp(functionDefToDecl(tfd), args.map(rec): _*)
+
+ case fa @ Application(caller, args) =>
+ val ft @ FunctionType(froms, to) = normalizeType(caller.getType)
+ val funDecl = lambdas.cachedB(ft) {
+ val sortSeq = (ft +: froms).map(tpe => typeToSort(tpe))
+ val returnSort = typeToSort(to)
+
+ val name = FreshIdentifier("dynLambda").uniqueName
+ z3.mkFreshFuncDecl(name, sortSeq, returnSort)
+ }
+ z3.mkApp(funDecl, (caller +: args).map(rec): _*)
+
+ case ElementOfSet(e, s) => z3.mkSetMember(rec(e), rec(s))
+ case SubsetOf(s1, s2) => z3.mkSetSubset(rec(s1), rec(s2))
+ case SetIntersection(s1, s2) => z3.mkSetIntersect(rec(s1), rec(s2))
+ case SetUnion(s1, s2) => z3.mkSetUnion(rec(s1), rec(s2))
+ 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 RawArrayValue(keyTpe, elems, default) =>
+ val ar = z3.mkConstArray(typeToSort(keyTpe), rec(default))
+
+ elems.foldLeft(ar) {
+ case (array, (k, v)) => z3.mkStore(array, rec(k), rec(v))
+ }
+
+ /**
+ * ===== Map operations =====
+ */
+ case m @ FiniteMap(elems, from, to) =>
+ val MapType(_, t) = normalizeType(m.getType)
+
+ rec(RawArrayValue(from, elems.map{
+ case (k, v) => (k, CaseClass(library.someType(t), Seq(v)))
+ }.toMap, CaseClass(library.noneType(t), Seq())))
+
+ case MapApply(m, k) =>
+ val mt @ MapType(_, t) = normalizeType(m.getType)
+ typeToSort(mt)
+
+ val el = z3.mkSelect(rec(m), rec(k))
+
+ // Really ?!? We don't check that it is actually != None?
+ selectors.toB(library.someType(t), 0)(el)
+
+ case MapIsDefinedAt(m, k) =>
+ val mt @ MapType(_, t) = normalizeType(m.getType)
+ typeToSort(mt)
+
+ val el = z3.mkSelect(rec(m), rec(k))
+
+ testers.toB(library.someType(t))(el)
+
+ case MapUnion(m1, FiniteMap(elems, _, _)) =>
+ val mt @ MapType(_, t) = normalizeType(m1.getType)
+ typeToSort(mt)
+
+ elems.foldLeft(rec(m1)) { case (m, (k,v)) =>
+ z3.mkStore(m, rec(k), rec(CaseClass(library.someType(t), Seq(v))))
+ }
+
+
+ case gv @ GenericValue(tp, id) =>
+ z3.mkApp(genericValueToDecl(gv))
+
+ case other =>
+ unsupported(other)
}
-
-
- case gv @ GenericValue(tp, id) =>
- z3.mkApp(genericValueToDecl(gv))
-
- case other =>
- unsupported(other)
- }
-
- rec(expr)
+ }.rec(expr)
}
protected[leon] def fromZ3Formula(model: Z3Model, tree: Z3AST, tpe: TypeTree): Expr = {
-
- def rec(t: Z3AST, tpe: TypeTree): Expr = {
+ def rec(t: Z3AST, expected_tpe: TypeTree): Expr = {
val kind = z3.getASTKind(t)
- kind match {
+ val tpe = Z3StringTypeConversion.convert(expected_tpe)(program)
+ val res = kind match {
case Z3NumeralIntAST(Some(v)) =>
val leading = t.toString.substring(0, 2 min t.toString.length)
if(leading == "#x") {
@@ -758,6 +769,11 @@ trait AbstractZ3Solver extends Solver {
}
case _ => unsound(t, "unexpected AST")
}
+ expected_tpe match {
+ case StringType =>
+ StringLiteral(Z3StringTypeConversion.convertToString(res)(program))
+ case _ => res
+ }
}
rec(tree, normalizeType(tpe))
@@ -774,7 +790,8 @@ trait AbstractZ3Solver extends Solver {
}
def idToFreshZ3Id(id: Identifier): Z3AST = {
- z3.mkFreshConst(id.uniqueName, typeToSort(id.getType))
+ val correctType = Z3StringTypeConversion.convert(id.getType)(program)
+ z3.mkFreshConst(id.uniqueName, typeToSort(correctType))
}
def reset() = {
diff --git a/src/main/scala/leon/solvers/z3/Z3StringConversion.scala b/src/main/scala/leon/solvers/z3/Z3StringConversion.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3daf1ad4964ad73e8c4d9701ae4e65d0f4170897
--- /dev/null
+++ b/src/main/scala/leon/solvers/z3/Z3StringConversion.scala
@@ -0,0 +1,94 @@
+package leon
+package solvers
+package z3
+
+import purescala.Common._
+import purescala.Expressions._
+import purescala.Constructors._
+import purescala.Types._
+import purescala.Definitions._
+import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
+import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
+import _root_.smtlib.interpreters.Z3Interpreter
+import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
+import _root_.smtlib.theories.ArraysEx
+import leon.utils.Bijection
+
+object Z3StringTypeConversion {
+ def convert(t: TypeTree)(implicit p: Program) = new Z3StringTypeConversion { def getProgram = p }.convertType(t)
+ def convertToString(e: Expr)(implicit p: Program) = new Z3StringTypeConversion{ def getProgram = p }.convertToString(e)
+}
+
+trait Z3StringTypeConversion {
+ val stringBijection = new Bijection[String, Expr]()
+
+ lazy val conschar = program.lookupCaseClass("leon.collection.Cons") match {
+ case Some(cc) => cc.typed(Seq(CharType))
+ case _ => throw new Exception("Could not find Cons in Z3 solver")
+ }
+ lazy val nilchar = program.lookupCaseClass("leon.collection.Nil") match {
+ case Some(cc) => cc.typed(Seq(CharType))
+ case _ => throw new Exception("Could not find Nil in Z3 solver")
+ }
+ lazy val listchar = program.lookupAbstractClass("leon.collection.List") match {
+ case Some(cc) => cc.typed(Seq(CharType))
+ case _ => throw new Exception("Could not find List in Z3 solver")
+ }
+ def lookupFunDef(s: String): FunDef = program.lookupFunDef(s) match {
+ case Some(fd) => fd
+ case _ => throw new Exception("Could not find function "+s+" in program")
+ }
+ lazy val list_size = lookupFunDef("leon.collection.List.size").typed(Seq(CharType))
+ lazy val list_++ = lookupFunDef("leon.collection.List.++").typed(Seq(CharType))
+ lazy val list_take = lookupFunDef("leon.collection.List.take").typed(Seq(CharType))
+ lazy val list_drop = lookupFunDef("leon.collection.List.drop").typed(Seq(CharType))
+ lazy val list_slice = lookupFunDef("leon.collection.List.slice").typed(Seq(CharType))
+
+ private lazy val program = getProgram
+
+ def getProgram: Program
+
+ def convertType(t: TypeTree): TypeTree = t match {
+ case StringType => listchar
+ case _ => t
+ }
+ def convertToString(e: Expr)(implicit p: Program): String =
+ stringBijection.cachedA(e) {
+ e match {
+ case CaseClass(_, Seq(CharLiteral(c), l)) => c + convertToString(l)
+ case CaseClass(_, Seq()) => ""
+ }
+ }
+ def convertFromString(v: String) =
+ stringBijection.cachedB(v) {
+ v.toList.foldRight(CaseClass(nilchar, Seq())){
+ case (char, l) => CaseClass(conschar, Seq(CharLiteral(char), l))
+ }
+ }
+}
+
+trait Z3StringConversion[TargetType] extends Z3StringTypeConversion {
+ def convertToTarget(e: Expr)(implicit bindings: Map[Identifier, TargetType]): TargetType
+ def targetApplication(fd: TypedFunDef, args: Seq[TargetType])(implicit bindings: Map[Identifier, TargetType]): TargetType
+
+ object StringConverted {
+ def unapply(e: Expr)(implicit bindings: Map[Identifier, TargetType]): Option[TargetType] = e match {
+ case StringLiteral(v) =>
+ // No string support for z3 at this moment.
+ val stringEncoding = convertFromString(v)
+ Some(convertToTarget(stringEncoding))
+ case StringLength(a) =>
+ Some(targetApplication(list_size, Seq(convertToTarget(a))))
+ case StringConcat(a, b) =>
+ Some(targetApplication(list_++, Seq(convertToTarget(a), convertToTarget(b))))
+ case SubString(a, start, Plus(start2, length)) if start == start2 =>
+ Some(targetApplication(list_take,
+ Seq(targetApplication(list_drop, Seq(convertToTarget(a), convertToTarget(start))), convertToTarget(length))))
+ case SubString(a, start, end) =>
+ Some(targetApplication(list_slice, Seq(convertToTarget(a), convertToTarget(start), convertToTarget(end))))
+ case _ => None
+ }
+
+ def apply(t: TypeTree): TypeTree = convertType(t)
+ }
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
index 4d100210911734504a96bd005d0299ae0f1b8906..0ddd21078ffe772986bd5487d964d352184cd2e6 100644
--- a/src/main/scala/leon/utils/Library.scala
+++ b/src/main/scala/leon/utils/Library.scala
@@ -16,7 +16,6 @@ case class Library(pgm: Program) {
lazy val Some = lookup("leon.lang.Some").collectFirst { case ccd : CaseClassDef => ccd }
lazy val None = lookup("leon.lang.None").collectFirst { case ccd : CaseClassDef => ccd }
- //lazy val String = lookup("leon.lang.string.String").collectFirst { case ccd : CaseClassDef => ccd }
lazy val StrOps = lookup("leon.lang.StrOps").collectFirst { case md: ModuleDef => md }
lazy val Dummy = lookup("leon.lang.Dummy").collectFirst { case ccd : CaseClassDef => ccd }
diff --git a/src/test/scala/leon/integration/solvers/SolversSuite.scala b/src/test/scala/leon/integration/solvers/SolversSuite.scala
index 24ebf35916d9abce077fdd7d8ee5752fd3c1e0d3..d568e471f08eb4cf1a558675419daabd9e9c940a 100644
--- a/src/test/scala/leon/integration/solvers/SolversSuite.scala
+++ b/src/test/scala/leon/integration/solvers/SolversSuite.scala
@@ -72,13 +72,13 @@ class SolversSuite extends LeonTestSuiteWithProgram {
val model = solver.getModel
for (v <- vs) {
if (model.isDefinedAt(v.id)) {
- assert(model(v.id).getType === v.getType, "Extracting value of type "+v.getType)
+ assert(model(v.id).getType === v.getType, s"Solver $solver - Extracting value of type "+v.getType)
} else {
- fail("Model does not contain "+v.id+" of type "+v.getType)
+ fail(s"Solver $solver - Model does not contain "+v.id.uniqueName+" of type "+v.getType)
}
}
case _ =>
- fail("Constraint "+cnstr.asString+" is unsat!?")
+ fail(s"Solver $solver - Constraint "+cnstr.asString+" is unsat!?")
}
} finally {
solver.free()
diff --git a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
index d64df7f8c43b1f5f77bb93bce85d8a69cbf230ed..7c0d3e13c044f4cd2491041cf28319986a6df42b 100644
--- a/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/StringSolverSuite.scala
@@ -199,7 +199,6 @@ class StringSolverSuite extends FunSuite with Matchers with ScalaFutures {
val solution = solve(problem)
solution should not be 'empty
val firstSolution = solution(0)
- println("First solution " + firstSolution)
firstSolution(idMap("const8")) should equal("List(")
firstSolution(idMap("const4")) should equal("")
}
@@ -216,7 +215,6 @@ T2: internal
T2: ret Pop() -> 5"""
val problem: Problem = List(lhs === expected)
- println("Problem to solve:" + StringSolver.renderProblem(problem))
solve(problem) should not be 'empty
}
diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala
index c58a4b0aceab03a00257ed48429028412e9cf643..6c2df0820a2b0f0c19ee393c12e1d70b36bbf233 100644
--- a/src/test/scala/leon/regression/termination/TerminationSuite.scala
+++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala
@@ -38,7 +38,7 @@ class TerminationSuite extends LeonRegressionSuite {
"verification/purescala/valid/InductiveQuantification.scala"
)
- val t = if (ignored.exists(displayName.endsWith)) {
+ val t = if (ignored.exists(displayName.replaceAll("\\\\","/").endsWith)) {
ignore _
} else {
test _
diff --git a/src/test/scala/leon/test/LeonRegressionSuite.scala b/src/test/scala/leon/test/LeonRegressionSuite.scala
index 58fdce2c6b789ddae0bbaee845f54ad6fe09de2c..4181fee97e7a4a38e3f30349458366ba62138d12 100644
--- a/src/test/scala/leon/test/LeonRegressionSuite.scala
+++ b/src/test/scala/leon/test/LeonRegressionSuite.scala
@@ -33,7 +33,7 @@ trait LeonRegressionSuite extends FunSuite with Timeouts {
body
} catch {
case fe: LeonFatalError =>
- throw new TestFailedException("Uncaught LeonFatalError", fe, 5)
+ throw new TestFailedException("Uncaught LeonFatalError" + fe.msg.map(": " + _).getOrElse(""), fe, 5)
}
}
}
diff --git a/testcases/verification/case-studies/LambdaSound.scala b/testcases/verification/case-studies/LambdaSound.scala
index 6208d2039eaf16ba1dbeae614bf6432e2309ee1e..fa59efbc001614acbd338b83883248d07a736a2d 100644
--- a/testcases/verification/case-studies/LambdaSound.scala
+++ b/testcases/verification/case-studies/LambdaSound.scala
@@ -3,7 +3,6 @@ import leon.annotation._
import leon.collection._
import leon.lang.synthesis._
import leon._
-import leon.lang.string._
object Lambda {
case class Id(v: BigInt)
diff --git a/testcases/verification/editor/AsciiToPos.scala b/testcases/verification/editor/AsciiToPos.scala
index 4ec536ce71c8f684dc1a2329c51de19cf575269f..1514ccc13733e6e3571a51081a89a2c490a72f30 100644
--- a/testcases/verification/editor/AsciiToPos.scala
+++ b/testcases/verification/editor/AsciiToPos.scala
@@ -1,6 +1,5 @@
import leon.lang._
import leon.lang.synthesis._
-import leon.lang.string._
import leon.collection._
object Justify {
@@ -14,7 +13,7 @@ object Justify {
Cons(wordAcc, tokenize0(t, ""))
}
} else {
- tokenize0(t, String(List(h)) + wordAcc)
+ tokenize0(t, h + wordAcc)
}
}
diff --git a/testcases/verification/higher-order/valid/MonadsException.scala b/testcases/verification/higher-order/valid/MonadsException.scala
index 2c80332435b1fb65653932fb93906d6540685e13..27c87d26177ef8c0d42f49766ab56a2c1e68b13c 100644
--- a/testcases/verification/higher-order/valid/MonadsException.scala
+++ b/testcases/verification/higher-order/valid/MonadsException.scala
@@ -1,5 +1,4 @@
import leon.lang._
-import leon.lang.string._
object TryMonad {
diff --git a/testcases/verification/monads/Freshen.scala b/testcases/verification/monads/Freshen.scala
index de8c7eda592ba211a948c4beb5f2925d6a53974f..6fe0ef38f7e673f4e0f9ffbee8bbf0e7e7a5eafa 100644
--- a/testcases/verification/monads/Freshen.scala
+++ b/testcases/verification/monads/Freshen.scala
@@ -6,7 +6,6 @@ import leon.lang._
object Freshen {
import State._
- import leon.lang.string._
case class Id(name: String, id: BigInt)
diff --git a/testcases/web/demos/005_Tutorial-Monad.scala b/testcases/web/demos/005_Tutorial-Monad.scala
index 093e4a2d805a9e8e3ee07dc79eb1adfecc81acdb..ba08a0e1f3f18af7c954c2a06b7c06cc26522369 100644
--- a/testcases/web/demos/005_Tutorial-Monad.scala
+++ b/testcases/web/demos/005_Tutorial-Monad.scala
@@ -1,4 +1,3 @@
-import leon.lang.string._
import leon.annotation._
sealed abstract class Outcome[T] {
diff --git a/testcases/web/synthesis/24_String_DoubleList.scala b/testcases/web/synthesis/24_String_DoubleList.scala
index 0d89d3f233b310f9968ba36206623b75bb44f7c7..652f5e4b84ed8837dc56cdce10393a480232c1b0 100644
--- a/testcases/web/synthesis/24_String_DoubleList.scala
+++ b/testcases/web/synthesis/24_String_DoubleList.scala
@@ -26,7 +26,7 @@ object DoubleListRender {
(res : String) => (a, res) passes {
case N() =>
"[]"
- case B(NN()) =>
+ case B(NN(), N()) =>
"[()]"
}
}