Copyright  (c) Levent Erkok 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
 User queries
 Create a fresh variable
 Create a fresh array
 Checking satisfiability
 Querying the solver
 Getting solver information
 Entering and exiting assertion stack
 Higher level tactics
 Resetting the solver state
 Constructing assignments
 Terminating the query
 Controlling the solver behavior
 Miscellaneous
 Solver options
Control sublanguage for interacting with SMT solvers.
Synopsis
 class MonadIO m => ExtractIO m where
 class Monad m => MonadQuery m where
 queryState :: m State
 class Queriable m a b  a > b where
 class Fresh m a where
 type Query = QueryT IO
 query :: Query a > Symbolic a
 freshVar_ :: SymVal a => Query (SBV a)
 freshVar :: SymVal a => String > Query (SBV a)
 freshArray_ :: (SymArray array, HasKind a, HasKind b) => Maybe (SBV b) > Query (array a b)
 freshArray :: (SymArray array, HasKind a, HasKind b) => String > Maybe (SBV b) > Query (array a b)
 data CheckSatResult
 checkSat :: Query CheckSatResult
 ensureSat :: Query ()
 checkSatUsing :: String > Query CheckSatResult
 checkSatAssuming :: [SBool] > Query CheckSatResult
 checkSatAssumingWithUnsatisfiableSet :: [SBool] > Query (CheckSatResult, Maybe [SBool])
 class SMTValue a where
 sexprToVal :: SExpr > Maybe a
 getValue :: SMTValue a => SBV a > Query a
 registerUISMTFunction :: (MonadIO m, SolverContext m, MonadSymbolic m) => SMTFunction fun a r => fun > m ()
 getFunction :: SMTFunction fun a r => fun > Query ([(a, r)], r)
 getUninterpretedValue :: HasKind a => SBV a > Query String
 getModel :: Query SMTModel
 getAssignment :: Query [(String, Bool)]
 getSMTResult :: Query SMTResult
 getUnknownReason :: Query SMTReasonUnknown
 getObservables :: Query [(String, CV)]
 getUnsatCore :: Query [String]
 getProof :: Query String
 getInterpolant :: [String] > Query String
 getAssertions :: Query [String]
 data SMTInfoFlag
 data SMTErrorBehavior
 data SMTInfoResponse
 getInfo :: SMTInfoFlag > Query SMTInfoResponse
 getOption :: (a > SMTOption) > Query (Maybe SMTOption)
 getAssertionStackDepth :: Query Int
 push :: Int > Query ()
 pop :: Int > Query ()
 inNewAssertionStack :: Query a > Query a
 caseSplit :: Bool > [(String, SBool)] > Query (Maybe (String, SMTResult))
 resetAssertions :: Query ()
 (>) :: SymVal a => SBV a > a > Assignment
 mkSMTResult :: [Assignment] > Query SMTResult
 exit :: Query ()
 ignoreExitCode :: SMTConfig > Bool
 timeout :: Int > Query a > Query a
 queryDebug :: [String] > Query ()
 echo :: String > Query ()
 io :: IO a > Query a
 data SMTOption
 = DiagnosticOutputChannel FilePath
  ProduceAssertions Bool
  ProduceAssignments Bool
  ProduceProofs Bool
  ProduceInterpolants Bool
  ProduceUnsatAssumptions Bool
  ProduceUnsatCores Bool
  RandomSeed Integer
  ReproducibleResourceLimit Integer
  SMTVerbosity Integer
  OptionKeyword String [String]
  SetLogic Logic
  SetInfo String [String]
Documentation
In certain cases, the user might want to take over the communication with the solver, programmatically querying the engine and issuing commands accordingly. Queries can be extremely powerful as they allow direct control of the solver. Here's a simple example:
module Test where import Data.SBV import Data.SBV.Control  queries require this module to be imported! test :: Symbolic (Maybe (Integer, Integer)) test = do x < sInteger "x"  a free variable named "x" y < sInteger "y"  a free variable named "y"  require the sum to be 10 constrain $ x + y .== 10  Go into the Query mode query $ do  Query the solver: Are the constraints satisfiable? cs < checkSat case cs of Unk > error "Solver said unknown!" Unsat > return Nothing  no solution! Sat >  Query the values: do xv < getValue x yv < getValue y io $ putStrLn $ "Solver returned: " ++ show (xv, yv)  We can now add new constraints,  Or perform arbitrary computations and tell  the solver anything we want! constrain $ x .> literal xv + literal yv  call checkSat again csNew < checkSat case csNew of Unk > error "Solver said unknown!" Unsat > return Nothing Sat > do xv2 < getValue x yv2 < getValue y return $ Just (xv2, yv2)
Note the type of test
: it returns an optional pair of integers in the Symbolic
monad. We turn
it into an IO value with the runSMT
function: (There's also runSMTWith
that uses a user specified
solver instead of the default.)
pair :: IO (Maybe (Integer, Integer)) pair = runSMT test
When run, this can return:
*Test> pair Solver returned: (10,0) Just (11,1)
demonstrating that the user has full contact with the solver and can guide it as the program executes. SBV provides access to many SMTLib features in the query mode, as exported from this very module.
For other examples see:
 Documentation.SBV.Examples.Queries.AllSat: Simulating SBV's
allSat
using queries.  Documentation.SBV.Examples.Queries.CaseSplit: Performing a casesplit during a query.
 Documentation.SBV.Examples.Queries.Enums: Using enumerations in queries.
 Documentation.SBV.Examples.Queries.FourFours: Solution to a fun arithmetic puzzle, coded using queries.
 Documentation.SBV.Examples.Queries.GuessNumber: The famous number guessing game.
 Documentation.SBV.Examples.Queries.UnsatCore: Extracting unsatcores using queries.
 Documentation.SBV.Examples.Queries.Interpolants: Extracting interpolants using queries.
User queries
class MonadIO m => ExtractIO m where Source #
Monads which support IO
operations and can extract all IO
behavior for
interoperation with functions like catches
, which takes
an IO
action in negative position. This function can not be implemented
for transformers like ReaderT r
or StateT s
, whose resultant IO
actions are a function of some environment or state.
Instances
ExtractIO IO Source #  Trivial IO extraction for 
ExtractIO m => ExtractIO (MaybeT m) Source #  IO extraction for 
ExtractIO m => ExtractIO (ExceptT e m) Source #  IO extraction for 
(Monoid w, ExtractIO m) => ExtractIO (WriterT w m) Source #  IO extraction for lazy 
(Monoid w, ExtractIO m) => ExtractIO (WriterT w m) Source #  IO extraction for strict 
class Monad m => MonadQuery m where Source #
Computations which support query operations.
Nothing
queryState :: m State Source #
queryState :: (MonadTrans t, MonadQuery m', m ~ t m') => m State Source #
Instances
class Queriable m a b  a > b where Source #
An queriable value. This is a generalization of the Fresh
class, in case one needs
to be more specific about how projections/embeddings are done.
^ Create a new symbolic value of type a
project :: a > QueryT m b Source #
^ Extract the current value in a SAT context
Instances
(MonadIO m, SymVal a, SMTValue a) => Queriable m (SBV a) a Source #  Generic 
Queriable IO (AppS Integer) (AppC Integer) Source # 

Queriable IO (LenS Integer) (LenC Integer) Source #  We have to write the bijection between 
(MonadIO m, SymVal a, SMTValue a, Foldable t, Traversable t, Fresh m (t (SBV a))) => Queriable m (t (SBV a)) (t a) Source #  Generic 
class Fresh m a where Source #
Create a fresh variable of some type in the underlying query monad transformer.
For further control on how these variables are projected and embedded, see the
Queriable
class.
Instances
Fresh IO (S SInteger) Source # 

Fresh IO (S SInteger) Source # 

Fresh IO (S SInteger) Source # 

Fresh IO (S SInteger) Source # 

(SymVal a, SMTValue a) => Fresh IO (FibS (SBV a)) Source # 

(SymVal a, SMTValue a) => Fresh IO (GCDS (SBV a)) Source # 

(SymVal a, SMTValue a) => Fresh IO (DivS (SBV a)) Source # 

(SymVal a, SMTValue a) => Fresh IO (SqrtS (SBV a)) Source # 

(SymVal a, SMTValue a) => Fresh IO (SumS (SBV a)) Source # 

type Query = QueryT IO Source #
A query is a userguided mechanism to directly communicate and extract results from the solver.
Create a fresh variable
freshVar :: SymVal a => String > Query (SBV a) Source #
Create a fresh variable in query mode. You should prefer
creating input variables using sBool
, sInt32
, etc., which act
as primary inputs to the model and can be existential or universal.
Use freshVar
only in query mode for anonymous temporary variables.
Such variables are always existential. Note that freshVar
should hardly be
needed: Your input variables and symbolic expressions should suffice for
most major use cases.
NB. For a version which generalizes over the underlying monad, see freshVar
Create a fresh array
freshArray_ :: (SymArray array, HasKind a, HasKind b) => Maybe (SBV b) > Query (array a b) Source #
Similar to freshArray
, except creates unnamed array.
NB. For a version which generalizes over the underlying monad, see freshArray_
freshArray :: (SymArray array, HasKind a, HasKind b) => String > Maybe (SBV b) > Query (array a b) Source #
Create a fresh array in query mode. Again, you should prefer
creating arrays before the queries start using newArray
, but this
method can come in handy in occasional cases where you need a new array
after you start the query based interaction.
NB. For a version which generalizes over the underlying monad, see freshArray
Checking satisfiability
data CheckSatResult Source #
Result of a checkSat
or checkSatAssuming
call.
Sat  Satisfiable: A model is available, which can be queried with 
Unsat  Unsatisfiable: No model is available. Unsat cores might be obtained via 
Unk  Unknown: Use 
Instances
Eq CheckSatResult Source #  
Defined in Data.SBV.Control.Types (==) :: CheckSatResult > CheckSatResult > Bool # (/=) :: CheckSatResult > CheckSatResult > Bool #  
Show CheckSatResult Source #  
Defined in Data.SBV.Control.Types showsPrec :: Int > CheckSatResult > ShowS # show :: CheckSatResult > String # showList :: [CheckSatResult] > ShowS # 
checkSat :: Query CheckSatResult Source #
Check for satisfiability.
NB. For a version which generalizes over the underlying monad, see checkSat
ensureSat :: Query () Source #
Ensure that the current context is satisfiable. If not, this function will throw an error.
NB. For a version which generalizes over the underlying monad, see ensureSat
checkSatUsing :: String > Query CheckSatResult Source #
Check for satisfiability with a custom checksatusing command.
NB. For a version which generalizes over the underlying monad, see checkSatUsing
checkSatAssuming :: [SBool] > Query CheckSatResult Source #
Check for satisfiability, under the given conditions. Similar to checkSat
except it allows making
further assumptions as captured by the first argument of booleans. (Also see checkSatAssumingWithUnsatisfiableSet
for a variant that returns the subset of the given assumptions that led to the Unsat
conclusion.)
NB. For a version which generalizes over the underlying monad, see checkSatAssuming
checkSatAssumingWithUnsatisfiableSet :: [SBool] > Query (CheckSatResult, Maybe [SBool]) Source #
Check for satisfiability, under the given conditions. Returns the unsatisfiable
set of assumptions. Similar to checkSat
except it allows making further assumptions
as captured by the first argument of booleans. If the result is Unsat
, the user will
also receive a subset of the given assumptions that led to the Unsat
conclusion. Note
that while this set will be a subset of the inputs, it is not necessarily guaranteed to be minimal.
You must have arranged for the production of unsat assumptions first via
setOption
$ProduceUnsatAssumptions
True
for this call to not error out!
Usage note: getUnsatCore
is usually easier to use than checkSatAssumingWithUnsatisfiableSet
, as it
allows the use of named assertions, as obtained by namedConstraint
. If getUnsatCore
fills your needs, you should definitely prefer it over checkSatAssumingWithUnsatisfiableSet
.
NB. For a version which generalizes over the underlying monad, see checkSatAssumingWithUnsatisfiableSet
Querying the solver
Extracting values
class SMTValue a where Source #
A class which allows for sexprconversion to values
Nothing
sexprToVal :: SExpr > Maybe a Source #
sexprToVal :: Read a => SExpr > Maybe a Source #
Instances
getValue :: SMTValue a => SBV a > Query a Source #
Get the value of a term.
NB. For a version which generalizes over the underlying monad, see getValue
registerUISMTFunction :: (MonadIO m, SolverContext m, MonadSymbolic m) => SMTFunction fun a r => fun > m () Source #
Registering an uninterpreted SMT function. This is typically not necessary as uses of the UI function itself will register it automatically. But there are cases where doing this explicitly can come in handy.
getFunction :: SMTFunction fun a r => fun > Query ([(a, r)], r) Source #
Get the value of an uninterpreted function, as a list of domain, value pairs. The final value is the "else" clause, i.e., what the function maps values outside of the domain of the first list.
getUninterpretedValue :: HasKind a => SBV a > Query String Source #
Get the value of an uninterpreted sort, as a String
NB. For a version which generalizes over the underlying monad, see getUninterpretedValue
getModel :: Query SMTModel Source #
Collect model values. It is implicitly assumed that we are in a checksat
context. See getSMTResult
for a variant that issues a checksat first and
returns an SMTResult
.
NB. For a version which generalizes over the underlying monad, see getModel
getAssignment :: Query [(String, Bool)] Source #
Retrieve the assignment. This is a lightweight version of getValue
, where the
solver returns the truth value for all named subterms of type Bool
.
You must have first arranged for assignments to be produced via
setOption
$ProduceAssignments
True
for this call to not error out!
NB. For a version which generalizes over the underlying monad, see getAssignment
getSMTResult :: Query SMTResult Source #
Issue checksat and get an SMT Result out.
NB. For a version which generalizes over the underlying monad, see getSMTResult
getUnknownReason :: Query SMTReasonUnknown Source #
Get the reason unknown. Only internally used.
NB. For a version which generalizes over the underlying monad, see getUnknownReason
getObservables :: Query [(String, CV)] Source #
Get the observables recorded during a query run.
NB. For a version which generalizes over the underlying monad, see getObservables
Extracting the unsat core
getUnsatCore :: Query [String] Source #
Retrieve the unsatcore. Note you must have arranged for unsat cores to be produced first via
setOption
$ProduceUnsatCores
True
for this call to not error out!
NB. There is no notion of a minimal unsatcore, in case unsatisfiability can be derived in multiple ways. Furthermore, Z3 does not guarantee that the generated unsat core does not have any redundant assertions either, as doing so can incur a performance penalty. (There might be assertions in the set that is not needed.) To ensure all the assertions in the core are relevant, use:
setOption
$OptionKeyword
":smt.core.minimize" ["true"]
Note that this only works with Z3.
NB. For a version which generalizes over the underlying monad, see getUnsatCore
Extracting a proof
getProof :: Query String Source #
Retrieve the proof. Note you must have arranged for proofs to be produced first via
setOption
$ProduceProofs
True
for this call to not error out!
A proof is simply a String
, as returned by the solver. In the future, SBV might
provide a better datatype, depending on the use cases. Please get in touch if you
use this function and can suggest a better API.
NB. For a version which generalizes over the underlying monad, see getProof
Extracting interpolants
getInterpolant :: [String] > Query String Source #
Retrieve an interpolant after an Unsat
result is obtained. Note you must have arranged for
interpolants to be produced first via
setOption
$ProduceInterpolants
True
for this call to not error out!
To get an interpolant for a pair of formulas A
and B
, use a constrainWithAttribute
call to attach
interplation groups to A
and B
. Then call getInterpolant
["A"]
, assuming those are the names
you gave to the formulas in the A
group.
An interpolant for A
and B
is a formula I
such that:
A .=> I and B .=> sNot I
That is, it's evidence that A
and B
cannot be true together
since A
implies I
but B
implies not I
; establishing that A
and B
cannot
be satisfied at the same time. Furthermore, I
will have only the symbols that are common
to A
and B
.
N.B. As of Z3 version 4.8.0; Z3 no longer supports interpolants. Use the MathSAT backend for extracting interpolants. See Documentation.SBV.Examples.Queries.Interpolants for an example.
NB. For a version which generalizes over the underlying monad, see getInterpolant
Extracting assertions
getAssertions :: Query [String] Source #
Retrieve assertions. Note you must have arranged for assertions to be available first via
setOption
$ProduceAssertions
True
for this call to not error out!
Note that the set of assertions returned is merely a list of strings, just like the
case for getProof
. In the future, SBV might provide a better datatype, depending
on the use cases. Please get in touch if you use this function and can suggest
a better API.
NB. For a version which generalizes over the underlying monad, see getAssertions
Getting solver information
data SMTInfoFlag Source #
Collectable information from the solver.
AllStatistics  
AssertionStackLevels  
Authors  
ErrorBehavior  
Name  
ReasonUnknown  
Version  
InfoKeyword String 
Instances
Show SMTInfoFlag Source #  
Defined in Data.SBV.Control.Types showsPrec :: Int > SMTInfoFlag > ShowS # show :: SMTInfoFlag > String # showList :: [SMTInfoFlag] > ShowS # 
data SMTErrorBehavior Source #
Behavior of the solver for errors.
Instances
Show SMTErrorBehavior Source #  
Defined in Data.SBV.Control.Types showsPrec :: Int > SMTErrorBehavior > ShowS # show :: SMTErrorBehavior > String # showList :: [SMTErrorBehavior] > ShowS # 
data SMTInfoResponse Source #
Collectable information from the solver.
Instances
Show SMTInfoResponse Source #  
Defined in Data.SBV.Control.Types showsPrec :: Int > SMTInfoResponse > ShowS # show :: SMTInfoResponse > String # showList :: [SMTInfoResponse] > ShowS # 
getInfo :: SMTInfoFlag > Query SMTInfoResponse Source #
Ask solver for info.
NB. For a version which generalizes over the underlying monad, see getInfo
getOption :: (a > SMTOption) > Query (Maybe SMTOption) Source #
Retrieve the value of an 'SMTOption.' The curious function argument is on purpose here,
simply pass the constructor name. Example: the call
will return
either getOption
ProduceUnsatCores
Nothing
or Just (ProduceUnsatCores True)
or Just (ProduceUnsatCores False)
.
Result will be Nothing
if the solver does not support this option.
NB. For a version which generalizes over the underlying monad, see getOption
Entering and exiting assertion stack
getAssertionStackDepth :: Query Int Source #
The current assertion stack depth, i.e., pops after start. Always nonnegative.
NB. For a version which generalizes over the underlying monad, see getAssertionStackDepth
push :: Int > Query () Source #
Push the context, entering a new one. Pushes multiple levels if n > 1.
NB. For a version which generalizes over the underlying monad, see push
pop :: Int > Query () Source #
Pop the context, exiting a new one. Pops multiple levels if n > 1. It's an error to pop levels that don't exist.
NB. For a version which generalizes over the underlying monad, see pop
inNewAssertionStack :: Query a > Query a Source #
Run the query in a new assertion stack. That is, we push the context, run the query commands, and pop it back.
NB. For a version which generalizes over the underlying monad, see inNewAssertionStack
Higher level tactics
caseSplit :: Bool > [(String, SBool)] > Query (Maybe (String, SMTResult)) Source #
Search for a result via a sequence of casesplits, guided by the user. If one of
the conditions lead to a satisfiable result, returns Just
that result. If none of them
do, returns Nothing
. Note that we automatically generate a coverage case and search
for it automatically as well. In that latter case, the string returned will be Coverage.
The first argument controls printing progress messages See Documentation.SBV.Examples.Queries.CaseSplit
for an example use case.
NB. For a version which generalizes over the underlying monad, see caseSplit
Resetting the solver state
resetAssertions :: Query () Source #
Reset the solver, by forgetting all the assertions. However, bindings are kept as is,
as opposed to a full reset of the solver. Use this variant to cleanup the solver
state while leaving the bindings intact. Pops all assertion levels. Declarations and
definitions resulting from the setLogic
command are unaffected. Note that SBV
implicitly uses globaldeclarations, so bindings will remain intact.
NB. For a version which generalizes over the underlying monad, see resetAssertions
Constructing assignments
(>) :: SymVal a => SBV a > a > Assignment infix 1 Source #
Make an assignment. The type Assignment
is abstract, the result is typically passed
to mkSMTResult
:
mkSMTResult [ a > 332 , b > 2.3 , c > True ]
End users should use getModel
for automatically constructing models from the current solver state.
However, an explicit Assignment
might be handy in complex scenarios where a model needs to be
created manually.
Terminating the query
mkSMTResult :: [Assignment] > Query SMTResult Source #
Produce the query result from an assignment.
NB. For a version which generalizes over the underlying monad, see mkSMTResult
Exit the solver. This action will cause the solver to terminate. Needless to say, trying to communicate with the solver after issuing "exit" will simply fail.
NB. For a version which generalizes over the underlying monad, see exit
Controlling the solver behavior
ignoreExitCode :: SMTConfig > Bool Source #
If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.
timeout :: Int > Query a > Query a Source #
Timeout a query action, typically a command call to the underlying SMT solver.
The duration is in microseconds (1/10^6
seconds). If the duration
is negative, then no timeout is imposed. When specifying long timeouts, be careful not to exceed
maxBound :: Int
. (On a 64 bit machine, this bound is practically infinite. But on a 32 bit
machine, it corresponds to about 36 minutes!)
Semantics: The call timeout n q
causes the timeout value to be applied to all interactive calls that take place
as we execute the query q
. That is, each call that happens during the execution of q
gets a separate
timeout value, as opposed to one timeout value that limits the whole query. This is typically the intended behavior.
It is advisible to apply this combinator to calls that involve a single call to the solver for
finer control, as opposed to an entire set of interactions. However, different use cases might call for different scenarios.
If the solver responds within the timeout specified, then we continue as usual. However, if the backend solver timesout using this mechanism, there is no telling what the state of the solver will be. Thus, we raise an error in this case.
NB. For a version which generalizes over the underlying monad, see timeout
Miscellaneous
queryDebug :: [String] > Query () Source #
If verbose
is True
, print the message, useful for debugging messages
in custom queries. Note that redirectVerbose
will be respected: If a
file redirection is given, the output will go to the file.
NB. For a version which generalizes over the underlying monad, see queryDebug
echo :: String > Query () Source #
Echo a string. Note that the echoing is done by the solver, not by SBV.
NB. For a version which generalizes over the underlying monad, see echo
io :: IO a > Query a Source #
Perform an arbitrary IO action.
NB. For a version which generalizes over the underlying monad, see io
Solver options
Option values that can be set in the solver, following the SMTLib specification http://smtlib.cs.uiowa.edu/language.shtml.
Note that not all solvers may support all of these!
Furthermore, SBV doesn't support the following options allowed by SMTLib.
:interactivemode
(Deprecated in SMTLib, useProduceAssertions
instead.):printsuccess
(SBV critically needs this to be True in query mode.):producemodels
(SBV always sets this option so it can extract models.):regularoutputchannel
(SBV always requires regular output to come on stdout for query purposes.):globaldeclarations
(SBV always uses global declarations since definitions are accumulative.)
Note that SetLogic
and SetInfo
are, strictly speaking, not SMTLib options. However, we treat it as such here
uniformly, as it fits better with how options work.