sbv-7.3: 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

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.

data IStage Source #

Stage of an interactive run

Constructors

ISetup 
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

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 # 
Enum RoundingMode Source # 
Eq RoundingMode Source # 
Data RoundingMode Source # 

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 # 
Read RoundingMode Source # 
Show RoundingMode Source # 
HasKind RoundingMode Source #

RoundingMode kind

SymWord RoundingMode Source #

RoundingMode can be used symbolically

SatModel RoundingMode Source #

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

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

RoundingMode can be used symbolically

SymWord L Source #

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

SymWord Q Source # 
SymWord B Source # 
SymWord BinOp Source # 
SymWord UnOp Source # 
SymWord Day Source # 
SymWord U2Member Source # 
SymWord Location Source # 
SymWord Color Source # 
SymWord Nationality Source # 
SymWord Beverage Source # 
SymWord Pet Source # 
SymWord Sport Source # 
SymWord Word4 Source #

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

SymWord E Source # 

data CW Source #

CW represents a concrete word of a fixed size: Endianness is mostly irrelevant (see the FromBits class). For signed words, the most significant digit is considered to be the sign.

Constructors

CW 

Fields

Instances

Eq CW Source # 

Methods

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

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

Ord CW Source # 

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.

Methods

showsPrec :: Int -> CW -> ShowS #

show :: CW -> String #

showList :: [CW] -> ShowS #

HasKind CW Source #

Kind instance for CW

PrettyNum CW Source # 
SatModel CW Source #

CW as extracted from a model; trivial definition

Methods

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

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

SDivisible CW Source # 

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

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:

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.

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 
AlgPolyRoot (Integer, Polynomial) (Maybe String) 

Instances

Eq AlgReal Source # 

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.

Num AlgReal Source # 
Ord AlgReal Source # 
Real AlgReal Source # 
Show AlgReal Source # 
Random AlgReal Source # 

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

Arbitrary AlgReal Source # 

Methods

arbitrary :: Gen AlgReal

shrink :: AlgReal -> [AlgReal]

HasKind AlgReal Source # 
SatModel AlgReal Source #

AlgReal as extracted from a model

Methods

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

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

SMTValue AlgReal Source # 

Methods

sexprToVal :: SExpr -> Maybe AlgReal Source #

IEEEFloatConvertable AlgReal Source # 

data ExtCW Source #

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

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

Methods

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

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

Ord SW Source # 

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 # 

Methods

showsPrec :: Int -> SW -> ShowS #

show :: SW -> String #

showList :: [SW] -> ShowS #

NFData SW Source # 

Methods

rnf :: SW -> () #

HasKind SW Source # 

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 #

Equality constraint on SBV values. Not desirable since we can't really compare two symbolic values, but will do.

Methods

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

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

Show SVal Source # 

Methods

showsPrec :: Int -> SVal -> ShowS #

show :: SVal -> String #

showList :: [SVal] -> ShowS #

NFData SVal Source # 

Methods

rnf :: SVal -> () #

HasKind SVal Source # 

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

Boolean SBool Source # 
Provable SBool Source # 
Provable Predicate Source # 
SDivisible SInteger Source # 
SDivisible SInt64 Source # 
SDivisible SInt32 Source # 
SDivisible SInt16 Source # 
SDivisible SInt8 Source # 
SDivisible SWord64 Source # 
SDivisible SWord32 Source # 
SDivisible SWord16 Source # 
SDivisible SWord8 Source # 
SDivisible SWord4 Source #

SDvisible instance, using default methods

FromBits SInt64 Source # 
FromBits SInt32 Source # 
FromBits SInt16 Source # 
FromBits SInt8 Source # 
FromBits SWord64 Source # 
FromBits SWord32 Source # 
FromBits SWord16 Source # 
FromBits SWord8 Source # 
FromBits SBool Source # 
FromBits SWord4 Source #

Conversion from bits

Polynomial SWord64 Source # 
Polynomial SWord32 Source # 
Polynomial SWord16 Source # 
Polynomial SWord8 Source # 
Splittable SWord64 SWord32 Source # 
Splittable SWord32 SWord16 Source # 
Splittable SWord16 SWord8 Source # 
Eq (SBV a) Source # 

Methods

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

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

Show (SBV a) Source # 

Methods

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

show :: SBV a -> String #

showList :: [SBV a] -> ShowS #

Generic (SBV a) Source # 

Associated Types

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

Methods

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

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

NFData (SBV a) Source # 

Methods

rnf :: SBV a -> () #

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

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

Methods

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

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

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 # 

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 # 
HasKind a => Uninterpreted (SBV a) Source # 
SymWord a => Mergeable (SBV a) Source # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 
(SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) Source # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 

Methods

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

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

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 # 

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 # 

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 # 

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 # 

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 # 

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 # 
type Rep (SBV a) = D1 * (MetaData "SBV" "Data.SBV.Core.Data" "sbv-7.3-9TxzYQvebLZI3wS7UzYUG5" True) (C1 * (MetaCons "SBV" PrefixI True) (S1 * (MetaSel (Just Symbol "unSBV") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SVal)))

newtype NodeId Source #

A symbolic node id

Constructors

NodeId Int 

Instances

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

A new array, the contents are uninitialized

ArrayMutate Int SW SW

An array created by mutating another array at a given cell

ArrayMerge SW Int Int

An array created by symbolically merging two other arrays

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.

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. (There are some differences between these models, however, see the corresponding declaration.)

Minimal complete definition: All methods are required, no defaults.

Minimal complete definition

newArray_, newArray, readArray, writeArray, mergeArrays

Methods

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

Create a new anonymous array

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

Create a named new array

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

Instances

SymArray SArray Source # 

Methods

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

newArray :: (HasKind a, HasKind b) => String -> 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 #

newtype SFunArray a b Source #

Arrays implemented internally as functions

  • Internally handled by the library and not mapped to SMT-Lib
  • Reading an uninitialized value is considered an error (will throw exception)
  • Cannot check for equality (internally represented as functions)
  • Can quick-check
  • Typically faster as it gets compiled away during translation

Constructors

SFunArray (SBV a -> SBV b) 

Instances

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

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 # 

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 # 

Methods

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

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

mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b Source #

Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use newArray.)

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 and yields an unspecified result
  • Can check for equality of these arrays
  • 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 # 

Methods

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

newArray :: (HasKind a, HasKind b) => String -> 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 #

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

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 # 

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 # 

Methods

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

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

EqSymbolic (SArray a b) Source # 

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] 

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://ittc.ku.edu/~andygill/paper.php?label=DSLExtract09

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

Instances

NFData (Cached a) Source # 

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 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. This class can be automatically derived for data-types that have a Data instance; this is useful for creating uninterpreted sorts.

Instances

HasKind Bool Source # 
HasKind Double Source # 
HasKind Float Source # 
HasKind Int8 Source # 
HasKind Int16 Source # 
HasKind Int32 Source # 
HasKind Int64 Source # 
HasKind Integer Source # 
HasKind Word8 Source # 
HasKind Word16 Source # 
HasKind Word32 Source # 
HasKind Word64 Source # 
HasKind AlgReal Source # 
HasKind Kind Source # 
HasKind ExtCW Source #

Kind instance for Extended CW

HasKind GeneralizedCW Source #

Kind instance for generalized CW

HasKind CW Source #

Kind instance for CW

HasKind RoundingMode Source #

RoundingMode kind

HasKind SVal Source # 
HasKind SW Source # 
HasKind L Source #

Similarly, HasKinds default implementation is sufficient.

HasKind Q Source # 
HasKind B Source # 
HasKind BinOp Source # 
HasKind UnOp Source # 
HasKind Day Source # 
HasKind U2Member Source # 
HasKind Location Source # 
HasKind Color Source # 
HasKind Nationality Source # 
HasKind Beverage Source # 
HasKind Pet Source # 
HasKind Sport Source # 
HasKind Word4 Source #

HasKind instance; simply returning the underlying kind for the type

HasKind E Source # 
HasKind (SBV a) Source # 

data Op Source #

Symbolic operations

Instances

Eq Op Source # 

Methods

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

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

Ord Op Source # 

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 # 

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 # 

Methods

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

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

Ord PBOp Source # 

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 # 

Methods

showsPrec :: Int -> PBOp -> ShowS #

show :: PBOp -> String #

showList :: [PBOp] -> ShowS #

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 # 

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 # 

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 # 

Methods

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

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

Applicative Symbolic Source # 

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 # 

Methods

liftIO :: IO a -> Symbolic a #

Provable Predicate Source # 
MonadReader State Symbolic Source # 

Methods

ask :: Symbolic State

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

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

NFData a => SExecutable (Symbolic a) Source # 

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 #

Return and clean and incState

The state of the symbolic interpreter

Instances

NFData State Source # 

Methods

rnf :: State -> () #

MonadReader State Symbolic Source # 

Methods

ask :: Symbolic State

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

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

MonadState State Query Source # 

Methods

get :: Query State

put :: State -> Query ()

state :: (State -> (a, State)) -> Query 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.

data Kind Source #

Kind of symbolic value

Instances

Eq Kind Source #

We want to equate user-sorts only by name

Methods

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

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

Ord Kind Source #

We want to order user-sorts only by name

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 # 

Methods

showsPrec :: Int -> Kind -> ShowS #

show :: Kind -> String #

showList :: [Kind] -> ShowS #

HasKind Kind Source # 

class Outputtable a where Source #

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

Minimal complete definition

output

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 # 

Methods

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

Outputtable a => Outputtable [a] Source # 

Methods

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

Outputtable (SBV a) Source # 

Methods

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

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

Methods

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

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

Methods

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

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

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 # 

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 # 

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 # 

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 # 

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

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.

Minimal complete definition

constrain, namedConstraint, setOption

Methods

constrain :: SBool -> m () Source #

Add a constraint, any satisfying instance must satisfy this condition

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

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

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 -> Maybe 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] 

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 

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

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 # 

Methods

rnf :: SMTScript -> () #

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

Unsatisfiable

Satisfiable SMTConfig SMTModel

Satisfiable with model

SatExtField SMTConfig SMTModel

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

Unknown SMTConfig String

Prover returned unknown, with the given reason

ProofError SMTConfig [String]

Prover errored out