From 1249ca17488e86c4f8349083b645faf68c154093 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 8 Aug 2016 15:05:13 +0200
Subject: [PATCH] Tidy up
---
.../inox/solvers/smtlib/CVC4Target.scala | 29 ++++++-----
.../inox/solvers/smtlib/SMTLIBSolver.scala | 10 ++--
.../inox/solvers/smtlib/SMTLIBTarget.scala | 8 +--
.../scala/inox/solvers/smtlib/Z3Target.scala | 52 ++++++++-----------
4 files changed, 46 insertions(+), 53 deletions(-)
diff --git a/src/main/scala/inox/solvers/smtlib/CVC4Target.scala b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
index 3936ea873..e9961b451 100644
--- a/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
+++ b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
@@ -6,7 +6,7 @@ package smtlib
import org.apache.commons.lang3.StringEscapeUtils
-import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, Forall => SMTForall, _}
+import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.Commands._
import _root_.smtlib.interpreters.CVC4Interpreter
import _root_.smtlib.theories.experimental.Sets
@@ -156,19 +156,22 @@ trait CVC4Target extends SMTLIBTarget {
}
}
- case SubsetOf(ss, s) => Sets.Subset(toSMT(ss), toSMT(s))
- case ElementOfSet(e, s) => Sets.Member(toSMT(e), toSMT(s))
- 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(StringEscapeUtils.escapeJava(v))
- case StringLength(a) => Strings.Length(toSMT(a))
- case StringConcat(a, b) => Strings.Concat(toSMT(a), toSMT(b))
+ case SubsetOf(ss, s) => Sets.Subset(toSMT(ss), toSMT(s))
+ case ElementOfSet(e, s) => Sets.Member(toSMT(e), toSMT(s))
+ 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))
+
+ /** String operations */
+ case StringLiteral(v) =>
+ declareSort(StringType)
+ Strings.StringLit(StringEscapeUtils.escapeJava(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)))
+ 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/inox/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala
index 4e3597e5a..2dd091e00 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala
@@ -4,9 +4,9 @@ package inox
package solvers
package smtlib
-import _root_.smtlib.parser.Commands.{Assert => SMTAssert, FunDef => SMTFunDef, _}
+import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
import _root_.smtlib.parser.Terms.{Identifier => _, _}
-import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
+import _root_.smtlib.parser.CommandsResponses._
trait SMTLIBSolver extends Solver with SMTLIBTarget {
@@ -33,7 +33,7 @@ trait SMTLIBSolver extends Solver with SMTLIBTarget {
variablesOf(expr).foreach(declareVariable)
val term = toSMT(expr)(Map())
- emit(SMTAssert(term))
+ emit(Assert(term))
} catch {
case _ : SolverUnsupportedError =>
// Store that there was an error. Now all following check()
@@ -44,7 +44,7 @@ trait SMTLIBSolver extends Solver with SMTLIBTarget {
override def reset() = {
emit(Reset(), rawOut = true) match {
- case ErrorResponse(msg) =>
+ case Error(msg) =>
reporter.warning(s"Failed to reset $name: $msg")
throw new CantResetException(this)
case _ =>
@@ -105,7 +105,7 @@ trait SMTLIBSolver extends Solver with SMTLIBTarget {
}
}
- def checkAssumptions(config: Configuration)(assumptions: Set[Trees]): config.Response[Model, Cores] = ???
+ def checkAssumptions(config: Configuration)(assumptions: Set[Trees]): config.Response[Model, Cores] = ??? //TODO
def push(): Unit = {
constructors.push()
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
index 52c3ec00c..9077286e7 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -4,7 +4,6 @@ package inox
package solvers
package smtlib
-import inox.utils.Interruptible
import utils._
import _root_.smtlib.common._
@@ -12,19 +11,16 @@ import _root_.smtlib.printer.{ RecursivePrinter => SMTPrinter }
import _root_.smtlib.parser.Commands.{
Constructor => SMTConstructor,
FunDef => SMTFunDef,
- Assert => SMTAssert,
_
}
import _root_.smtlib.parser.Terms.{
Forall => SMTForall,
- Exists => _,
Identifier => SMTIdentifier,
Let => SMTLet,
_
}
-import _root_.smtlib.parser.CommandsResponses.{ Error => ErrorResponse, _ }
+import _root_.smtlib.parser.CommandsResponses._
import _root_.smtlib.theories.{Constructors => SmtLibConstructors, _}
-import _root_.smtlib.theories.experimental._
import _root_.smtlib.interpreters.ProcessInterpreter
trait SMTLIBTarget extends Interruptible with ADTManagers {
@@ -94,7 +90,7 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
o.flush()
}
interpreter.eval(cmd) match {
- case err @ ErrorResponse(msg) if !hasError && !interrupted && !rawOut =>
+ case err @ Error(msg) if !hasError && !interrupted && !rawOut =>
ctx.reporter.warning(s"Unexpected error from $targetName solver: $msg")
//println(Thread.currentThread().getStackTrace.map(_.toString).take(10).mkString("\n"))
// Store that there was an error. Now all following check()
diff --git a/src/main/scala/inox/solvers/smtlib/Z3Target.scala b/src/main/scala/inox/solvers/smtlib/Z3Target.scala
index 2a59c4a97..179262886 100644
--- a/src/main/scala/inox/solvers/smtlib/Z3Target.scala
+++ b/src/main/scala/inox/solvers/smtlib/Z3Target.scala
@@ -34,7 +34,19 @@ trait Z3Target extends SMTLIBTarget {
protected val extSym = SSymbol("_")
- protected var setSort: Option[SSymbol] = None
+ protected lazy val setSort: SSymbol = {
+ val s = SSymbol("Set")
+ val t = SSymbol("T")
+
+ val arraySort = Sort(
+ SMTIdentifier(SSymbol("Array")),
+ Seq(Sort(SMTIdentifier(t)), BoolSort())
+ )
+
+ val cmd = DefineSort(s, Seq(t), arraySort)
+ emit(cmd)
+ s
+ }
override protected def declareSort(t: Type): Sort = {
val tpe = normalizeType(t)
@@ -42,7 +54,7 @@ trait Z3Target extends SMTLIBTarget {
tpe match {
case SetType(base) =>
super.declareSort(BooleanType)
- declareSetSort(base)
+ Sort(SMTIdentifier(setSort), Seq(declareSort(base)))
case BagType(base) =>
declareSort(MapType(base, IntegerType))
case _ =>
@@ -51,29 +63,8 @@ trait Z3Target extends SMTLIBTarget {
}
}
- protected def declareSetSort(of: Type): Sort = {
- setSort match {
- case None =>
- val s = SSymbol("Set")
- val t = SSymbol("T")
- setSort = Some(s)
-
- val arraySort = Sort(SMTIdentifier(SSymbol("Array")),
- Seq(Sort(SMTIdentifier(t)), BoolSort()))
-
- val cmd = DefineSort(s, Seq(t), arraySort)
- emit(cmd)
-
- case _ =>
- }
-
- Sort(SMTIdentifier(setSort.get), Seq(declareSort(of)))
- }
-
override protected def fromSMT(t: Term, otpe: Option[Type] = None)
(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): Expr = {
-
-
(t, otpe) match {
case (QualifiedIdentifier(ExtendedIdentifier(SSymbol("as-array"), k: SSymbol), _), Some(tpe)) =>
if (letDefs contains k) {
@@ -113,8 +104,7 @@ trait Z3Target extends SMTLIBTarget {
* ===== Set operations =====
*/
case fs @ FiniteSet(elems, base) =>
- val st @ SetType(base) = fs.getType
- declareSort(st)
+ declareSort(fs.getType)
toSMT(FiniteMap(elems map ((_, BooleanLiteral(true))), BooleanLiteral(false), BooleanType))
case SubsetOf(ss, s) =>
@@ -151,8 +141,10 @@ trait Z3Target extends SMTLIBTarget {
val bid = FreshIdentifier("b", true)
val eid = FreshIdentifier("e", true)
val (bSym, eSym) = (id2sym(bid), id2sym(eid))
- SMTLet(VarBinding(bSym, toSMT(b)), Seq(VarBinding(eSym, toSMT(e))), ArraysEx.Store(bSym, eSym,
- Ints.Add(ArraysEx.Select(bSym, eSym), Ints.NumeralLit(1))))
+ SMTLet(
+ VarBinding(bSym, toSMT(b)), Seq(VarBinding(eSym, toSMT(e))),
+ ArraysEx.Store(bSym, eSym, Ints.Add(ArraysEx.Select(bSym, eSym), Ints.NumeralLit(1)))
+ )
case MultiplicityInBag(e, b) =>
ArraysEx.Select(toSMT(b), toSMT(e))
@@ -175,8 +167,10 @@ trait Z3Target extends SMTLIBTarget {
val all2 = ArrayConst(declareSort(IntegerType), Ints.NumeralLit(2))
- SMTLet(VarBinding(dSym, ArrayMap(minus, toSMT(b1), toSMT(b2))), Seq(),
- ArrayMap(div, ArrayMap(plus, dSym, ArrayMap(abs, dSym)), all2))
+ SMTLet(
+ VarBinding(dSym, ArrayMap(minus, toSMT(b1), toSMT(b2))), Seq(),
+ ArrayMap(div, ArrayMap(plus, dSym, ArrayMap(abs, dSym)), all2)
+ )
case _ =>
super.toSMT(e)
--
GitLab