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

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

Data.SBV.Trans.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

More generalized alternative to `Data.SBV.Control` for advanced client use

Synopsis

- class MonadIO m => ExtractIO m where
  - extractIO :: m a -> IO (m a)
- class Monad m => MonadQuery m where
  - queryState :: m State
- data QueryT m a
- type Query = QueryT IO
- query :: ExtractIO m => QueryT m a -> SymbolicT m a
- freshVar_ :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => m (SBV a)
- freshVar :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => String -> m (SBV a)
- freshArray_ :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b)
- freshArray :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b)
- data CheckSatResult
  - = Sat
  - | Unsat
  - | Unk
- checkSat :: (MonadIO m, MonadQuery m) => m CheckSatResult
- ensureSat :: (MonadIO m, MonadQuery m) => m ()
- checkSatUsing :: (MonadIO m, MonadQuery m) => String -> m CheckSatResult
- checkSatAssuming :: (MonadIO m, MonadQuery m) => [SBool] -> m CheckSatResult
- checkSatAssumingWithUnsatisfiableSet :: (MonadIO m, MonadQuery m) => [SBool] -> m (CheckSatResult, Maybe [SBool])
- getValue :: (MonadIO m, MonadQuery m, SymVal a) => SBV a -> m a
- getFunction :: (MonadIO m, MonadQuery m, SolverContext m, MonadSymbolic m, SymVal a, SymVal r, SMTFunction fun a r) => fun -> m ([(a, r)], r)
- getUninterpretedValue :: (MonadIO m, MonadQuery m, HasKind a) => SBV a -> m String
- getModel :: (MonadIO m, MonadQuery m) => m SMTModel
- getAssignment :: (MonadIO m, MonadQuery m) => m [(String, Bool)]
- getSMTResult :: (MonadIO m, MonadQuery m) => m SMTResult
- getUnknownReason :: (MonadIO m, MonadQuery m) => m SMTReasonUnknown
- getObservables :: (MonadIO m, MonadQuery m) => m [(String, CV)]
- getUnsatCore :: (MonadIO m, MonadQuery m) => m [String]
- getProof :: (MonadIO m, MonadQuery m) => m String
- getInterpolantMathSAT :: (MonadIO m, MonadQuery m) => [String] -> m String
- getInterpolantZ3 :: (MonadIO m, MonadQuery m) => [SBool] -> m String
- getAssertions :: (MonadIO m, MonadQuery m) => m [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 :: (MonadIO m, MonadQuery m) => SMTInfoFlag -> m SMTInfoResponse
- getOption :: (MonadIO m, MonadQuery m) => (a -> SMTOption) -> m (Maybe SMTOption)
- getAssertionStackDepth :: (MonadIO m, MonadQuery m) => m Int
- push :: (MonadIO m, MonadQuery m) => Int -> m ()
- pop :: (MonadIO m, MonadQuery m) => Int -> m ()
- inNewAssertionStack :: (MonadIO m, MonadQuery m) => m a -> m a
- caseSplit :: (MonadIO m, MonadQuery m) => Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult))
- resetAssertions :: (MonadIO m, MonadQuery m) => m ()
- (|->) :: SymVal a => SBV a -> a -> Assignment
- mkSMTResult :: (MonadIO m, MonadQuery m) => [Assignment] -> m SMTResult
- exit :: (MonadIO m, MonadQuery m) => m ()
- ignoreExitCode :: SMTConfig -> Bool
- timeout :: (MonadIO m, MonadQuery m) => Int -> m a -> m a
- queryDebug :: (MonadIO m, MonadQuery m) => [String] -> m ()
- echo :: (MonadIO m, MonadQuery m) => String -> m ()
- io :: MonadIO m => IO a -> m 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]

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

data QueryT m a Source #

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

#### Instances

Instances details

MonadTrans QueryT Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods lift :: Monad m => m a -> QueryT m a
MonadSymbolic Query Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods symbolicEnv :: Query State Source #
MonadError e m => MonadError e (QueryT m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods throwError :: e -> QueryT m a catchError :: QueryT m a -> (e -> QueryT m a) -> QueryT m a
MonadWriter w m => MonadWriter w (QueryT m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods writer :: (a, w) -> QueryT m a tell :: w -> QueryT m () listen :: QueryT m a -> QueryT m (a, w) pass :: QueryT m (a, w -> w) -> QueryT m a
MonadReader r m => MonadReader r (QueryT m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods ask :: QueryT m r local :: (r -> r) -> QueryT m a -> QueryT m a reader :: (r -> a) -> QueryT m a
MonadState s m => MonadState s (QueryT m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods get :: QueryT m s put :: s -> QueryT m () state :: (s -> (a, s)) -> QueryT m a
Monad m => Monad (QueryT m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods (>>=) :: QueryT m a -> (a -> QueryT m b) -> QueryT m b (>>) :: QueryT m a -> QueryT m b -> QueryT m b return :: a -> QueryT m a
Functor m => Functor (QueryT m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods fmap :: (a -> b) -> QueryT m a -> QueryT m b (<$) :: a -> QueryT m b -> QueryT m a
Applicative m => Applicative (QueryT m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods pure :: a -> QueryT m a (<*>) :: QueryT m (a -> b) -> QueryT m a -> QueryT m b liftA2 :: (a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c (*>) :: QueryT m a -> QueryT m b -> QueryT m b (<*) :: QueryT m a -> QueryT m b -> QueryT m a
MonadIO m => MonadIO (QueryT m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods liftIO :: IO a -> QueryT m a
Monad m => MonadQuery (QueryT m) Source # |
Instance details Defined in Data.SBV.Core.Symbolic Methods queryState :: QueryT m State Source #
MonadIO m => SolverContext (QueryT m) Source # | `QueryT` as a `SolverContext`.

Instance details

Defined in Data.SBV.Control.Utils

Methods

constrain :: SBool -> QueryT m () Source #

softConstrain :: SBool -> QueryT m () Source #

namedConstraint :: String -> SBool -> QueryT m () Source #

constrainWithAttribute :: [(String, String)] -> SBool -> QueryT m () Source #

setInfo :: String -> [String] -> QueryT m () Source #

setOption :: SMTOption -> QueryT m () Source #

setLogic :: Logic -> QueryT m () Source #

addAxiom :: String -> [String] -> QueryT m () Source #

setTimeOut :: Integer -> QueryT m () Source #

contextState :: QueryT m State Source #

type Query = QueryT IO Source #

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

query :: ExtractIO m => QueryT m a -> SymbolicT m a Source #

Run a custom query.

# Create a fresh variable

freshVar_ :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => m (SBV a) Source #

Generalization of `freshVar_`

freshVar :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => String -> m (SBV a) Source #

Generalization of `freshVar`

# Create a fresh array

freshArray_ :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b) Source #

Generalization of `freshArray_`

freshArray :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b) Source #

Generalization of `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 :: (MonadIO m, MonadQuery m) => m CheckSatResult Source #

Generalization of `checkSat`

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

Generalization of `ensureSat`

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

Generalization of `checkSatUsing`

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

Generalization of `checkSatAssuming`

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

Generalization of `checkSatAssumingWithUnsatisfiableSet`

# Querying the solver

## Extracting values

getValue :: (MonadIO m, MonadQuery m, SymVal a) => SBV a -> m a Source #

Generalization of `getValue`

getFunction :: (MonadIO m, MonadQuery m, SolverContext m, MonadSymbolic m, SymVal a, SymVal r, SMTFunction fun a r) => fun -> m ([(a, r)], r) Source #

Generalization of `getFunction`

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

Generalization of `getUninterpretedValue`

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

Generalization of `getModel`

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

Generalization of `getAssignment`

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

Generalization of `getSMTResult`

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

Generalization of `getUnknownReason`

getObservables :: (MonadIO m, MonadQuery m) => m [(String, CV)] Source #

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

Generalization of `getUnsatCore`

## Extracting a proof

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

Generalization of `getProof`

## Extracting interpolants

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

Generalization of `getInterpolantMathSAT`. Use this version with MathSAT.

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

Generalization of `getInterpolantZ3`. Use this version with Z3.

## Extracting assertions

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

Generalization of `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 :: (MonadIO m, MonadQuery m) => SMTInfoFlag -> m SMTInfoResponse Source #

Generalization of `getInfo`

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

Generalization of `getInfo`

# Entering and exiting assertion stack

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

Generalization of `getAssertionStackDepth`

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

Generalization of `push`

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

Generalization of `pop`

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

Generalization of `inNewAssertionStack`

# Higher level tactics

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

Generalization of `caseSplit`

# Resetting the solver state

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

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

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

Generalization of `exit`

# Controlling the solver behavior

ignoreExitCode :: SMTConfig -> Bool Source #

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

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

Generalization of `timeout`

# Miscellaneous

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

Generalization of `queryDebug`

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

Generalization of `echo`

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

Generalization of `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]))))))