Further trimming of imports

LeventErkok · Nov 6, 2024 · 8cc319a · 8cc319a
1 parent f5fe211
commit 8cc319a
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 6 deletions.
diff --git a/Data/SBV/Control/Query.hs b/Data/SBV/Control/Query.hs
@@ -23,9 +23,8 @@ module Data.SBV.Control.Query (
        send, ask, retrieveResponse
      , CheckSatResult(..), checkSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUnsatisfiableSet
      , getUnsatCore, getProof, getInterpolantMathSAT, getInterpolantZ3, getAbduct, getAbductNext, getAssignment, getOption
-     , freshVar, freshVar_
      , push, pop, getAssertionStackDepth
-     , inNewAssertionStack, echo, caseSplit, resetAssertions, exit, getAssertions, getValue, getUninterpretedValue, getModel, getSMTResult
+     , inNewAssertionStack, echo, caseSplit, resetAssertions, exit, getAssertions, getUninterpretedValue, getModel, getSMTResult
      , getLexicographicOptResults, getIndependentOptResults, getParetoOptResults, getAllSatResult, getUnknownReason, getObservables, ensureSat
      , SMTOption(..), SMTInfoFlag(..), SMTErrorBehavior(..), SMTReasonUnknown(..), SMTInfoResponse(..), getInfo
      , Logic(..), Assignment(..)

diff --git a/Data/SBV/Trans/Control.hs b/Data/SBV/Trans/Control.hs
@@ -17,15 +17,12 @@ module Data.SBV.Trans.Control (
      -- * User queries
        ExtractIO(..), MonadQuery(..), QueryT, Query, query
 
-     -- * Create a fresh variable
-     , freshVar_, freshVar
-
      -- * Checking satisfiability
      , CheckSatResult(..), checkSat, ensureSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUnsatisfiableSet
 
      -- * Querying the solver
      -- ** Extracting values
-     , getValue, getFunction, getUninterpretedValue, getModel, getAssignment, getSMTResult, getUnknownReason, getObservables
+     , getFunction, getUninterpretedValue, getModel, getAssignment, getSMTResult, getUnknownReason, getObservables
 
      -- ** Extracting the unsat core
      , getUnsatCore

diff --git a/Documentation/SBV/Examples/Transformers/SymbolicEval.hs b/Documentation/SBV/Examples/Transformers/SymbolicEval.hs
@@ -30,6 +30,8 @@
 
 module Documentation.SBV.Examples.Transformers.SymbolicEval where
 
+import Data.SBV (getValue)
+
 import Control.Monad.Except   (Except, ExceptT, MonadError, mapExceptT, runExceptT, throwError)
 import Control.Monad.Identity (Identity(runIdentity))
 import Control.Monad.IO.Class (MonadIO)