sbv-8.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Control

Contents

- User queries
- Create a fresh variable
- Create a fresh array
- Checking satisfiability
- Querying the solver
  - Extracting values
  - Extracting the unsat core
  - Extracting a proof
  - Extracting interpolants
  - Extracting assertions
- 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

Description

Control sublanguage for interacting with SMT solvers.

Synopsis

- class MonadIO m => ExtractIO m where
  - extractIO :: m a -> IO (m a)
- class Monad m => MonadQuery m where
  - queryState :: m State
- class Queriable m a b | a -> b where
  - create :: QueryT m a
  - project :: a -> QueryT m b
  - embed :: b -> QueryT m a
- class Fresh m a where
  - fresh :: QueryT m a
- 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
  - = Sat
  - | Unsat
  - | Unk
- checkSat :: Query CheckSatResult
- ensureSat :: Query ()
- checkSatUsing :: String -> Query CheckSatResult
- checkSatAssuming :: [SBool] -> Query CheckSatResult
- checkSatAssumingWithUnsatisfiableSet :: [SBool] -> Query (CheckSatResult, Maybe [SBool])
- getValue :: SymVal a => SBV a -> Query a
- registerUISMTFunction :: (MonadIO m, SolverContext m, MonadSymbolic m) => SMTFunction fun a r => fun -> m ()
- getFunction :: (SymVal a, SymVal r, 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
- getInterpolantMathSAT :: [String] -> Query String
- getInterpolantZ3 :: [SBool] -> Query String
- getAssertions :: Query [String]
- data SMTInfoFlag
  - = AllStatistics
  - | AssertionStackLevels
  - | Authors
  - | ErrorBehavior
  - | Name
  - | ReasonUnknown
  - | Version
  - | InfoKeyword String
- data SMTErrorBehavior
  - = ErrorImmediateExit
  - | ErrorContinuedExecution
- data SMTInfoResponse
  - = Resp_Unsupported
  - | Resp_AllStatistics [(String, String)]
  - | Resp_AssertionStackLevels Integer
  - | Resp_Authors [String]
  - | Resp_Error SMTErrorBehavior
  - | Resp_Name String
  - | Resp_ReasonUnknown SMTReasonUnknown
  - | Resp_Version String
  - | Resp_InfoKeyword String [String]
- 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. Note that `z3` is best supported (and tested), if you use another solver your results may vary!)

        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 case-split 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 unsat-cores 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.

Methods

extractIO :: m a -> IO (m a) Source #

Law: the `m a` yielded by `IO` is pure with respect to `IO`.

#### Instances

Instances details

ExtractIO IO Source # | Trivial IO extraction for `IO`.
Instance details Defined in Data.SBV.Utils.ExtractIO Methods extractIO :: IO a -> IO (IO a) Source #
ExtractIO m => ExtractIO (MaybeT m) Source # | IO extraction for `MaybeT`.
Instance details Defined in Data.SBV.Utils.ExtractIO Methods extractIO :: MaybeT m a -> IO (MaybeT m a) Source #
ExtractIO m => ExtractIO (ExceptT e m) Source # | IO extraction for `ExceptT`.
Instance details Defined in Data.SBV.Utils.ExtractIO Methods extractIO :: ExceptT e m a -> IO (ExceptT e m a) Source #
(Monoid w, ExtractIO m) => ExtractIO (WriterT w m) Source # | IO extraction for lazy `WriterT`.
Instance details Defined in Data.SBV.Utils.ExtractIO Methods extractIO :: WriterT w m a -> IO (WriterT w m a) Source #
(Monoid w, ExtractIO m) => ExtractIO (WriterT w m) Source # | IO extraction for strict `WriterT`.
Instance details Defined in Data.SBV.Utils.ExtractIO Methods extractIO :: WriterT w m a -> IO (WriterT w m a) Source #

class Monad m => MonadQuery m where Source #

Computations which support query operations.

Minimal complete definition

Nothing

Methods

queryState :: m State Source #

default queryState :: (MonadTrans t, MonadQuery m', m ~ t m') => m State Source #

#### Instances

Instances details

MonadQuery Q Source # |
Instance details Defined in Documentation.SBV.Examples.Transformers.SymbolicEval Methods queryState :: Q State Source #
MonadQuery m => MonadQuery (MaybeT m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods queryState :: MaybeT m State Source #
Monad m => MonadQuery (QueryT m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods queryState :: QueryT m State Source #
MonadQuery m => MonadQuery (ExceptT e m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods queryState :: ExceptT e m State Source #
(MonadQuery m, Monoid w) => MonadQuery (WriterT w m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods queryState :: WriterT w m State Source #
(MonadQuery m, Monoid w) => MonadQuery (WriterT w m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods queryState :: WriterT w m State Source #
MonadQuery m => MonadQuery (ReaderT r m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods queryState :: ReaderT r m State Source #
MonadQuery m => MonadQuery (StateT s m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods queryState :: StateT s m State Source #
MonadQuery m => MonadQuery (StateT s m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods queryState :: StateT s m State Source #

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.

Methods

create :: QueryT m a Source #

^ Create a new symbolic value of type `a`

project :: a -> QueryT m b Source #

^ Extract the current value in a SAT context

embed :: b -> QueryT m a Source #

^ Create a literal value. Morally, `embed` and `project` are inverses of each other via the `QueryT` monad transformer.

#### Instances

Instances details

(MonadIO m, SymVal a) => Queriable m (SBV a) a Source # | Generic `Queriable` instance for `SymVal`/`SMTValue` values
Instance details Defined in Data.SBV.Control.Utils Methods create :: QueryT m (SBV a) Source # project :: SBV a -> QueryT m a Source # embed :: a -> QueryT m (SBV a) Source #
Queriable IO (AppS Integer) (AppC Integer) Source # | `Queriable` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Append Methods create :: QueryT IO (AppS Integer) Source # project :: AppS Integer -> QueryT IO (AppC Integer) Source # embed :: AppC Integer -> QueryT IO (AppS Integer) Source #
Queriable IO (LenS Integer) (LenC Integer) Source # | We have to write the bijection between `LenS` and `LenC` explicitly. Luckily, the definition is more or less boilerplate.
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Length Methods create :: QueryT IO (LenS Integer) Source # project :: LenS Integer -> QueryT IO (LenC Integer) Source # embed :: LenC Integer -> QueryT IO (LenS Integer) Source #
(MonadIO m, SymVal a, Foldable t, Traversable t, Fresh m (t (SBV a))) => Queriable m (t (SBV a)) (t a) Source # | Generic `Queriable` instance for things that are `Fresh` and look like containers:
Instance details Defined in Data.SBV.Control.Utils Methods create :: QueryT m (t (SBV a)) Source # project :: t (SBV a) -> QueryT m (t a) Source # embed :: t a -> QueryT m (t (SBV a)) Source #

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.

Methods

fresh :: QueryT m a Source #

#### Instances

Instances details

Fresh IO (S SInteger) Source # | `Fresh` instance for our state
Instance details Defined in Documentation.SBV.Examples.ProofTools.BMC Methods fresh :: QueryT IO (S SInteger) Source #
Fresh IO (S SInteger) Source # | `Fresh` instance for our state
Instance details Defined in Documentation.SBV.Examples.ProofTools.Fibonacci Methods fresh :: QueryT IO (S SInteger) Source #
Fresh IO (S SInteger) Source # | `Fresh` instance for our state
Instance details Defined in Documentation.SBV.Examples.ProofTools.Strengthen Methods fresh :: QueryT IO (S SInteger) Source #
Fresh IO (S SInteger) Source # | `Fresh` instance for our state
Instance details Defined in Documentation.SBV.Examples.ProofTools.Sum Methods fresh :: QueryT IO (S SInteger) Source #
SymVal a => Fresh IO (IncS (SBV a)) Source # | `Fresh` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Basics Methods fresh :: QueryT IO (IncS (SBV a)) Source #
SymVal a => Fresh IO (FibS (SBV a)) Source # | `Fresh` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Fib Methods fresh :: QueryT IO (FibS (SBV a)) Source #
SymVal a => Fresh IO (GCDS (SBV a)) Source # | `Fresh` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.GCD Methods fresh :: QueryT IO (GCDS (SBV a)) Source #
SymVal a => Fresh IO (DivS (SBV a)) Source # | `Fresh` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.IntDiv Methods fresh :: QueryT IO (DivS (SBV a)) Source #
SymVal a => Fresh IO (SqrtS (SBV a)) Source # | `Fresh` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.IntSqrt Methods fresh :: QueryT IO (SqrtS (SBV a)) Source #
SymVal a => Fresh IO (SumS (SBV a)) Source # | `Fresh` instance for the program state
Instance details Defined in Documentation.SBV.Examples.WeakestPreconditions.Sum Methods fresh :: QueryT IO (SumS (SBV a)) Source #

type Query = QueryT IO Source #

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

query :: Query a -> Symbolic a Source #

Run a custom query

# Create a fresh variable

freshVar_ :: SymVal a => Query (SBV a) Source #

Similar to `freshVar`, except creates unnamed variable.

NB. For a version which generalizes over the underlying monad, see `freshVar_`

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.

Constructors

Sat | Satisfiable: A model is available, which can be queried with `getValue`.
Unsat | Unsatisfiable: No model is available. Unsat cores might be obtained via `getUnsatCore`.
Unk | Unknown: Use `getUnknownReason` to obtain an explanation why this might be the case.

#### Instances

Instances details

Eq CheckSatResult Source # |
Instance details Defined in Data.SBV.Control.Types Methods (==) :: CheckSatResult -> CheckSatResult -> Bool (/=) :: CheckSatResult -> CheckSatResult -> Bool
Show CheckSatResult Source # |
Instance details Defined in Data.SBV.Control.Types Methods 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 check-sat-using 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

getValue :: SymVal 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 :: (SymVal a, SymVal r, 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 check-sat context. See `getSMTResult` for a variant that issues a check-sat 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 check-sat 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 unsat-core. 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 unsat-core, 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

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

Interpolant extraction for MathSAT. Compare with `getInterpolantZ3`, which performs similar function (but with a different use model) in Z3.

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 `getInterpolantMathSAT` `["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`.

NB. Interpolant extraction isn't standardized well in SMTLib. Currently both MathSAT and Z3 support them, but with slightly differing APIs. So, we support two APIs with slightly differing types to accommodate both. See Documentation.SBV.Examples.Queries.Interpolants for example usages in these solvers.

NB. For a version which generalizes over the underlying monad, see `getInterpolantMathSAT`

getInterpolantZ3 :: [SBool] -> Query String Source #

Interpolant extraction for z3. Compare with `getInterpolantMathSAT`, which performs similar function (but with a different use model) in MathSAT.

Unlike the MathSAT variant, you should simply call `getInterpolantZ3` on symbolic booleans to retrieve the interpolant. Do not call `checkSat` or create named constraints. This makes it harder to identify formulas, but the current state of affairs in interpolant API requires this kludge.

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

In Z3, 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.

NB. Interpolant extraction isn't standardized well in SMTLib. Currently both MathSAT and Z3 support them, but with slightly differing APIs. So, we support two APIs with slightly differing types to accommodate both. See Documentation.SBV.Examples.Queries.Interpolants for example usages in these solvers.

NB. For a version which generalizes over the underlying monad, see `getInterpolantZ3`

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

Constructors

AllStatistics |
AssertionStackLevels |
Authors |
ErrorBehavior |
Name |
ReasonUnknown |
Version |
InfoKeyword String |

#### Instances

Instances details

Show SMTInfoFlag Source # |
Instance details Defined in Data.SBV.Control.Types Methods showsPrec :: Int -> SMTInfoFlag -> ShowS show :: SMTInfoFlag -> String showList :: [SMTInfoFlag] -> ShowS

data SMTErrorBehavior Source #

Behavior of the solver for errors.

Constructors

ErrorImmediateExit |
ErrorContinuedExecution |

#### Instances

Instances details

Show SMTErrorBehavior Source # |
Instance details Defined in Data.SBV.Control.Types Methods showsPrec :: Int -> SMTErrorBehavior -> ShowS show :: SMTErrorBehavior -> String showList :: [SMTErrorBehavior] -> ShowS

data SMTInfoResponse Source #

Collectable information from the solver.

Constructors

Resp_Unsupported |
Resp_AllStatistics [(String, String)] |
Resp_AssertionStackLevels Integer |
Resp_Authors [String] |
Resp_Error SMTErrorBehavior |
Resp_Name String |
Resp_ReasonUnknown SMTReasonUnknown |
Resp_Version String |
Resp_InfoKeyword String [String] |

#### Instances

Instances details

Show SMTInfoResponse Source # |
Instance details Defined in Data.SBV.Control.Types Methods 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 ``getOption` `ProduceUnsatCores`` will return either `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 non-negative.

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

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 :: Query () Source #

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

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

data SMTOption Source #

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.

Constructors

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] |

#### Instances

Instances details

Show SMTOption Source # |
Instance details Defined in Data.SBV.Control.Types Methods showsPrec :: Int -> SMTOption -> ShowS show :: SMTOption -> String showList :: [SMTOption] -> ShowS
Generic SMTOption Source # |
Instance details Defined in Data.SBV.Control.Types Associated Types type Rep SMTOption :: Type -> Type Methods from :: SMTOption -> Rep SMTOption x to :: Rep SMTOption x -> SMTOption
NFData SMTOption Source # |
Instance details Defined in Data.SBV.Control.Types Methods rnf :: SMTOption -> ()
type Rep SMTOption Source # |

Instance details

Defined in Data.SBV.Control.Types

type Rep SMTOption = D1 ('MetaData "SMTOption" "Data.SBV.Control.Types" "sbv-8.7-9mSEXJN8olRBwPWTmi3EMV" 'False) (((C1 ('MetaCons "DiagnosticOutputChannel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath)) :+: (C1 ('MetaCons "ProduceAssertions" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: C1 ('MetaCons "ProduceAssignments" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :+: (C1 ('MetaCons "ProduceProofs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: (C1 ('MetaCons "ProduceInterpolants" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: C1 ('MetaCons "ProduceUnsatAssumptions" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) :+: ((C1 ('MetaCons "ProduceUnsatCores" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: (C1 ('MetaCons "RandomSeed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: C1 ('MetaCons "ReproducibleResourceLimit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))) :+: ((C1 ('MetaCons "SMTVerbosity" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: C1 ('MetaCons "OptionKeyword" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]))) :+: (C1 ('MetaCons "SetLogic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Logic)) :+: C1 ('MetaCons "SetInfo" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]))))))