grisette-0.1.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellSafe-Inferred
LanguageHaskell2010

Grisette.IR.SymPrim

Description

 
Synopsis

Symbolic type implementation

Extended types

data IntN (n :: Nat) Source #

Symbolic signed bit vectors.

Instances

Instances details
ToSym Int16 (Sym (IntN 16)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int16 -> Sym (IntN 16) Source #

ToSym Int32 (Sym (IntN 32)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int32 -> Sym (IntN 32) Source #

ToSym Int64 (Sym (IntN 64)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int64 -> Sym (IntN 64) Source #

ToSym Int8 (Sym (IntN 8)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int8 -> Sym (IntN 8) Source #

ToSym Int (Sym (IntN 64)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int -> Sym (IntN 64) Source #

Lift (IntN n :: Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

lift :: Quote m => IntN n -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => IntN n -> Code m (IntN n) #

(KnownNat n, 1 <= n) => Bits (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

(.&.) :: IntN n -> IntN n -> IntN n #

(.|.) :: IntN n -> IntN n -> IntN n #

xor :: IntN n -> IntN n -> IntN n #

complement :: IntN n -> IntN n #

shift :: IntN n -> Int -> IntN n #

rotate :: IntN n -> Int -> IntN n #

zeroBits :: IntN n #

bit :: Int -> IntN n #

setBit :: IntN n -> Int -> IntN n #

clearBit :: IntN n -> Int -> IntN n #

complementBit :: IntN n -> Int -> IntN n #

testBit :: IntN n -> Int -> Bool #

bitSizeMaybe :: IntN n -> Maybe Int #

bitSize :: IntN n -> Int #

isSigned :: IntN n -> Bool #

shiftL :: IntN n -> Int -> IntN n #

unsafeShiftL :: IntN n -> Int -> IntN n #

shiftR :: IntN n -> Int -> IntN n #

unsafeShiftR :: IntN n -> Int -> IntN n #

rotateL :: IntN n -> Int -> IntN n #

rotateR :: IntN n -> Int -> IntN n #

popCount :: IntN n -> Int #

SupportedPrim (IntN n) => Bits (Sym (IntN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(.&.) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

(.|.) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

xor :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

complement :: Sym (IntN n) -> Sym (IntN n) #

shift :: Sym (IntN n) -> Int -> Sym (IntN n) #

rotate :: Sym (IntN n) -> Int -> Sym (IntN n) #

zeroBits :: Sym (IntN n) #

bit :: Int -> Sym (IntN n) #

setBit :: Sym (IntN n) -> Int -> Sym (IntN n) #

clearBit :: Sym (IntN n) -> Int -> Sym (IntN n) #

complementBit :: Sym (IntN n) -> Int -> Sym (IntN n) #

testBit :: Sym (IntN n) -> Int -> Bool #

bitSizeMaybe :: Sym (IntN n) -> Maybe Int #

bitSize :: Sym (IntN n) -> Int #

isSigned :: Sym (IntN n) -> Bool #

shiftL :: Sym (IntN n) -> Int -> Sym (IntN n) #

unsafeShiftL :: Sym (IntN n) -> Int -> Sym (IntN n) #

shiftR :: Sym (IntN n) -> Int -> Sym (IntN n) #

unsafeShiftR :: Sym (IntN n) -> Int -> Sym (IntN n) #

rotateL :: Sym (IntN n) -> Int -> Sym (IntN n) #

rotateR :: Sym (IntN n) -> Int -> Sym (IntN n) #

popCount :: Sym (IntN n) -> Int #

(KnownNat n, 1 <= n) => FiniteBits (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

(KnownNat n, 1 <= n) => Bounded (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

minBound :: IntN n #

maxBound :: IntN n #

(KnownNat n, 1 <= n) => Enum (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

succ :: IntN n -> IntN n #

pred :: IntN n -> IntN n #

toEnum :: Int -> IntN n #

fromEnum :: IntN n -> Int #

enumFrom :: IntN n -> [IntN n] #

enumFromThen :: IntN n -> IntN n -> [IntN n] #

enumFromTo :: IntN n -> IntN n -> [IntN n] #

enumFromThenTo :: IntN n -> IntN n -> IntN n -> [IntN n] #

Generic (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Associated Types

type Rep (IntN n) :: Type -> Type #

Methods

from :: IntN n -> Rep (IntN n) x #

to :: Rep (IntN n) x -> IntN n #

(KnownNat n, 1 <= n) => Num (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

(+) :: IntN n -> IntN n -> IntN n #

(-) :: IntN n -> IntN n -> IntN n #

(*) :: IntN n -> IntN n -> IntN n #

negate :: IntN n -> IntN n #

abs :: IntN n -> IntN n #

signum :: IntN n -> IntN n #

fromInteger :: Integer -> IntN n #

SupportedPrim (IntN n) => Num (Sym (IntN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(+) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

(-) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

(*) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

negate :: Sym (IntN n) -> Sym (IntN n) #

abs :: Sym (IntN n) -> Sym (IntN n) #

signum :: Sym (IntN n) -> Sym (IntN n) #

fromInteger :: Integer -> Sym (IntN n) #

(KnownNat n, 1 <= n) => Integral (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

quot :: IntN n -> IntN n -> IntN n #

rem :: IntN n -> IntN n -> IntN n #

div :: IntN n -> IntN n -> IntN n #

mod :: IntN n -> IntN n -> IntN n #

quotRem :: IntN n -> IntN n -> (IntN n, IntN n) #

divMod :: IntN n -> IntN n -> (IntN n, IntN n) #

toInteger :: IntN n -> Integer #

(KnownNat n, 1 <= n) => Real (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

toRational :: IntN n -> Rational #

(KnownNat n, 1 <= n) => Show (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

showsPrec :: Int -> IntN n -> ShowS #

show :: IntN n -> String #

showList :: [IntN n] -> ShowS #

NFData (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

rnf :: IntN n -> () #

Eq (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

(==) :: IntN n -> IntN n -> Bool #

(/=) :: IntN n -> IntN n -> Bool #

(KnownNat n, 1 <= n) => Ord (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

compare :: IntN n -> IntN n -> Ordering #

(<) :: IntN n -> IntN n -> Bool #

(<=) :: IntN n -> IntN n -> Bool #

(>) :: IntN n -> IntN n -> Bool #

(>=) :: IntN n -> IntN n -> Bool #

max :: IntN n -> IntN n -> IntN n #

min :: IntN n -> IntN n -> IntN n #

SupportedPrim (IntN n) => SEq (Sym (IntN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(==~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

(/=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

SupportedPrim (IntN n) => SOrd (Sym (IntN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

(<=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

(>~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

(>=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

symCompare :: Sym (IntN n) -> Sym (IntN n) -> UnionM Ordering Source #

(KnownNat w, 1 <= w) => SupportedPrim (IntN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (IntN w) Source #

Hashable (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

hashWithSalt :: Int -> IntN n -> Int #

hash :: IntN n -> Int #

ToCon (Sym (IntN 8)) Int8 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 8) -> Maybe Int8 Source #

ToCon (Sym (IntN 16)) Int16 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 16) -> Maybe Int16 Source #

ToCon (Sym (IntN 32)) Int32 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 32) -> Maybe Int32 Source #

ToCon (Sym (IntN 64)) Int64 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 64) -> Maybe Int64 Source #

ToCon (Sym (IntN 64)) Int Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 64) -> Maybe Int Source #

(KnownNat n, 1 <= n, KnownNat ix, KnownNat w, 1 <= w, (ix + w) <= n) => BVSelect (IntN n) ix w (IntN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvselect :: proxy ix -> proxy w -> IntN n -> IntN w Source #

(KnownNat ix, KnownNat w, KnownNat ow, (ix + w) <= ow, 1 <= ow, 1 <= w) => BVSelect (Sym (IntN ow)) ix w (Sym (IntN w)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvselect :: proxy ix -> proxy w -> Sym (IntN ow) -> Sym (IntN w) Source #

(KnownNat n, 1 <= n, KnownNat r, n <= r) => BVExtend (IntN n) r (IntN r) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvzeroExtend :: proxy r -> IntN n -> IntN r Source #

bvsignExtend :: proxy r -> IntN n -> IntN r Source #

bvextend :: proxy r -> IntN n -> IntN r Source #

(KnownNat w, KnownNat w', 1 <= w, 1 <= w', w <= w', (w + 1) <= w', 1 <= (w' - w), KnownNat (w' - w)) => BVExtend (Sym (IntN w)) w' (Sym (IntN w')) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvzeroExtend :: proxy w' -> Sym (IntN w) -> Sym (IntN w') Source #

bvsignExtend :: proxy w' -> Sym (IntN w) -> Sym (IntN w') Source #

bvextend :: proxy w' -> Sym (IntN w) -> Sym (IntN w') Source #

(KnownNat n, 1 <= n, KnownNat m, 1 <= m, KnownNat w, 1 <= w, w ~ (n + m)) => BVConcat (IntN n) (IntN m) (IntN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvconcat :: IntN n -> IntN m -> IntN w Source #

(KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') => BVConcat (Sym (IntN n)) (Sym (IntN w)) (Sym (IntN w')) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvconcat :: Sym (IntN n) -> Sym (IntN w) -> Sym (IntN w') Source #

type Rep (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

type Rep (IntN n) = D1 ('MetaData "IntN" "Grisette.IR.SymPrim.Data.BV" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'True) (C1 ('MetaCons "IntN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unIntN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))
type PrimConstraint (IntN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

type PrimConstraint (IntN w) = (KnownNat w, 1 <= w)

data WordN (n :: Nat) Source #

Symbolic unsigned bit vectors.

Instances

Instances details
ToSym Word16 (Sym (WordN 16)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word16 -> Sym (WordN 16) Source #

ToSym Word32 (Sym (WordN 32)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word32 -> Sym (WordN 32) Source #

ToSym Word64 (Sym (WordN 64)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word64 -> Sym (WordN 64) Source #

ToSym Word8 (Sym (WordN 8)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word8 -> Sym (WordN 8) Source #

ToSym Word (Sym (WordN 64)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word -> Sym (WordN 64) Source #

Lift (WordN n :: Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

lift :: Quote m => WordN n -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => WordN n -> Code m (WordN n) #

(KnownNat n, 1 <= n) => Bits (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

(.&.) :: WordN n -> WordN n -> WordN n #

(.|.) :: WordN n -> WordN n -> WordN n #

xor :: WordN n -> WordN n -> WordN n #

complement :: WordN n -> WordN n #

shift :: WordN n -> Int -> WordN n #

rotate :: WordN n -> Int -> WordN n #

zeroBits :: WordN n #

bit :: Int -> WordN n #

setBit :: WordN n -> Int -> WordN n #

clearBit :: WordN n -> Int -> WordN n #

complementBit :: WordN n -> Int -> WordN n #

testBit :: WordN n -> Int -> Bool #

bitSizeMaybe :: WordN n -> Maybe Int #

bitSize :: WordN n -> Int #

isSigned :: WordN n -> Bool #

shiftL :: WordN n -> Int -> WordN n #

unsafeShiftL :: WordN n -> Int -> WordN n #

shiftR :: WordN n -> Int -> WordN n #

unsafeShiftR :: WordN n -> Int -> WordN n #

rotateL :: WordN n -> Int -> WordN n #

rotateR :: WordN n -> Int -> WordN n #

popCount :: WordN n -> Int #

SupportedPrim (WordN n) => Bits (Sym (WordN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(.&.) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

(.|.) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

xor :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

complement :: Sym (WordN n) -> Sym (WordN n) #

shift :: Sym (WordN n) -> Int -> Sym (WordN n) #

rotate :: Sym (WordN n) -> Int -> Sym (WordN n) #

zeroBits :: Sym (WordN n) #

bit :: Int -> Sym (WordN n) #

setBit :: Sym (WordN n) -> Int -> Sym (WordN n) #

clearBit :: Sym (WordN n) -> Int -> Sym (WordN n) #

complementBit :: Sym (WordN n) -> Int -> Sym (WordN n) #

testBit :: Sym (WordN n) -> Int -> Bool #

bitSizeMaybe :: Sym (WordN n) -> Maybe Int #

bitSize :: Sym (WordN n) -> Int #

isSigned :: Sym (WordN n) -> Bool #

shiftL :: Sym (WordN n) -> Int -> Sym (WordN n) #

unsafeShiftL :: Sym (WordN n) -> Int -> Sym (WordN n) #

shiftR :: Sym (WordN n) -> Int -> Sym (WordN n) #

unsafeShiftR :: Sym (WordN n) -> Int -> Sym (WordN n) #

rotateL :: Sym (WordN n) -> Int -> Sym (WordN n) #

rotateR :: Sym (WordN n) -> Int -> Sym (WordN n) #

popCount :: Sym (WordN n) -> Int #

(KnownNat n, 1 <= n) => FiniteBits (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

(KnownNat n, 1 <= n) => Bounded (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

minBound :: WordN n #

maxBound :: WordN n #

(KnownNat n, 1 <= n) => Enum (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

succ :: WordN n -> WordN n #

pred :: WordN n -> WordN n #

toEnum :: Int -> WordN n #

fromEnum :: WordN n -> Int #

enumFrom :: WordN n -> [WordN n] #

enumFromThen :: WordN n -> WordN n -> [WordN n] #

enumFromTo :: WordN n -> WordN n -> [WordN n] #

enumFromThenTo :: WordN n -> WordN n -> WordN n -> [WordN n] #

Generic (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Associated Types

type Rep (WordN n) :: Type -> Type #

Methods

from :: WordN n -> Rep (WordN n) x #

to :: Rep (WordN n) x -> WordN n #

(KnownNat n, 1 <= n) => Num (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

(+) :: WordN n -> WordN n -> WordN n #

(-) :: WordN n -> WordN n -> WordN n #

(*) :: WordN n -> WordN n -> WordN n #

negate :: WordN n -> WordN n #

abs :: WordN n -> WordN n #

signum :: WordN n -> WordN n #

fromInteger :: Integer -> WordN n #

SupportedPrim (WordN n) => Num (Sym (WordN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(+) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

(-) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

(*) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

negate :: Sym (WordN n) -> Sym (WordN n) #

abs :: Sym (WordN n) -> Sym (WordN n) #

signum :: Sym (WordN n) -> Sym (WordN n) #

fromInteger :: Integer -> Sym (WordN n) #

(KnownNat n, 1 <= n) => Integral (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

quot :: WordN n -> WordN n -> WordN n #

rem :: WordN n -> WordN n -> WordN n #

div :: WordN n -> WordN n -> WordN n #

mod :: WordN n -> WordN n -> WordN n #

quotRem :: WordN n -> WordN n -> (WordN n, WordN n) #

divMod :: WordN n -> WordN n -> (WordN n, WordN n) #

toInteger :: WordN n -> Integer #

(KnownNat n, 1 <= n) => Real (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

toRational :: WordN n -> Rational #

(KnownNat n, 1 <= n) => Show (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

showsPrec :: Int -> WordN n -> ShowS #

show :: WordN n -> String #

showList :: [WordN n] -> ShowS #

NFData (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

rnf :: WordN n -> () #

Eq (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

(==) :: WordN n -> WordN n -> Bool #

(/=) :: WordN n -> WordN n -> Bool #

Ord (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

compare :: WordN n -> WordN n -> Ordering #

(<) :: WordN n -> WordN n -> Bool #

(<=) :: WordN n -> WordN n -> Bool #

(>) :: WordN n -> WordN n -> Bool #

(>=) :: WordN n -> WordN n -> Bool #

max :: WordN n -> WordN n -> WordN n #

min :: WordN n -> WordN n -> WordN n #

SupportedPrim (WordN n) => SEq (Sym (WordN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(==~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

(/=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

SupportedPrim (WordN n) => SOrd (Sym (WordN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

(<=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

(>~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

(>=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

symCompare :: Sym (WordN n) -> Sym (WordN n) -> UnionM Ordering Source #

(KnownNat w, 1 <= w) => SupportedPrim (WordN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (WordN w) Source #

Hashable (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

hashWithSalt :: Int -> WordN n -> Int #

hash :: WordN n -> Int #

ToCon (Sym (WordN 8)) Word8 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 8) -> Maybe Word8 Source #

ToCon (Sym (WordN 16)) Word16 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 16) -> Maybe Word16 Source #

ToCon (Sym (WordN 32)) Word32 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 32) -> Maybe Word32 Source #

ToCon (Sym (WordN 64)) Word64 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 64) -> Maybe Word64 Source #

ToCon (Sym (WordN 64)) Word Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 64) -> Maybe Word Source #

(KnownNat n, 1 <= n, KnownNat ix, KnownNat w, 1 <= w, (ix + w) <= n) => BVSelect (WordN n) ix w (WordN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvselect :: proxy ix -> proxy w -> WordN n -> WordN w Source #

(KnownNat ix, KnownNat w, KnownNat ow, (ix + w) <= ow, 1 <= ow, 1 <= w) => BVSelect (Sym (WordN ow)) ix w (Sym (WordN w)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvselect :: proxy ix -> proxy w -> Sym (WordN ow) -> Sym (WordN w) Source #

(KnownNat n, 1 <= n, KnownNat r, n <= r) => BVExtend (WordN n) r (WordN r) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvzeroExtend :: proxy r -> WordN n -> WordN r Source #

bvsignExtend :: proxy r -> WordN n -> WordN r Source #

bvextend :: proxy r -> WordN n -> WordN r Source #

(KnownNat w, KnownNat w', 1 <= w, 1 <= w', (w + 1) <= w', w <= w', 1 <= (w' - w), KnownNat (w' - w)) => BVExtend (Sym (WordN w)) w' (Sym (WordN w')) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvzeroExtend :: proxy w' -> Sym (WordN w) -> Sym (WordN w') Source #

bvsignExtend :: proxy w' -> Sym (WordN w) -> Sym (WordN w') Source #

bvextend :: proxy w' -> Sym (WordN w) -> Sym (WordN w') Source #

(KnownNat n, 1 <= n, KnownNat m, 1 <= m, KnownNat w, 1 <= w, w ~ (n + m)) => BVConcat (WordN n) (WordN m) (WordN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

Methods

bvconcat :: WordN n -> WordN m -> WordN w Source #

(KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') => BVConcat (Sym (WordN n)) (Sym (WordN w)) (Sym (WordN w')) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvconcat :: Sym (WordN n) -> Sym (WordN w) -> Sym (WordN w') Source #

type Rep (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.BV

type Rep (WordN n) = D1 ('MetaData "WordN" "Grisette.IR.SymPrim.Data.BV" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'True) (C1 ('MetaCons "WordN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unWordN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))
type PrimConstraint (WordN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

type PrimConstraint (WordN w) = (KnownNat w, 1 <= w)

data a =-> b infixr 0 Source #

Functions as a table. Use the # operator to apply the function.

>>> :set -XTypeOperators
>>> let f = TabularFun [(1, 2), (3, 4)] 0 :: Int =-> Int
>>> f # 1
2
>>> f # 2
0
>>> f # 3
4

Constructors

TabularFun 

Fields

Instances

Instances details
(Lift a, Lift b) => Lift (a =-> b :: Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

Methods

lift :: Quote m => (a =-> b) -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => (a =-> b) -> Code m (a =-> b) #

NFData a => NFData1 ((=->) a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

Methods

liftRnf :: (a0 -> ()) -> (a =-> a0) -> () #

Generic1 ((=->) a :: Type -> Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

Associated Types

type Rep1 ((=->) a) :: k -> Type #

Methods

from1 :: forall (a0 :: k). (a =-> a0) -> Rep1 ((=->) a) a0 #

to1 :: forall (a0 :: k). Rep1 ((=->) a) a0 -> a =-> a0 #

Generic (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

Associated Types

type Rep (a =-> b) :: Type -> Type #

Methods

from :: (a =-> b) -> Rep (a =-> b) x #

to :: Rep (a =-> b) x -> a =-> b #

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

Defined in Grisette.IR.SymPrim.Data.TabularFun

Methods

showsPrec :: Int -> (a =-> b) -> ShowS #

show :: (a =-> b) -> String #

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

(NFData a, NFData b) => NFData (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

Methods

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

(Eq a, Eq b) => Eq (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

Methods

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

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

(SupportedPrim a, SupportedPrim b) => Function (a =~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type Arg (a =~> b) Source #

type Ret (a =~> b) Source #

Methods

(#) :: (a =~> b) -> Arg (a =~> b) -> Ret (a =~> b) Source #

Eq a => Function (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

Associated Types

type Arg (a =-> b) Source #

type Ret (a =-> b) Source #

Methods

(#) :: (a =-> b) -> Arg (a =-> b) -> Ret (a =-> b) Source #

(SupportedPrim a, SupportedPrim b) => SupportedPrim (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

Associated Types

type PrimConstraint (a =-> b) Source #

Methods

withPrim :: proxy (a =-> b) -> (PrimConstraint (a =-> b) => a0) -> a0 Source #

termCache :: Cache (Term (a =-> b)) Source #

pformatCon :: (a =-> b) -> String Source #

pformatSym :: TypedSymbol (a =-> b) -> String Source #

defaultValue :: a =-> b Source #

defaultValueDynamic :: proxy (a =-> b) -> ModelValue Source #

(Hashable a, Hashable b) => Hashable (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

Methods

hashWithSalt :: Int -> (a =-> b) -> Int #

hash :: (a =-> b) -> Int #

type Rep1 ((=->) a :: Type -> Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

type Rep1 ((=->) a :: Type -> Type) = D1 ('MetaData "=->" "Grisette.IR.SymPrim.Data.TabularFun" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'False) (C1 ('MetaCons "TabularFun" 'PrefixI 'True) (S1 ('MetaSel ('Just "funcTable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) ([] :.: Rec1 ((,) a)) :*: S1 ('MetaSel ('Just "defaultFuncValue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1))
type Rep (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

type Rep (a =-> b) = D1 ('MetaData "=->" "Grisette.IR.SymPrim.Data.TabularFun" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'False) (C1 ('MetaCons "TabularFun" 'PrefixI 'True) (S1 ('MetaSel ('Just "funcTable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(a, b)]) :*: S1 ('MetaSel ('Just "defaultFuncValue") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)))
type Arg (a =~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Arg (a =~> b) = Sym a
type Arg (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

type Arg (a =-> b) = a
type Ret (a =~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Ret (a =~> b) = Sym b
type Ret (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

type Ret (a =-> b) = b
type PrimConstraint (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

data a --> b infixr 0 Source #

General symbolic function type. Use the # operator to apply the function. Note that this function should be applied to symbolic values only. It is by itself already a symbolic value, but can be considered partially concrete as the function body is specified. Use -~> for uninterpreted general symbolic functions.

The result would be partially evaluated.

>>> :set -XOverloadedStrings
>>> :set -XTypeOperators
>>> let f = ("x" :: TypedSymbol Integer) --> ("x" + 1 + "y" :: SymInteger) :: Integer --> Integer
>>> f # 1    -- 1 has the type SymInteger
(+ 2 y)
>>> f # "a"  -- "a" has the type SymInteger
(+ 1 (+ a y))

Instances

Instances details
Lift (a --> b :: Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

lift :: Quote m => (a --> b) -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => (a --> b) -> Code m (a --> b) #

Show (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

showsPrec :: Int -> (a --> b) -> ShowS #

show :: (a --> b) -> String #

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

NFData (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

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

Eq (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

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

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

(SupportedPrim a, SupportedPrim b) => Function (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type Arg (a --> b) Source #

type Ret (a --> b) Source #

Methods

(#) :: (a --> b) -> Arg (a --> b) -> Ret (a --> b) Source #

(SupportedPrim a, SupportedPrim b) => Function (a -~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type Arg (a -~> b) Source #

type Ret (a -~> b) Source #

Methods

(#) :: (a -~> b) -> Arg (a -~> b) -> Ret (a -~> b) Source #

(SupportedPrim a, SupportedPrim b) => SupportedPrim (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (a --> b) Source #

Methods

withPrim :: proxy (a --> b) -> (PrimConstraint (a --> b) => a0) -> a0 Source #

termCache :: Cache (Term (a --> b)) Source #

pformatCon :: (a --> b) -> String Source #

pformatSym :: TypedSymbol (a --> b) -> String Source #

defaultValue :: a --> b Source #

defaultValueDynamic :: proxy (a --> b) -> ModelValue Source #

Hashable (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

hashWithSalt :: Int -> (a --> b) -> Int #

hash :: (a --> b) -> Int #

type Arg (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Arg (a --> b) = Sym a
type Arg (a -~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Arg (a -~> b) = Sym a
type Ret (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Ret (a --> b) = Sym b
type Ret (a -~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Ret (a -~> b) = Sym b
type PrimConstraint (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

(-->) :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Sym b -> a --> b Source #

Construction of general symbolic functions.

Symbolic types

class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t Source #

Indicates that a type is supported and can be represented as a symbolic term.

Minimal complete definition

defaultValue

Instances

Instances details
SupportedPrim Integer Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint Integer Source #

SupportedPrim Bool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint Bool Source #

(KnownNat w, 1 <= w) => SupportedPrim (IntN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (IntN w) Source #

(KnownNat w, 1 <= w) => SupportedPrim (WordN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (WordN w) Source #

(SupportedPrim a, SupportedPrim b) => SupportedPrim (a --> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (a --> b) Source #

Methods

withPrim :: proxy (a --> b) -> (PrimConstraint (a --> b) => a0) -> a0 Source #

termCache :: Cache (Term (a --> b)) Source #

pformatCon :: (a --> b) -> String Source #

pformatSym :: TypedSymbol (a --> b) -> String Source #

defaultValue :: a --> b Source #

defaultValueDynamic :: proxy (a --> b) -> ModelValue Source #

(SupportedPrim a, SupportedPrim b) => SupportedPrim (a =-> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.TabularFun

Associated Types

type PrimConstraint (a =-> b) Source #

Methods

withPrim :: proxy (a =-> b) -> (PrimConstraint (a =-> b) => a0) -> a0 Source #

termCache :: Cache (Term (a =-> b)) Source #

pformatCon :: (a =-> b) -> String Source #

pformatSym :: TypedSymbol (a =-> b) -> String Source #

defaultValue :: a =-> b Source #

defaultValueDynamic :: proxy (a =-> b) -> ModelValue Source #

data Sym a Source #

Symbolic primitive type.

Symbolic Boolean, integer, and bit vector types are supported.

>>> :set -XOverloadedStrings
>>> "a" :: Sym Bool
a
>>> "a" &&~ "b" :: Sym Bool
(&& a b)
>>> "i" + 1 :: Sym Integer
(+ 1 i)

For more symbolic operations, please refer to the documentation of the grisette-core package.

Grisette also supports uninterpreted functions. You can use the --> (general function) or =-> (tabular function) types to define uninterpreted functions. The following code shows the examples

>>> :set -XTypeOperators
>>> let ftab = "ftab" :: Sym (Integer =-> Integer)
>>> ftab # "x"
(apply ftab x)
>>> solve (UnboundedReasoning z3) (ftab # 1 ==~ 2 &&~ ftab # 2 ==~ 3 &&~ ftab # 3 ==~ 4)
Right (Model {
  ftab ->
    TabularFun {funcTable = [(3,4),(2,3)], defaultFuncValue = 2}
      :: (=->) Integer Integer
}) -- possible result (reformatted)
>>> let fgen = "fgen" :: Sym (Integer --> Integer)
>>> fgen # "x"
(apply fgen x)
>>> solve (UnboundedReasoning z3) (fgen # 1 ==~ 2 &&~ fgen # 2 ==~ 3 &&~ fgen # 3 ==~ 4)
Right (Model {
  fgen ->
    \(arg@0:FuncArg :: Integer) ->
      (ite (= arg@0:FuncArg 2) 3 (ite (= arg@0:FuncArg 3) 4 2))
        :: (-->) Integer Integer
}) -- possible result (reformatted)

Instances

Instances details
SupportedPrim a => GenSym () (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (UnionM (Sym a)) Source #

SupportedPrim a => GenSymSimple () (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (Sym a) Source #

SupportedPrim a => Solvable a (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: a -> Sym a Source #

conView :: Sym a -> Maybe a Source #

ssym :: String -> Sym a Source #

isym :: String -> Int -> Sym a Source #

sinfosym :: (Typeable a0, Ord a0, Lift a0, NFData a0, Show a0, Hashable a0) => String -> a0 -> Sym a Source #

iinfosym :: (Typeable a0, Ord a0, Lift a0, NFData a0, Show a0, Hashable a0) => String -> Int -> a0 -> Sym a Source #

ToSym Int16 (Sym (IntN 16)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int16 -> Sym (IntN 16) Source #

ToSym Int32 (Sym (IntN 32)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int32 -> Sym (IntN 32) Source #

ToSym Int64 (Sym (IntN 64)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int64 -> Sym (IntN 64) Source #

ToSym Int8 (Sym (IntN 8)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int8 -> Sym (IntN 8) Source #

ToSym Word16 (Sym (WordN 16)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word16 -> Sym (WordN 16) Source #

ToSym Word32 (Sym (WordN 32)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word32 -> Sym (WordN 32) Source #

ToSym Word64 (Sym (WordN 64)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word64 -> Sym (WordN 64) Source #

ToSym Word8 (Sym (WordN 8)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word8 -> Sym (WordN 8) Source #

ToSym Int (Sym (IntN 64)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int -> Sym (IntN 64) Source #

ToSym Word (Sym (WordN 64)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word -> Sym (WordN 64) Source #

SupportedPrim a => ToSym a (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: a -> Sym a Source #

Lift (Sym a :: Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

lift :: Quote m => Sym a -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => Sym a -> Code m (Sym a) #

SupportedPrim (IntN n) => Bits (Sym (IntN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(.&.) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

(.|.) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

xor :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

complement :: Sym (IntN n) -> Sym (IntN n) #

shift :: Sym (IntN n) -> Int -> Sym (IntN n) #

rotate :: Sym (IntN n) -> Int -> Sym (IntN n) #

zeroBits :: Sym (IntN n) #

bit :: Int -> Sym (IntN n) #

setBit :: Sym (IntN n) -> Int -> Sym (IntN n) #

clearBit :: Sym (IntN n) -> Int -> Sym (IntN n) #

complementBit :: Sym (IntN n) -> Int -> Sym (IntN n) #

testBit :: Sym (IntN n) -> Int -> Bool #

bitSizeMaybe :: Sym (IntN n) -> Maybe Int #

bitSize :: Sym (IntN n) -> Int #

isSigned :: Sym (IntN n) -> Bool #

shiftL :: Sym (IntN n) -> Int -> Sym (IntN n) #

unsafeShiftL :: Sym (IntN n) -> Int -> Sym (IntN n) #

shiftR :: Sym (IntN n) -> Int -> Sym (IntN n) #

unsafeShiftR :: Sym (IntN n) -> Int -> Sym (IntN n) #

rotateL :: Sym (IntN n) -> Int -> Sym (IntN n) #

rotateR :: Sym (IntN n) -> Int -> Sym (IntN n) #

popCount :: Sym (IntN n) -> Int #

SupportedPrim (WordN n) => Bits (Sym (WordN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(.&.) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

(.|.) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

xor :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

complement :: Sym (WordN n) -> Sym (WordN n) #

shift :: Sym (WordN n) -> Int -> Sym (WordN n) #

rotate :: Sym (WordN n) -> Int -> Sym (WordN n) #

zeroBits :: Sym (WordN n) #

bit :: Int -> Sym (WordN n) #

setBit :: Sym (WordN n) -> Int -> Sym (WordN n) #

clearBit :: Sym (WordN n) -> Int -> Sym (WordN n) #

complementBit :: Sym (WordN n) -> Int -> Sym (WordN n) #

testBit :: Sym (WordN n) -> Int -> Bool #

bitSizeMaybe :: Sym (WordN n) -> Maybe Int #

bitSize :: Sym (WordN n) -> Int #

isSigned :: Sym (WordN n) -> Bool #

shiftL :: Sym (WordN n) -> Int -> Sym (WordN n) #

unsafeShiftL :: Sym (WordN n) -> Int -> Sym (WordN n) #

shiftR :: Sym (WordN n) -> Int -> Sym (WordN n) #

unsafeShiftR :: Sym (WordN n) -> Int -> Sym (WordN n) #

rotateL :: Sym (WordN n) -> Int -> Sym (WordN n) #

rotateR :: Sym (WordN n) -> Int -> Sym (WordN n) #

popCount :: Sym (WordN n) -> Int #

SupportedPrim t => IsString (Sym t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

fromString :: String -> Sym t #

Generic (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

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

Methods

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

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

SupportedPrim (IntN n) => Num (Sym (IntN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(+) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

(-) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

(*) :: Sym (IntN n) -> Sym (IntN n) -> Sym (IntN n) #

negate :: Sym (IntN n) -> Sym (IntN n) #

abs :: Sym (IntN n) -> Sym (IntN n) #

signum :: Sym (IntN n) -> Sym (IntN n) #

fromInteger :: Integer -> Sym (IntN n) #

SupportedPrim (WordN n) => Num (Sym (WordN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(+) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

(-) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

(*) :: Sym (WordN n) -> Sym (WordN n) -> Sym (WordN n) #

negate :: Sym (WordN n) -> Sym (WordN n) #

abs :: Sym (WordN n) -> Sym (WordN n) #

signum :: Sym (WordN n) -> Sym (WordN n) #

fromInteger :: Integer -> Sym (WordN n) #

Num (Sym Integer) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SupportedPrim a => Show (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

show :: Sym a -> String #

showList :: [Sym a] -> ShowS #

NFData (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

rnf :: Sym a -> () #

SupportedPrim a => Eq (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

SupportedPrim a => ITEOp (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

Methods

ites :: SymBool -> Sym a -> Sym a -> Sym a Source #

LogicalOp (Sym Bool) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

SupportedPrim (IntN n) => SEq (Sym (IntN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(==~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

(/=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

SupportedPrim (WordN n) => SEq (Sym (WordN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(==~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

(/=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

SupportedPrim Integer => SEq (Sym Integer) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SupportedPrim Bool => SEq (Sym Bool) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymBoolOp (Sym Bool) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SupportedPrim a => EvaluateSym (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

evaluateSym :: Bool -> Model -> Sym a -> Sym a Source #

SupportedPrim a => ExtractSymbolics (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SignedDivMod (Sym Integer) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymIntegerOp (Sym Integer) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SupportedPrim a => Mergeable (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

SupportedPrim (IntN n) => SOrd (Sym (IntN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

(<=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

(>~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

(>=~) :: Sym (IntN n) -> Sym (IntN n) -> SymBool Source #

symCompare :: Sym (IntN n) -> Sym (IntN n) -> UnionM Ordering Source #

SupportedPrim (WordN n) => SOrd (Sym (WordN n)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

(<=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

(>~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

(>=~) :: Sym (WordN n) -> Sym (WordN n) -> SymBool Source #

symCompare :: Sym (WordN n) -> Sym (WordN n) -> UnionM Ordering Source #

SupportedPrim Integer => SOrd (Sym Integer) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SOrd (Sym Bool) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SupportedPrim a => SimpleMergeable (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> Sym a -> Sym a -> Sym a Source #

SubstituteSym (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Sym a -> Sym a Source #

SupportedPrim a => Hashable (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

hashWithSalt :: Int -> Sym a -> Int #

hash :: Sym a -> Int #

ToCon (Sym (IntN 8)) Int8 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 8) -> Maybe Int8 Source #

ToCon (Sym (IntN 16)) Int16 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 16) -> Maybe Int16 Source #

ToCon (Sym (IntN 32)) Int32 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 32) -> Maybe Int32 Source #

ToCon (Sym (IntN 64)) Int64 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 64) -> Maybe Int64 Source #

ToCon (Sym (IntN 64)) Int Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 64) -> Maybe Int Source #

ToCon (Sym (WordN 8)) Word8 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 8) -> Maybe Word8 Source #

ToCon (Sym (WordN 16)) Word16 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 16) -> Maybe Word16 Source #

ToCon (Sym (WordN 32)) Word32 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 32) -> Maybe Word32 Source #

ToCon (Sym (WordN 64)) Word64 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 64) -> Maybe Word64 Source #

ToCon (Sym (WordN 64)) Word Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 64) -> Maybe Word Source #

SupportedPrim a => ToCon (Sym a) a Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym a -> Maybe a Source #

(KnownNat ix, KnownNat w, KnownNat ow, (ix + w) <= ow, 1 <= ow, 1 <= w) => BVSelect (Sym (IntN ow)) ix w (Sym (IntN w)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvselect :: proxy ix -> proxy w -> Sym (IntN ow) -> Sym (IntN w) Source #

(KnownNat ix, KnownNat w, KnownNat ow, (ix + w) <= ow, 1 <= ow, 1 <= w) => BVSelect (Sym (WordN ow)) ix w (Sym (WordN w)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvselect :: proxy ix -> proxy w -> Sym (WordN ow) -> Sym (WordN w) Source #

(KnownNat w, KnownNat w', 1 <= w, 1 <= w', w <= w', (w + 1) <= w', 1 <= (w' - w), KnownNat (w' - w)) => BVExtend (Sym (IntN w)) w' (Sym (IntN w')) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvzeroExtend :: proxy w' -> Sym (IntN w) -> Sym (IntN w') Source #

bvsignExtend :: proxy w' -> Sym (IntN w) -> Sym (IntN w') Source #

bvextend :: proxy w' -> Sym (IntN w) -> Sym (IntN w') Source #

(KnownNat w, KnownNat w', 1 <= w, 1 <= w', (w + 1) <= w', w <= w', 1 <= (w' - w), KnownNat (w' - w)) => BVExtend (Sym (WordN w)) w' (Sym (WordN w')) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvzeroExtend :: proxy w' -> Sym (WordN w) -> Sym (WordN w') Source #

bvsignExtend :: proxy w' -> Sym (WordN w) -> Sym (WordN w') Source #

bvextend :: proxy w' -> Sym (WordN w) -> Sym (WordN w') Source #

SupportedPrim a => GenSym (Sym a) (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => Sym a -> m (UnionM (Sym a)) Source #

SupportedPrim a => GenSymSimple (Sym a) (Sym a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => Sym a -> m (Sym a) Source #

SupportedPrim a => ToCon (Sym a) (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym a -> Maybe (Sym a) Source #

SupportedPrim a => ToSym (Sym a) (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Sym a -> Sym a Source #

(KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') => BVConcat (Sym (IntN n)) (Sym (IntN w)) (Sym (IntN w')) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvconcat :: Sym (IntN n) -> Sym (IntN w) -> Sym (IntN w') Source #

(KnownNat w', KnownNat n, KnownNat w, w' ~ (n + w), 1 <= n, 1 <= w, 1 <= w') => BVConcat (Sym (WordN n)) (Sym (WordN w)) (Sym (WordN w')) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

bvconcat :: Sym (WordN n) -> Sym (WordN w) -> Sym (WordN w') Source #

(SupportedPrim a, SupportedPrim b) => Function (a -~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type Arg (a -~> b) Source #

type Ret (a -~> b) Source #

Methods

(#) :: (a -~> b) -> Arg (a -~> b) -> Ret (a -~> b) Source #

(SupportedPrim a, SupportedPrim b) => Function (a =~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type Arg (a =~> b) Source #

type Ret (a =~> b) Source #

Methods

(#) :: (a =~> b) -> Arg (a =~> b) -> Ret (a =~> b) Source #

type Rep (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Rep (Sym a) = D1 ('MetaData "Sym" "Grisette.IR.SymPrim.Data.SymPrim" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'True) (C1 ('MetaCons "Sym" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term a))))
type Arg (a -~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Arg (a -~> b) = Sym a
type Arg (a =~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Arg (a =~> b) = Sym a
type Ret (a -~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Ret (a -~> b) = Sym b
type Ret (a =~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Ret (a =~> b) = Sym b

data TypedSymbol t where Source #

A typed symbol is a symbol that is associated with a type. Note that the same symbol bodies with different types are considered different symbols and can coexist in a term.

Simple symbols can be created with the OverloadedStrings extension:

>>> :set -XOverloadedStrings
>>> "a" :: TypedSymbol Bool
a :: Bool

Constructors

SimpleSymbol :: SupportedPrim t => String -> TypedSymbol t 
IndexedSymbol :: SupportedPrim t => String -> Int -> TypedSymbol t 
WithInfo :: forall t a. (SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => TypedSymbol t -> a -> TypedSymbol t 

Instances

Instances details
SymbolSetOps SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelOps Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Lift (TypedSymbol t :: Type) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

lift :: Quote m => TypedSymbol t -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => TypedSymbol t -> Code m (TypedSymbol t) #

SupportedPrim t => IsString (TypedSymbol t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Show (TypedSymbol t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

NFData (TypedSymbol t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

rnf :: TypedSymbol t -> () #

Eq (TypedSymbol t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Ord (TypedSymbol t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Hashable (TypedSymbol t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Methods

hashWithSalt :: Int -> TypedSymbol t -> Int #

hash :: TypedSymbol t -> Int #

SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair t) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

symSize :: Sym a -> Int Source #

Get the size of a symbolic term. Duplicate sub-terms are counted for only once.

symsSize :: [Sym a] -> Int Source #

Get the sum of the sizes of a list of symbolic terms. Duplicate sub-terms are counted for only once.

Symbolic type synonyms

type SymBool = Sym Bool Source #

Symbolic Boolean type.

type SymInteger = Sym Integer Source #

Symbolic integer type (unbounded, mathematical integer).

type SymIntN n = Sym (IntN n) Source #

Symbolic signed bit vector type.

type SymWordN n = Sym (WordN n) Source #

Symbolic unsigned bit vector type.

type (=~>) a b = Sym (a =-> b) infixr 0 Source #

Symbolic tabular function type.

type (-~>) a b = Sym (a --> b) infixr 0 Source #

Symbolic general function type.

Symbolic constant sets and models

newtype SymbolSet Source #

Symbolic constant set.

Instances

Instances details
Monoid SymbolSet Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Semigroup SymbolSet Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Generic SymbolSet Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Associated Types

type Rep SymbolSet :: Type -> Type #

Show SymbolSet Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Eq SymbolSet Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ExtractSymbolics SymbolSet Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Hashable SymbolSet Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

SymbolSetOps SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelOps Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair t) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Rep SymbolSet Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

type Rep SymbolSet = D1 ('MetaData "SymbolSet" "Grisette.IR.SymPrim.Data.Prim.Model" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'True) (C1 ('MetaCons "SymbolSet" 'PrefixI 'True) (S1 ('MetaSel ('Just "unSymbolSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet SomeTypedSymbol))))

newtype Model Source #

Model returned by the solver.

Instances

Instances details
Generic Model Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Associated Types

type Rep Model :: Type -> Type #

Methods

from :: Model -> Rep Model x #

to :: Rep Model x -> Model #

Show Model Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

showsPrec :: Int -> Model -> ShowS #

show :: Model -> String #

showList :: [Model] -> ShowS #

Eq Model Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

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

Hashable Model Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

hashWithSalt :: Int -> Model -> Int #

hash :: Model -> Int #

ModelOps Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair t) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Rep Model Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

type Rep Model = D1 ('MetaData "Model" "Grisette.IR.SymPrim.Data.Prim.Model" "grisette-0.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" 'True) (C1 ('MetaCons "Model" 'PrefixI 'True) (S1 ('MetaSel ('Just "unModel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SomeTypedSymbol ModelValue))))

data ModelValuePair t Source #

A type used for building a model by hand.

>>> buildModel ("x" ::= (1 :: Integer), "y" ::= True) :: Model
Model {x -> 1 :: Integer, y -> True :: Bool}

Constructors

(TypedSymbol t) ::= t 

Instances

Instances details
Show t => Show (ModelValuePair t) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair t) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.Model