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

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Control

Contents

Description

Control sublanguage for interacting with SMT solvers.

Synopsis

Documentation

In certain cases, the user might want to take over the communication with the solver, programmatically querying the engine and issuing commands accordingly. Even with human guidance, perhaps, where the user can take a look at the engine state and issue commands to guide the proof. This is an advanced feature, as the user is given full access to the underlying SMT solver, so the usual protections provided by SBV are no longer there to prevent mistakes.

Having said that, 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:

User queries

data Query a Source #

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

Instances

Monad Query Source # 

Methods

(>>=) :: Query a -> (a -> Query b) -> Query b #

(>>) :: Query a -> Query b -> Query b #

return :: a -> Query a #

fail :: String -> Query a #

Functor Query Source # 

Methods

fmap :: (a -> b) -> Query a -> Query b #

(<$) :: a -> Query b -> Query a #

Applicative Query Source # 

Methods

pure :: a -> Query a #

(<*>) :: Query (a -> b) -> Query a -> Query b #

(*>) :: Query a -> Query b -> Query b #

(<*) :: Query a -> Query b -> Query a #

MonadIO Query Source # 

Methods

liftIO :: IO a -> Query a #

MonadState State Query Source # 

Methods

get :: Query State

put :: State -> Query ()

state :: (State -> (a, State)) -> Query a

query :: Query a -> Symbolic a Source #

Run a custom query

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.

Constructors

Sat 
Unsat 
Unk 

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

Methods

sexprToVal :: SExpr -> Maybe a Source #

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

Instances

SMTValue Bool Source # 

Methods

sexprToVal :: SExpr -> Maybe Bool Source #

SMTValue Double Source # 

Methods

sexprToVal :: SExpr -> Maybe Double Source #

SMTValue Float Source # 

Methods

sexprToVal :: SExpr -> Maybe Float Source #

SMTValue Int8 Source # 

Methods

sexprToVal :: SExpr -> Maybe Int8 Source #

SMTValue Int16 Source # 

Methods

sexprToVal :: SExpr -> Maybe Int16 Source #

SMTValue Int32 Source # 

Methods

sexprToVal :: SExpr -> Maybe Int32 Source #

SMTValue Int64 Source # 

Methods

sexprToVal :: SExpr -> Maybe Int64 Source #

SMTValue Integer Source # 

Methods

sexprToVal :: SExpr -> Maybe Integer Source #

SMTValue Word8 Source # 

Methods

sexprToVal :: SExpr -> Maybe Word8 Source #

SMTValue Word16 Source # 

Methods

sexprToVal :: SExpr -> Maybe Word16 Source #

SMTValue Word32 Source # 

Methods

sexprToVal :: SExpr -> Maybe Word32 Source #

SMTValue Word64 Source # 

Methods

sexprToVal :: SExpr -> Maybe Word64 Source #

SMTValue AlgReal Source # 

Methods

sexprToVal :: SExpr -> Maybe AlgReal Source #

SMTValue E Source # 

Methods

sexprToVal :: SExpr -> Maybe E Source #

SMTValue Color Source # 

Methods

sexprToVal :: SExpr -> Maybe Color Source #

SMTValue Nationality Source # 

Methods

sexprToVal :: SExpr -> Maybe Nationality Source #

SMTValue Beverage Source # 

Methods

sexprToVal :: SExpr -> Maybe Beverage Source #

SMTValue Pet Source # 

Methods

sexprToVal :: SExpr -> Maybe Pet Source #

SMTValue Sport Source # 

Methods

sexprToVal :: SExpr -> Maybe Sport Source #

SMTValue U2Member Source # 

Methods

sexprToVal :: SExpr -> Maybe U2Member Source #

SMTValue Location Source # 

Methods

sexprToVal :: SExpr -> Maybe Location Source #

SMTValue Day Source # 

Methods

sexprToVal :: SExpr -> Maybe Day Source #

SMTValue BinOp Source # 

Methods

sexprToVal :: SExpr -> Maybe BinOp Source #

SMTValue UnOp Source # 

Methods

sexprToVal :: SExpr -> Maybe UnOp Source #

getValue :: SMTValue a => SBV a -> Query a Source #

Get the value of a term.

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.

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.

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 setOption $ ProduceUnsatCores True) for this call to not error out!

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.

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.

Getting solver information

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

Entering and exiting assertion stack

getAssertionStackDepth :: Query Int Source #

The current assertion stack depth, i.e., pops after start. Always non-negative.

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.

Communicating results back

Constructing assignments

(|->) :: SymWord a => SBV a -> a -> Assignment infix 1 Source #

Make an assignment. The type Assignment is abstract, see success for an example use case.

Miscellaneous

echo :: String -> Query () Source #

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

Terminating the query

mkSMTResult :: [Assignment] -> Query SMTResult Source #

Produce the query result from an assignment.

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.

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.

Performing actions

io :: IO a -> Query a Source #

Perform an arbitrary IO action.

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.

Instances

Show SMTOption Source # 
Generic SMTOption Source # 

Associated Types

type Rep SMTOption :: * -> * #

NFData SMTOption Source # 

Methods

rnf :: SMTOption -> () #

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

Logics supported

data Logic Source #

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.

Constructors

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!

Instances

Show Logic Source # 

Methods

showsPrec :: Int -> Logic -> ShowS #

show :: Logic -> String #

showList :: [Logic] -> ShowS #

Generic Logic Source # 

Associated Types

type Rep Logic :: * -> * #

Methods

from :: Logic -> Rep Logic x #

to :: Rep Logic x -> Logic #

NFData Logic Source # 

Methods

rnf :: Logic -> () #

GShow Logic Source # 
type Rep Logic Source # 
type Rep Logic = D1 (MetaData "Logic" "Data.SBV.Control.Types" "sbv-7.0-Dr9nfrJTFD01AI4IYir1JV" False) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "AUFLIA" PrefixI False) U1) ((:+:) (C1 (MetaCons "AUFLIRA" PrefixI False) U1) (C1 (MetaCons "AUFNIRA" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "LRA" PrefixI False) U1) (C1 (MetaCons "QF_ABV" PrefixI False) U1)) ((:+:) (C1 (MetaCons "QF_AUFBV" PrefixI False) U1) (C1 (MetaCons "QF_AUFLIA" PrefixI False) U1)))) ((:+:) ((:+:) (C1 (MetaCons "QF_AX" PrefixI False) U1) ((:+:) (C1 (MetaCons "QF_BV" PrefixI False) U1) (C1 (MetaCons "QF_IDL" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "QF_LIA" PrefixI False) U1) (C1 (MetaCons "QF_LRA" PrefixI False) U1)) ((:+:) (C1 (MetaCons "QF_NIA" PrefixI False) U1) (C1 (MetaCons "QF_NRA" PrefixI False) U1))))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "QF_RDL" PrefixI False) U1) ((:+:) (C1 (MetaCons "QF_UF" PrefixI False) U1) (C1 (MetaCons "QF_UFBV" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "QF_UFIDL" PrefixI False) U1) (C1 (MetaCons "QF_UFLIA" PrefixI False) U1)) ((:+:) (C1 (MetaCons "QF_UFLRA" PrefixI False) U1) (C1 (MetaCons "QF_UFNRA" PrefixI False) U1)))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "QF_UFNIRA" PrefixI False) U1) (C1 (MetaCons "UFLRA" PrefixI False) U1)) ((:+:) (C1 (MetaCons "UFNIA" PrefixI False) U1) (C1 (MetaCons "QF_FPBV" PrefixI False) U1))) ((:+:) ((:+:) (C1 (MetaCons "QF_FP" PrefixI False) U1) (C1 (MetaCons "QF_FD" PrefixI False) U1)) ((:+:) (C1 (MetaCons "Logic_ALL" PrefixI False) U1) (C1 (MetaCons "CustomLogic" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String))))))))