From f793baedd02d5c72811e02e69f50acc9d462795c Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 31 Aug 2015 13:35:52 +0200
Subject: [PATCH] Remove some dead stuff
---
.../leon/purescala/ScopeSimplifier.scala | 2 +-
.../leon/solvers/smtlib/SMTLIBZ3Solver.scala | 4 +--
.../leon/solvers/z3/AbstractZ3Solver.scala | 26 ++++++++-----------
.../scala/leon/solvers/z3/FairZ3Solver.scala | 3 ---
4 files changed, 13 insertions(+), 22 deletions(-)
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 40102267f..7fb5699e3 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -12,7 +12,7 @@ class ScopeSimplifier extends Transformer {
case class Scope(inScope: Set[Identifier] = Set(), oldToNew: Map[Identifier, Identifier] = Map(), funDefs: Map[FunDef, FunDef] = Map()) {
def register(oldNew: (Identifier, Identifier)): Scope = {
- val (oldId, newId) = oldNew
+ val newId = oldNew._2
copy(inScope = inScope + newId, oldToNew = oldToNew + oldNew)
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index 36c4523da..67909f60d 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -8,10 +8,8 @@ import purescala._
import Common._
import Definitions.Program
import Expressions._
-import Extractors._
import Types._
import Constructors._
-import ExprOps.simplestValue
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
@@ -101,7 +99,7 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve
* ===== Set operations =====
*/
case fs @ FiniteSet(elems, base) =>
- val ss = declareSort(fs.getType)
+ declareSort(fs.getType)
toSMT(RawArrayValue(base, elems.map {
case k => k -> BooleanLiteral(true)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 9492e8b93..6aabf292f 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -23,7 +23,6 @@ import scala.collection.mutable.{Map => MutableMap}
// with a Z3 instance"
trait AbstractZ3Solver extends Solver {
- val context : LeonContext
val program : Program
val library = program.library
@@ -59,7 +58,7 @@ trait AbstractZ3Solver extends Solver {
override def interrupt() {
interrupted = true
if(z3 ne null) {
- z3.interrupt
+ z3.interrupt()
}
}
@@ -206,9 +205,9 @@ trait AbstractZ3Solver extends Solver {
sorts += RealType -> z3.mkRealSort
sorts += BooleanType -> z3.mkBoolSort
- testers.clear
- constructors.clear
- selectors.clear
+ testers.clear()
+ constructors.clear()
+ selectors.clear()
}
def normalizeType(t: TypeTree): TypeTree = {
@@ -276,12 +275,10 @@ trait AbstractZ3Solver extends Solver {
// TODO: Leave that as a specialization?
case LetTuple(ids, e, b) => {
- var ix = 1
- z3Vars = z3Vars ++ ids.map((id) => {
- val entry = id -> rec(tupleSelect(e, ix, ids.size))
- ix += 1
+ 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
@@ -293,7 +290,6 @@ trait AbstractZ3Solver extends Solver {
case me @ MatchExpr(s, cs) =>
rec(matchToIfThenElse(me))
-
case Let(i, e, b) => {
val re = rec(e)
z3Vars = z3Vars + (i -> re)
@@ -506,14 +502,14 @@ trait AbstractZ3Solver extends Solver {
* ===== Map operations =====
*/
case m @ FiniteMap(elems, from, to) =>
- val mt @ MapType(f, t) = normalizeType(m.getType)
+ 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 MapGet(m, k) =>
- val mt @ MapType(f, t) = normalizeType(m.getType)
+ val mt @ MapType(_, t) = normalizeType(m.getType)
typeToSort(mt)
val el = z3.mkSelect(rec(m), rec(k))
@@ -522,7 +518,7 @@ trait AbstractZ3Solver extends Solver {
selectors.toB(library.someType(t), 0)(el)
case MapIsDefinedAt(m, k) =>
- val mt @ MapType(f, t) = normalizeType(m.getType)
+ val mt @ MapType(_, t) = normalizeType(m.getType)
typeToSort(mt)
val el = z3.mkSelect(rec(m), rec(k))
@@ -530,7 +526,7 @@ trait AbstractZ3Solver extends Solver {
testers.toB(library.someType(t))(el)
case MapUnion(m1, FiniteMap(elems, _, _)) =>
- val mt @ MapType(f, t) = normalizeType(m1.getType)
+ val mt @ MapType(_, t) = normalizeType(m1.getType)
typeToSort(mt)
elems.foldLeft(rec(m1)) { case (m, (k,v)) =>
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index a1fc339da..89d19afb9 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -319,9 +319,6 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
// distinction is made inside.
case Some(false) =>
- //@mk this seems to be dead code
- val z3Core = solver.getUnsatCore()
-
def coreElemToBlocker(c: Z3AST): (Z3AST, Boolean) = {
z3.getASTKind(c) match {
case Z3AppAST(decl, args) =>
--
GitLab