sbv-7.13: 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.

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 IStage Bool SMTConfig

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

CodeGen

Code generation mode.

Concrete

Concrete simulation mode.

Instances
Show SBVRunMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

data IStage Source #

Stage of an interactive run

Constructors

ISetup 
ISafe 
IRun 

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.

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, SymWord a) => SBV a Source #

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

sInfinity :: (Floating a, SymWord 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

SymWord 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

parseCWs :: [CW] -> Maybe (RoundingMode, [CW]) Source #

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

type SRoundingMode = SBV RoundingMode Source #

The symbolic variant of RoundingMode

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

A SymWord is a potential symbolic bitvector that can be created instances of to be fed to a symbolic program. Note that these methods are typically not needed in casual uses with prove, sat, allSat etc, as default instances automatically provide the necessary bits.

Minimal complete definition

Nothing

Methods

forall :: String -> Symbolic (SBV a) Source #

Create a user named input (universal)

forall_ :: Symbolic (SBV a) Source #

Create an automatically named input

mkForallVars :: Int -> Symbolic [SBV a] Source #

Get a bunch of new words

exists :: String -> Symbolic (SBV a) Source #

Create an existential variable

exists_ :: Symbolic (SBV a) Source #

Create an automatically named existential variable

mkExistVars :: Int -> Symbolic [SBV a] Source #

Create a bunch of existentials

free :: String -> Symbolic (SBV a) Source #

Create a free variable, universal in a proof, existential in sat

free_ :: Symbolic (SBV a) Source #

Create an unnamed free variable, universal in proof, existential in sat

mkFreeVars :: Int -> Symbolic [SBV a] Source #

Create a bunch of free vars

symbolic :: String -> Symbolic (SBV a) Source #

Similar to free; Just a more convenient name

symbolics :: [String] -> Symbolic [SBV a] Source #

Similar to mkFreeVars; but automatically gives names based on the strings

literal :: a -> SBV a Source #

Turn a literal constant to symbolic

unliteral :: SBV a -> Maybe a Source #

Extract a literal, if the value is concrete

fromCW :: CW -> a Source #

Extract a literal, from a CW representation

isConcrete :: SBV a -> Bool Source #

Is the symbolic word concrete?

isSymbolic :: SBV a -> Bool Source #

Is the symbolic word really symbolic?

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

Does it concretely satisfy the given predicate?

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a) Source #

One stop allocator

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

Turn a literal constant to symbolic

fromCW :: Read a => CW -> a Source #

Extract a literal, from a CW representation

mkSymWord :: (Read a, Data a) => Maybe Quantifier -> Maybe String -> Symbolic (SBV a) Source #

One stop allocator

Instances
SymWord Bool Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord Char Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord Double Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord Float Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord Int8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord Int16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord Int32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord Int64 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord Integer Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord Word8 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord Word16 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord Word32 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord Word64 Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord () Source #

Base type of () allows simple construction for uninterpreted types.

Instance details

Defined in Data.SBV.Core.Model

SymWord AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord RoundingMode Source #

RoundingMode can be used symbolically

Instance details

Defined in Data.SBV.Core.Data

SymWord State Source # 
Instance details

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

SymWord E Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

SymWord Word4 Source #

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

Instance details

Defined in Documentation.SBV.Examples.Misc.Word4

SymWord Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymWord Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymWord Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymWord Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymWord Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

SymWord Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Garden

SymWord Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

SymWord U2Member Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

SymWord Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

SymWord Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

SymWord BinOp Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

SymWord UnOp Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

SymWord B Source # 
Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Deduce

SymWord Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

SymWord L Source #

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

Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

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

Defined in Data.SBV.Core.Model

data CW Source #

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

Constructors

CW 

Fields

Instances
Eq CW Source # 
Instance details

Defined in Data.SBV.Core.Concrete

Methods

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

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

Ord CW Source # 
Instance details

Defined in Data.SBV.Core.Concrete

Methods

compare :: CW -> CW -> Ordering #

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

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

(>) :: CW -> CW -> Bool #

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

max :: CW -> CW -> CW #

min :: CW -> CW -> CW #

Show CW Source #

Show instance for CW.

Instance details

Defined in Data.SBV.Core.Concrete

Methods

showsPrec :: Int -> CW -> ShowS #

show :: CW -> String #

showList :: [CW] -> ShowS #

NFData CW Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: CW -> () #

HasKind CW Source #

Kind instance for CW

Instance details

Defined in Data.SBV.Core.Concrete

PrettyNum CW Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

SatModel CW Source #

CW as extracted from a model; trivial definition

Instance details

Defined in Data.SBV.SMT.SMT

Methods

parseCWs :: [CW] -> Maybe (CW, [CW]) Source #

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

SDivisible CW Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

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

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

sQuot :: CW -> CW -> CW Source #

sRem :: CW -> CW -> CW Source #

sDiv :: CW -> CW -> CW Source #

sMod :: CW -> CW -> CW Source #

data CWVal Source #

A constant value

Constructors

CWAlgReal !AlgReal

algebraic real

CWInteger !Integer

bit-vector/unbounded integer

CWFloat !Float

float

CWDouble !Double

double

CWChar !Char

character

CWString !String

string

CWList ![CWVal]

list

CWUserSort !(Maybe Int, String)

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

Instances
Eq CWVal Source #

Eq instance for CWVal. Note that we cannot simply derive Eq/Ord, since CWAlgReal 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

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

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

Ord CWVal Source #

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

Instance details

Defined in Data.SBV.Core.Concrete

Methods

compare :: CWVal -> CWVal -> Ordering #

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

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

(>) :: CWVal -> CWVal -> Bool #

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

max :: CWVal -> CWVal -> CWVal #

min :: CWVal -> CWVal -> CWVal #

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

SymWord 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

parseCWs :: [CW] -> Maybe (AlgReal, [CW]) Source #

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

SMTValue AlgReal Source # 
Instance details

Defined in Data.SBV.Control.Utils

Methods

sexprToVal :: SExpr -> Maybe AlgReal Source #

Metric SReal Source # 
Instance details

Defined in Data.SBV.Core.Model

IEEEFloatConvertable AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Floating

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

data ExtCW Source #

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

Instances
Show ExtCW Source #

Show instance, shows with the kind

Instance details

Defined in Data.SBV.Core.Concrete

Methods

showsPrec :: Int -> ExtCW -> ShowS #

show :: ExtCW -> String #

showList :: [ExtCW] -> ShowS #

HasKind ExtCW Source #

Kind instance for Extended CW

Instance details

Defined in Data.SBV.Core.Concrete

data GeneralizedCW Source #

A generalized CW allows for expressions involving infinite and epsilon values/intervals Used in optimization problems.

Constructors

ExtendedCW ExtCW 
RegularCW CW 

isRegularCW :: GeneralizedCW -> Bool Source #

Is this a regular CW?

cwSameType :: CW -> CW -> Bool Source #

Are two CW's of the same type?

cwToBool :: CW -> Bool Source #

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

mkConstCW :: Integral a => Kind -> a -> CW Source #

Create a constant word from an integral.

liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> (Char -> Char -> b) -> (String -> String -> b) -> ([CWVal] -> [CWVal] -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b Source #

Lift a binary function through a CW

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

Map a unary function through a CW.

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

Map a binary function through a CW.

data SW Source #

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

Constructors

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

Defined in Data.SBV.Core.Symbolic

Methods

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

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

Ord SW Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

compare :: SW -> SW -> Ordering #

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

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

(>) :: SW -> SW -> Bool #

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

max :: SW -> SW -> SW #

min :: SW -> SW -> SW #

Show SW Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

showsPrec :: Int -> SW -> ShowS #

show :: SW -> String #

showList :: [SW] -> ShowS #

NFData SW Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SW -> () #

HasKind SW Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

trueSW :: SW Source #

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

falseSW :: SW Source #

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

trueCW :: CW Source #

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

falseCW :: CW Source #

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

normCW :: CW -> CW Source #

Normalize a CW. 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 CW (Cached SW)) 
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

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 #

Boolean SBool Source # 
Instance details

Defined in Data.SBV.Core.Data

Provable SBool Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Provable Predicate Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Metric SReal Source # 
Instance details

Defined in Data.SBV.Core.Model

Metric SInteger Source # 
Instance details

Defined in Data.SBV.Core.Model

Metric SInt64 Source # 
Instance details

Defined in Data.SBV.Core.Model

Metric SInt32 Source # 
Instance details

Defined in Data.SBV.Core.Model

Metric SInt16 Source # 
Instance details

Defined in Data.SBV.Core.Model

Metric SInt8 Source # 
Instance details

Defined in Data.SBV.Core.Model

Metric SWord64 Source # 
Instance details

Defined in Data.SBV.Core.Model

Metric SWord32 Source # 
Instance details

Defined in Data.SBV.Core.Model

Metric SWord16 Source # 
Instance details

Defined in Data.SBV.Core.Model

Metric SWord8 Source # 
Instance details

Defined in Data.SBV.Core.Model

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 #

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

SymWord [a] => IsList (SList a) Source #

IsList instance allows list literals to be written compactly.

Instance details

Defined in Data.SBV.Core.Data

Associated Types

type Item (SList a) :: Type #

Methods

fromList :: [Item (SList a)] -> SList a #

fromListN :: Int -> [Item (SList a)] -> SList a #

toList :: SList a -> [Item (SList a)] #

(SymWord a, Bounded a) => Bounded (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

minBound :: SBV a #

maxBound :: SBV a #

(Show a, Bounded a, Integral a, Num a, SymWord a) => Enum (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

succ :: SBV a -> SBV a #

pred :: SBV a -> SBV a #

toEnum :: Int -> SBV a #

fromEnum :: SBV a -> Int #

enumFrom :: SBV a -> [SBV a] #

enumFromThen :: SBV a -> SBV a -> [SBV a] #

enumFromTo :: SBV a -> SBV a -> [SBV a] #

enumFromThenTo :: SBV a -> SBV a -> SBV a -> [SBV a] #

Eq (SBV a) Source #

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

Instance details

Defined in Data.SBV.Core.Data

Methods

(==) :: SBV a -> SBV a -> Bool #

(/=) :: SBV a -> SBV a -> Bool #

(SymWord a, Fractional a, Floating a) => Floating (SBV a) Source #

Define Floating instance on SBV's; only for base types that are already floating; i.e., SFloat and SDouble Note that most of the fields are "undefined" for symbolic values, we add methods as they are supported by SMTLib. Currently, the only symbolicly available function in this class is sqrt.

Instance details

Defined in Data.SBV.Core.Model

Methods

pi :: SBV a #

exp :: SBV a -> SBV a #

log :: SBV a -> SBV a #

sqrt :: SBV a -> SBV a #

(**) :: SBV a -> SBV a -> SBV a #

logBase :: SBV a -> SBV a -> SBV a #

sin :: SBV a -> SBV a #

cos :: SBV a -> SBV a #

tan :: SBV a -> SBV a #

asin :: SBV a -> SBV a #

acos :: SBV a -> SBV a #

atan :: SBV a -> SBV a #

sinh :: SBV a -> SBV a #

cosh :: SBV a -> SBV a #

tanh :: SBV a -> SBV a #

asinh :: SBV a -> SBV a #

acosh :: SBV a -> SBV a #

atanh :: SBV a -> SBV a #

log1p :: SBV a -> SBV a #

expm1 :: SBV a -> SBV a #

log1pexp :: SBV a -> SBV a #

log1mexp :: SBV a -> SBV a #

(SymWord a, Fractional a) => Fractional (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

(/) :: SBV a -> SBV a -> SBV a #

recip :: SBV a -> SBV a #

fromRational :: Rational -> SBV a #

(Ord a, Num a, SymWord a) => Num (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

(+) :: SBV a -> SBV a -> SBV a #

(-) :: SBV a -> SBV a -> SBV a #

(*) :: SBV a -> SBV a -> SBV a #

negate :: SBV a -> SBV a #

abs :: SBV a -> SBV a #

signum :: SBV a -> SBV a #

fromInteger :: Integer -> SBV a #

Show (SBV a) Source #

A Show instance is not particularly "desirable," when the value is symbolic, but we do need this instance as otherwise we cannot simply evaluate Haskell functions that return symbolic values and have their constant values printed easily!

Instance details

Defined in Data.SBV.Core.Data

Methods

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

show :: SBV a -> String #

showList :: [SBV a] -> ShowS #

Generic (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Data

Associated Types

type Rep (SBV a) :: Type -> Type #

Methods

from :: SBV a -> Rep (SBV a) x #

to :: Rep (SBV a) x -> SBV a #

Testable (Symbolic SBool) Source # 
Instance details

Defined in Data.SBV.Core.Model

(SymWord a, Arbitrary a) => Arbitrary (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

arbitrary :: Gen (SBV a) #

shrink :: SBV a -> [SBV a] #

(Num a, Bits a, SymWord a) => Bits (SBV a) Source #

Using popCount or testBit on non-concrete values will result in an error. Use sPopCount or sTestBit instead.

Instance details

Defined in Data.SBV.Core.Model

Methods

(.&.) :: SBV a -> SBV a -> SBV a #

(.|.) :: SBV a -> SBV a -> SBV a #

xor :: SBV a -> SBV a -> SBV a #

complement :: SBV a -> SBV a #

shift :: SBV a -> Int -> SBV a #

rotate :: SBV a -> Int -> SBV a #

zeroBits :: SBV a #

bit :: Int -> SBV a #

setBit :: SBV a -> Int -> SBV a #

clearBit :: SBV a -> Int -> SBV a #

complementBit :: SBV a -> Int -> SBV a #

testBit :: SBV a -> Int -> Bool #

bitSizeMaybe :: SBV a -> Maybe Int #

bitSize :: SBV a -> Int #

isSigned :: SBV a -> Bool #

shiftL :: SBV a -> Int -> SBV a #

unsafeShiftL :: SBV a -> Int -> SBV a #

shiftR :: SBV a -> Int -> SBV a #

unsafeShiftR :: SBV a -> Int -> SBV a #

rotateL :: SBV a -> Int -> SBV a #

rotateR :: SBV a -> Int -> SBV a #

popCount :: SBV a -> Int #

NFData (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

rnf :: SBV a -> () #

(Random a, SymWord a) => Random (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

randomR :: RandomGen g => (SBV a, SBV a) -> g -> (SBV a, g) #

random :: RandomGen g => g -> (SBV a, g) #

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

randoms :: RandomGen g => g -> [SBV a] #

randomRIO :: (SBV a, SBV a) -> IO (SBV a) #

randomIO :: IO (SBV a) #

HasKind (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Data

Outputtable (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

output :: SBV a -> Symbolic (SBV a) Source #

(SymWord a, PrettyNum a) => PrettyNum (SBV a) Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

Methods

hexS :: SBV a -> String Source #

binS :: SBV a -> String Source #

hex :: SBV a -> String Source #

bin :: SBV a -> String Source #

SExecutable [SBV a] Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

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

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

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

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

SExecutable (SBV a) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

HasKind a => Uninterpreted (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

SymWord a => Mergeable (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: Bool -> SBool -> SBV a -> SBV a -> SBV a Source #

select :: (SymWord b, Num b) => [SBV a] -> SBV a -> SBV b -> SBV a Source #

SymWord a => OrdSymbolic (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

(.<) :: SBV a -> SBV a -> SBool Source #

(.<=) :: SBV a -> SBV a -> SBool Source #

(.>) :: SBV a -> SBV a -> SBool Source #

(.>=) :: SBV a -> SBV a -> SBool Source #

smin :: SBV a -> SBV a -> SBV a Source #

smax :: SBV a -> SBV a -> SBV a Source #

inRange :: SBV a -> (SBV a, SBV a) -> SBool Source #

EqSymbolic (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

(.==) :: SBV a -> SBV a -> SBool Source #

(./=) :: SBV a -> SBV a -> SBool Source #

distinct :: [SBV a] -> SBool Source #

allEqual :: [SBV a] -> SBool Source #

sElem :: SBV a -> [SBV a] -> SBool Source #

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

Defined in Data.SBV.Provers.Prover

Methods

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

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

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

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

(SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((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) -> Symbolic () Source #

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

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

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

(SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((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) -> Symbolic () Source #

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

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

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

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((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) -> Symbolic () Source #

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

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

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

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SExecutable p) => SExecutable ((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) -> Symbolic () Source #

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

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

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

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, SExecutable p) => SExecutable ((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) -> Symbolic () Source #

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

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

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

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

Defined in Data.SBV.Provers.Prover

Methods

sName_ :: (SBV a -> p) -> Symbolic () Source #

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

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

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

(NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

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

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

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

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

(SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

forAll_ :: ((SBV a, SBV b) -> p) -> Predicate Source #

forAll :: [String] -> ((SBV a, SBV b) -> p) -> Predicate Source #

forSome_ :: ((SBV a, SBV b) -> p) -> Predicate Source #

forSome :: [String] -> ((SBV a, SBV b) -> p) -> Predicate Source #

prove :: ((SBV a, SBV b) -> p) -> IO ThmResult Source #

proveWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO ThmResult Source #

sat :: ((SBV a, SBV b) -> p) -> IO SatResult Source #

satWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO SatResult Source #

allSat :: ((SBV a, SBV b) -> p) -> IO AllSatResult Source #

allSatWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO AllSatResult Source #

optimize :: OptimizeStyle -> ((SBV a, SBV b) -> p) -> IO OptimizeResult Source #

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b) -> p) -> IO OptimizeResult Source #

isVacuous :: ((SBV a, SBV b) -> p) -> IO Bool Source #

isVacuousWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool Source #

isTheorem :: ((SBV a, SBV b) -> p) -> IO Bool Source #

isTheoremWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool Source #

isSatisfiable :: ((SBV a, SBV b) -> p) -> IO Bool Source #

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool Source #

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #

satWithAll :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #

satWithAny :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #

generateSMTBenchmark :: Bool -> ((SBV a, SBV b) -> p) -> IO String Source #

(SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

forAll_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate Source #

forAll :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate Source #

forSome_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate Source #

forSome :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate Source #

prove :: ((SBV a, SBV b, SBV c) -> p) -> IO ThmResult Source #

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO ThmResult Source #

sat :: ((SBV a, SBV b, SBV c) -> p) -> IO SatResult Source #

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO SatResult Source #

allSat :: ((SBV a, SBV b, SBV c) -> p) -> IO AllSatResult Source #

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO AllSatResult Source #

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c) -> p) -> IO OptimizeResult Source #

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c) -> p) -> IO OptimizeResult Source #

isVacuous :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool Source #

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool Source #

isTheorem :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool Source #

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool Source #

isSatisfiable :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool Source #

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool Source #

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c) -> p) -> IO String Source #

(SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source #

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source #

forSome_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source #

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source #

prove :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO ThmResult Source #

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO ThmResult Source #

sat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO SatResult Source #

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO SatResult Source #

allSat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO AllSatResult Source #

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO AllSatResult Source #

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO OptimizeResult Source #

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO OptimizeResult Source #

isVacuous :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool Source #

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool Source #

isTheorem :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool Source #

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool Source #

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool Source #

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool Source #

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO String Source #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source #

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source #

forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source #

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source #

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

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

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

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO SatResult Source #

allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO AllSatResult Source #

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO AllSatResult Source #

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO OptimizeResult Source #

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO OptimizeResult Source #

isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool Source #

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool Source #

isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool Source #

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool Source #

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool Source #

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool Source #

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO String Source #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source #

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

forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source #

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

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

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

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

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO SatResult Source #

allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO AllSatResult Source #

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO AllSatResult Source #

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO OptimizeResult Source #

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO OptimizeResult Source #

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

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool Source #

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

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool Source #

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

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool Source #

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO String Source #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((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) -> Predicate Source #

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

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

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

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

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

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

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO SatResult Source #

allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO AllSatResult Source #

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO AllSatResult Source #

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO OptimizeResult Source #

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO OptimizeResult Source #

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

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool Source #

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

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool Source #

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

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool Source #

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO String Source #

(SymWord a, Provable p) => Provable (SBV a -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

(SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

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

cgUninterpret :: String -> [String] -> ((SBV c, SBV b) -> SBV a) -> (SBV c, SBV b) -> SBV a Source #

sbvUninterpret :: Maybe ([String], (SBV c, SBV b) -> SBV a) -> String -> (SBV c, SBV b) -> SBV a Source #

(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

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

cgUninterpret :: String -> [String] -> ((SBV d, SBV c, SBV b) -> SBV a) -> (SBV d, SBV c, SBV b) -> SBV a Source #

sbvUninterpret :: Maybe ([String], (SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV d, SBV c, SBV b) -> SBV a Source #

(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

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

cgUninterpret :: String -> [String] -> ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

sbvUninterpret :: Maybe ([String], (SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

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

cgUninterpret :: String -> [String] -> ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

sbvUninterpret :: Maybe ([String], (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

(SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

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

cgUninterpret :: String -> [String] -> ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

sbvUninterpret :: Maybe ([String], (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

(SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

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

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

sbvUninterpret :: Maybe ([String], (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a Source #

(SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

uninterpret :: String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

(SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

uninterpret :: String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

uninterpret :: String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

uninterpret :: String -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a Source #

(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

uninterpret :: String -> SBV d -> SBV c -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV d -> SBV c -> SBV b -> SBV a) -> SBV d -> SBV c -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV d -> SBV c -> SBV b -> SBV a Source #

(SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

uninterpret :: String -> SBV c -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV c -> SBV b -> SBV a) -> SBV c -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV c -> SBV b -> SBV a) -> String -> SBV c -> SBV b -> SBV a Source #

(SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

uninterpret :: String -> SBV b -> SBV a Source #

cgUninterpret :: String -> [String] -> (SBV b -> SBV a) -> SBV b -> SBV a Source #

sbvUninterpret :: Maybe ([String], SBV b -> SBV a) -> String -> SBV b -> SBV a Source #

SymWord e => Mergeable (STree i e) Source # 
Instance details

Defined in Data.SBV.Tools.STree

Methods

symbolicMerge :: Bool -> SBool -> STree i e -> STree i e -> STree i e Source #

select :: (SymWord b, Num b) => [STree i e] -> STree i e -> SBV b -> STree i e Source #

(SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: ((SBV a, SBV b) -> z) -> ((SBV a, SBV b) -> z) -> IO ThmResult Source #

(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: ((SBV a, SBV b, SBV c) -> z) -> ((SBV a, SBV b, SBV c) -> z) -> IO ThmResult Source #

(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: ((SBV a, SBV b, SBV c, SBV d) -> z) -> ((SBV a, SBV b, SBV c, SBV d) -> z) -> IO ThmResult Source #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) -> IO ThmResult Source #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) -> IO ThmResult Source #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) -> IO ThmResult Source #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) -> IO ThmResult Source #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) -> IO ThmResult Source #

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) -> IO ThmResult Source #

(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> z) -> IO ThmResult Source #

(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: (SBV a -> SBV b -> SBV c -> z) -> (SBV a -> SBV b -> SBV c -> z) -> IO ThmResult Source #

(SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: (SBV a -> SBV b -> z) -> (SBV a -> SBV b -> z) -> IO ThmResult Source #

(SymWord a, EqSymbolic z) => Equality (SBV a -> z) Source # 
Instance details

Defined in Data.SBV

Methods

(===) :: (SBV a -> z) -> (SBV a -> z) -> IO ThmResult Source #

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

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

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

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

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

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d) => SExecutable (SBV a, SBV b, SBV c, SBV d) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

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

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

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

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

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

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

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

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

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

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

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

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

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

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

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f, NFData g, SymWord g) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) 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) -> Symbolic () Source #

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

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

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

type Rep (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Data

type Rep (SBV a) = D1 (MetaData "SBV" "Data.SBV.Core.Data" "sbv-7.13-FaWek6vu3G08BLmNYer5ul" True) (C1 (MetaCons "SBV" PrefixI True) (S1 (MetaSel (Just "unSBV") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 SVal)))
type Item (SList a) Source # 
Instance details

Defined in Data.SBV.Core.Data

type Item (SList a) = a

newtype NodeId Source #

A symbolic node id

Constructors

NodeId Int 
Instances
Eq NodeId Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

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

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

Ord NodeId Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

mkSymSBV :: forall a. Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a) Source #

Create a symbolic variable.

data ArrayContext Source #

The context of a symbolic array as created

Constructors

ArrayFree (Maybe SW)

A new array, the contents are initialized with the given value, if any

ArrayMutate ArrayIndex SW SW

An array created by mutating another array at a given cell

ArrayMerge SW ArrayIndex ArrayIndex

An array created by symbolically merging two other arrays

Instances
Show ArrayContext Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

NFData ArrayContext Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: ArrayContext -> () #

type ArrayInfo = (String, (Kind, Kind), ArrayContext) Source #

Representation for symbolic arrays

class SymArray array where Source #

Flat arrays of symbolic values An array a b is an array indexed by the type SBV a, with elements of type SBV b.

If a default value is supplied, then all the array elements will be initialized to this value. Otherwise, they will be left unspecified, i.e., a read from an unwritten location will produce an uninterpreted constant.

While it's certainly possible for user to create instances of SymArray, the SArray and SFunArray instances already provided should cover most use cases in practice. Note that there are a few differences between these two models in terms of use models:

  • SArray produces SMTLib arrays, and requires a solver that understands the array theory. SFunArray is internally handled, and thus can be used with any solver. (Note that all solvers except abc support arrays, so this isn't a big decision factor.)
  • For both arrays, if a default value is supplied, then reading from uninitialized cell will return that value. If the default is not given, then reading from uninitialized cells is still OK for both arrays, and will produce an uninterpreted constant in both cases.
  • Only SArray supports checking equality of arrays. (That is, checking if an entire array is equivalent to another.) SFunArrays cannot be checked for equality. In general, checking wholesale equality of arrays is a difficult decision problem and should be avoided if possible.
  • Only SFunArray supports compilation to C. Programs using SArray will not be accepted by the C-code generator.
  • You cannot use quickcheck on programs that contain these arrays. (Neither SArray nor SFunArray.)
  • With SArray, SBV transfers all array-processing to the SMT-solver. So, it can generate programs more quickly, but they might end up being too hard for the solver to handle. With SFunArray, SBV only generates code for individual elements and the array itself never shows up in the resulting SMTLib program. This puts more onus on the SBV side and might have some performance impacts, but it might generate problems that are easier for the SMT solvers to handle.

As a rule of thumb, try SArray first. These should generate compact code. However, if the backend solver has hard time solving the generated problems, switch to SFunArray. If you still have issues, please report so we can see what the problem might be!

Minimal complete definition

readArray, writeArray, mergeArrays, newArrayInState

Methods

newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b) Source #

Create a new anonymous array, possibly with a default initial value.

newArray :: (HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b) Source #

Create a named new array, possibly with a default initial value.

readArray :: array a b -> SBV a -> SBV b Source #

Read the array element at a

writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a b Source #

Update the element at a to be b

mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a b Source #

Merge two given arrays on the symbolic condition Intuitively: mergeArrays cond a b = if cond then a else b. Merging pushes the if-then-else choice down on to elements

newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (array a b) Source #

Internal function, not exported to the user

Instances
SymArray SFunArray Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (SFunArray a b) Source #

newArray :: (HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (SFunArray a b) Source #

readArray :: SFunArray a b -> SBV a -> SBV b Source #

writeArray :: SymWord b => SFunArray a b -> SBV a -> SBV b -> SFunArray a b Source #

mergeArrays :: SymWord b => SBV Bool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #

newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SFunArray a b) Source #

SymArray SArray Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (SArray a b) Source #

newArray :: (HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (SArray a b) Source #

readArray :: SArray a b -> SBV a -> SBV b Source #

writeArray :: SymWord b => SArray a b -> SBV a -> SBV b -> SArray a b Source #

mergeArrays :: SymWord b => SBV Bool -> SArray a b -> SArray a b -> SArray a b Source #

newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SArray a b) Source #

newtype SFunArray a b Source #

Arrays implemented internally, without translating to SMT-Lib functions:

  • Internally handled by the library and not mapped to SMT-Lib, hence can be used with solvers that don't support arrays. (Such as abc.)
  • Reading from an unintialized value is OK. If the default value is given in newArray, it will be the result. Otherwise, the read yields an uninterpreted constant.
  • Cannot check for equality of arrays.
  • Can be used in code-generation (i.e., compilation to C).
  • Can not quick-check theorems using SFunArray values
  • Typically faster as it gets compiled away during translation.

Constructors

SFunArray 

Fields

Instances
SymArray SFunArray Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (SFunArray a b) Source #

newArray :: (HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (SFunArray a b) Source #

readArray :: SFunArray a b -> SBV a -> SBV b Source #

writeArray :: SymWord b => SFunArray a b -> SBV a -> SBV b -> SFunArray a b Source #

mergeArrays :: SymWord b => SBV Bool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #

newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SFunArray a b) Source #

(HasKind a, HasKind b) => Show (SFunArray a b) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

showsPrec :: Int -> SFunArray a b -> ShowS #

show :: SFunArray a b -> String #

showList :: [SFunArray a b] -> ShowS #

(HasKind a, HasKind b, Provable p) => Provable (SFunArray a b -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

forAll_ :: (SFunArray a b -> p) -> Predicate Source #

forAll :: [String] -> (SFunArray a b -> p) -> Predicate Source #

forSome_ :: (SFunArray a b -> p) -> Predicate Source #

forSome :: [String] -> (SFunArray a b -> p) -> Predicate Source #

prove :: (SFunArray a b -> p) -> IO ThmResult Source #

proveWith :: SMTConfig -> (SFunArray a b -> p) -> IO ThmResult Source #

sat :: (SFunArray a b -> p) -> IO SatResult Source #

satWith :: SMTConfig -> (SFunArray a b -> p) -> IO SatResult Source #

allSat :: (SFunArray a b -> p) -> IO AllSatResult Source #

allSatWith :: SMTConfig -> (SFunArray a b -> p) -> IO AllSatResult Source #

optimize :: OptimizeStyle -> (SFunArray a b -> p) -> IO OptimizeResult Source #

optimizeWith :: SMTConfig -> OptimizeStyle -> (SFunArray a b -> p) -> IO OptimizeResult Source #

isVacuous :: (SFunArray a b -> p) -> IO Bool Source #

isVacuousWith :: SMTConfig -> (SFunArray a b -> p) -> IO Bool Source #

isTheorem :: (SFunArray a b -> p) -> IO Bool Source #

isTheoremWith :: SMTConfig -> (SFunArray a b -> p) -> IO Bool Source #

isSatisfiable :: (SFunArray a b -> p) -> IO Bool Source #

isSatisfiableWith :: SMTConfig -> (SFunArray a b -> p) -> IO Bool Source #

proveWithAll :: [SMTConfig] -> (SFunArray a b -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #

proveWithAny :: [SMTConfig] -> (SFunArray a b -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #

satWithAll :: [SMTConfig] -> (SFunArray a b -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #

satWithAny :: [SMTConfig] -> (SFunArray a b -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #

generateSMTBenchmark :: Bool -> (SFunArray a b -> p) -> IO String Source #

SymWord b => Mergeable (SFunArray a b) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: Bool -> SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #

select :: (SymWord b0, Num b0) => [SFunArray a b] -> SFunArray a b -> SBV b0 -> SFunArray a b Source #

newtype SArray a b Source #

Arrays implemented in terms of SMT-arrays: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml

  • Maps directly to SMT-lib arrays
  • Reading from an unintialized value is OK. If the default value is given in newArray, it will be the result. Otherwise, the read yields an uninterpreted constant.
  • Can check for equality of these arrays
  • Cannot be used in code-generation (i.e., compilation to C)
  • Cannot quick-check theorems using SArray values
  • Typically slower as it heavily relies on SMT-solving for the array theory

Constructors

SArray 

Fields

Instances
SymArray SArray Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (SArray a b) Source #

newArray :: (HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (SArray a b) Source #

readArray :: SArray a b -> SBV a -> SBV b Source #

writeArray :: SymWord b => SArray a b -> SBV a -> SBV b -> SArray a b Source #

mergeArrays :: SymWord b => SBV Bool -> SArray a b -> SArray a b -> SArray a b Source #

newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> State -> IO (SArray a b) Source #

(HasKind a, HasKind b) => Show (SArray a b) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

showsPrec :: Int -> SArray a b -> ShowS #

show :: SArray a b -> String #

showList :: [SArray a b] -> ShowS #

(HasKind a, HasKind b, Provable p) => Provable (SArray a b -> p) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

Methods

forAll_ :: (SArray a b -> p) -> Predicate Source #

forAll :: [String] -> (SArray a b -> p) -> Predicate Source #

forSome_ :: (SArray a b -> p) -> Predicate Source #

forSome :: [String] -> (SArray a b -> p) -> Predicate Source #

prove :: (SArray a b -> p) -> IO ThmResult Source #

proveWith :: SMTConfig -> (SArray a b -> p) -> IO ThmResult Source #

sat :: (SArray a b -> p) -> IO SatResult Source #

satWith :: SMTConfig -> (SArray a b -> p) -> IO SatResult Source #

allSat :: (SArray a b -> p) -> IO AllSatResult Source #

allSatWith :: SMTConfig -> (SArray a b -> p) -> IO AllSatResult Source #

optimize :: OptimizeStyle -> (SArray a b -> p) -> IO OptimizeResult Source #

optimizeWith :: SMTConfig -> OptimizeStyle -> (SArray a b -> p) -> IO OptimizeResult Source #

isVacuous :: (SArray a b -> p) -> IO Bool Source #

isVacuousWith :: SMTConfig -> (SArray a b -> p) -> IO Bool Source #

isTheorem :: (SArray a b -> p) -> IO Bool Source #

isTheoremWith :: SMTConfig -> (SArray a b -> p) -> IO Bool Source #

isSatisfiable :: (SArray a b -> p) -> IO Bool Source #

isSatisfiableWith :: SMTConfig -> (SArray a b -> p) -> IO Bool Source #

proveWithAll :: [SMTConfig] -> (SArray a b -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #

proveWithAny :: [SMTConfig] -> (SArray a b -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #

satWithAll :: [SMTConfig] -> (SArray a b -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #

satWithAny :: [SMTConfig] -> (SArray a b -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #

generateSMTBenchmark :: Bool -> (SArray a b -> p) -> IO String Source #

SymWord b => Mergeable (SArray a b) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

symbolicMerge :: Bool -> SBool -> SArray a b -> SArray a b -> SArray a b Source #

select :: (SymWord b0, Num b0) => [SArray a b] -> SArray a b -> SBV b0 -> SArray a b Source #

EqSymbolic (SArray a b) Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

(.==) :: SArray a b -> SArray a b -> SBool Source #

(./=) :: SArray a b -> SArray a b -> SBool Source #

distinct :: [SArray a b] -> SBool Source #

allEqual :: [SArray a b] -> SBool Source #

sElem :: SArray a b -> [SArray a b] -> SBool Source #

sbvToSW :: State -> SBV a -> IO SW Source #

Convert a symbolic value to a symbolic-word

sbvToSymSW :: SBV a -> Symbolic SW Source #

Convert a symbolic value to an SW, inside the Symbolic monad

forceSWArg :: SW -> IO () Source #

Forcing an argument; this is a necessary evil to make sure all the arguments to an uninterpreted function are evaluated before called; the semantics of uinterpreted functions is necessarily strict; deviating from Haskell's

data SBVExpr Source #

A symbolic expression

Constructors

SBVApp !Op ![SW] 
Instances
Eq SBVExpr Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

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

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

Ord SBVExpr Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Show SBVExpr Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

NFData SBVExpr Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SBVExpr -> () #

newExpr :: State -> Kind -> SBVExpr -> IO SW Source #

Create a new expression; hash-cons as necessary

cache :: (State -> IO a) -> Cached a Source #

Cache a state-based computation

data Cached a Source #

We implement a peculiar caching mechanism, applicable to the use case in implementation of SBV's. Whenever we do a state based computation, we do not want to keep on evaluating it in the then-current state. That will produce essentially a semantically equivalent value. Thus, we want to run it only once, and reuse that result, capturing the sharing at the Haskell level. This is similar to the "type-safe observable sharing" work, but also takes into the account of how symbolic simulation executes.

See Andy Gill's type-safe obervable sharing trick for the inspiration behind this technique: http://ku-fpg.github.io/files/Gill-09-TypeSafeReification.pdf

Note that this is *not* a general memo utility!

Instances
NFData (Cached a) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: Cached a -> () #

uncache :: Cached SW -> State -> IO SW Source #

Uncache a previously cached computation

uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex Source #

Uncache, retrieving SMT array indexes

class HasKind a where Source #

A class for capturing values that have a sign and a size (finite or infinite) minimal complete definition: kindOf, unless you can take advantage of the default signature: This class can be automatically derived for data-types that have a Data instance; this is useful for creating uninterpreted sorts. So, in reality, end users should almost never need to define any methods.

Minimal complete definition

Nothing

Instances
HasKind Bool Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Char Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Double Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Float Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Int8 Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Int16 Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Int32 Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Int64 Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Integer Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Word8 Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Word16 Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Word32 Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Word64 Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind () Source # 
Instance details

Defined in Data.SBV.Core.Model

HasKind AlgReal Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind Kind Source # 
Instance details

Defined in Data.SBV.Core.Kind

HasKind ExtCW Source #

Kind instance for Extended CW

Instance details

Defined in Data.SBV.Core.Concrete

HasKind GeneralizedCW Source #

Kind instance for generalized CW

Instance details

Defined in Data.SBV.Core.Concrete

HasKind CW Source #

Kind instance for CW

Instance details

Defined in Data.SBV.Core.Concrete

HasKind RoundingMode Source #

RoundingMode kind

Instance details

Defined in Data.SBV.Core.Symbolic

HasKind SVal Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

HasKind SW Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

HasKind State Source # 
Instance details

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

HasKind E Source # 
Instance details

Defined in Documentation.SBV.Examples.Misc.Enumerate

HasKind Word4 Source #

HasKind instance; simply returning the underlying kind for the type

Instance details

Defined in Documentation.SBV.Examples.Misc.Word4

HasKind Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

HasKind Nationality Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

HasKind Beverage Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

HasKind Pet Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

HasKind Sport Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Fish

HasKind Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.Garden

HasKind Color Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.HexPuzzle

HasKind U2Member Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

HasKind Location Source # 
Instance details

Defined in Documentation.SBV.Examples.Puzzles.U2Bridge

HasKind Day Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.Enums

HasKind BinOp Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

HasKind UnOp Source # 
Instance details

Defined in Documentation.SBV.Examples.Queries.FourFours

HasKind B Source # 
Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Deduce

HasKind Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.Sort

HasKind L Source #

Similarly, HasKinds default implementation is sufficient.

Instance details

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

(Typeable a, HasKind a) => HasKind [a] Source # 
Instance details

Defined in Data.SBV.Core.Kind

Methods

kindOf :: [a] -> Kind Source #

hasSign :: [a] -> Bool Source #

intSizeOf :: [a] -> Int Source #

isBoolean :: [a] -> Bool Source #

isBounded :: [a] -> Bool Source #

isReal :: [a] -> Bool Source #

isFloat :: [a] -> Bool Source #

isDouble :: [a] -> Bool Source #

isInteger :: [a] -> Bool Source #

isUninterpreted :: [a] -> Bool Source #

isChar :: [a] -> Bool Source #

isString :: [a] -> Bool Source #

isList :: [a] -> Bool Source #

showType :: [a] -> String Source #

HasKind (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Data

data Op Source #

Symbolic operations

Instances
Eq Op Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

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

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

Ord Op Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

compare :: Op -> Op -> Ordering #

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

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

(>) :: Op -> Op -> Bool #

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

max :: Op -> Op -> Op #

min :: Op -> Op -> Op #

Show Op Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

showsPrec :: Int -> Op -> ShowS #

show :: Op -> String #

showList :: [Op] -> ShowS #

data PBOp Source #

Pseudo-boolean operations

Constructors

PB_AtMost Int

At most k

PB_AtLeast Int

At least k

PB_Exactly Int

Exactly k

PB_Le [Int] Int

At most k, with coefficients given. Generalizes PB_AtMost

PB_Ge [Int] Int

At least k, with coefficients given. Generalizes PB_AtLeast

PB_Eq [Int] Int

Exactly k, with coefficients given. Generalized PB_Exactly

Instances
Eq PBOp Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

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

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

Ord PBOp Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

compare :: PBOp -> PBOp -> Ordering #

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

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

(>) :: PBOp -> PBOp -> Bool #

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

max :: PBOp -> PBOp -> PBOp #

min :: PBOp -> PBOp -> PBOp #

Show PBOp Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

showsPrec :: Int -> PBOp -> ShowS #

show :: PBOp -> String #

showList :: [PBOp] -> ShowS #

data FPOp Source #

Floating point operations

Instances
Eq FPOp Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

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

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

Ord FPOp Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

compare :: FPOp -> FPOp -> Ordering #

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

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

(>) :: FPOp -> FPOp -> Bool #

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

max :: FPOp -> FPOp -> FPOp #

min :: FPOp -> FPOp -> FPOp #

Show FPOp Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

showsPrec :: Int -> FPOp -> ShowS #

show :: FPOp -> String #

showList :: [FPOp] -> ShowS #

data StrOp Source #

String operations. Note that we do not define StrAt as it translates to StrSubstr trivially.

Constructors

StrConcat

Concatenation of one or more strings

StrLen

String length

StrUnit

Unit string

StrSubstr

Retrieves substring of s at offset

StrIndexOf

Retrieves first position of sub in s, -1 if there are no occurrences

StrContains

Does s contain the substring sub?

StrPrefixOf

Is pre a prefix of s?

StrSuffixOf

Is suf a suffix of s?

StrReplace

Replace the first occurrence of src by dst in s

StrStrToNat

Retrieve integer encoded by string s (ground rewriting only)

StrNatToStr

Retrieve string encoded by integer i (ground rewriting only)

StrInRe RegExp

Check if string is in the regular expression

Instances
Eq StrOp Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

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

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

Ord StrOp Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

compare :: StrOp -> StrOp -> Ordering #

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

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

(>) :: StrOp -> StrOp -> Bool #

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

max :: StrOp -> StrOp -> StrOp #

min :: StrOp -> StrOp -> StrOp #

Show StrOp Source #

Show instance for StrOp. Note that the mapping here is important to match the SMTLib equivalents, see here: http://rise4fun.com/z3/tutorialcontent/sequences

Instance details

Defined in Data.SBV.Core.Symbolic

Methods

showsPrec :: Int -> StrOp -> ShowS #

show :: StrOp -> String #

showList :: [StrOp] -> ShowS #

data SeqOp Source #

Sequence operations.

Constructors

SeqConcat

See StrConcat

SeqLen

See StrLen

SeqUnit

See StrUnit

SeqSubseq

See StrSubseq

SeqIndexOf

See StrIndexOf

SeqContains

See StrContains

SeqPrefixOf

See StrPrefixOf

SeqSuffixOf

See StrSuffixOf

SeqReplace

See StrReplace

Instances
Eq SeqOp Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

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

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

Ord SeqOp Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

compare :: SeqOp -> SeqOp -> Ordering #

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

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

(>) :: SeqOp -> SeqOp -> Bool #

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

max :: SeqOp -> SeqOp -> SeqOp #

min :: SeqOp -> SeqOp -> SeqOp #

Show SeqOp Source #

Show instance for SeqOp. Again, mapping is important.

Instance details

Defined in Data.SBV.Core.Symbolic

Methods

showsPrec :: Int -> SeqOp -> ShowS #

show :: SeqOp -> String #

showList :: [SeqOp] -> ShowS #

data RegExp Source #

Regular expressions. Note that regular expressions themselves are concrete, but the match function from the RegExpMatchable class can check membership against a symbolic string/character. Also, we are preferring a datatype approach here, as opposed to coming up with some string-representation; there are way too many alternatives already so inventing one isn't a priority. Please get in touch if you would like a parser for this type as it might be easier to use.

Constructors

Literal String

Precisely match the given string

All

Accept every string

None

Accept no strings

Range Char Char

Accept range of characters

Conc [RegExp]

Concatenation

KStar RegExp

Kleene Star: Zero or more

KPlus RegExp

Kleene Plus: One or more

Opt RegExp

Zero or one

Loop Int Int RegExp

From n repetitions to m repetitions

Union [RegExp]

Union of regular expressions

Inter RegExp RegExp

Intersection of regular expressions

Instances
Eq RegExp Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

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

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

Num RegExp Source #

Regular expressions as a Num instance. Note that only + (union) and * (concatenation) make sense.

Instance details

Defined in Data.SBV.Core.Symbolic

Ord RegExp Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Show RegExp Source #

Show instance for RegExp. The mapping is done so the outcome matches the SMTLib string reg-exp operations

Instance details

Defined in Data.SBV.Core.Symbolic

IsString RegExp Source #

With overloaded strings, we can have direct literal regular expressions.

Instance details

Defined in Data.SBV.Core.Symbolic

Methods

fromString :: String -> RegExp #

type NamedSymVar = (SW, String) Source #

NamedSymVar pairs symbolic words and user given/automatically generated names

getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int Source #

Create a new table; hash-cons as necessary

newtype SBVPgm Source #

A program is a sequence of assignments

Constructors

SBVPgm 
Instances
NFData SBVPgm Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SBVPgm -> () #

data Symbolic a Source #

A Symbolic computation. Represented by a reader monad carrying the state of the computation, layered on top of IO for creating unique references to hold onto intermediate results.

Instances
Monad Symbolic Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

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

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

return :: a -> Symbolic a #

fail :: String -> Symbolic a #

Functor Symbolic Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

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

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

MonadFail Symbolic Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

fail :: String -> Symbolic a #

Applicative Symbolic Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

pure :: a -> Symbolic a #

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

liftA2 :: (a -> b -> c) -> Symbolic a -> Symbolic b -> Symbolic c #

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

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

MonadIO Symbolic Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

liftIO :: IO a -> Symbolic a #

SolverContext Symbolic Source #

Symbolic computations provide a context for writing symbolic programs.

Instance details

Defined in Data.SBV.Core.Model

Provable Goal Source # 
Instance details

Defined in Data.SBV

Provable Predicate Source # 
Instance details

Defined in Data.SBV.Provers.Prover

MonadReader State Symbolic Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

ask :: Symbolic State #

local :: (State -> State) -> Symbolic a -> Symbolic a #

reader :: (State -> a) -> Symbolic a #

Testable (Symbolic SVal) Source # 
Instance details

Defined in Data.SBV.Core.Model

Testable (Symbolic SBool) Source # 
Instance details

Defined in Data.SBV.Core.Model

NFData a => SExecutable (Symbolic a) Source # 
Instance details

Defined in Data.SBV.Provers.Prover

runSymbolic :: SBVRunMode -> Symbolic a -> IO (a, Result) Source #

Run a symbolic computation, and return a extra value paired up with the Result

data State Source #

The state of the symbolic interpreter

Instances
NFData State Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: State -> () #

MonadState State Query Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

get :: Query State #

put :: State -> Query () #

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

MonadReader State Symbolic Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

ask :: Symbolic State #

local :: (State -> State) -> Symbolic a -> Symbolic a #

reader :: (State -> a) -> Symbolic a #

getPathCondition :: State -> SBool Source #

Get the current path condition

extendPathCondition :: State -> (SBool -> SBool) -> State Source #

Extend the path condition with the given test value.

inSMTMode :: State -> IO Bool Source #

Are we running in proof mode?

data SBVRunMode Source #

Different means of running a symbolic piece of code

Constructors

SMTMode IStage Bool SMTConfig

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

CodeGen

Code generation mode.

Concrete

Concrete simulation mode.

Instances
Show SBVRunMode Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

data Kind Source #

Kind of symbolic value

Instances
Eq Kind Source # 
Instance details

Defined in Data.SBV.Core.Kind

Methods

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

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

Ord Kind Source # 
Instance details

Defined in Data.SBV.Core.Kind

Methods

compare :: Kind -> Kind -> Ordering #

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

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

(>) :: Kind -> Kind -> Bool #

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

max :: Kind -> Kind -> Kind #

min :: Kind -> Kind -> Kind #

Show Kind Source #

The interesting about the show instance is that it can tell apart two kinds nicely; since it conveniently ignores the enumeration constructors. Also, when we construct a KUserSort, we make sure we don't use any of the reserved names; see constructUKind for details.

Instance details

Defined in Data.SBV.Core.Kind

Methods

showsPrec :: Int -> Kind -> ShowS #

show :: Kind -> String #

showList :: [Kind] -> ShowS #

NFData Kind Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: Kind -> () #

HasKind Kind Source # 
Instance details

Defined in Data.SBV.Core.Kind

class Outputtable a where Source #

A class representing what can be returned from a symbolic computation.

Methods

output :: a -> Symbolic a Source #

Mark an interim result as an output. Useful when constructing Symbolic programs that return multiple values, or when the result is programmatically computed.

Instances
Outputtable () Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

output :: () -> Symbolic () Source #

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

Defined in Data.SBV.Core.Data

Methods

output :: [a] -> Symbolic [a] Source #

Outputtable (SBV a) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

output :: SBV a -> Symbolic (SBV a) Source #

(Outputtable a, Outputtable b) => Outputtable (a, b) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

output :: (a, b) -> Symbolic (a, b) Source #

(Outputtable a, Outputtable b, Outputtable c) => Outputtable (a, b, c) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

output :: (a, b, c) -> Symbolic (a, b, c) Source #

(Outputtable a, Outputtable b, Outputtable c, Outputtable d) => Outputtable (a, b, c, d) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

output :: (a, b, c, d) -> Symbolic (a, b, c, d) Source #

(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e) => Outputtable (a, b, c, d, e) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

output :: (a, b, c, d, e) -> Symbolic (a, b, c, d, e) Source #

(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f) => Outputtable (a, b, c, d, e, f) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

output :: (a, b, c, d, e, f) -> Symbolic (a, b, c, d, e, f) Source #

(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g) => Outputtable (a, b, c, d, e, f, g) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

output :: (a, b, c, d, e, f, g) -> Symbolic (a, b, c, d, e, f, g) Source #

(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g, Outputtable h) => Outputtable (a, b, c, d, e, f, g, h) Source # 
Instance details

Defined in Data.SBV.Core.Data

Methods

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

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

class SolverContext m where Source #

Actions we can do in a context: Either at problem description time or while we are dynamically querying. Symbolic and Query are two instances of this class. Note that we use this mechanism internally and do not export it from SBV.

Methods

constrain :: SBool -> m () Source #

Add a constraint, any satisfying instance must satisfy this condition

softConstrain :: SBool -> m () Source #

Add a soft constraint. The solver will try to satisfy this condition if possible, but won't if it cannot

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

Add a named constraint. The name is used in unsat-core extraction.

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

Add a constraint, with arbitrary attributes. Used in interpolant generation.

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

Set info. Example: setInfo ":status" ["unsat"].

setOption :: SMTOption -> m () Source #

Set an option.

setLogic :: Logic -> m () Source #

Set the logic.

setTimeOut :: Integer -> m () Source #

Set a solver time-out value, in milli-seconds. This function essentially translates to the SMTLib call (set-info :timeout val), and your backend solver may or may not support it! The amount given is in milliseconds. Also see the function timeOut for finer level control of time-outs, directly from SBV.

internalVariable :: State -> Kind -> IO SW Source #

Create an internal variable, which acts as an input but isn't visible to the user. Such variables are existentially quantified in a SAT context, and universally quantified in a proof context.

internalConstraint :: State -> Bool -> [(String, String)] -> SVal -> IO () Source #

Require a boolean condition to be true in the state. Only used for internal purposes.

isCodeGenMode :: State -> IO Bool Source #

Is this a CodeGen run? (i.e., generating code)

newtype SBVType Source #

A simple type for SBV computations, used mainly for uninterpreted constants. We keep track of the signedness/size of the arguments. A non-function will have just one entry in the list.

Constructors

SBVType [Kind] 
Instances
Eq SBVType Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

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

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

Ord SBVType Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Show SBVType Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

NFData SBVType Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SBVType -> () #

newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO () Source #

Create a new uninterpreted symbol, possibly with user given code

addAxiom :: String -> [String] -> Symbolic () Source #

Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere string, use for commenting purposes. The second argument is intended to hold the multiple-lines of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom itself, to see whether it's actually well-formed or is sensical by any means. A separate formalization of SMT-Lib would be very useful here.

data Quantifier Source #

Quantifiers: forall or exists. Note that we allow arbitrary nestings.

Constructors

ALL 
EX 
Instances
Eq Quantifier Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

NFData Quantifier Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: Quantifier -> () #

needsExistentials :: [Quantifier] -> Bool Source #

Are there any existential quantifiers?

data SMTLibPgm Source #

Representation of an SMT-Lib program. In between pre and post goes the refuted models

Instances
Show SMTLibPgm Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

NFData SMTLibPgm Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SMTLibPgm -> () #

data SMTLibVersion Source #

Representation of SMTLib Program versions. As of June 2015, we're dropping support for SMTLib1, and supporting SMTLib2 only. We keep this data-type around in case SMTLib3 comes along and we want to support 2 and 3 simultaneously.

Constructors

SMTLib2 

smtLibVersionExtension :: SMTLibVersion -> String Source #

The extension associated with the version

smtLibReservedNames :: [String] Source #

Names reserved by SMTLib. This list is current as of Dec 6 2015; but of course there's no guarantee it'll stay that way.

data SolverCapabilities Source #

Translation tricks needed for specific capabilities afforded by each solver

Constructors

SolverCapabilities 

Fields

extractSymbolicSimulationState :: State -> IO Result Source #

Grab the program from a running symbolic simulation state.

data SMTScript Source #

A script, to be passed to the solver.

Constructors

SMTScript 

Fields

Instances
NFData SMTScript Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SMTScript -> () #

data Solver Source #

Solvers that SBV is aware of

Constructors

Z3 
Yices 
Boolector 
CVC4 
MathSAT 
ABC 
Instances
Bounded Solver Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Enum Solver Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Show Solver Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

data SMTSolver Source #

An SMT solver

Constructors

SMTSolver 

Fields

data SMTResult Source #

The result of an SMT solver call. Each constructor is tagged with the SMTConfig that created it so that further tools can inspect it and build layers of results, if needed. For ordinary uses of the library, this type should not be needed, instead use the accessor functions on it. (Custom Show instances and model extractors.)

Constructors

Unsatisfiable SMTConfig (Maybe [String])

Unsatisfiable. If unsat-cores are enabled, they will be returned in the second parameter.

Satisfiable SMTConfig SMTModel

Satisfiable with model

SatExtField SMTConfig SMTModel

Prover returned a model, but in an extension field containing Infinite/epsilon

Unknown SMTConfig SMTReasonUnknown

Prover returned unknown, with the given reason

ProofError SMTConfig [String]

Prover errored out

data SMTModel Source #

A model, as returned by a solver

Constructors

SMTModel 

Fields

Instances
Show SMTModel Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

NFData SMTModel Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SMTModel -> () #

data SMTConfig Source #

Solver configuration. See also z3, yices, cvc4, boolector, mathSAT, etc. which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as z3{verbose=True}.)

Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite precision value on the screen. The field printRealPrec controls the printing precision, by specifying the number of digits after the decimal point. The default value is 16, but it can be set to any positive integer.

When printing, SBV will add the suffix ... at the and of a real-value, if the given bound is not sufficient to represent the real-value exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation of the real value is not finite, i.e., if it is not rational.

The printBase field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis.

Constructors

SMTConfig 

Fields

Instances
NFData SMTConfig Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SMTConfig -> () #

data OptimizeStyle Source #

Style of optimization. Note that in the pareto case the user is allowed to specify a max number of fronts to query the solver for, since there might potentially be an infinite number of them and there is no way to know exactly how many ahead of time. If Nothing is given, SBV will possibly loop forever if the number is really infinite.

Constructors

Lexicographic

Objectives are optimized in the order given, earlier objectives have higher priority.

Independent

Each objective is optimized independently.

Pareto (Maybe Int)

Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse.

data Penalty Source #

Penalty for a soft-assertion. The default penalty is 1, with all soft-assertions belonging to the same objective goal. A positive weight and an optional group can be provided by using the Penalty constructor.

Constructors

DefaultPenalty

Default: Penalty of 1 and no group attached

Penalty Rational (Maybe String)

Penalty with a weight and an optional group

Instances
Show Penalty Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

NFData Penalty Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: Penalty -> () #

data Objective a Source #

Objective of optimization. We can minimize, maximize, or give a soft assertion with a penalty for not satisfying it.

Constructors

Minimize String a

Minimize this metric

Maximize String a

Maximize this metric

AssertWithPenalty String a Penalty

A soft assertion, with an associated penalty

Instances
Functor Objective Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

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

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

Show a => Show (Objective a) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

NFData a => NFData (Objective a) Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: Objective a -> () #

data QueryState Source #

The state we keep track of as we interact with the solver

newtype Query a Source #

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

Constructors

Query (StateT State IO a) 
Instances
Monad Query Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

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

Defined in Data.SBV.Core.Symbolic

Methods

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

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

Applicative Query Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

pure :: a -> Query a #

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

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

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

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

MonadIO Query Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

liftIO :: IO a -> Query a #

SolverContext Query Source #

Query as a SolverContext.

Instance details

Defined in Data.SBV.Control.Utils

MonadState State Query Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

get :: Query State #

put :: State -> Query () #

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

newtype SMTProblem Source #

Internal representation of a symbolic simulation result

Constructors

SMTProblem

SMTLib representation, given the config

Operations useful for instantiating SBV type classes

genLiteral :: Integral a => Kind -> a -> SBV b Source #

Generate a finite constant bitvector

genFromCW :: Integral a => CW -> a Source #

Convert a constant to an integral value

data CW Source #

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

Constructors

CW 

Fields

Instances
Eq CW Source # 
Instance details

Defined in Data.SBV.Core.Concrete

Methods

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

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

Ord CW Source # 
Instance details

Defined in Data.SBV.Core.Concrete

Methods

compare :: CW -> CW -> Ordering #

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

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

(>) :: CW -> CW -> Bool #

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

max :: CW -> CW -> CW #

min :: CW -> CW -> CW #

Show CW Source #

Show instance for CW.

Instance details

Defined in Data.SBV.Core.Concrete

Methods

showsPrec :: Int -> CW -> ShowS #

show :: CW -> String #

showList :: [CW] -> ShowS #

NFData CW Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: CW -> () #

HasKind CW Source #

Kind instance for CW

Instance details

Defined in Data.SBV.Core.Concrete

PrettyNum CW Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

SatModel CW Source #

CW as extracted from a model; trivial definition

Instance details

Defined in Data.SBV.SMT.SMT

Methods

parseCWs :: [CW] -> Maybe (CW, [CW]) Source #

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

SDivisible CW Source # 
Instance details

Defined in Data.SBV.Core.Model

Methods

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

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

sQuot :: CW -> CW -> CW Source #

sRem :: CW -> CW -> CW Source #

sDiv :: CW -> CW -> CW Source #

sMod :: CW -> CW -> CW Source #

genMkSymVar :: Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a) Source #

Generically make a symbolic var

genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW]) Source #

Parse a signed/sized value from a sequence of CWs

showModel :: SMTConfig -> SMTModel -> String Source #

Show a model in human readable form. Ignore bindings to those variables that start with "__internal_sbv_" and also those marked as "nonModelVar" in the config; as these are only for internal purposes

data SMTModel Source #

A model, as returned by a solver

Constructors

SMTModel 

Fields

Instances
Show SMTModel Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

NFData SMTModel Source # 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SMTModel -> () #

liftQRem :: SymWord a => SBV a -> SBV a -> (SBV a, SBV a) Source #

Lift quotRem to symbolic words. Division by 0 is defined s.t. x/0 = 0; which holds even when x is 0 itself.

liftDMod :: (SymWord a, Num a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a) Source #

Lift divMod to symbolic words. Division by 0 is defined s.t. x/0 = 0; which holds even when x is 0 itself. Essentially, this is conversion from quotRem (truncate to 0) to divMod (truncate towards negative infinity)

registerKind :: State -> Kind -> IO () Source #

Register a new kind with the system, used for uninterpreted sorts. NB: Is it safe to have new kinds in query mode? It could be that the new kind might introduce a constraint that effects the logic. For instance, if we're seeing Double for the first time and using a BV logic, then things would fall apart. But this should be rare, and hopefully the success-response checking mechanism will catch the rare cases where this is an issue. In either case, the user can always arrange for the right logic by calling setLogic appropriately, so it seems safe to just allow for this.

Compilation to C, extras

compileToC' :: String -> SBVCodeGen () -> IO (CgConfig, CgPgmBundle) Source #

Lower level version of compileToC, producing a CgPgmBundle

compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO (CgConfig, CgPgmBundle) Source #

Lower level version of compileToCLib, producing a CgPgmBundle

Code generation primitives

The codegen monad

newtype SBVCodeGen a Source #

The code-generation monad. Allows for precise layout of input values reference parameters (for returning composite values in languages such as C), and return values.

Constructors

SBVCodeGen (StateT CgState Symbolic a) 
Instances
Monad SBVCodeGen Source # 
Instance details

Defined in Data.SBV.Compilers.CodeGen

Methods

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

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

return :: a -> SBVCodeGen a #

fail :: String -> SBVCodeGen a #

Functor SBVCodeGen Source # 
Instance details

Defined in Data.SBV.Compilers.CodeGen

Methods

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

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

MonadFail SBVCodeGen Source # 
Instance details

Defined in Data.SBV.Compilers.CodeGen

Methods

fail :: String -> SBVCodeGen a #

Applicative SBVCodeGen Source # 
Instance details

Defined in Data.SBV.Compilers.CodeGen

Methods

pure :: a -> SBVCodeGen a #

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

liftA2 :: (a -> b -> c) -> SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen c #

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

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

MonadIO SBVCodeGen Source # 
Instance details

Defined in Data.SBV.Compilers.CodeGen

Methods

liftIO :: IO a -> SBVCodeGen a #

MonadState CgState SBVCodeGen Source # 
Instance details

Defined in Data.SBV.Compilers.CodeGen

cgSym :: Symbolic a -> SBVCodeGen a Source #

Reach into symbolic monad from code-generation

Specifying inputs, SBV variants

cgInput :: SymWord a => String -> SBVCodeGen (SBV a) Source #

Creates an atomic input in the generated code.

cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a] Source #

Creates an array input in the generated code.

cgOutput :: String -> SBV a -> SBVCodeGen () Source #

Creates an atomic output in the generated code.

cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen () Source #

Creates an array output in the generated code.

cgReturn :: SBV a -> SBVCodeGen () Source #

Creates a returned (unnamed) value in the generated code.

cgReturnArr :: SymWord a => [SBV a] -> SBVCodeGen () Source #

Creates a returned (unnamed) array value in the generated code.

Specifying inputs, SVal variants

svCgInput :: Kind -> String -> SBVCodeGen SVal Source #

Creates an atomic input in the generated code.

svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal] Source #

Creates an array input in the generated code.

svCgOutput :: String -> SVal -> SBVCodeGen () Source #

Creates an atomic output in the generated code.

svCgOutputArr :: String -> [SVal] -> SBVCodeGen () Source #

Creates an array output in the generated code.

svCgReturn :: SVal -> SBVCodeGen () Source #

Creates a returned (unnamed) value in the generated code.

svCgReturnArr :: [SVal] -> SBVCodeGen () Source #

Creates a returned (unnamed) array value in the generated code.

Settings

cgPerformRTCs :: Bool -> SBVCodeGen () Source #

Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off. Default: False.

cgSetDriverValues :: [Integer] -> SBVCodeGen () Source #

Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.

cgAddPrototype :: [String] -> SBVCodeGen () Source #

Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.

cgAddDecl :: [String] -> SBVCodeGen () Source #

Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.

cgAddLDFlags :: [String] -> SBVCodeGen () Source #

Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.

cgIgnoreSAssert :: Bool -> SBVCodeGen () Source #

Ignore assertions (those generated by sAssert calls) in the generated C code

cgOverwriteFiles :: Bool -> SBVCodeGen () Source #

If passed True, then we will not ask the user if we're overwriting files as we generate the C code. Otherwise, we'll prompt.

cgIntegerSize :: Int -> SBVCodeGen () Source #

Sets number of bits to be used for representing the SInteger type in the generated C code. The argument must be one of 8, 16, 32, or 64. Note that this is essentially unsafe as the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as typical in most C implementations.

cgSRealType :: CgSRealType -> SBVCodeGen () Source #

Sets the C type to be used for representing the SReal type in the generated C code. The setting can be one of C's "float", "double", or "long double", types, depending on the precision needed. Note that this is essentially unsafe as the semantics of infinite precision SReal values becomes reduced to the corresponding floating point type in C, and hence it is subject to rounding errors.

data CgSRealType Source #

Possible mappings for the SReal type when translated to C. Used in conjunction with the function cgSRealType. Note that the particular characteristics of the mapped types depend on the platform and the compiler used for compiling the generated C program. See http://en.wikipedia.org/wiki/C_data_types for details.

Constructors

CgFloat
float
CgDouble
double
CgLongDouble
long double

Infrastructure

class CgTarget a where Source #

Abstract over code generation for different languages

data CgConfig Source #

Options for code-generation.

Constructors

CgConfig 

Fields

data CgState Source #

Code-generation state

Instances
MonadState CgState SBVCodeGen Source # 
Instance details

Defined in Data.SBV.Compilers.CodeGen

data CgPgmBundle Source #

Representation of a collection of generated programs.

Instances
Show CgPgmBundle Source # 
Instance details

Defined in Data.SBV.Compilers.CodeGen

data CgPgmKind Source #

Different kinds of "files" we can produce. Currently this is quite C specific.

data CgVal Source #

Abstraction of target language values

Constructors

CgAtomic SW 
CgArray [SW] 

defaultCgConfig :: CgConfig Source #

Default options for code generation. The run-time checks are turned-off, and the driver values are completely random.

initCgState :: CgState Source #

Initial configuration for code-generation

isCgDriver :: CgPgmKind -> Bool Source #

Is this a driver program?

isCgMakefile :: CgPgmKind -> Bool Source #

Is this a make file?

Generating collateral

cgGenerateDriver :: Bool -> SBVCodeGen () Source #

Should we generate a driver program? Default: True. When a library is generated, it will have a driver if any of the contituent functions has a driver. (See compileToCLib.)

cgGenerateMakefile :: Bool -> SBVCodeGen () Source #

Should we generate a Makefile? Default: True.

codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO (CgConfig, CgPgmBundle) Source #

Generate code for a symbolic program, returning a Code-gen bundle, i.e., collection of makefiles, source code, headers, etc.

renderCgPgmBundle :: Maybe FilePath -> (CgConfig, CgPgmBundle) -> IO () Source #

Render a code-gen bundle to a directory or to stdout

Various math utilities around floats

fpRound0 :: (RealFloat a, Integral b) => a -> b Source #

A variant of round; except defaulting to 0 when fed NaN or Infinity

fpRatio0 :: RealFloat a => a -> Rational Source #

A variant of toRational; except defaulting to 0 when fed NaN or Infinity

fpMaxH :: RealFloat a => a -> a -> a Source #

The SMT-Lib (in particular Z3) implementation for min/max for floats does not agree with Haskell's; and also it does not agree with what the hardware does. Sigh.. See: http://ghc.haskell.org/trac/ghc/ticket/10378 http://github.com/Z3Prover/z3/issues/68 So, we codify here what the Z3 (SMTLib) is implementing for fpMax. The discrepancy with Haskell is that the NaN propagation doesn't work in Haskell The discrepancy with x86 is that given +0/-0, x86 returns the second argument; SMTLib is non-deterministic

fpMinH :: RealFloat a => a -> a -> a Source #

SMTLib compliant definition for fpMin. See the comments for fpMax.

fp2fp :: (RealFloat a, RealFloat b) => a -> b Source #

Convert double to float and back. Essentially fromRational . toRational except careful on NaN, Infinities, and -0.

fpRemH :: RealFloat a => a -> a -> a Source #

Compute the "floating-point" remainder function, the float/double value that remains from the division of x and y. There are strict rules around 0's, Infinities, and NaN's as coded below, See http://smt-lib.org/papers/BTRW14.pdf, towards the end of section 4.c.

fpRoundToIntegralH :: RealFloat a => a -> a Source #

Convert a float to the nearest integral representable in that type

fpIsEqualObjectH :: RealFloat a => a -> a -> Bool Source #

Check that two floats are the exact same values, i.e., +0/-0 does not compare equal, and NaN's compare equal to themselves.

fpCompareObjectH :: RealFloat a => a -> a -> Ordering Source #

Ordering for floats, avoiding the +0-0NaN issues. Note that this is essentially used for indexing into a map, so we need to be total. Thus, the order we pick is: NaN -oo -0 +0 +oo The placement of NaN here is questionable, but immaterial.

fpIsNormalizedH :: RealFloat a => a -> Bool Source #

Check if a number is "normal." Note that +0/-0 is not considered a normal-number and also this is not simply the negation of isDenormalized!

Pretty number printing

class PrettyNum a where Source #

PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.

Minimal complete definition: hexS and binS

Methods

hexS :: a -> String Source #

Show a number in hexadecimal (starting with 0x and type.)

binS :: a -> String Source #

Show a number in binary (starting with 0b and type.)

hex :: a -> String Source #

Show a number in hex, without prefix, or types.

bin :: a -> String Source #

Show a number in bin, without prefix, or types.

Instances
PrettyNum Bool Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

PrettyNum Int8 Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

PrettyNum Int16 Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

PrettyNum Int32 Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

PrettyNum Int64 Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

PrettyNum Integer Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

PrettyNum Word8 Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

PrettyNum Word16 Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

PrettyNum Word32 Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

PrettyNum Word64 Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

PrettyNum String Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

PrettyNum CW Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

(SymWord a, PrettyNum a) => PrettyNum (SBV a) Source # 
Instance details

Defined in Data.SBV.Utils.PrettyNum

Methods

hexS :: SBV a -> String Source #

binS :: SBV a -> String Source #

hex :: SBV a -> String Source #

bin :: SBV a -> String Source #

readBin :: Num a => String -> a Source #

A more convenient interface for reading binary numbers, also supports negative numbers

shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String Source #

Show as a hexadecimal value. First bool controls whether type info is printed while the second boolean controls wether 0x prefix is printed. The tuple is the signedness and the bit-length of the input. The length of the string will not depend on the value, but rather the bit-length.

chex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String Source #

Show as hexadecimal, but for C programs. We have to be careful about printing min-bounds, since C does some funky casting, possibly losing the sign bit. In those cases, we use the defined constants in stdint.h. We also properly append the necessary suffixes as needed.

shexI :: Bool -> Bool -> Integer -> String Source #

Show as a hexadecimal value, integer version. Almost the same as shex above except we don't have a bit-length so the length of the string will depend on the actual value.

sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String Source #

Similar to shex; except in binary.

sbinI :: Bool -> Bool -> Integer -> String Source #

Similar to shexI; except in binary.

showCFloat :: Float -> String Source #

A version of show for floats that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included.

showCDouble :: Double -> String Source #

A version of show for doubles that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included.

showHFloat :: Float -> String Source #

A version of show for floats that generates correct Haskell literals for nan/infinite

showHDouble :: Double -> String Source #

A version of show for doubles that generates correct Haskell literals for nan/infinite

showSMTFloat :: RoundingMode -> Float -> String Source #

A version of show for floats that generates correct SMTLib literals using the rounding mode

showSMTDouble :: RoundingMode -> Double -> String Source #

A version of show for doubles that generates correct SMTLib literals using the rounding mode

smtRoundingMode :: RoundingMode -> String Source #

Convert a rounding mode to the format SMT-Lib2 understands.

cwToSMTLib :: RoundingMode -> CW -> String Source #

Convert a CW to an SMTLib2 compliant value

mkSkolemZero :: RoundingMode -> Kind -> String Source #

Create a skolem 0 for the kind

Timing computations

data Timing Source #

Specify how to save timing information, if at all.

showTDiff :: NominalDiffTime -> String Source #

Show NominalDiffTime in human readable form. NominalDiffTime is essentially picoseconds (10^-12 seconds). We show it so that it's represented at the day:hour:minute:second.XXX granularity.

Coordinating with the solver

In rare cases it might be necessary to send an arbitrary string down to the solver. Needless to say, this should be avoided if at all possible. Users should prefer the provided API. If you do find yourself needing send and ask directly, please get in touch to see if SBV can support a typed API for your use case. Similarly, the function retrieveResponseFromSolver might occasionally be necessary to clean-up the communication buffer. We would like to hear if you do need these functions regularly so we can provide better support.

sendStringToSolver :: String -> Query () Source #

Send an arbitrary string to the solver in a query. Note that this is inherently dangerous as it can put the solver in an arbitrary state and confuse SBV. If you use this feature, you are on your own!

sendRequestToSolver :: String -> Query String Source #

Send an arbitrary string to the solver in a query, and return a response. Note that this is inherently dangerous as it can put the solver in an arbitrary state and confuse SBV.

retrieveResponseFromSolver :: String -> Maybe Int -> Query [String] Source #

Retrieve multiple responses from the solver, until it responds with a user given tag that we shall arrange for internally. The optional timeout is in milliseconds. If the time-out is exceeded, then we will raise an error. Note that this is inherently dangerous as it can put the solver in an arbitrary state and confuse SBV. If you use this feature, you are on your own!

Defining new metrics

addSValOptGoal :: Objective SVal -> Symbolic () Source #

Add an optimization goal