sbv-7.10: 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 length, and internally processed as one unit as opposed to a fixed-length list of characters.

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

sRoundTowardPositive :: SRoundingMode Source #

Symbolic variant of RoundNearestPositive

class (HasKind a, Ord 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.

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 String Source # 
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 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.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

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

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

Defined in Data.SBV.Core.Model

Methods

fromString :: String -> SString #

Testable SBool # 
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, Bounded a) => Bounded (SBV a) # 
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) # 
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 #

Equality constraint on SBV values. Not desirable since we can't really compare two symbolic values, but will do. Note that we do need this instance since we want Bits as a class for SBV that we implement, which necessiates the Eq class.

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

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) # 
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) # 
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) :: * -> * #

Methods

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

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

Testable (Symbolic SBool) # 
Instance details

Defined in Data.SBV.Core.Model

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