From 24c618eb611680ce7e7cf8ecee9269fdf5cc3443 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 24 Aug 2015 14:22:46 +0200
Subject: [PATCH] asString in AbstractZ3Solver
---
.../leon/solvers/z3/AbstractZ3Solver.scala | 18 +++++++++---------
1 file changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 94bc6afb2..9eb08e152 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -260,7 +260,7 @@ trait AbstractZ3Solver extends Solver {
case other =>
sorts.cachedB(other) {
- reporter.warning(other.getPos, "Resorting to uninterpreted type for : " + other)
+ reporter.warning(other.getPos, "Resorting to uninterpreted type for : " + other.asString)
val symbol = z3.mkIntSymbol(FreshIdentifier("unint").globalId)
z3.mkUninterpretedSort(symbol)
}
@@ -546,7 +546,7 @@ trait AbstractZ3Solver extends Solver {
z3.mkApp(genericValueToDecl(gv))
case _ => {
- reporter.warning(ex.getPos, "Can't handle this in translation to Z3: " + ex)
+ reporter.warning(ex.getPos, "Can't handle this in translation to Z3: " + ex.asString)
throw new IllegalArgumentException
}
}
@@ -558,7 +558,7 @@ trait AbstractZ3Solver extends Solver {
case rav: RawArrayValue =>
fromRawArray(rav, tpe)
case _ =>
- scala.sys.error("Unable to extract from raw array for "+r)
+ scala.sys.error("Unable to extract from raw array for "+r.asString)
}
protected def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match {
@@ -570,7 +570,7 @@ trait AbstractZ3Solver extends Solver {
case _ =>
- scala.sys.error("Unable to extract from raw array for "+tpe)
+ scala.sys.error("Unable to extract from raw array for "+tpe.asString)
}
protected[leon] def fromZ3Formula(model: Z3Model, tree: Z3AST, tpe: TypeTree): Expr = {
@@ -588,7 +588,7 @@ trait AbstractZ3Solver extends Solver {
case Int32Type => IntLiteral(hexa.toInt)
case CharType => CharLiteral(hexa.toInt.toChar)
case _ =>
- reporter.warning("Unexpected target type for BV value: " + tpe)
+ reporter.warning("Unexpected target type for BV value: " + tpe.asString)
throw new IllegalArgumentException
}
case None => {
@@ -607,7 +607,7 @@ trait AbstractZ3Solver extends Solver {
case Int32Type => IntLiteral(hexa.toInt)
case CharType => CharLiteral(hexa.toInt.toChar)
case _ =>
- reporter.warning("Unexpected target type for BV value: " + tpe)
+ reporter.warning("Unexpected target type for BV value: " + tpe.asString)
throw new IllegalArgumentException
}
case None => {
@@ -680,10 +680,10 @@ trait AbstractZ3Solver extends Solver {
// We expect a RawArrayValue with keys in from and values in Option[to],
// with default value == None
if (r.default.getType != library.noneType(to)) {
- reporter.warning("Co-finite maps are not supported. (Default was "+r.default+")")
+ reporter.warning("Co-finite maps are not supported. (Default was "+r.default.asString+")")
throw new IllegalArgumentException
}
- require(r.keyTpe == from, s"Type error in solver model, expected $from, found ${r.keyTpe}")
+ require(r.keyTpe == from, s"Type error in solver model, expected ${from.asString}, found ${r.keyTpe.asString}")
val elems = r.elems.flatMap {
case (k, CaseClass(leonSome, Seq(x))) => Some(k -> x)
@@ -737,7 +737,7 @@ trait AbstractZ3Solver extends Solver {
// case OpMod => Modulo(rargs(0), rargs(1))
case other =>
reporter.warning("Don't know what to do with this declKind : " + other)
- reporter.warning("Expected type: " + tpe)
+ reporter.warning("Expected type: " + tpe.asString)
reporter.warning("Tree: " + t)
reporter.warning("The arguments are : " + args)
throw new IllegalArgumentException
--
GitLab