From 767204a7e69ffdcc6f0ce33eff8b7bc0b6193ea3 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 30 Sep 2015 13:40:41 +0200
Subject: [PATCH] Cleanup smtlib
---
.../scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala | 1 -
.../leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala | 4 ----
src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala | 1 -
.../scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala | 1 -
.../scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala | 5 +----
src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala | 7 -------
.../leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala | 6 ------
src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala | 4 ++--
src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala | 3 ---
9 files changed, 3 insertions(+), 29 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index 830216880..f02cce59c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -3,7 +3,6 @@
package leon
package solvers.smtlib
-import purescala.Common.Identifier
import purescala.Definitions.Program
import purescala.Expressions.Expr
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
index b882bafe2..737b8535c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
@@ -4,12 +4,8 @@ package leon
package solvers
package smtlib
-import purescala.Common._
import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Constructors._
-import purescala.Types._
import purescala.Definitions._
import purescala.DefOps.typedTransitiveCallees
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index d5515b42e..620a294ed 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -6,7 +6,6 @@ package smtlib
import purescala.Common._
import purescala.Expressions._
-import purescala.Extractors._
import purescala.Constructors._
import purescala.Types._
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
index fbaa73cc2..ba0187239 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
@@ -5,7 +5,6 @@ package solvers
package smtlib
import purescala.Common.Identifier
-import purescala.Expressions.Expr
import verification.VC
trait SMTLIBQuantifiedSolver {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
index 7aa281b67..b6d6fbfb3 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
@@ -8,11 +8,8 @@ import purescala.Expressions._
import purescala.Definitions._
import purescala.Constructors._
import purescala.ExprOps._
-import purescala.DefOps.typedTransitiveCallees
-import _root_.smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _}
-import _root_.smtlib.parser.Terms.{Exists => SMTExists, Forall => SMTForall, _ }
-import _root_.smtlib.theories.Core.Equals
+import _root_.smtlib.parser.Commands.{Assert => _, FunDef => _, _}
trait SMTLIBQuantifiedTarget extends SMTLIBTarget {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index edb558e95..05476ac11 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -4,21 +4,14 @@ package leon
package solvers
package smtlib
-import utils._
import purescala.Common._
import purescala.Expressions._
-import purescala.Extractors._
import purescala.ExprOps._
-import purescala.Types._
-import purescala.Constructors._
import purescala.Definitions._
-import _root_.smtlib.common._
import _root_.smtlib.parser.Commands.{Assert => SMTAssert, _}
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
-import _root_.smtlib.theories._
-import _root_.smtlib.interpreters.ProcessInterpreter
abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
extends Solver with SMTLIBTarget with NaiveAssumptionSolver {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
index 0735b2396..4c8eedce5 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
@@ -4,19 +4,13 @@ package leon
package solvers
package smtlib
-import purescala.Common._
import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Constructors._
-import purescala.Types._
import purescala.Definitions._
import purescala.DefOps.typedTransitiveCallees
import _root_.smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _}
import _root_.smtlib.parser.Terms.{Exists => SMTExists, Forall => SMTForall, _ }
-import _root_.smtlib.theories.Core.{Equals => SMTEquals}
-import _root_.smtlib.parser.Commands._
trait SMTLIBZ3QuantifiedTarget extends SMTLIBZ3Target with SMTLIBQuantifiedTarget {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index 0e289ff80..86cf40f47 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -8,10 +8,10 @@ import purescala.Definitions.Program
import purescala.Common.Identifier
import purescala.Expressions.Expr
-import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
+import _root_.smtlib.parser.Terms.{Identifier => _, _}
import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
import _root_.smtlib.parser.CommandsResponses.GetModelResponseSuccess
-import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
+import _root_.smtlib.theories.Core.{Equals => _, _}
class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolver(context, program) with SMTLIBZ3Target {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 657100814..eac8f47f9 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -6,18 +6,15 @@ package smtlib
import purescala.Common._
import purescala.Expressions._
-import purescala.Extractors._
import purescala.Constructors._
import purescala.Types._
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
import _root_.smtlib.interpreters.Z3Interpreter
-import _root_.smtlib.parser.CommandsResponses.GetModelResponseSuccess
import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
import _root_.smtlib.theories.ArraysEx
-
trait SMTLIBZ3Target extends SMTLIBTarget {
def targetName = "z3"
--
GitLab