diff --git a/Data/SBV/Control/Query.hs b/Data/SBV/Control/Query.hs index 9b66f690b..fce28e802 100644 --- 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 index b688b9df3..45d92dba8 100644 --- 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 index 3cd696df5..12a386937 100644 --- 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)