From 70362f1222f8515b574a00efeeecca8e0a1cd0e1 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 7 Nov 2016 13:29:39 +0100
Subject: [PATCH] Removed automatic complaining for unsupported in solvers
---
src/main/scala/inox/ast/Printers.scala | 7 ++++++-
src/main/scala/inox/solvers/Solver.scala | 8 ++------
src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala | 2 ++
3 files changed, 10 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala
index 27ac8db61..af0858fbc 100644
--- a/src/main/scala/inox/ast/Printers.scala
+++ b/src/main/scala/inox/ast/Printers.scala
@@ -239,7 +239,12 @@ trait Printers {
}
case fs @ FiniteSet(rs, _) => p"{${rs.distinct}}"
case fs @ FiniteBag(rs, _) => p"{${rs.toMap.toSeq}}"
- case fm @ FiniteMap(rs, _, _, _) => p"{${rs.toMap.toSeq}}"
+ case fm @ FiniteMap(rs, dflt, _, _) =>
+ if (rs.isEmpty) {
+ p"{* -> $dflt}"
+ } else {
+ p"{${rs.toMap.toSeq}, * -> $dflt}"
+ }
case Not(ElementOfSet(e, s)) => p"$e \u2209 $s"
case ElementOfSet(e, s) => p"$e \u2208 $s"
case SubsetOf(l, r) => p"$l \u2286 $r"
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index b90817b93..72b736e0c 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -39,15 +39,11 @@ trait AbstractSolver extends Interruptible {
extends Unsupported(t, SolverUnsupportedError.msg(t,reason))
protected def unsupported(t: Tree): Nothing = {
- val err = SolverUnsupportedError(t, None)
- reporter.warning(err.getMessage)
- throw err
+ throw SolverUnsupportedError(t, None)
}
protected def unsupported(t: Tree, str: String): Nothing = {
- val err = SolverUnsupportedError(t, Some(str))
- reporter.warning(err.getMessage)
- throw err
+ throw SolverUnsupportedError(t, Some(str))
}
def assertCnstr(expression: Trees): Unit
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
index dfbeebdaa..ad9f5daf9 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -322,8 +322,10 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
case al @ MapApply(a, i) =>
ArraysEx.Select(toSMT(a), toSMT(i))
+
case al @ MapUpdated(map, k, v) =>
ArraysEx.Store(toSMT(map), toSMT(k), toSMT(v))
+
case ra @ FiniteMap(elems, default, keyTpe, valueType) =>
val s = declareSort(ra.getType)
--
GitLab