Grisette.IR.SymPrim.Data.SymPrim

Documentation

newtype Sym a

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)

Constructors

Sym

Fields

• underlyingTerm :: Term a

Instances

SupportedPrim a => GenSym () (Sym a)

Defined in Grisette.Core.Data.Class.GenSym

Methods

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

SupportedPrim a => GenSymSimple () (Sym a)

Defined in Grisette.Core.Data.Class.GenSym

Methods

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

SupportedPrim a => Solvable a (Sym a)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: a -> Sym a

conView :: Sym a -> Maybe a

ssym :: String -> Sym a

isym :: String -> Int -> Sym a

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

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

ToSym Int16 (Sym (IntN 16))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int16 -> Sym (IntN 16)

ToSym Int32 (Sym (IntN 32))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int32 -> Sym (IntN 32)

ToSym Int64 (Sym (IntN 64))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int64 -> Sym (IntN 64)

ToSym Int8 (Sym (IntN 8))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int8 -> Sym (IntN 8)

ToSym Word16 (Sym (WordN 16))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word16 -> Sym (WordN 16)

ToSym Word32 (Sym (WordN 32))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word32 -> Sym (WordN 32)

ToSym Word64 (Sym (WordN 64))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word64 -> Sym (WordN 64)

ToSym Word8 (Sym (WordN 8))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word8 -> Sym (WordN 8)

ToSym Int (Sym (IntN 64))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int -> Sym (IntN 64)

ToSym Word (Sym (WordN 64))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word -> Sym (WordN 64)

SupportedPrim a => ToSym a (Sym a)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: a -> Sym a

Lift (Sym a :: Type)

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

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

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)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

fromString :: String -> Sym t

Generic (Sym a)

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

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

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)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(+) :: Sym Integer -> Sym Integer -> Sym Integer

(-) :: Sym Integer -> Sym Integer -> Sym Integer

(*) :: Sym Integer -> Sym Integer -> Sym Integer

negate :: Sym Integer -> Sym Integer

abs :: Sym Integer -> Sym Integer

signum :: Sym Integer -> Sym Integer

fromInteger :: Integer -> Sym Integer

SupportedPrim a => Show (Sym a)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

showsPrec :: Int -> Sym a -> ShowS

show :: Sym a -> String

showList :: [Sym a] -> ShowS

NFData (Sym a)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

rnf :: Sym a -> ()

SupportedPrim a => Eq (Sym a)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

SupportedPrim a => ITEOp (Sym a)

Defined in Grisette.Core.Data.Class.Bool

Methods

ites :: SymBool -> Sym a -> Sym a -> Sym a

LogicalOp (Sym Bool)

Defined in Grisette.Core.Data.Class.Bool

Methods

(||~) :: Sym Bool -> Sym Bool -> Sym Bool

(&&~) :: Sym Bool -> Sym Bool -> Sym Bool

nots :: Sym Bool -> Sym Bool

xors :: Sym Bool -> Sym Bool -> Sym Bool

implies :: Sym Bool -> Sym Bool -> Sym Bool

SupportedPrim (IntN n) => SEq (Sym (IntN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

SupportedPrim (WordN n) => SEq (Sym (WordN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

SupportedPrim Integer => SEq (Sym Integer)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(==~) :: Sym Integer -> Sym Integer -> SymBool

(/=~) :: Sym Integer -> Sym Integer -> SymBool

SupportedPrim Bool => SEq (Sym Bool)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(==~) :: Sym Bool -> Sym Bool -> SymBool

(/=~) :: Sym Bool -> Sym Bool -> SymBool

SymBoolOp (Sym Bool)

Defined in Grisette.IR.SymPrim.Data.SymPrim

SupportedPrim a => EvaluateSym (Sym a)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

SupportedPrim a => ExtractSymbolics (Sym a)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

extractSymbolics :: Sym a -> SymbolSet

SignedDivMod (Sym Integer)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

divs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => Sym Integer -> Sym Integer -> uf (Sym Integer)

mods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => Sym Integer -> Sym Integer -> uf (Sym Integer)

SymIntegerOp (Sym Integer)

Defined in Grisette.IR.SymPrim.Data.SymPrim

SupportedPrim a => Mergeable (Sym a)

Defined in Grisette.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (Sym a)

SupportedPrim (IntN n) => SOrd (Sym (IntN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

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

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

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

SupportedPrim (WordN n) => SOrd (Sym (WordN n))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

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

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

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

SupportedPrim Integer => SOrd (Sym Integer)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym Integer -> Sym Integer -> SymBool

(<=~) :: Sym Integer -> Sym Integer -> SymBool

(>~) :: Sym Integer -> Sym Integer -> SymBool

(>=~) :: Sym Integer -> Sym Integer -> SymBool

symCompare :: Sym Integer -> Sym Integer -> UnionM Ordering

SOrd (Sym Bool)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

(<~) :: Sym Bool -> Sym Bool -> SymBool

(<=~) :: Sym Bool -> Sym Bool -> SymBool

(>~) :: Sym Bool -> Sym Bool -> SymBool

(>=~) :: Sym Bool -> Sym Bool -> SymBool

symCompare :: Sym Bool -> Sym Bool -> UnionM Ordering

SupportedPrim a => SimpleMergeable (Sym a)

Defined in Grisette.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> Sym a -> Sym a -> Sym a

SubstituteSym (Sym a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SupportedPrim a => Hashable (Sym a)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

hashWithSalt :: Int -> Sym a -> Int

hash :: Sym a -> Int

ToCon (Sym (IntN 8)) Int8

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

ToCon (Sym (IntN 16)) Int16

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

ToCon (Sym (IntN 32)) Int32

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

ToCon (Sym (IntN 64)) Int64

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

ToCon (Sym (IntN 64)) Int

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

ToCon (Sym (WordN 8)) Word8

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

ToCon (Sym (WordN 16)) Word16

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

ToCon (Sym (WordN 32)) Word32

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

ToCon (Sym (WordN 64)) Word64

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

ToCon (Sym (WordN 64)) Word

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

SupportedPrim a => ToCon (Sym a) a

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym a -> Maybe a

(KnownNat ix, KnownNat w, KnownNat ow, (ix + w) <= ow, 1 <= ow, 1 <= w) => BVSelect (Sym (IntN ow)) ix w (Sym (IntN w))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

(KnownNat ix, KnownNat w, KnownNat ow, (ix + w) <= ow, 1 <= ow, 1 <= w) => BVSelect (Sym (WordN ow)) ix w (Sym (WordN w))

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

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

SupportedPrim a => GenSym (Sym a) (Sym a)

Defined in Grisette.Core.Data.Class.GenSym

Methods

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

SupportedPrim a => GenSymSimple (Sym a) (Sym a)

Defined in Grisette.Core.Data.Class.GenSym

Methods

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

SupportedPrim a => ToCon (Sym a) (Sym a)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

SupportedPrim a => ToSym (Sym a) (Sym a)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Sym a -> Sym a

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

(SupportedPrim a, SupportedPrim b) => Function (a -~> b)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type Arg (a -~> b)

type Ret (a -~> b)

Methods

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

(SupportedPrim a, SupportedPrim b) => Function (a =~> b)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type Arg (a =~> b)

type Ret (a =~> b)

Methods

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

type Rep (Sym a)

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)

Defined in Grisette.IR.SymPrim.Data.SymPrim

type Arg (a -~> b) = Sym a

type Arg (a =~> b)

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

type Ret (a -~> b)

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

type Ret (a =~> b)

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

type SymBool = Sym Bool

Symbolic Boolean type.

type SymInteger = Sym Integer

Symbolic integer type (unbounded, mathematical integer).

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

Construction of general symbolic functions.

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

Symbolic tabular function type.

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

Symbolic general function type.

type SymWordN n = Sym (WordN n)

Symbolic unsigned bit vector type.

type SymIntN n = Sym (IntN n)

Symbolic signed bit vector type.

symSize :: Sym a -> Int

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

symsSize :: [Sym a] -> Int

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

data ModelSymPair t

Constructors

(Sym t) := t

Instances

SupportedPrim t => Show (ModelSymPair t)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

showsPrec :: Int -> ModelSymPair t -> ShowS

show :: ModelSymPair t -> String

showList :: [ModelSymPair t] -> ShowS

ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: ModelSymPair t -> Model

ModelRep (ModelSymPair a, ModelSymPair b) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b) -> Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c) -> Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) -> Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) -> Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) -> Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g) -> Model

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h) -> Model

Orphan instances

(SupportedPrim a, SupportedPrim b) => Function (a --> b)

Associated Types

type Arg (a --> b)

type Ret (a --> b)

Methods

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