Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

Control sublanguage for interacting with SMT solvers.

- data Query a
- query :: Query a -> Symbolic a
- freshVar_ :: forall a. SymWord a => Query (SBV a)
- freshVar :: forall a. SymWord a => String -> Query (SBV a)
- data CheckSatResult
- checkSat :: Query CheckSatResult
- checkSatUsing :: String -> Query CheckSatResult
- checkSatAssuming :: [SBool] -> Query CheckSatResult
- checkSatAssumingWithUnsatisfiableSet :: [SBool] -> Query (CheckSatResult, Maybe [SBool])
- class SMTValue a where
- getValue :: SMTValue a => SBV a -> Query a
- getUninterpretedValue :: HasKind a => SBV a -> Query String
- getModel :: Query SMTModel
- getAssignment :: Query [(String, Bool)]
- getSMTResult :: Query SMTResult
- getUnknownReason :: Query String
- getUnsatCore :: Query [String]
- getProof :: Query String
- getInterpolant :: [String] -> Query [String]
- getAssertions :: Query [String]
- data SMTInfoFlag
- data SMTErrorBehavior
- data SMTReasonUnknown
- 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 ()
- (|->) :: SymWord a => SBV a -> a -> Assignment
- mkSMTResult :: [Assignment] -> Query SMTResult
- exit :: Query ()
- ignoreExitCode :: SMTConfig -> Bool
- timeout :: Int -> Query a -> Query a
- 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]

- data Logic

# 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:

- Data.SBV.Examples.Queries.AllSat: Simulating SBV's
`allSat`

using queries. - Data.SBV.Examples.Queries.CaseSplit: Performing a case-split during a query.
- Data.SBV.Examples.Queries.Enums: Using enumerations in queries.
- Data.SBV.Examples.Queries.FourFours: Solution to a fun arithmetic puzzle, coded using queries.
- Data.SBV.Examples.Queries.GuessNumber: The famous number guessing game.
- Data.SBV.Examples.Queries.UnsatCore: Extracting unsat-cores using queries.
- Data.SBV.Examples.Queries.Interpolants: Extracting interpolants using queries.

# User queries

A query is a user-guided mechanism to directly communicate and extract results from the solver.

# Create a fresh variable

freshVar_ :: forall a. SymWord a => Query (SBV a) Source #

Similar to `freshVar`

, except creates unnamed variable.

freshVar :: forall a. SymWord 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.

# Checking satisfiability

data CheckSatResult Source #

Result of a `checkSat`

or `checkSatAssuming`

call.

checkSat :: Query CheckSatResult Source #

Check for satisfiability.

checkSatUsing :: String -> Query CheckSatResult Source #

Check for satisfiability with a custom check-sat-using command.

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.)

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*

)
for this call to not error out!`setOption`

$ `ProduceUnsatAssumptions`

`True`

Usage note: `getUnsatCore`

is usually easier to use than `checkSatAssumingWithUnsatisfiableSet`

, as it
allows the use of named assertions, as obtained by `namedAssert`

. If `getUnsatCore`

fills your needs, you should definitely prefer it over `checkSatAssumingWithUnsatisfiableSet`

.

# Querying the solver

## Extracting values

class SMTValue a where Source #

A class which allows for sexpr-conversion to values

sexprToVal :: SExpr -> Maybe a Source #

sexprToVal :: Read a => SExpr -> Maybe a Source #

getUninterpretedValue :: HasKind a => SBV a -> Query String Source #

Get the value of an uninterpreted sort, as a String

getModel :: Query SMTModel Source #

Collect model values. It is implicitly assumed that we are in a check-sat
context. See `getSMTResult`

for a variant that issues a check-sat first and
returns an `SMTResult`

.

getSMTResult :: Query SMTResult Source #

Issue check-sat and get an SMT Result out.

getUnknownReason :: Query String Source #

Get the reason unknown. Only internally used.

## Extracting the unsat core

getUnsatCore :: Query [String] Source #

Retrieve the unsat-core. Note you must have arranged for
unsat cores to be produced first (*via*

)
for this call to not error out!`setOption`

$ `ProduceUnsatCores`

`True`

## Extracting a proof

getProof :: Query String Source #

Retrieve the proof. Note you must have arranged for
proofs to be produced first (*via*

)
for this call to not error out!`setOption`

$ `ProduceProofs`

`True`

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.

## Extracting interpolants

getInterpolant :: [String] -> Query [String] Source #

Retrieve interpolants after an `Unsat`

result is obtained. Note you must have arranged for
interpolants to be produced first (*via*

)
for this call to not error out!`setOption`

$ `ProduceInterpolants`

`True`

To get an interpolant for a pair of formulas `A`

and `B`

, use a `namedConstraint`

to attach
names to `A`

and `B`

. Then call `getInterpolant`

`["A", "B"]`

, assuming those are the names
you gave to the formulas.

An interpolant for `A`

and `B`

is a formula `I`

such that:

A ==> I and B ==> not 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`

.

Interpolants generalize to sequences: If you pass more than two formulas, then you will get
a sequence of interpolants. In general, for `N`

formulas that are not satisfiable together, you will be
returned `N-1`

interpolants. If formulas are `A1 .. An`

, then interpolants will be `I1 .. I(N-1)`

, such
that `A1 ==> I1`

, `A2 /\ I1 ==> I2`

, `A3 /\ I2 ==> I3`

, ..., and finally `AN ===> not I(N-1)`

.

Currently, SBV only returns simple and sequence interpolants, and does not support tree-interpolants. If you need these, please get in touch. Furthermore, the result will be a list of mere strings representing the interpolating formulas, as opposed to a more structured type. Please get in touch if you use this function and can suggest a better API.

## Extracting assertions

getAssertions :: Query [String] Source #

Retrieve assertions. Note you must have arranged for
assertions to be available first (*via*

)
for this call to not error out!`setOption`

$ `ProduceAssertions`

`True`

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.

# Getting solver information

data SMTInfoFlag Source #

Collectable information from the solver.

data SMTErrorBehavior Source #

Behavior of the solver for errors.

data SMTReasonUnknown Source #

Reason for reporting unknown.

data SMTInfoResponse Source #

Collectable information from the solver.

getInfo :: SMTInfoFlag -> Query SMTInfoResponse Source #

Ask solver for info.

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.

# Entering and exiting assertion stack

push :: Int -> Query () Source #

Push the context, entering a new one. Pushes multiple levels if *n* > 1.

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.

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.

# Tactics

caseSplit :: Bool -> [(String, SBool)] -> Query (Maybe (String, SMTResult)) Source #

Search for a result via a sequence of case-splits, 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

# Resetting the solver state

resetAssertions :: Query () Source #

Reset the solver, by forgetting all the assertions. However, bindings are kept as is,
as opposed to `reset`

. Use this variant to clean-up 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 global-declarations, so bindings will remain intact.

# Constructing assignments

(|->) :: SymWord 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.

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.

# 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
time-out 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 time-out specified, then we continue as usual. However, if the backend solver times-out using this mechanism, there is no telling what the state of the solver will be. Thus, we raise an error in this case.

# Miscellaneous

echo :: String -> Query () Source #

Echo a string. Note that the echoing is done by the solver, not by SBV.

# 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.

`:interactive-mode`

(Deprecated in SMTLib, use`ProduceAssertions`

instead.)`:print-success`

(SBV critically needs this to be True in query mode.)`:produce-models`

(SBV always sets this option so it can extract models.)`:regular-output-channel`

(SBV always requires regular output to come on stdout for query purposes.)`:global-declarations`

(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.

# Logics supported

SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the
user can override this choice using the tactic `SetOptions`

This is especially handy if one is experimenting with custom
logics that might be supported on new solvers. See http://smtlib.cs.uiowa.edu/logics.shtml for the official list.

AUFLIA | Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values. |

AUFLIRA | Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value. |

AUFNIRA | Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value. |

LRA | Linear formulas in linear real arithmetic. |

QF_ABV | Quantifier-free formulas over the theory of bitvectors and bitvector arrays. |

QF_AUFBV | Quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols. |

QF_AUFLIA | Quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols. |

QF_AX | Quantifier-free formulas over the theory of arrays with extensionality. |

QF_BV | Quantifier-free formulas over the theory of fixed-size bitvectors. |

QF_IDL | Difference Logic over the integers. Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant. |

QF_LIA | Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables. |

QF_LRA | Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables. |

QF_NIA | Quantifier-free integer arithmetic. |

QF_NRA | Quantifier-free real arithmetic. |

QF_RDL | Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant. |

QF_UF | Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols. |

QF_UFBV | Unquantified formulas over bitvectors with uninterpreted sort function and symbols. |

QF_UFIDL | Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols. |

QF_UFLIA | Unquantified linear integer arithmetic with uninterpreted sort and function symbols. |

QF_UFLRA | Unquantified linear real arithmetic with uninterpreted sort and function symbols. |

QF_UFNRA | Unquantified non-linear real arithmetic with uninterpreted sort and function symbols. |

QF_UFNIRA | Unquantified non-linear real integer arithmetic with uninterpreted sort and function symbols. |

UFLRA | Linear real arithmetic with uninterpreted sort and function symbols. |

UFNIA | Non-linear integer arithmetic with uninterpreted sort and function symbols. |

QF_FPBV | Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors. |

QF_FP | Quantifier-free formulas over the theory of floating point numbers. |

QF_FD | Quantifier-free finite domains |

Logic_ALL | The catch-all value |

CustomLogic String | In case you need a really custom string! |