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

Documentation

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

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

Minimal complete definition

defaultValue

Associated Types

type PrimConstraint t :: Constraint

type PrimConstraint t = ()

Methods

withPrim :: proxy t -> (PrimConstraint t => a) -> a

default withPrim :: PrimConstraint t => proxy t -> (PrimConstraint t => a) -> a

termCache :: Cache (Term t)

pformatCon :: t -> String

default pformatCon :: Show t => t -> String

pformatSym :: TypedSymbol t -> String

defaultValue :: t

defaultValueDynamic :: proxy t -> ModelValue

Instances

SupportedPrim Integer

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

Associated Types

type PrimConstraint Integer

Methods

withPrim :: proxy Integer -> (PrimConstraint Integer => a) -> a

termCache :: Cache (Term Integer)

pformatCon :: Integer -> String

pformatSym :: TypedSymbol Integer -> String

defaultValue :: Integer

defaultValueDynamic :: proxy Integer -> ModelValue

SupportedPrim Bool

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

Associated Types

type PrimConstraint Bool

Methods

withPrim :: proxy Bool -> (PrimConstraint Bool => a) -> a

termCache :: Cache (Term Bool)

pformatCon :: Bool -> String

pformatSym :: TypedSymbol Bool -> String

defaultValue :: Bool

defaultValueDynamic :: proxy Bool -> ModelValue

(KnownNat w, 1 <= w) => SupportedPrim (IntN w)

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

Associated Types

type PrimConstraint (IntN w)

Methods

withPrim :: proxy (IntN w) -> (PrimConstraint (IntN w) => a) -> a

termCache :: Cache (Term (IntN w))

pformatCon :: IntN w -> String

pformatSym :: TypedSymbol (IntN w) -> String

defaultValue :: IntN w

defaultValueDynamic :: proxy (IntN w) -> ModelValue

(KnownNat w, 1 <= w) => SupportedPrim (WordN w)

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

Associated Types

type PrimConstraint (WordN w)

Methods

withPrim :: proxy (WordN w) -> (PrimConstraint (WordN w) => a) -> a

termCache :: Cache (Term (WordN w))

pformatCon :: WordN w -> String

pformatSym :: TypedSymbol (WordN w) -> String

defaultValue :: WordN w

defaultValueDynamic :: proxy (WordN w) -> ModelValue

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

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

Associated Types

type PrimConstraint (a --> b)

Methods

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

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

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

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

defaultValue :: a --> b

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

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

Defined in Grisette.IR.SymPrim.Data.TabularFun

Associated Types

type PrimConstraint (a =-> b)

Methods

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

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

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

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

defaultValue :: a =-> b

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

class SupportedPrim con => SymRep con

Type family to resolve the symbolic type associated with a concrete type.

Associated Types

type SymType con

Instances

SymRep Integer

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType Integer

SymRep Bool

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType Bool

(KnownNat n, 1 <= n) => SymRep (IntN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType (IntN n)

(KnownNat n, 1 <= n) => SymRep (WordN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType (WordN n)

(SymRep ca, SymRep cb) => SymRep (ca --> cb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType (ca --> cb)

(SymRep a, SymRep b) => SymRep (a =-> b)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType (a =-> b)

class ConRep sym

Type family to resolve the concrete type associated with a symbolic type.

Associated Types

type ConType sym

Instances

ConRep SymBool

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type ConType SymBool

ConRep SymInteger

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type ConType SymInteger

(KnownNat n, 1 <= n) => ConRep (SymIntN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type ConType (SymIntN n)

(KnownNat n, 1 <= n) => ConRep (SymWordN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type ConType (SymWordN n)

(ConRep a, ConRep b) => ConRep (a -~> b)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type ConType (a -~> b)

(ConRep a, ConRep b) => ConRep (a =~> b)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type ConType (a =~> b)

class (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) => LinkedRep con sym | con -> sym, sym -> con where

One-to-one mapping between symbolic types and concrete types.

Methods

underlyingTerm :: sym -> Term con

wrapTerm :: Term con -> sym

Instances

LinkedRep Integer SymInteger

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

underlyingTerm :: SymInteger -> Term Integer

wrapTerm :: Term Integer -> SymInteger

LinkedRep Bool SymBool

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

underlyingTerm :: SymBool -> Term Bool

wrapTerm :: Term Bool -> SymBool

(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

underlyingTerm :: SymIntN n -> Term (IntN n)

wrapTerm :: Term (IntN n) -> SymIntN n

(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

underlyingTerm :: SymWordN n -> Term (WordN n)

wrapTerm :: Term (WordN n) -> SymWordN n

(LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca --> cb) (sa -~> sb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

underlyingTerm :: (sa -~> sb) -> Term (ca --> cb)

wrapTerm :: Term (ca --> cb) -> sa -~> sb

(LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca =-> cb) (sa =~> sb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

underlyingTerm :: (sa =~> sb) -> Term (ca =-> cb)

wrapTerm :: Term (ca =-> cb) -> sa =~> sb

class (SupportedPrim arg, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => UnaryOp tag arg t | tag arg -> t where

Methods

partialEvalUnary :: (Typeable tag, Typeable t) => tag -> Term arg -> Term t

pformatUnary :: tag -> Term arg -> String

class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => BinaryOp tag arg1 arg2 t | tag arg1 arg2 -> t where

Methods

partialEvalBinary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term t

pformatBinary :: tag -> Term arg1 -> Term arg2 -> String

class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim arg3, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => TernaryOp tag arg1 arg2 arg3 t | tag arg1 arg2 arg3 -> t where

Methods

partialEvalTernary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t

pformatTernary :: tag -> Term arg1 -> Term arg2 -> Term arg3 -> String

data TypedSymbol t where

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

SymbolSetOps SymbolSet TypedSymbol

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

Methods

emptySet :: SymbolSet

isEmptySet :: SymbolSet -> Bool

containsSymbol :: TypedSymbol a -> SymbolSet -> Bool

insertSymbol :: TypedSymbol a -> SymbolSet -> SymbolSet

intersectionSet :: SymbolSet -> SymbolSet -> SymbolSet

unionSet :: SymbolSet -> SymbolSet -> SymbolSet

differenceSet :: SymbolSet -> SymbolSet -> SymbolSet

ModelOps Model SymbolSet TypedSymbol

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

Methods

emptyModel :: Model

isEmptyModel :: Model -> Bool

modelContains :: TypedSymbol a -> Model -> Bool

valueOf :: TypedSymbol t -> Model -> Maybe t

insertValue :: TypedSymbol t -> t -> Model -> Model

exceptFor :: SymbolSet -> Model -> Model

exceptFor' :: TypedSymbol t -> Model -> Model

restrictTo :: SymbolSet -> Model -> Model

extendTo :: SymbolSet -> Model -> Model

exact :: SymbolSet -> Model -> Model

Lift (TypedSymbol t :: Type)

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)

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

Methods

fromString :: String -> TypedSymbol t

Show (TypedSymbol t)

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

Methods

showsPrec :: Int -> TypedSymbol t -> ShowS

show :: TypedSymbol t -> String

showList :: [TypedSymbol t] -> ShowS

NFData (TypedSymbol t)

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

Methods

rnf :: TypedSymbol t -> ()

Eq (TypedSymbol t)

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

Methods

(==) :: TypedSymbol t -> TypedSymbol t -> Bool

(/=) :: TypedSymbol t -> TypedSymbol t -> Bool

Ord (TypedSymbol t)

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

Methods

compare :: TypedSymbol t -> TypedSymbol t -> Ordering

(<) :: TypedSymbol t -> TypedSymbol t -> Bool

(<=) :: TypedSymbol t -> TypedSymbol t -> Bool

(>) :: TypedSymbol t -> TypedSymbol t -> Bool

(>=) :: TypedSymbol t -> TypedSymbol t -> Bool

max :: TypedSymbol t -> TypedSymbol t -> TypedSymbol t

min :: TypedSymbol t -> TypedSymbol t -> TypedSymbol t

Hashable (TypedSymbol t)

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

Methods

hashWithSalt :: Int -> TypedSymbol t -> Int

hash :: TypedSymbol t -> Int

SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol

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

Methods

buildSymbolSet :: TypedSymbol t -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol

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

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c) SymbolSet TypedSymbol

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

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) SymbolSet TypedSymbol

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

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) SymbolSet TypedSymbol

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

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) SymbolSet TypedSymbol

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

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) SymbolSet TypedSymbol

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

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) SymbolSet TypedSymbol

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

Methods

buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) -> SymbolSet

data SomeTypedSymbol where

Constructors

SomeTypedSymbol :: forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol

Instances

Show SomeTypedSymbol

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

Methods

showsPrec :: Int -> SomeTypedSymbol -> ShowS

show :: SomeTypedSymbol -> String

showList :: [SomeTypedSymbol] -> ShowS

NFData SomeTypedSymbol

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

Methods

rnf :: SomeTypedSymbol -> ()

Eq SomeTypedSymbol

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

Methods

(==) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool

(/=) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool

Ord SomeTypedSymbol

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

Methods

compare :: SomeTypedSymbol -> SomeTypedSymbol -> Ordering

(<) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool

(<=) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool

(>) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool

(>=) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool

max :: SomeTypedSymbol -> SomeTypedSymbol -> SomeTypedSymbol

min :: SomeTypedSymbol -> SomeTypedSymbol -> SomeTypedSymbol

Hashable SomeTypedSymbol

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

Methods

hashWithSalt :: Int -> SomeTypedSymbol -> Int

hash :: SomeTypedSymbol -> Int

showUntyped :: TypedSymbol t -> String

withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a

someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol

data Term t where

Constructors

ConTerm :: SupportedPrim t => !Id -> !t -> Term t

SymTerm :: SupportedPrim t => !Id -> !(TypedSymbol t) -> Term t

UnaryTerm :: UnaryOp tag arg t => !Id -> !tag -> !(Term arg) -> Term t

BinaryTerm :: BinaryOp tag arg1 arg2 t => !Id -> !tag -> !(Term arg1) -> !(Term arg2) -> Term t

TernaryTerm :: TernaryOp tag arg1 arg2 arg3 t => !Id -> !tag -> !(Term arg1) -> !(Term arg2) -> !(Term arg3) -> Term t

NotTerm :: !Id -> !(Term Bool) -> Term Bool

OrTerm :: !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool

AndTerm :: !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool

EqvTerm :: SupportedPrim t => !Id -> !(Term t) -> !(Term t) -> Term Bool

ITETerm :: SupportedPrim t => !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t

AddNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> !(Term t) -> Term t

UMinusNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> Term t

TimesNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> !(Term t) -> Term t

AbsNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> Term t

SignumNumTerm :: (SupportedPrim t, Num t) => !Id -> !(Term t) -> Term t

LTNumTerm :: (SupportedPrim t, Num t, Ord t) => !Id -> !(Term t) -> !(Term t) -> Term Bool

LENumTerm :: (SupportedPrim t, Num t, Ord t) => !Id -> !(Term t) -> !(Term t) -> Term Bool

AndBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !(Term t) -> Term t

OrBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !(Term t) -> Term t

XorBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !(Term t) -> Term t

ComplementBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> Term t

ShiftBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !Int -> Term t

RotateBitsTerm :: (SupportedPrim t, Bits t) => !Id -> !(Term t) -> !Int -> Term t

BVConcatTerm :: (SupportedPrim (bv a), SupportedPrim (bv b), SupportedPrim (bv (a + b)), KnownNat a, KnownNat b, 1 <= a, 1 <= b, SizedBV bv) => !Id -> !(Term (bv a)) -> !(Term (bv b)) -> Term (bv (a + b))

BVSelectTerm :: (SupportedPrim (bv n), SupportedPrim (bv w), KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n, SizedBV bv) => !Id -> !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv n)) -> Term (bv w)

BVExtendTerm :: (SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l, KnownNat r, 1 <= l, l <= r, SizedBV bv) => !Id -> !Bool -> !(TypeRep r) -> !(Term (bv l)) -> Term (bv r)

TabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => !Id -> Term (a =-> b) -> Term a -> Term b

GeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => !Id -> Term (a --> b) -> Term a -> Term b

DivIntegralTerm :: (SupportedPrim t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t

ModIntegralTerm :: (SupportedPrim t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t

QuotIntegralTerm :: (SupportedPrim t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t

RemIntegralTerm :: (SupportedPrim t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t

DivBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t

ModBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t

QuotBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t

RemBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !Id -> !(Term t) -> !(Term t) -> Term t

Instances

Lift (Term t :: Type)

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

Methods

lift :: Quote m => Term t -> m Exp

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

Show (Term ty)

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

Methods

showsPrec :: Int -> Term ty -> ShowS

show :: Term ty -> String

showList :: [Term ty] -> ShowS

NFData (Term a)

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

Methods

rnf :: Term a -> ()

SupportedPrim t => Eq (Term t)

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

Methods

(==) :: Term t -> Term t -> Bool

(/=) :: Term t -> Term t -> Bool

SupportedPrim t => Eq (Description (Term t))

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

Methods

(==) :: Description (Term t) -> Description (Term t) -> Bool

(/=) :: Description (Term t) -> Description (Term t) -> Bool

SupportedPrim t => Hashable (Term t)

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

Methods

hashWithSalt :: Int -> Term t -> Int

hash :: Term t -> Int

SupportedPrim t => Hashable (Description (Term t))

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

Methods

hashWithSalt :: Int -> Description (Term t) -> Int

hash :: Description (Term t) -> Int

SupportedPrim t => Interned (Term t)

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

Associated Types

data Description (Term t)

type Uninterned (Term t)

Methods

describe :: Uninterned (Term t) -> Description (Term t)

identify :: Id -> Uninterned (Term t) -> Term t

seedIdentity :: p (Term t) -> Id

cacheWidth :: p (Term t) -> Int

modifyAdvice :: IO (Term t) -> IO (Term t)

cache :: Cache (Term t)

data Description (Term t)

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

data Description (Term t) where

• DConTerm :: forall t. t -> Description (Term t)
• DSymTerm :: forall t. TypedSymbol t -> Description (Term t)
• DUnaryTerm :: forall tag arg t. (Eq tag, Hashable tag) => !(TypeRep tag, tag) -> !(TypeRep arg, Id) -> Description (Term t)
• DBinaryTerm :: forall tag arg1 arg2 t. (Eq tag, Hashable tag) => !(TypeRep tag, tag) -> !(TypeRep arg1, Id) -> !(TypeRep arg2, Id) -> Description (Term t)
• DTernaryTerm :: forall tag arg1 arg2 arg3 t. (Eq tag, Hashable tag) => !(TypeRep tag, tag) -> !(TypeRep arg1, Id) -> !(TypeRep arg2, Id) -> !(TypeRep arg3, Id) -> Description (Term t)
• DNotTerm :: !Id -> Description (Term Bool)
• DOrTerm :: !Id -> !Id -> Description (Term Bool)
• DAndTerm :: !Id -> !Id -> Description (Term Bool)
• DEqvTerm :: forall args. TypeRep args -> !Id -> !Id -> Description (Term Bool)
• DITETerm :: forall t. !Id -> !Id -> !Id -> Description (Term t)
• DAddNumTerm :: forall t. !Id -> !Id -> Description (Term t)
• DUMinusNumTerm :: forall t. !Id -> Description (Term t)
• DTimesNumTerm :: forall t. !Id -> !Id -> Description (Term t)
• DAbsNumTerm :: forall t. !Id -> Description (Term t)
• DSignumNumTerm :: forall t. !Id -> Description (Term t)
• DLTNumTerm :: forall args. TypeRep args -> !Id -> !Id -> Description (Term Bool)
• DLENumTerm :: forall args. TypeRep args -> !Id -> !Id -> Description (Term Bool)
• DAndBitsTerm :: forall t. !Id -> !Id -> Description (Term t)
• DOrBitsTerm :: forall t. !Id -> !Id -> Description (Term t)
• DXorBitsTerm :: forall t. !Id -> !Id -> Description (Term t)
• DComplementBitsTerm :: forall t. !Id -> Description (Term t)
• DShiftBitsTerm :: forall t. !Id -> !Int -> Description (Term t)
• DRotateBitsTerm :: forall t. !Id -> !Int -> Description (Term t)
• DBVConcatTerm :: forall bv1 bv2 t. TypeRep bv1 -> TypeRep bv2 -> !Id -> !Id -> Description (Term t)
• DBVSelectTerm :: forall (bv :: Nat -> TYPE LiftedRep) (n :: Nat) (w :: Nat) (ix :: Nat). !(TypeRep ix) -> !(TypeRep (bv n), Id) -> Description (Term (bv w))
• DBVExtendTerm :: forall (bv :: Nat -> TYPE LiftedRep) (l :: Nat) (r :: Nat). !Bool -> !(TypeRep r) -> !(TypeRep (bv l), Id) -> Description (Term (bv r))
• DTabularFunApplyTerm :: forall a t. !(TypeRep (a =-> t), Id) -> !(TypeRep a, Id) -> Description (Term t)
• DGeneralFunApplyTerm :: forall a t. !(TypeRep (a --> t), Id) -> !(TypeRep a, Id) -> Description (Term t)
• DDivIntegralTerm :: forall t. !Id -> !Id -> Description (Term t)
• DModIntegralTerm :: forall t. !Id -> !Id -> Description (Term t)
• DQuotIntegralTerm :: forall t. !Id -> !Id -> Description (Term t)
• DRemIntegralTerm :: forall t. !Id -> !Id -> Description (Term t)
• DDivBoundedIntegralTerm :: forall t. !Id -> !Id -> Description (Term t)
• DModBoundedIntegralTerm :: forall t. !Id -> !Id -> Description (Term t)
• DQuotBoundedIntegralTerm :: forall t. !Id -> !Id -> Description (Term t)
• DRemBoundedIntegralTerm :: forall t. !Id -> !Id -> Description (Term t)

type Uninterned (Term t)

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

type Uninterned (Term t) = UTerm t

data UTerm t where

Constructors

UConTerm :: SupportedPrim t => !t -> UTerm t

USymTerm :: SupportedPrim t => !(TypedSymbol t) -> UTerm t

UUnaryTerm :: UnaryOp tag arg t => !tag -> !(Term arg) -> UTerm t

UBinaryTerm :: BinaryOp tag arg1 arg2 t => !tag -> !(Term arg1) -> !(Term arg2) -> UTerm t

UTernaryTerm :: TernaryOp tag arg1 arg2 arg3 t => !tag -> !(Term arg1) -> !(Term arg2) -> !(Term arg3) -> UTerm t

UNotTerm :: !(Term Bool) -> UTerm Bool

UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool

UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool

UEqvTerm :: SupportedPrim t => !(Term t) -> !(Term t) -> UTerm Bool

UITETerm :: SupportedPrim t => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t

UAddNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t

UUMinusNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t

UTimesNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t

UAbsNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t

USignumNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t

ULTNumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool

ULENumTerm :: (SupportedPrim t, Num t, Ord t) => !(Term t) -> !(Term t) -> UTerm Bool

UAndBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t

UOrBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t

UXorBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !(Term t) -> UTerm t

UComplementBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> UTerm t

UShiftBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !Int -> UTerm t

URotateBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> !Int -> UTerm t

UBVConcatTerm :: (SupportedPrim (bv a), SupportedPrim (bv b), SupportedPrim (bv (a + b)), KnownNat a, KnownNat b, 1 <= a, 1 <= b, SizedBV bv) => !(Term (bv a)) -> !(Term (bv b)) -> UTerm (bv (a + b))

UBVSelectTerm :: (SupportedPrim (bv n), SupportedPrim (bv w), KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n, SizedBV bv) => !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv n)) -> UTerm (bv w)

UBVExtendTerm :: (SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l, KnownNat r, 1 <= l, l <= r, SizedBV bv) => !Bool -> !(TypeRep r) -> !(Term (bv l)) -> UTerm (bv r)

UTabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a =-> b) -> Term a -> UTerm b

UGeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> UTerm b

UDivIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t

UModIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t

UQuotIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t

URemIntegralTerm :: (SupportedPrim t, Integral t) => !(Term t) -> !(Term t) -> UTerm t

UDivBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t

UModBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t

UQuotBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t

URemBoundedIntegralTerm :: (SupportedPrim t, Bounded t, Integral t) => !(Term t) -> !(Term t) -> UTerm t

data a --> b where infixr 0

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

Constructors

GeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b

Instances

Lift (a --> b :: Type)

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)

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (ca --> cb)) (sa -~> sb)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: UnionM (ca --> cb) -> sa -~> sb

Show (a --> b)

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)

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

Methods

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

Eq (a --> b)

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

Methods

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

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

(LinkedRep a sa, LinkedRep b sb) => Function (a --> b)

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

Associated Types

type Arg (a --> b)

type Ret (a --> b)

Methods

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

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

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

Associated Types

type PrimConstraint (a --> b)

Methods

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

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

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

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

defaultValue :: a --> b

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

(SymRep ca, SymRep cb) => SymRep (ca --> cb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType (ca --> cb)

Hashable (a --> b)

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

Methods

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

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

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Solvable (ca --> cb) (sa -~> sb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: (ca --> cb) -> sa -~> sb

conView :: (sa -~> sb) -> Maybe (ca --> cb)

ssym :: String -> sa -~> sb

isym :: String -> Int -> sa -~> sb

sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> sa -~> sb

iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> sa -~> sb

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa -~> sb) (ca --> cb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: (sa -~> sb) -> Maybe (ca --> cb)

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca --> cb) (sa -~> sb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: (ca --> cb) -> sa -~> sb

(LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca --> cb) (sa -~> sb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

underlyingTerm :: (sa -~> sb) -> Term (ca --> cb)

wrapTerm :: Term (ca --> cb) -> sa -~> sb

type Arg (a --> b)

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

type Arg (a --> b) = SymType a

type Ret (a --> b)

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

type Ret (a --> b) = SymType b

type PrimConstraint (a --> b)

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

type PrimConstraint (a --> b) = (SupportedPrim a, SupportedPrim b)

type SymType (ca --> cb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

type SymType (ca --> cb) = SymType ca -~> SymType cb

buildGeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b