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

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

Data.SBV.Internals

Contents

Description

Low level functions to access the SBV infrastructure, for developers who want to build further tools on top of SBV. End-users of the library should not need to use this module.

NB. There are various coding invariants in SBV that are maintained throughout the code. Indiscriminate use of functions in this module can break those invariants. So, you are on your own if you do utilize the functions here. (Unfortunately, what exactly those invariants are is a very good but also a very difficult question to answer!)

Synopsis

Running symbolic programs manually

data Result Source #

Result of running a symbolic computation

Constructors

Result 

Fields

Instances
Show Result Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

NFData Result Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: Result -> () #

data SBVRunMode Source #

Different means of running a symbolic piece of code

Constructors

SMTMode QueryContext IStage Bool SMTConfig

In regular mode, with a stage. Bool is True if this is SAT.

CodeGen

Code generation mode.

Concrete (Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)]))

Concrete simulation mode, with given environment if any. If Nothing: Random.

Instances
Show SBVRunMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

data IStage Source #

Stage of an interactive run

Constructors

ISetup 
ISafe 
IRun 

data QueryContext Source #

Query execution context

Constructors

QueryInternal

Triggered from inside SBV

QueryExternal

Triggered from user code

Instances
Show QueryContext Source #

Show instance for QueryContext, for debugging purposes

Instance details

Defined in Data.SBV.Core.Symbolic

Solver capabilities

data SolverCapabilities Source #

Translation tricks needed for specific capabilities afforded by each solver

Constructors

SolverCapabilities 

Fields

Internal structures useful for low-level programming

type SBool = SBV Bool Source #

A symbolic boolean/bit

type SWord8 = SBV Word8 Source #

8-bit unsigned symbolic value

type SWord16 = SBV Word16 Source #

16-bit unsigned symbolic value

type SWord32 = SBV Word32 Source #

32-bit unsigned symbolic value

type SWord64 = SBV Word64 Source #

64-bit unsigned symbolic value

type SInt8 = SBV Int8 Source #

8-bit signed symbolic value, 2's complement representation

type SInt16 = SBV Int16 Source #

16-bit signed symbolic value, 2's complement representation

type SInt32 = SBV Int32 Source #

32-bit signed symbolic value, 2's complement representation

type SInt64 = SBV Int64 Source #

64-bit signed symbolic value, 2's complement representation

type SInteger = SBV Integer Source #

Infinite precision signed symbolic value

type SReal = SBV AlgReal Source #

Infinite precision symbolic algebraic real value

type SFloat = SBV Float Source #

IEEE-754 single-precision floating point numbers

type SDouble = SBV Double Source #

IEEE-754 double-precision floating point numbers

type SChar = SBV Char Source #

A symbolic character. Note that, as far as SBV's symbolic strings are concerned, a character is currently an 8-bit unsigned value, corresponding to the ISO-8859-1 (Latin-1) character set: http://en.wikipedia.org/wiki/ISO/IEC_8859-1. A Haskell Char, on the other hand, is based on unicode. Therefore, there isn't a 1-1 correspondence between a Haskell character and an SBV character for the time being. This limitation is due to the SMT-solvers only supporting this particular subset. However, there is a pending proposal to add support for unicode, and SBV will track these changes to have full unicode support as solvers become available. For details, see: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml

type SString = SBV String Source #

A symbolic string. Note that a symbolic string is not a list of symbolic characters, that is, it is not the case that SString = [SChar], unlike what one might expect following Haskell strings. An SString is a symbolic value of its own, of possibly arbitrary but finite length, and internally processed as one unit as opposed to a fixed-length list of characters.

type SList a = SBV [a] Source #

A symbolic list of items. Note that a symbolic list is not a list of symbolic items, that is, it is not the case that SList a = [a], unlike what one might expect following haskell lists/sequences. An SList is a symbolic value of its own, of possibly arbitrary but finite length, and internally processed as one unit as opposed to a fixed-length list of items. Note that lists can be nested, i.e., we do allow lists of lists of ... items.

type SEither a b = SBV (Either a b) Source #

Symbolic Either

type SMaybe a = SBV (Maybe a) Source #

Symbolic Maybe

type STuple a b = SBV (a, b) Source #

Symbolic 2-tuple. NB. STuple and STuple2 are equivalent.

type STuple2 a b = SBV (a, b) Source #

Symbolic 2-tuple. NB. STuple and STuple2 are equivalent.

type STuple3 a b c = SBV (a, b, c) Source #

Symbolic 3-tuple.

type STuple4 a b c d = SBV (a, b, c, d) Source #

Symbolic 4-tuple.

type STuple5 a b c d e = SBV (a, b, c, d, e) Source #

Symbolic 5-tuple.

type STuple6 a b c d e f = SBV (a, b, c, d, e, f) Source #

Symbolic 6-tuple.

type STuple7 a b c d e f g = SBV (a, b, c, d, e, f, g) Source #

Symbolic 7-tuple.

type STuple8 a b c d e f g h = SBV (a, b, c, d, e, f, g, h) Source #

Symbolic 8-tuple.

data RCSet a Source #

A RCSet is either a regular set or a set given by its complement from the corresponding universal set.

Constructors

RegularSet (Set a) 
ComplementSet (Set a) 
Instances
Show a => Show (RCSet a) Source #

Show instance. Regular sets are shown as usual. Complements are shown "U -" notation.

Instance details

Defined in Data.SBV.Core.Concrete

Methods

showsPrec :: Int -> RCSet a -> ShowS #

show :: RCSet a -> String #

showList :: [RCSet a] -> ShowS #

HasKind a => HasKind (RCSet a) Source # 
Instance details

Defined in Data.SBV.Core.Concrete

(Ord a, SymVal a) => SymVal (RCSet a) Source # 
Instance details

Defined in Data.SBV.Core.Model

(Ord a, SymVal a) => SMTValue (RCSet a) Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe (RCSet a) Source #

type SSet a = SBV (RCSet a) Source #

Symbolic Set. Note that we use RCSet, which supports both regular sets and complements, i.e., those obtained from the universal set (of the right type) by removing elements.

nan :: Floating a => a Source #

Not-A-Number for Double and Float. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here.

infinity :: Floating a => a Source #

Infinity for Double and Float. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here.

sNaN :: (Floating a, SymVal a) => SBV a Source #

Symbolic variant of Not-A-Number. This value will inhabit both SDouble and SFloat.

sInfinity :: (Floating a, SymVal a) => SBV a Source #

Symbolic variant of infinity. This value will inhabit both SDouble and SFloat.

data RoundingMode Source #

Rounding mode to be used for the IEEE floating-point operations. Note that Haskell's default is RoundNearestTiesToEven. If you use a different rounding mode, then the counter-examples you get may not match what you observe in Haskell.

Constructors

RoundNearestTiesToEven

Round to nearest representable floating point value. If precisely at half-way, pick the even number. (In this context, even means the lowest-order bit is zero.)

RoundNearestTiesToAway

Round to nearest representable floating point value. If precisely at half-way, pick the number further away from 0. (That is, for positive values, pick the greater; for negative values, pick the smaller.)

RoundTowardPositive

Round towards positive infinity. (Also known as rounding-up or ceiling.)

RoundTowardNegative

Round towards negative infinity. (Also known as rounding-down or floor.)

RoundTowardZero

Round towards zero. (Also known as truncation.)

Instances
Bounded RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Enum RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Eq RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Data RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RoundingMode #

toConstr :: RoundingMode -> Constr #

dataTypeOf :: RoundingMode -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RoundingMode) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RoundingMode) #

gmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r #

gmapQ :: (forall d. Data d => d -> u) -> RoundingMode -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RoundingMode -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode #

Ord RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Read RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Show RoundingMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

HasKind RoundingMode Source #

RoundingMode kind

Instance details

Defined in Data.SBV.Core.Symbolic

SymVal RoundingMode Source #

RoundingMode can be used symbolically

Instance details

Defined in Data.SBV.Core.Data

SatModel RoundingMode Source #

A rounding mode, extracted from a model. (Default definition suffices)

Instance details

Defined in Data.SBV.SMT.SMT

Methods

parseCVs :: [CV] -> Maybe (RoundingMode, [CV]) Source #

cvtModel :: (RoundingMode -> Maybe b) -> Maybe (RoundingMode, [CV]) -> Maybe (b, [CV]) Source #

type SRoundingMode = SBV RoundingMode Source #

The symbolic variant of RoundingMode

class (HasKind a, Typeable a) => SymVal a where Source #

A SymVal is a potential symbolic value that can be created instances of to be fed to a symbolic program.

Minimal complete definition

Nothing

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV a) Source #

Generalization of mkSymVal

literal :: a -> SBV a Source #

Turn a literal constant to symbolic

fromCV :: CV -> a Source #

Extract a literal, from a CV representation

isConcretely :: SBV a -> (a -> Bool) -> Bool Source #

Does it concretely satisfy the given predicate?

mkSymVal :: (MonadSymbolic m, Read a, Data a) => Maybe Quantifier -> Maybe String -> m (SBV a) Source #

Generalization of mkSymVal

literal :: Show a => a -> SBV a Source #

Turn a literal constant to symbolic

fromCV :: Read a => CV -> a Source #

Extract a literal, from a CV representation

forall :: MonadSymbolic m => String -> m (SBV a) Source #

Generalization of forall

forall_ :: MonadSymbolic m => m (SBV a) Source #

Generalization of forall_

mkForallVars :: MonadSymbolic m => Int -> m [SBV a] Source #

Generalization of mkForallVars

exists :: MonadSymbolic m => String -> m (SBV a) Source #

Generalization of exists

exists_ :: MonadSymbolic m => m (SBV a) Source #

Generalization of exists_

mkExistVars :: MonadSymbolic m => Int -> m [SBV a] Source #

Generalization of mkExistVars

free :: MonadSymbolic m => String -> m (SBV a) Source #

Generalization of free

free_ :: MonadSymbolic m => m (SBV a) Source #

Generalization of free_

mkFreeVars :: MonadSymbolic m => Int -> m [SBV a] Source #

Generalization of mkFreeVars

symbolic :: MonadSymbolic m => String -> m (SBV a) Source #

Generalization of symbolic

symbolics :: MonadSymbolic m => [String] -> m [SBV a] Source #

Generalization of symbolics

unliteral :: SBV a -> Maybe a Source #

Extract a literal, if the value is concrete

isConcrete :: SBV a -> Bool Source #

Is the symbolic word concrete?

isSymbolic :: SBV a -> Bool Source #

Is the symbolic word really symbolic?

Instances
SymVal Bool Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal Char Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal Double Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal Float Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal Int8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal Int16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal Int32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal Int64 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal Integer Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal Word8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal Word16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal Word32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal Word64 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal () Source #

SymVal for 0-tuple (i.e., unit)

Instance details

Defined in Data.SBV.Core.Model

SymVal AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Model

SymVal RoundingMode Source #

RoundingMode can be used symbolically

Instance details

Defined in Data.SBV.Core.Data

SymVal State Source # 
Instance details

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

SymVal E Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

SymVal Word4 Source #

SymVal instance, allowing this type to be used in proofs/sat etc.

Instance details

Defined in Documentation.SBV.Examples.Misc.Word4

SymVal Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Optimization.Enumerate

SymVal Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymVal Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymVal Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymVal Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymVal Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymVal Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Garden

SymVal Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

SymVal U2Member Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

SymVal Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

SymVal Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

SymVal BinOp Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

SymVal UnOp Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

SymVal B Source # 
Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Deduce

SymVal Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

SymVal L Source #

Declare instances to make L a usable uninterpreted sort. First we need the SymVal instance, with the default definition sufficing.

Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

SymVal a => SymVal [a] Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV [a]) Source #

literal :: [a] -> SBV [a] Source #

fromCV :: CV -> [a] Source #

isConcretely :: SBV [a] -> ([a] -> Bool) -> Bool Source #

forall :: MonadSymbolic m => String -> m (SBV [a]) Source #

forall_ :: MonadSymbolic m => m (SBV [a]) Source #

mkForallVars :: MonadSymbolic m => Int -> m [SBV [a]] Source #

exists :: MonadSymbolic m => String -> m (SBV [a]) Source #

exists_ :: MonadSymbolic m => m (SBV [a]) Source #

mkExistVars :: MonadSymbolic m => Int -> m [SBV [a]] Source #

free :: MonadSymbolic m => String -> m (SBV [a]) Source #

free_ :: MonadSymbolic m => m (SBV [a]) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV [a]] Source #

symbolic :: MonadSymbolic m => String -> m (SBV [a]) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV [a]] Source #

unliteral :: SBV [a] -> Maybe [a] Source #

isConcrete :: SBV [a] -> Bool Source #

isSymbolic :: SBV [a] -> Bool Source #

SymVal a => SymVal (Maybe a) Source # 
Instance details

Defined in Data.SBV.Core.Model

(Ord a, SymVal a) => SymVal (RCSet a) Source # 
Instance details

Defined in Data.SBV.Core.Model

(SymVal a, SymVal b) => SymVal (Either a b) Source # 
Instance details

Defined in Data.SBV.Core.Model

(SymVal a, SymVal b) => SymVal (a, b) Source #

SymVal for 2-tuples

Instance details

Defined in Data.SBV.Core.Model

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV (a, b)) Source #

literal :: (a, b) -> SBV (a, b) Source #

fromCV :: CV -> (a, b) Source #

isConcretely :: SBV (a, b) -> ((a, b) -> Bool) -> Bool Source #

forall :: MonadSymbolic m => String -> m (SBV (a, b)) Source #

forall_ :: MonadSymbolic m => m (SBV (a, b)) Source #

mkForallVars :: MonadSymbolic m => Int -> m [SBV (a, b)] Source #

exists :: MonadSymbolic m => String -> m (SBV (a, b)) Source #

exists_ :: MonadSymbolic m => m (SBV (a, b)) Source #

mkExistVars :: MonadSymbolic m => Int -> m [SBV (a, b)] Source #

free :: MonadSymbolic m => String -> m (SBV (a, b)) Source #

free_ :: MonadSymbolic m => m (SBV (a, b)) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV (a, b)] Source #

symbolic :: MonadSymbolic m => String -> m (SBV (a, b)) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV (a, b)] Source #

unliteral :: SBV (a, b) -> Maybe (a, b) Source #

isConcrete :: SBV (a, b) -> Bool Source #

isSymbolic :: SBV (a, b) -> Bool Source #

(SymVal a, SymVal b, SymVal c) => SymVal (a, b, c) Source #

SymVal for 3-tuples

Instance details

Defined in Data.SBV.Core.Model

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV (a, b, c)) Source #

literal :: (a, b, c) -> SBV (a, b, c) Source #

fromCV :: CV -> (a, b, c) Source #

isConcretely :: SBV (a, b, c) -> ((a, b, c) -> Bool) -> Bool Source #

forall :: MonadSymbolic m => String -> m (SBV (a, b, c)) Source #

forall_ :: MonadSymbolic m => m (SBV (a, b, c)) Source #

mkForallVars :: MonadSymbolic m => Int -> m [SBV (a, b, c)] Source #

exists :: MonadSymbolic m => String -> m (SBV (a, b, c)) Source #

exists_ :: MonadSymbolic m => m (SBV (a, b, c)) Source #

mkExistVars :: MonadSymbolic m => Int -> m [SBV (a, b, c)] Source #

free :: MonadSymbolic m => String -> m (SBV (a, b, c)) Source #

free_ :: MonadSymbolic m => m (SBV (a, b, c)) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV (a, b, c)] Source #

symbolic :: MonadSymbolic m => String -> m (SBV (a, b, c)) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV (a, b, c)] Source #

unliteral :: SBV (a, b, c) -> Maybe (a, b, c) Source #

isConcrete :: SBV (a, b, c) -> Bool Source #

isSymbolic :: SBV (a, b, c) -> Bool Source #

(SymVal a, SymVal b, SymVal c, SymVal d) => SymVal (a, b, c, d) Source #

SymVal for 4-tuples

Instance details

Defined in Data.SBV.Core.Model

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV (a, b, c, d)) Source #

literal :: (a, b, c, d) -> SBV (a, b, c, d) Source #

fromCV :: CV -> (a, b, c, d) Source #

isConcretely :: SBV (a, b, c, d) -> ((a, b, c, d) -> Bool) -> Bool Source #

forall :: MonadSymbolic m => String -> m (SBV (a, b, c, d)) Source #

forall_ :: MonadSymbolic m => m (SBV (a, b, c, d)) Source #

mkForallVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d)] Source #

exists :: MonadSymbolic m => String -> m (SBV (a, b, c, d)) Source #

exists_ :: MonadSymbolic m => m (SBV (a, b, c, d)) Source #

mkExistVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d)] Source #

free :: MonadSymbolic m => String -> m (SBV (a, b, c, d)) Source #

free_ :: MonadSymbolic m => m (SBV (a, b, c, d)) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d)] Source #

symbolic :: MonadSymbolic m => String -> m (SBV (a, b, c, d)) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV (a, b, c, d)] Source #

unliteral :: SBV (a, b, c, d) -> Maybe (a, b, c, d) Source #

isConcrete :: SBV (a, b, c, d) -> Bool Source #

isSymbolic :: SBV (a, b, c, d) -> Bool Source #

(SymVal a, SymVal b, SymVal c, SymVal d, SymVal e) => SymVal (a, b, c, d, e) Source #

SymVal for 5-tuples

Instance details

Defined in Data.SBV.Core.Model

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV (a, b, c, d, e)) Source #

literal :: (a, b, c, d, e) -> SBV (a, b, c, d, e) Source #

fromCV :: CV -> (a, b, c, d, e) Source #

isConcretely :: SBV (a, b, c, d, e) -> ((a, b, c, d, e) -> Bool) -> Bool Source #

forall :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e)) Source #

forall_ :: MonadSymbolic m => m (SBV (a, b, c, d, e)) Source #

mkForallVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d, e)] Source #

exists :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e)) Source #

exists_ :: MonadSymbolic m => m (SBV (a, b, c, d, e)) Source #

mkExistVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d, e)] Source #

free :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e)) Source #

free_ :: MonadSymbolic m => m (SBV (a, b, c, d, e)) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d, e)] Source #

symbolic :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e)) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV (a, b, c, d, e)] Source #

unliteral :: SBV (a, b, c, d, e) -> Maybe (a, b, c, d, e) Source #

isConcrete :: SBV (a, b, c, d, e) -> Bool Source #

isSymbolic :: SBV (a, b, c, d, e) -> Bool Source #

(SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f) => SymVal (a, b, c, d, e, f) Source #

SymVal for 6-tuples

Instance details

Defined in Data.SBV.Core.Model

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV (a, b, c, d, e, f)) Source #

literal :: (a, b, c, d, e, f) -> SBV (a, b, c, d, e, f) Source #

fromCV :: CV -> (a, b, c, d, e, f) Source #

isConcretely :: SBV (a, b, c, d, e, f) -> ((a, b, c, d, e, f) -> Bool) -> Bool Source #

forall :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e, f)) Source #

forall_ :: MonadSymbolic m => m (SBV (a, b, c, d, e, f)) Source #

mkForallVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d, e, f)] Source #

exists :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e, f)) Source #

exists_ :: MonadSymbolic m => m (SBV (a, b, c, d, e, f)) Source #

mkExistVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d, e, f)] Source #

free :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e, f)) Source #

free_ :: MonadSymbolic m => m (SBV (a, b, c, d, e, f)) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d, e, f)] Source #

symbolic :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e, f)) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV (a, b, c, d, e, f)] Source #

unliteral :: SBV (a, b, c, d, e, f) -> Maybe (a, b, c, d, e, f) Source #

isConcrete :: SBV (a, b, c, d, e, f) -> Bool Source #

isSymbolic :: SBV (a, b, c, d, e, f) -> Bool Source #

(SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g) => SymVal (a, b, c, d, e, f, g) Source #

SymVal for 7-tuples

Instance details

Defined in Data.SBV.Core.Model

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV (a, b, c, d, e, f, g)) Source #

literal :: (a, b, c, d, e, f, g) -> SBV (a, b, c, d, e, f, g) Source #

fromCV :: CV -> (a, b, c, d, e, f, g) Source #

isConcretely :: SBV (a, b, c, d, e, f, g) -> ((a, b, c, d, e, f, g) -> Bool) -> Bool Source #

forall :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e, f, g)) Source #

forall_ :: MonadSymbolic m => m (SBV (a, b, c, d, e, f, g)) Source #

mkForallVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d, e, f, g)] Source #

exists :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e, f, g)) Source #

exists_ :: MonadSymbolic m => m (SBV (a, b, c, d, e, f, g)) Source #

mkExistVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d, e, f, g)] Source #

free :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e, f, g)) Source #

free_ :: MonadSymbolic m => m (SBV (a, b, c, d, e, f, g)) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d, e, f, g)] Source #

symbolic :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e, f, g)) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV (a, b, c, d, e, f, g)] Source #

unliteral :: SBV (a, b, c, d, e, f, g) -> Maybe (a, b, c, d, e, f, g) Source #

isConcrete :: SBV (a, b, c, d, e, f, g) -> Bool Source #

isSymbolic :: SBV (a, b, c, d, e, f, g) -> Bool Source #

(SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h) => SymVal (a, b, c, d, e, f, g, h) Source #

SymVal for 8-tuples

Instance details

Defined in Data.SBV.Core.Model

Methods

mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV (a, b, c, d, e, f, g, h)) Source #

literal :: (a, b, c, d, e, f, g, h) -> SBV (a, b, c, d, e, f, g, h) Source #

fromCV :: CV -> (a, b, c, d, e, f, g, h) Source #

isConcretely :: SBV (a, b, c, d, e, f, g, h) -> ((a, b, c, d, e, f, g, h) -> Bool) -> Bool Source #

forall :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e, f, g, h)) Source #

forall_ :: MonadSymbolic m => m (SBV (a, b, c, d, e, f, g, h)) Source #

mkForallVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d, e, f, g, h)] Source #

exists :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e, f, g, h)) Source #

exists_ :: MonadSymbolic m => m (SBV (a, b, c, d, e, f, g, h)) Source #

mkExistVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d, e, f, g, h)] Source #

free :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e, f, g, h)) Source #

free_ :: MonadSymbolic m => m (SBV (a, b, c, d, e, f, g, h)) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV (a, b, c, d, e, f, g, h)] Source #

symbolic :: MonadSymbolic m => String -> m (SBV (a, b, c, d, e, f, g, h)) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV (a, b, c, d, e, f, g, h)] Source #

unliteral :: SBV (a, b, c, d, e, f, g, h) -> Maybe (a, b, c, d, e, f, g, h) Source #

isConcrete :: SBV (a, b, c, d, e, f, g, h) -> Bool Source #

isSymbolic :: SBV (a, b, c, d, e, f, g, h) -> Bool Source #

data CV Source #

CV represents a concrete word of a fixed size: For signed words, the most significant digit is considered to be the sign.

Constructors

CV 

Fields

Instances
Eq CV Source # 
Instance details

Defined in Data.SBV.Core.Concrete

Methods

(==) :: CV -> CV -> Bool #

(/=) :: CV -> CV -> Bool #

Ord CV Source # 
Instance details

Defined in Data.SBV.Core.Concrete

Methods

compare :: CV -> CV -> Ordering #

(<) :: CV -> CV -> Bool #

(<=) :: CV -> CV -> Bool #

(>) :: CV -> CV -> Bool #

(>=) :: CV -> CV -> Bool #

max :: CV -> CV -> CV #

min :: CV -> CV -> CV #

Show CV Source #

Show instance for CV.

Instance details

Defined in Data.SBV.Core.Concrete

Methods

showsPrec :: Int -> CV -> ShowS #

show :: CV -> String #

showList :: [CV] -> ShowS #

NFData CV Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: CV -> () #

HasKind CV Source #

Kind instance for CV

Instance details

Defined in Data.SBV.Core.Concrete

PrettyNum CV Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

SatModel CV Source #

CV as extracted from a model; trivial definition

Instance details

Defined in Data.SBV.SMT.SMT

Methods

parseCVs :: [CV] -> Maybe (CV, [CV]) Source #

cvtModel :: (CV -> Maybe b) -> Maybe (CV, [CV]) -> Maybe (b, [CV]) Source #

SDivisible CV Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

sQuotRem :: CV -> CV -> (CV, CV) Source #

sDivMod :: CV -> CV -> (CV, CV) Source #

sQuot :: CV -> CV -> CV Source #

sRem :: CV -> CV -> CV Source #

sDiv :: CV -> CV -> CV Source #

sMod :: CV -> CV -> CV Source #

data CVal Source #

A constant value

Constructors

CAlgReal !AlgReal

Algebraic real

CInteger !Integer

Bit-vector/unbounded integer

CFloat !Float

Float

CDouble !Double

Double

CChar !Char

Character

CString !String

String

CList ![CVal]

List

CSet !(RCSet CVal)

Set. Can be regular or complemented.

CUserSort !(Maybe Int, String)

Value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations

CTuple ![CVal]

Tuple

CMaybe !(Maybe CVal)

Maybe

CEither !(Either CVal CVal)

Disjoint union

Instances
Eq CVal Source #

Eq instance for CVVal. Note that we cannot simply derive Eq/Ord, since CVAlgReal doesn't have proper instances for these when values are infinitely precise reals. However, we do need a structural eq/ord for Map indexes; so define custom ones here:

Instance details

Defined in Data.SBV.Core.Concrete

Methods

(==) :: CVal -> CVal -> Bool #

(/=) :: CVal -> CVal -> Bool #

Ord CVal Source #

Ord instance for VWVal. Same comments as the Eq instance why this cannot be derived.

Instance details

Defined in Data.SBV.Core.Concrete

Methods

compare :: CVal -> CVal -> Ordering #

(<) :: CVal -> CVal -> Bool #

(<=) :: CVal -> CVal -> Bool #

(>) :: CVal -> CVal -> Bool #

(>=) :: CVal -> CVal -> Bool #

max :: CVal -> CVal -> CVal #

min :: CVal -> CVal -> CVal #

data AlgReal Source #

Algebraic reals. Note that the representation is left abstract. We represent rational results explicitly, while the roots-of-polynomials are represented implicitly by their defining equation

Constructors

AlgRational Bool Rational

bool says it's exact (i.e., SMT-solver did not return it with ? at the end.)

AlgPolyRoot (Integer, AlgRealPoly) (Maybe String)

which root of this polynomial and an approximate decimal representation with given precision, if available

Instances
Eq AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Methods

(==) :: AlgReal -> AlgReal -> Bool #

(/=) :: AlgReal -> AlgReal -> Bool #

Fractional AlgReal Source #

NB: Following the other types we have, we require `a/0` to be `0` for all a.

Instance details

Defined in Data.SBV.Core.AlgReals

Num AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Ord AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Real AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Show AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Arbitrary AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Random AlgReal Source # 
Instance details

Defined in Data.SBV.Core.AlgReals

Methods

randomR :: RandomGen g => (AlgReal, AlgReal) -> g -> (AlgReal, g) #

random :: RandomGen g => g -> (AlgReal, g) #

randomRs :: RandomGen g => (AlgReal, AlgReal) -> g -> [AlgReal] #

randoms :: RandomGen g => g -> [AlgReal] #

randomRIO :: (AlgReal, AlgReal) -> IO AlgReal #

randomIO :: IO AlgReal #

HasKind AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Kind

SymVal AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Model

SatModel AlgReal Source #

AlgReal as extracted from a model

Instance details

Defined in Data.SBV.SMT.SMT

Methods

parseCVs :: [CV] -> Maybe (AlgReal, [CV]) Source #

cvtModel :: (AlgReal -> Maybe b) -> Maybe (AlgReal, [CV]) -> Maybe (b, [CV]) Source #

SMTValue AlgReal Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe AlgReal Source #

Metric AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Model

Associated Types

type MetricSpace AlgReal :: Type Source #

IEEEFloatConvertible AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Floating

type MetricSpace AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Model

newtype AlgRealPoly Source #

A univariate polynomial, represented simply as a coefficient list. For instance, "5x^3 + 2x - 5" is represented as [(5, 3), (2, 1), (-5, 0)]

Constructors

AlgRealPoly [(Integer, Integer)] 

data ExtCV Source #

A simple expression type over extendent values, covering infinity, epsilon and intervals.

isRegularCV :: GeneralizedCV -> Bool Source #

Is this a regular CV?

cvSameType :: CV -> CV -> Bool Source #

Are two CV's of the same type?

cvToBool :: CV -> Bool Source #

Convert a CV to a Haskell boolean (NB. Assumes input is well-kinded)

mkConstCV :: Integral a => Kind -> a -> CV Source #

Create a constant word from an integral.

liftCV2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> (Char -> Char -> b) -> (String -> String -> b) -> ([CVal] -> [CVal] -> b) -> ([CVal] -> [CVal] -> b) -> (Maybe CVal -> Maybe CVal -> b) -> (Either CVal CVal -> Either CVal CVal -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CV -> CV -> b Source #

Lift a binary function through a CV.

mapCV :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> (Char -> Char) -> (String -> String) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CV -> CV Source #

Map a unary function through a CV.

mapCV2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> (Char -> Char -> Char) -> (String -> String -> String) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CV -> CV -> CV Source #

Map a binary function through a CV.

data SV Source #

A symbolic word, tracking it's signedness and size.

Constructors

SV !Kind !NodeId 
Instances
Eq SV Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

(==) :: SV -> SV -> Bool #

(/=) :: SV -> SV -> Bool #

Ord SV Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

compare :: SV -> SV -> Ordering #

(<) :: SV -> SV -> Bool #

(<=) :: SV -> SV -> Bool #

(>) :: SV -> SV -> Bool #

(>=) :: SV -> SV -> Bool #

max :: SV -> SV -> SV #

min :: SV -> SV -> SV #

Show SV Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

showsPrec :: Int -> SV -> ShowS #

show :: SV -> String #

showList :: [SV] -> ShowS #

NFData SV Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SV -> () #

HasKind SV Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

trueSV :: SV Source #

Constant True as an SV. Note that this value always occupies slot -1.

falseSV :: SV Source #

Constant False as an SV. Note that this value always occupies slot -2.

trueCV :: CV Source #

Constant True as a CV. We represent it using the integer value 1.

falseCV :: CV Source #

Constant False as a CV. We represent it using the integer value 0.

normCV :: CV -> CV Source #

Normalize a CV. Essentially performs modular arithmetic to make sure the value can fit in the given bit-size. Note that this is rather tricky for negative values, due to asymmetry. (i.e., an 8-bit negative number represents values in the range -128 to 127; thus we have to be careful on the negative side.)

data SVal Source #

The Symbolic value. Either a constant (Left) or a symbolic value (Right Cached). Note that caching is essential for making sure sharing is preserved.

Constructors

SVal !Kind !(Either CV (Cached SV)) 
Instances
Eq SVal Source #

This instance is only defined so that we can define an instance for Bits. == and /= simply throw an error.

Instance details

Defined in Data.SBV.Core.Symbolic

Methods

(==) :: SVal -> SVal -> Bool #

(/=) :: SVal -> SVal -> Bool #

Show SVal Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

showsPrec :: Int -> SVal -> ShowS #

show :: SVal -> String #

showList :: [SVal] -> ShowS #

NFData SVal Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SVal -> () #

HasKind SVal Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

ArithOverflow SVal Source # 
Instance details

Defined in Data.SBV.Tools.Overflow

Testable (Symbolic SVal) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

property :: Symbolic SVal -> Property #

propertyForAllShrinkShow :: Gen a -> (a -> [a]) -> (a -> [String]) -> (a -> Symbolic SVal) -> Property #

sTrue :: SBool Source #

Symbolic True

sNot :: SBool -> SBool Source #

Symbolic boolean negation

(.&&) :: SBool -> SBool -> SBool infixr 3 Source #

Symbolic conjunction

(.||) :: SBool -> SBool -> SBool infixr 2 Source #

Symbolic disjunction

(.<+>) :: SBool -> SBool -> SBool infixl 6 Source #

Symbolic logical xor

(.~&) :: SBool -> SBool -> SBool infixr 3 Source #

Symbolic nand

(.~|) :: SBool -> SBool -> SBool infixr 2 Source #

Symbolic nor

(.=>) :: SBool -> SBool -> SBool infixr 1 Source #

Symbolic implication

(.<=>) :: SBool -> SBool -> SBool infixr 1 Source #

Symbolic boolean equivalence

sAnd :: [SBool] -> SBool Source #

Generalization of and

sOr :: [SBool] -> SBool Source #

Generalization of or

sAny :: (a -> SBool) -> [a] -> SBool Source #

Generalization of any

sAll :: (a -> SBool) -> [a] -> SBool Source #

Generalization of all

fromBool :: Bool -> SBool Source #

Conversion from Bool to SBool

newtype SBV a Source #

The Symbolic value. The parameter a is phantom, but is extremely important in keeping the user interface strongly typed.

Constructors

SBV 

Fields

Instances
IsString SString Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

fromString :: String -> SString #

Testable SBool Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

property :: SBool -> Property #

propertyForAllShrinkShow :: Gen a -> (a -> [a]) -> (a -> [String]) -> (a -> SBool) -> Property #

SDivisible SInteger Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SInt64 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SInt32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SInt16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SInt8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SWord64 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SWord32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SWord16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SWord8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SDivisible SWord4 Source #

SDvisible instance, using default methods

Instance details

Defined in Documentation.SBV.Examples.Misc.Word4

Polynomial SWord64 Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

Polynomial SWord32 Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

Polynomial SWord16 Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

Polynomial SWord8 Source # 
Instance details

Defined in Data.SBV.Tools.Polynomial

ArithOverflow SInt64 Source # 
Instance details

Defined in Data.SBV.Tools.Overflow

ArithOverflow SInt32 Source # 
Instance details

Defined in Data.SBV.Tools.Overflow

ArithOverflow SInt16 Source # 
Instance details

Defined in Data.SBV.Tools.Overflow

ArithOverflow SInt8 Source # 
Instance details

Defined in Data.SBV.Tools.Overflow

ArithOverflow SWord64 Source # 
Instance details

Defined in Data.SBV.Tools.Overflow

ArithOverflow SWord32 Source # 
Instance details

Defined in Data.SBV.Tools.Overflow

ArithOverflow SWord16 Source # 
Instance details

Defined in Data.SBV.Tools.Overflow

ArithOverflow SWord8 Source # 
Instance details

Defined in Data.SBV.Tools.Overflow

RegExpMatchable SString Source #

Matching symbolic strings.

Instance details

Defined in Data.SBV.RegExp

Methods

match :: SString -> RegExp -> SBool Source #

RegExpMatchable SChar Source #

Matching a character simply means the singleton string matches the regex.

Instance details

Defined in Data.SBV.RegExp

Methods

match :: SChar -> RegExp -> SBool Source #

ExtractIO m => MProvable m SBool Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Splittable SWord64 SWord32 Source # 
Instance details

Defined in Data.SBV.Core.Splittable

Splittable SWord32 SWord16 Source # 
Instance details

Defined in Data.SBV.Core.Splittable

Splittable SWord16 SWord8 Source # 
Instance details

Defined in Data.SBV.Core.Splittable

Fresh IO (S SInteger) Source #

Fresh instance for our state

Instance details

Defined in Documentation.SBV.Examples.ProofTools.BMC

Fresh IO (S SInteger) Source #

Fresh instance for our state

Instance details

Defined in Documentation.SBV.Examples.ProofTools.Fibonacci

Fresh IO (S SInteger) Source #

Fresh instance for our state

Instance details

Defined in Documentation.SBV.Examples.ProofTools.Strengthen

Fresh IO (S SInteger) Source #

Fresh instance for our state

Instance details

Defined in Documentation.SBV.Examples.ProofTools.Sum

(SymVal a, SMTValue 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, SMTValue 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, SMTValue 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, SMTValue 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, SMTValue 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 #

ExtractIO m => SExecutable m [SBV a] Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

sName_ :: [SBV a] -> SymbolicT m () Source #

sName :: [String] -> [SBV a] -> SymbolicT m () Source #

safe :: [SBV a] -> m [SafeResult] Source #

safeWith :: SMTConfig -> [SBV a] -> m [SafeResult] Source #

ExtractIO m => SExecutable m (SBV a) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

sName_ :: SBV a -> SymbolicT m () Source #

sName :: [String] -> SBV a -> SymbolicT m () Source #

safe :: SBV a -> m [SafeResult] Source #

safeWith :: SMTConfig -> SBV a -> m [SafeResult] Source #

(MonadIO m, SymVal a, SMTValue 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 #

(MonadIO m, SymVal a, SMTValue 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 #

(SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> SymbolicT m () Source #

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> SymbolicT m () Source #

safe :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m [SafeResult] Source #

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m [SafeResult] Source #

(SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> SymbolicT m () Source #

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> SymbolicT m () Source #

safe :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m [SafeResult] Source #

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> m [SafeResult] Source #

(SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m () Source #

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m () Source #

safe :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m [SafeResult] Source #

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> m [SafeResult] Source #

(SymVal a, SymVal b, SymVal c, SymVal d, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d) -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m () Source #

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m () Source #

safe :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> m [SafeResult] Source #

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> m [SafeResult] Source #

(SymVal a, SymVal b, SymVal c, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c) -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

sName_ :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m () Source #

sName :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m () Source #

safe :: ((SBV a, SBV b, SBV c) -> p) -> m [SafeResult] Source #

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> m [SafeResult] Source #

(SymVal a, SymVal b, SExecutable m p) => SExecutable m ((SBV a, SBV b) -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

sName_ :: ((SBV a, SBV b) -> p) -> SymbolicT m () Source #

sName :: [String] -> ((SBV a, SBV b) -> p) -> SymbolicT m () Source #

safe :: ((SBV a, SBV b) -> p) -> m [SafeResult] Source #

safeWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> m [SafeResult] Source #

(SymVal a, SExecutable m p) => SExecutable m (SBV a -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

sName_ :: (SBV a -> p) -> SymbolicT m () Source #

sName :: [String] -> (SBV a -> p) -> SymbolicT m () Source #

safe :: (SBV a -> p) -> m [SafeResult] Source #

safeWith :: SMTConfig -> (SBV a -> p) -> m [SafeResult] Source #

(ExtractIO m, NFData a, SymVal a, NFData b, SymVal b) => SExecutable m (SBV a, SBV b) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

sName_ :: (SBV a, SBV b) -> SymbolicT m () Source #

sName :: [String] -> (SBV a, SBV b) -> SymbolicT m () Source #

safe :: (SBV a, SBV b) -> m [SafeResult] Source #

safeWith :: SMTConfig -> (SBV a, SBV b) -> m [SafeResult] Source #

(SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> SymbolicT m SBool Source #

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> SymbolicT m SBool Source #

forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> SymbolicT m SBool Source #

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> SymbolicT m SBool Source #

prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m ThmResult Source #

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m ThmResult Source #

sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> m SatResult Source #

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c,