Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Safe-Inferred
Language	Haskell2010

Grisette.IR.SymPrim.Data.SymPrim

Contents

Orphan instances

Description

Synopsis

newtype Sym a = Sym {
- underlyingTerm :: Term a
}
type SymBool = Sym Bool
type SymInteger = Sym Integer
(-->) :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Sym b -> a --> b
type (=~>) a b = Sym (a =-> b)
type (-~>) a b = Sym (a --> b)
type SymWordN n = Sym (WordN n)
type SymIntN n = Sym (IntN n)
symSize :: Sym a -> Int
symsSize :: [Sym a] -> Int
data ModelSymPair t = (Sym t) := t

Documentation

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

Constructors

Sym
Fields underlyingTerm :: Term a

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 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) 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 Methods (\|\|~) :: Sym Bool -> Sym Bool -> Sym Bool Source # (&&~) :: Sym Bool -> Sym Bool -> Sym Bool Source # nots :: Sym Bool -> Sym Bool Source # xors :: Sym Bool -> Sym Bool -> Sym Bool Source # implies :: Sym Bool -> Sym Bool -> Sym Bool Source #
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 Methods (==~) :: Sym Integer -> Sym Integer -> SymBool Source # (/=~) :: Sym Integer -> Sym Integer -> SymBool Source #
SupportedPrim Bool => SEq (Sym Bool) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods (==~) :: Sym Bool -> Sym Bool -> SymBool Source # (/=~) :: Sym Bool -> Sym Bool -> SymBool Source #
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 Methods extractSymbolics :: Sym a -> SymbolSet Source #
SignedDivMod (Sym Integer) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods divs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => Sym Integer -> Sym Integer -> uf (Sym Integer) Source # mods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => Sym Integer -> Sym Integer -> uf (Sym Integer) Source #
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 Methods rootStrategy :: MergingStrategy (Sym a) 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 #
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 Methods (<~) :: Sym Integer -> Sym Integer -> SymBool Source # (<=~) :: Sym Integer -> Sym Integer -> SymBool Source # (>~) :: Sym Integer -> Sym Integer -> SymBool Source # (>=~) :: Sym Integer -> Sym Integer -> SymBool Source # symCompare :: Sym Integer -> Sym Integer -> UnionM Ordering Source #
SOrd (Sym Bool) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods (<~) :: Sym Bool -> Sym Bool -> SymBool Source # (<=~) :: Sym Bool -> Sym Bool -> SymBool Source # (>~) :: Sym Bool -> Sym Bool -> SymBool Source # (>=~) :: Sym Bool -> Sym Bool -> SymBool Source # symCompare :: Sym Bool -> Sym Bool -> UnionM Ordering Source #
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

type SymBool = Sym Bool Source #

Symbolic Boolean type.

type SymInteger = Sym Integer Source #

Symbolic integer type (unbounded, mathematical integer).

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

Construction of general symbolic functions.

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.

type SymWordN n = Sym (WordN n) Source #

Symbolic unsigned bit vector type.

type SymIntN n = Sym (IntN n) Source #

Symbolic signed bit vector type.

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.

data ModelSymPair t Source #

Constructors

(Sym t) := t

Instances

Instances details

SupportedPrim t => Show (ModelSymPair t) Source #
Instance details 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 Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: ModelSymPair t -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) -> Model Source #
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 Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) -> Model Source #
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 Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g) -> Model Source #
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 Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h) -> Model Source #

Orphan instances

(SupportedPrim a, SupportedPrim b) => Function (a --> b) Source #
Instance details Associated Types type Arg (a --> b) Source # type Ret (a --> b) Source # Methods (#) :: (a --> b) -> Arg (a --> b) -> Ret (a --> b) Source #