From 859cfa888a0049c386cbab5808b0a6e1bbaee905 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 31 Aug 2015 13:10:14 +0200
Subject: [PATCH] Improve Identifier API, and "undefined" errors
Identifier fields which can be private are now private.
Identifier now inherits Ordered.
Define Undefined error, and its subclass SolverUndefinedError. Use it
mainly in solvers.
---
...nFatalError.scala => LeonExceptions.scala} | 5 ++
.../scala/leon/codegen/CompilationUnit.scala | 11 ++--
.../scala/leon/datagen/VanuatooDataGen.scala | 2 +-
.../leon/evaluators/CodeGenEvaluator.scala | 2 +-
src/main/scala/leon/purescala/Common.scala | 35 +++++++-----
src/main/scala/leon/solvers/ADTManager.scala | 8 ++-
src/main/scala/leon/solvers/Solver.scala | 13 ++++-
.../leon/solvers/SolverUnsupportedError.scala | 15 +++++
.../smtlib/SMTLIBCVC4ProofSolver.scala | 3 +-
.../smtlib/SMTLIBCVC4QuantifiedSolver.scala | 7 ++-
.../solvers/smtlib/SMTLIBCVC4Solver.scala | 4 +-
.../leon/solvers/smtlib/SMTLIBSolver.scala | 36 +++++-------
.../smtlib/SMTLIBZ3QuantifiedSolver.scala | 3 +-
.../leon/solvers/smtlib/SMTLIBZ3Solver.scala | 6 +-
.../leon/solvers/z3/AbstractZ3Solver.scala | 55 ++++++++-----------
.../scala/leon/solvers/z3/FairZ3Solver.scala | 2 +-
.../leon/synthesis/rules/CEGISLike.scala | 5 +-
.../leon/test/helpers/WithLikelyEq.scala | 2 +-
18 files changed, 122 insertions(+), 92 deletions(-)
rename src/main/scala/leon/{LeonFatalError.scala => LeonExceptions.scala} (59%)
create mode 100644 src/main/scala/leon/solvers/SolverUnsupportedError.scala
diff --git a/src/main/scala/leon/LeonFatalError.scala b/src/main/scala/leon/LeonExceptions.scala
similarity index 59%
rename from src/main/scala/leon/LeonFatalError.scala
rename to src/main/scala/leon/LeonExceptions.scala
index 70646a94c..eeaadd09a 100644
--- a/src/main/scala/leon/LeonFatalError.scala
+++ b/src/main/scala/leon/LeonExceptions.scala
@@ -2,8 +2,13 @@
package leon
+import purescala.Common.Tree
+
case class LeonFatalError(msg: Option[String]) extends Exception(msg.getOrElse(""))
object LeonFatalError {
def apply(msg: String) = new LeonFatalError(Some(msg))
}
+
+class Unsupported(t: Tree, msg: String)(implicit ctx: LeonContext)
+ extends Exception(s"${t.asString}@${t.getPos} $msg")
\ No newline at end of file
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 3d7fbe17d..54e3485d6 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -178,9 +178,12 @@ class CompilationUnit(val ctx: LeonContext,
}
l
- // Just slightly overkill...
case _ =>
- compileExpression(e, Seq()).evalToJVM(Seq(),monitor)
+ throw LeonFatalError("Unexpected expression in exprToJVM")
+
+ // Just slightly overkill...
+ //case _ =>
+ // compileExpression(e, Seq()).evalToJVM(Seq(),monitor)
}
// Note that this may produce untyped expressions! (typically: sets, maps)
@@ -274,9 +277,9 @@ class CompilationUnit(val ctx: LeonContext,
var compiledN = 0
- def compileExpression(e: Expr, args: Seq[Identifier]): CompiledExpression = {
+ def compileExpression(e: Expr, args: Seq[Identifier])(implicit ctx: LeonContext): CompiledExpression = {
if(e.getType == Untyped) {
- throw new IllegalArgumentException(s"Cannot compile untyped expression [$e].")
+ throw new Unsupported(e, s"Cannot compile untyped expression.")
}
compiledN += 1
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 72a905b82..0cf311562 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -236,7 +236,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
val newExpr = replaceFromIDs(map, expression)
- val ce = unit.compileExpression(newExpr, Seq(tid))
+ val ce = unit.compileExpression(newExpr, Seq(tid))(ctx)
Some((args : Expr) => {
try {
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index caf22c1e9..64456226b 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -36,7 +36,7 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
ctx.timers.evaluators.codegen.compilation.start()
try {
- val ce = unit.compileExpression(expression, argorder)
+ val ce = unit.compileExpression(expression, argorder)(ctx)
Some((args : Seq[Expr]) => {
try {
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 4399dc2bf..f04cbc99f 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -33,8 +33,15 @@ object Common {
* The name is stored in the decoded (source code) form rather than encoded (JVM) form.
* The type may be left blank (Untyped) for Identifiers that are not variables.
*/
- class Identifier private[Common](val name: String, val globalId: Int, val id: Int, val tpe: TypeTree, alwaysShowUniqueID: Boolean = false) extends Tree with Typed {
- self : Serializable =>
+ class Identifier private[Common](
+ val name: String,
+ private[Common] val globalId: Int,
+ private[Common] val id: Int,
+ private val tpe: TypeTree,
+ private val alwaysShowUniqueID: Boolean = false
+ ) extends Tree with Typed with Ordered[Identifier] {
+
+ self: Serializable =>
val getType = tpe
@@ -47,27 +54,27 @@ object Common {
override def hashCode: Int = globalId
override def toString: String = {
- if(alwaysShowUniqueID) {
- name + (if(id > 0) id else "")
+ if (alwaysShowUniqueID) {
+ name + (if (id > 0) id else "")
} else {
name
}
}
- def uniqueName : String = name + id
+ def uniqueNameDelimited(delim: String) = name + delim + id
- def toVariable : Variable = Variable(this)
+ def uniqueName: String = uniqueNameDelimited("")
- def freshen: Identifier = FreshIdentifier(name, tpe, alwaysShowUniqueID).copiedFrom(this)
+ def toVariable: Variable = Variable(this)
- }
-
- implicit object IdentifierOrdering extends Ordering[Identifier] {
- def compare(a: Identifier, b: Identifier) = {
- val ord = implicitly[Ordering[Tuple3[String, Int, Int]]]
+ def freshen: Identifier = FreshIdentifier(name, tpe, alwaysShowUniqueID).copiedFrom(this)
- ord.compare((a.name, a.id, a.globalId),
- (b.name, b.id, b.globalId))
+ override def compare(that: Identifier): Int = {
+ val ord = implicitly[Ordering[(String, Int, Int)]]
+ ord.compare(
+ (this.name, this.id, this.globalId),
+ (that.name, that.id, that.globalId)
+ )
}
}
diff --git a/src/main/scala/leon/solvers/ADTManager.scala b/src/main/scala/leon/solvers/ADTManager.scala
index 3339fe2b7..e811feaa1 100644
--- a/src/main/scala/leon/solvers/ADTManager.scala
+++ b/src/main/scala/leon/solvers/ADTManager.scala
@@ -49,9 +49,11 @@ class ADTManager(ctx: LeonContext) {
if (conflicts(t)) {
// There is no way to solve this, the type we requested is in conflict
- reporter.warning(s"Encountered ADT '$t' that can't be defined.")
- reporter.warning("It appears it has recursive references through non-structural types (such as arrays, maps, or sets).")
- throw new IllegalArgumentException
+ val str = "Encountered ADT that can't be defined.\n" +
+ "It appears it has recursive references through non-structural types (such as arrays, maps, or sets)."
+ val err = new Unsupported(t, str)(ctx)
+ reporter.warning(err.getMessage)
+ throw err
} else {
// We might be able to define some despite conflicts
if (conflicts.isEmpty) {
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 9f8aaace4..a9018b2de 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -5,7 +5,7 @@ package solvers
import utils.{DebugSectionSolver, Interruptible}
import purescala.Expressions._
-import purescala.Common.Identifier
+import leon.purescala.Common.{Tree, Identifier}
import verification.VC
trait Solver extends Interruptible {
@@ -33,6 +33,17 @@ trait Solver extends Interruptible {
def checkAssumptions(assumptions: Set[Expr]): Option[Boolean]
def getUnsatCore: Set[Expr]
+ protected def unsupported(t: Tree): Nothing = {
+ val err = SolverUnsupportedError(t, this, None)
+ leonContext.reporter.warning(err.getMessage)
+ throw err
+ }
+ protected def unsupported(t: Tree, str: String): Nothing = {
+ val err = SolverUnsupportedError(t, this, Some(str))
+ leonContext.reporter.warning(err.getMessage)
+ throw err
+ }
+
implicit val debugSection = DebugSectionSolver
private[solvers] def debugS(msg: String) = {
diff --git a/src/main/scala/leon/solvers/SolverUnsupportedError.scala b/src/main/scala/leon/solvers/SolverUnsupportedError.scala
new file mode 100644
index 000000000..5d519160d
--- /dev/null
+++ b/src/main/scala/leon/solvers/SolverUnsupportedError.scala
@@ -0,0 +1,15 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package solvers
+
+import purescala.Common.Tree
+
+object SolverUnsupportedError {
+ def msg(t: Tree, s: Solver, reason: Option[String]) = {
+ s" is unsupported by solver ${s.name}" + reason.map(":\n " + _ ).getOrElse("")
+ }
+}
+
+case class SolverUnsupportedError(t: Tree, s: Solver, reason: Option[String] = None)
+ extends Unsupported(t, SolverUnsupportedError.msg(t,s,reason))(s.leonContext)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index 83076f8dc..86da0be80 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -6,6 +6,7 @@ package solvers.smtlib
import leon.purescala.Common.Identifier
import leon.purescala.Definitions.Program
import leon.purescala.Expressions.Expr
+import leon.solvers.SolverUnsupportedError
import smtlib.parser.Commands.{Assert => SMTAssert}
import smtlib.parser.Terms.{Exists => SMTExists}
@@ -31,7 +32,7 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
override def assertCnstr(e: Expr) = try {
sendCommand(SMTAssert(quantifiedTerm(SMTExists, e)))
} catch {
- case _: IllegalArgumentException =>
+ case _ : SolverUnsupportedError =>
addError()
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 6bc216b53..232867dcc 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -3,6 +3,7 @@
package leon
package solvers.smtlib
+import leon.solvers.SolverUnsupportedError
import purescala._
import Expressions._
import Definitions._
@@ -51,7 +52,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
Seq(bodyAssert) ++ specAssert
} catch {
- case _ : IllegalArgumentException =>
+ case _ : SolverUnsupportedError =>
addError()
Seq()
}
@@ -79,7 +80,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
(p.id, id2sym(p.id): Term)
}.toMap)
} catch {
- case _: IllegalArgumentException =>
+ case _: SolverUnsupportedError =>
addError()
toSMT(Error(tfd.body.get.getType, ""))(Map())
}
@@ -101,7 +102,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
try {
sendCommand(SMTAssert(quantifiedTerm(SMTForall, term)))
} catch {
- case _ : IllegalArgumentException =>
+ case _ : SolverUnsupportedError =>
addError()
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index 801a71662..fa11aa421 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -96,9 +96,9 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
FiniteSet(se ++ selems, base)
case (FunctionApplication(SimpleSymbol(SSymbol("union")), elems), SetType(base)) =>
- FiniteSet(elems.map(fromSMT(_, tpe) match {
+ FiniteSet(elems.flatMap(fromSMT(_, tpe) match {
case FiniteSet(elems, _) => elems
- }).flatten.toSet, base)
+ }).toSet, base)
// FIXME (nicolas)
// some versions of CVC4 seem to generate array constants with "as const" notation instead of the __array_store_all__
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 25b7a6c0f..29540f2f4 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -28,7 +28,6 @@ import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
import _root_.smtlib.theories._
import _root_.smtlib.{Interpreter => SMTInterpreter}
-
abstract class SMTLIBSolver(val context: LeonContext,
val program: Program) extends Solver with NaiveAssumptionSolver {
@@ -109,7 +108,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
protected val library = program.library
- protected def id2sym(id: Identifier): SSymbol = SSymbol(id.name+"!"+id.id)
+ protected def id2sym(id: Identifier): SSymbol = SSymbol(id.uniqueNameDelimited("!"))
protected def freshSym(id: Identifier): SSymbol = freshSym(id.name)
protected def freshSym(name: String): SSymbol = id2sym(FreshIdentifier(name))
@@ -160,7 +159,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
protected def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match {
case SetType(base) =>
if (r.default != BooleanLiteral(false)) {
- unsupported("Co-finite sets are not supported.")
+ unsupported(r, "Solver returned a co-finite set which is not supported.")
}
require(r.keyTpe == base, s"Type error in solver model, expected $base, found ${r.keyTpe}")
@@ -176,7 +175,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
// 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("Co-finite maps are 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, found ${r.keyTpe}")
@@ -186,13 +185,8 @@ abstract class SMTLIBSolver(val context: LeonContext,
}.toSeq
FiniteMap(elems, from, to)
- case _ =>
- unsupported("Unable to extract from raw array for "+tpe)
- }
-
- protected def unsupported(str: String) = {
- reporter.warning(s"Unsupported in smt-$targetName: $str")
- throw new IllegalArgumentException(str)
+ case other =>
+ unsupported(other, "Unable to extract from raw array for "+tpe)
}
protected def declareSort(t: TypeTree): Sort = {
@@ -223,8 +217,8 @@ abstract class SMTLIBSolver(val context: LeonContext,
case _: ClassType | _: TupleType | _: ArrayType | UnitType =>
declareStructuralSort(tpe)
- case _ =>
- unsupported("Sort "+t)
+ case other =>
+ unsupported(other, s"Could not transform $other into an SMT sort")
}
}
}
@@ -565,7 +559,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
)
}
case o =>
- unsupported(s"Tree ${o.asString}")
+ unsupported(o, "")
}
}
@@ -605,7 +599,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
case cct: CaseClassType =>
CaseClass(cct, Nil)
case t =>
- unsupported("woot? for a single constructor for non-case-object: "+t.asString)
+ unsupported(t, "woot? for a single constructor for non-case-object")
}
case (SimpleSymbol(s), tpe) if lets contains s =>
@@ -613,7 +607,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
case (SimpleSymbol(s), _) =>
variables.getA(s).map(_.toVariable).getOrElse {
- unsupported("Unknown symbol: "+s)
+ reporter.fatalError("Unknown symbol: "+s)
}
case (FunctionApplication(SimpleSymbol(SSymbol("ite")), Seq(cond, thenn, elze)), t) =>
@@ -649,7 +643,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
}
case t =>
- unsupported("Woot? structural type that is non-structural: "+t)
+ unsupported(t, "Woot? structural type that is non-structural")
}
// EK: Since we have no type information, we cannot do type-directed
@@ -676,13 +670,13 @@ abstract class SMTLIBSolver(val context: LeonContext,
}
case _ =>
- unsupported("Function "+app+" not handled in fromSMT: "+s)
+ reporter.fatalError("Function "+app+" not handled in fromSMT: "+s)
}
}
case (QualifiedIdentifier(id, sort), tpe) =>
- unsupported("Unhandled case in fromSMT: " + id +": "+sort +" ("+tpe+")")
+ reporter.fatalError("Unhandled case in fromSMT: " + id +": "+sort +" ("+tpe+")")
case _ =>
- unsupported("Unhandled case in fromSMT: " + (s, tpe))
+ reporter.fatalError("Unhandled case in fromSMT: " + (s, tpe))
}
@@ -719,7 +713,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
val term = toSMT(expr)(Map())
sendCommand(SMTAssert(term))
} catch {
- case i : IllegalArgumentException =>
+ case _ : SolverUnsupportedError =>
// Store that there was an error. Now all following check()
// invocations will return None
addError()
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
index b520dfe5b..2ec571f1e 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
@@ -3,6 +3,7 @@
package leon
package solvers.smtlib
+import leon.solvers.SolverUnsupportedError
import purescala._
import DefOps._
import Definitions._
@@ -63,7 +64,7 @@ class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program)
try {
sendCommand(SMTAssert(quantifiedTerm(SMTForall, term)))
} catch {
- case _ : IllegalArgumentException =>
+ case _ : SolverUnsupportedError =>
addError()
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index 3a7b345fb..36c4523da 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -79,7 +79,7 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve
// Need to recover value form function model
fromRawArray(extractRawArray(letDefs(k), tpe), tpe)
} else {
- unsupported(" as-array on non-function or unknown symbol "+k)
+ throw LeonFatalError("Array on non-function or unknown symbol "+k)
}
case (FunctionApplication(
@@ -141,7 +141,7 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve
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+")")
+ case _ => unsupported(tpe, "Unsupported type for (un)packing into raw arrays (got kinds "+akind+" -> "+rkind+")")
}
def extractCases(e: Term): (Map[Expr, Expr], Expr) = e match {
@@ -157,7 +157,7 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve
RawArrayValue(argTpe, cases, default)
case _ =>
- unsupported("Unable to extract "+s)
+ throw LeonFatalError("Unable to extract "+s)
}
// EK: We use get-model instead in order to extract models for arrays
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 9eb08e152..9492e8b93 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -259,11 +259,7 @@ trait AbstractZ3Solver extends Solver {
}
case other =>
- sorts.cachedB(other) {
- reporter.warning(other.getPos, "Resorting to uninterpreted type for : " + other.asString)
- val symbol = z3.mkIntSymbol(FreshIdentifier("unint").globalId)
- z3.mkUninterpretedSort(symbol)
- }
+ throw SolverUnsupportedError(other, this)
}
protected[leon] def toZ3Formula(expr: Expr, initialMap: Map[Identifier, Z3AST] = Map.empty): Z3AST = {
@@ -545,10 +541,8 @@ trait AbstractZ3Solver extends Solver {
case gv @ GenericValue(tp, id) =>
z3.mkApp(genericValueToDecl(gv))
- case _ => {
- reporter.warning(ex.getPos, "Can't handle this in translation to Z3: " + ex.asString)
- throw new IllegalArgumentException
- }
+ case other =>
+ unsupported(other)
}
rec(expr)
@@ -587,13 +581,11 @@ trait AbstractZ3Solver extends Solver {
tpe match {
case Int32Type => IntLiteral(hexa.toInt)
case CharType => CharLiteral(hexa.toInt.toChar)
- case _ =>
- reporter.warning("Unexpected target type for BV value: " + tpe.asString)
- throw new IllegalArgumentException
+ case other =>
+ unsupported(other, "Unexpected target type for BV value")
}
case None => {
- reporter.warning("Z3NumeralIntAST with None: " + t)
- throw new IllegalArgumentException
+ throw LeonFatalError(s"Could not translate hexadecimal Z3 numeral $t")
}
}
} else {
@@ -607,12 +599,10 @@ 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.asString)
- throw new IllegalArgumentException
+ reporter.fatalError("Unexpected target type for BV value: " + tpe.asString)
}
case None => {
- reporter.warning("Z3NumeralIntAST with None: " + t)
- throw new IllegalArgumentException
+ reporter.fatalError(s"Could not translate Z3NumeralIntAST numeral $t")
}
}
}
@@ -648,12 +638,12 @@ trait AbstractZ3Solver extends Solver {
case (s : IntLiteral, RawArrayValue(_, elems, default)) =>
val entries = elems.map {
case (IntLiteral(i), v) => i -> v
- case _ => throw new IllegalArgumentException
+ case _ => reporter.fatalError("Translation from Z3 to Array failed")
}
finiteArray(entries, Some(s, default), to)
case _ =>
- throw new IllegalArgumentException
+ reporter.fatalError("Translation from Z3 to Array failed")
}
}
} else {
@@ -667,7 +657,7 @@ trait AbstractZ3Solver extends Solver {
}
RawArrayValue(from, entries, default)
- case None => throw new IllegalArgumentException
+ case None => reporter.fatalError("Translation from Z3 to Array failed")
}
case tp: TypeParameter =>
@@ -680,8 +670,7 @@ 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.asString+")")
- throw new IllegalArgumentException
+ unsupported(r, "Solver returned a co-finite set which is not supported.")
}
require(r.keyTpe == from, s"Type error in solver model, expected ${from.asString}, found ${r.keyTpe.asString}")
@@ -696,7 +685,7 @@ trait AbstractZ3Solver extends Solver {
case FunctionType(fts, tt) =>
model.getArrayValue(t) match {
- case None => throw new IllegalArgumentException
+ case None => reporter.fatalError("Translation from Z3 to function value failed")
case Some((map, elseZ3Value)) =>
val leonElseValue = rec(elseZ3Value, tt)
val leonMap = map.toSeq.map(p => rec(p._1, tupleTypeWrap(fts)) -> rec(p._2, tt))
@@ -705,7 +694,7 @@ trait AbstractZ3Solver extends Solver {
case tpe @ SetType(dt) =>
model.getSetValue(t) match {
- case None => throw new IllegalArgumentException
+ case None => reporter.fatalError("Translation from Z3 to set failed")
case Some(set) =>
val elems = set.map(e => rec(e, dt))
FiniteSet(elems, dt)
@@ -736,17 +725,17 @@ trait AbstractZ3Solver extends Solver {
// case OpIDiv => Division(rargs(0), rargs(1))
// 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.asString)
- reporter.warning("Tree: " + t)
- reporter.warning("The arguments are : " + args)
- throw new IllegalArgumentException
+ reporter.fatalError(
+ s"""|Don't know what to do with this declKind: $other
+ |Expected type: ${tpe.asString}
+ |Tree: $t
+ |The arguments are: $args""".stripMargin
+ )
}
}
}
case _ =>
- reporter.warning("Can't handle "+t)
- throw new IllegalArgumentException
+ reporter.fatalError(s"Don't know what to do with this Z3 tree: $t")
}
}
rec(tree, tpe)
@@ -756,7 +745,7 @@ trait AbstractZ3Solver extends Solver {
try {
Some(fromZ3Formula(model, tree, tpe))
} catch {
- case e: IllegalArgumentException => None
+ case e: Unsupported => None
}
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index eef9ffb90..a1fc339da 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -218,7 +218,7 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
solver.assertCnstr(cl)
}
} catch {
- case _: IllegalArgumentException =>
+ case _: SolverUnsupportedError =>
addError()
}
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 480960777..f745abec9 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -192,7 +192,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
grammar.printProductions(printer)
}
- bsOrdered = bs.toSeq.sortBy(_.id)
+ bsOrdered = bs.toSeq.sorted
setCExpr(computeCExpr())
}
@@ -545,7 +545,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
for ((c, alts) <- cTree) {
val activeBs = alts.map(_._1).filter(isBActive)
- val either = for (a1 <- activeBs; a2 <- activeBs if a1.globalId < a2.globalId) yield {
+ val ord = implicitly[Ordering[Identifier]]
+ val either = for (a1 <- activeBs; a2 <- activeBs if a1 < a2) yield {
Or(Not(a1.toVariable), Not(a2.toVariable))
}
diff --git a/src/test/scala/leon/test/helpers/WithLikelyEq.scala b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
index aee9e7671..d499f5617 100644
--- a/src/test/scala/leon/test/helpers/WithLikelyEq.scala
+++ b/src/test/scala/leon/test/helpers/WithLikelyEq.scala
@@ -32,7 +32,7 @@ trait WithLikelyEq {
def checkLikelyEq(ctx: LeonContext, pgm: Program = Program.empty)(e1: Expr, e2: Expr, pre: Option[Expr] = None, values: Map[Identifier, Expr] = Map()): Unit = {
val evaluator = new DefaultEvaluator(ctx, pgm)
- val freeVars = (variablesOf(e1) ++ variablesOf(e2)).toSeq.sortBy(_.globalId)
+ val freeVars = (variablesOf(e1) ++ variablesOf(e2)).toSeq.sorted
if (freeVars.isEmpty) {
val r1 = evaluator.eval(e1)
--
GitLab