Data.SBV.Control

Control sublanguage for interacting with SMT solvers.

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!"
                      DSat{} -> error "Solver said DSat!"
                      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!"
                                     DSat{} -> error "Solver said DSat!"
                                     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 :: Type -> Type) where

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)

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

Instances

ExtractIO IO

Trivial IO extraction for IO.

Defined in Data.SBV.Utils.ExtractIO

Methods

extractIO :: IO a -> IO (IO a)

ExtractIO m => ExtractIO (MaybeT m)

IO extraction for MaybeT.

Defined in Data.SBV.Utils.ExtractIO

Methods

extractIO :: MaybeT m a -> IO (MaybeT m a)

ExtractIO m => ExtractIO (ExceptT e m)

IO extraction for ExceptT.

Defined in Data.SBV.Utils.ExtractIO

Methods

extractIO :: ExceptT e m a -> IO (ExceptT e m a)

(Monoid w, ExtractIO m) => ExtractIO (WriterT w m)

IO extraction for lazy WriterT.

Defined in Data.SBV.Utils.ExtractIO

Methods

extractIO :: WriterT w m a -> IO (WriterT w m a)

(Monoid w, ExtractIO m) => ExtractIO (WriterT w m)

IO extraction for strict WriterT.

Defined in Data.SBV.Utils.ExtractIO

Methods

extractIO :: WriterT w m a -> IO (WriterT w m a)

class Monad m => MonadQuery (m :: Type -> Type) where

Computations which support query operations.

Minimal complete definition

Nothing

Methods

queryState :: m State

default queryState :: forall (t :: (Type -> Type) -> Type -> Type) (m' :: Type -> Type). (MonadTrans t, MonadQuery m', m ~ t m') => m State

Instances

MonadQuery Q

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

queryState :: Q State

Monad m => MonadQuery (QueryT m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: QueryT m State

MonadQuery m => MonadQuery (MaybeT m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: MaybeT m State

MonadQuery m => MonadQuery (ExceptT e m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: ExceptT e m State

MonadQuery m => MonadQuery (ReaderT r m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: ReaderT r m State

MonadQuery m => MonadQuery (StateT s m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: StateT s m State

MonadQuery m => MonadQuery (StateT s m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: StateT s m State

(MonadQuery m, Monoid w) => MonadQuery (WriterT w m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: WriterT w m State

(MonadQuery m, Monoid w) => MonadQuery (WriterT w m)

Defined in Data.SBV.Core.Symbolic

Methods

queryState :: WriterT w m State

type Query = QueryT IO

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

query :: Query a -> Symbolic a

Run a custom query

Checking satisfiability

data CheckSatResult

Result of a checkSat or checkSatAssuming call.

Constructors

Sat

Satisfiable: A model is available, which can be queried with getValue.

DSat (Maybe String)

Delta-satisfiable: A delta-sat model is available. String is the precision info, if available.

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

Show CheckSatResult

Defined in Data.SBV.Control.Types

Methods

showsPrec :: Int -> CheckSatResult -> ShowS

show :: CheckSatResult -> String

showList :: [CheckSatResult] -> ShowS

Eq CheckSatResult

Defined in Data.SBV.Control.Types

Methods

(==) :: CheckSatResult -> CheckSatResult -> Bool

(/=) :: CheckSatResult -> CheckSatResult -> Bool

checkSat :: (MonadIO m, MonadQuery m) => m CheckSatResult

Generalization of checkSat

ensureSat :: (MonadIO m, MonadQuery m) => m ()

Generalization of ensureSat

checkSatUsing :: (MonadIO m, MonadQuery m) => String -> m CheckSatResult

Generalization of checkSatUsing

checkSatAssuming :: (MonadIO m, MonadQuery m) => [SBool] -> m CheckSatResult

Generalization of checkSatAssuming

checkSatAssumingWithUnsatisfiableSet :: (MonadIO m, MonadQuery m) => [SBool] -> m (CheckSatResult, Maybe [SBool])

Generalization of checkSatAssumingWithUnsatisfiableSet

Querying the solver

Extracting values

registerUISMTFunction :: (MonadIO m, SolverContext m, SMTFunction fun a r) => fun -> m ()

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, typically in query contexts.

registerSMTType :: forall a m. (MonadIO m, SolverContext m, HasKind a) => Proxy a -> m ()

Register a kind with the solver. Like registerUISMTFunction, this is typically not necessary since SBV will register kinds as it encounters them automatically. But there are cases where doing this can explicitly can come handy, typically in query contexts.

getFunction :: (MonadIO m, MonadQuery m, SolverContext m, MonadSymbolic m, SymVal a, SymVal r, SMTFunction fun a r) => fun -> m (Either (String, (Bool, Maybe [String], SExpr)) ([(a, r)], r))

Generalization of getFunction

getUninterpretedValue :: (MonadIO m, MonadQuery m, HasKind a) => SBV a -> m String

Generalization of getUninterpretedValue

getModel :: (MonadIO m, MonadQuery m) => m SMTModel

Generalization of getModel

getAssignment :: (MonadIO m, MonadQuery m) => m [(String, Bool)]

Generalization of getAssignment

getSMTResult :: (MonadIO m, MonadQuery m) => m SMTResult

Generalization of getSMTResult

getUnknownReason :: (MonadIO m, MonadQuery m) => m SMTReasonUnknown

Generalization of getUnknownReason

getObservables :: (MonadIO m, MonadQuery m) => m [(Name, CV)]

Get observables, i.e., those explicitly labeled by the user with a call to observe.

Extracting the unsat core

getUnsatCore :: (MonadIO m, MonadQuery m) => m [String]

Generalization of getUnsatCore

Extracting a proof

getProof :: (MonadIO m, MonadQuery m) => m String

Generalization of getProof

Extracting interpolants

getInterpolantMathSAT :: (MonadIO m, MonadQuery m) => [String] -> m String

Generalization of getInterpolantMathSAT. Use this version with MathSAT.

getInterpolantZ3 :: (MonadIO m, MonadQuery m) => [SBool] -> m String

Generalization of getInterpolantZ3. Use this version with Z3.

Getting abducts

getAbduct :: (SolverContext m, MonadIO m, MonadQuery m) => Maybe String -> String -> SBool -> m String

Generalization of getAbduct.

getAbductNext :: (MonadIO m, MonadQuery m) => m String

Generalization of getAbductNext.

Extracting assertions

getAssertions :: (MonadIO m, MonadQuery m) => m [String]

Generalization of getAssertions

Getting solver information

data SMTInfoFlag

Collectable information from the solver.

Constructors

AllStatistics

AssertionStackLevels

Authors

ErrorBehavior

Name

ReasonUnknown

Version

InfoKeyword String

Instances

Show SMTInfoFlag

Defined in Data.SBV.Control.Types

Methods

showsPrec :: Int -> SMTInfoFlag -> ShowS

show :: SMTInfoFlag -> String

showList :: [SMTInfoFlag] -> ShowS

data SMTErrorBehavior

Behavior of the solver for errors.

Constructors

ErrorImmediateExit

ErrorContinuedExecution

Instances

Show SMTErrorBehavior

Defined in Data.SBV.Control.Types

Methods

showsPrec :: Int -> SMTErrorBehavior -> ShowS

show :: SMTErrorBehavior -> String

showList :: [SMTErrorBehavior] -> ShowS

data SMTInfoResponse

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

Show SMTInfoResponse

Defined in Data.SBV.Control.Types

Methods

showsPrec :: Int -> SMTInfoResponse -> ShowS

show :: SMTInfoResponse -> String

showList :: [SMTInfoResponse] -> ShowS

getInfo :: (MonadIO m, MonadQuery m) => SMTInfoFlag -> m SMTInfoResponse

Generalization of getInfo

getOption :: (MonadIO m, MonadQuery m) => (a -> SMTOption) -> m (Maybe SMTOption)

Generalization of getInfo

Entering and exiting assertion stack

getAssertionStackDepth :: (MonadIO m, MonadQuery m) => m Int

Generalization of getAssertionStackDepth

push :: (MonadIO m, MonadQuery m) => Int -> m ()

Generalization of push

pop :: (MonadIO m, MonadQuery m) => Int -> m ()

Generalization of pop

inNewAssertionStack :: (MonadIO m, MonadQuery m) => m a -> m a

Generalization of inNewAssertionStack

Higher level tactics

caseSplit :: (MonadIO m, MonadQuery m) => Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult))

Generalization of caseSplit

Resetting the solver state

resetAssertions :: (MonadIO m, MonadQuery m) => m ()

Generalization of resetAssertions

Constructing assignments

(|->) :: SymVal a => SBV a -> a -> Assignment infix 1

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 :: (MonadIO m, MonadQuery m) => [Assignment] -> m SMTResult

Generalization of mkSMTResult NB. This function does not allow users to create interpretations for UI-Funs. But that's probably not a good idea anyhow. Also, if you use the validateModel or optimizeValidateConstraints features, SBV will fail on models returned via this function.

exit :: (MonadIO m, MonadQuery m) => m ()

Generalization of exit

Controlling the solver behavior

ignoreExitCode :: SMTConfig -> Bool

If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.

timeout :: (MonadIO m, MonadQuery m) => Int -> m a -> m a

Generalization of timeout

Miscellaneous

queryDebug :: (MonadIO m, MonadQuery m) => [String] -> m ()

Generalization of queryDebug

echo :: (MonadIO m, MonadQuery m) => String -> m ()

Generalization of echo

io :: MonadIO m => IO a -> m a

Generalization of io

Solver options

data SMTOption

Option values that can be set in the solver, following the SMTLib specification https://smt-lib.org/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

ProduceAbducts Bool

RandomSeed Integer

ReproducibleResourceLimit Integer

SMTVerbosity Integer

OptionKeyword String [String]

SetLogic Logic

SetInfo String [String]

Instances

Show SMTOption

Defined in Data.SBV.Control.Types

Methods

showsPrec :: Int -> SMTOption -> ShowS

show :: SMTOption -> String

showList :: [SMTOption] -> ShowS