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.Prim.InternedTerm.Term

Description

Synopsis

class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where
- type PrimConstraint t :: Constraint
- withPrim :: proxy t -> (PrimConstraint t => a) -> a
- termCache :: Cache (Term t)
- pformatCon :: t -> String
- pformatSym :: TypedSymbol t -> String
- defaultValue :: t
- defaultValueDynamic :: proxy t -> ModelValue
class SupportedPrim con => SymRep con where
- type SymType con
class ConRep sym where
- type ConType sym
class (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) => LinkedRep con sym | con -> sym, sym -> con where
- underlyingTerm :: sym -> Term con
- wrapTerm :: Term con -> sym
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
- 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
- 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
- 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
- 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
data SomeTypedSymbol where
- SomeTypedSymbol :: forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol
showUntyped :: TypedSymbol t -> String
withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a
someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol
data Term t where
- 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
- BVToSignedTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n), forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n), Typeable ubv, Typeable sbv, KnownNat n, 1 <= n, BVSignConversion (ubv n) (sbv n)) => !Id -> !(Term (ubv n)) -> Term (sbv n)
- BVToUnsignedTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n), forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n), Typeable ubv, Typeable sbv, KnownNat n, 1 <= n, BVSignConversion (ubv n) (sbv n)) => !Id -> !(Term (sbv n)) -> Term (ubv n)
- BVConcatTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, KnownNat a, KnownNat b, KnownNat (a + b), 1 <= a, 1 <= b, 1 <= (a + b), SizedBV bv) => !Id -> !(Term (bv a)) -> !(Term (bv b)) -> Term (bv (a + b))
- BVSelectTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, 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 :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, 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
data UTerm t where
- 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
- UBVToSignedTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n), forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n), Typeable ubv, Typeable sbv, KnownNat n, 1 <= n, BVSignConversion (ubv n) (sbv n)) => !(Term (ubv n)) -> UTerm (sbv n)
- UBVToUnsignedTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n), forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n), Typeable ubv, Typeable sbv, KnownNat n, 1 <= n, BVSignConversion (ubv n) (sbv n)) => !(Term (sbv n)) -> UTerm (ubv n)
- UBVConcatTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, KnownNat a, KnownNat b, KnownNat (a + b), 1 <= a, 1 <= b, 1 <= (a + b), SizedBV bv) => !(Term (bv a)) -> !(Term (bv b)) -> UTerm (bv (a + b))
- UBVSelectTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, 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 :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, 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
- GeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
buildGeneralFun :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term b -> a --> b
prettyPrintTerm :: Term t -> Doc ann

Documentation

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

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

Minimal complete definition

defaultValue

Associated Types

type PrimConstraint t :: Constraint Source #

type PrimConstraint _ = ()

Methods

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

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

termCache :: Cache (Term t) Source #

pformatCon :: t -> String Source #

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

pformatSym :: TypedSymbol t -> String Source #

defaultValue :: t Source #

defaultValueDynamic :: proxy t -> ModelValue Source #

Instances

Instances details

SupportedPrim Integer Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term Associated Types type PrimConstraint Integer Source # Methods withPrim :: proxy Integer -> (PrimConstraint Integer => a) -> a Source # termCache :: Cache (Term Integer) Source # pformatCon :: Integer -> String Source # pformatSym :: TypedSymbol Integer -> String Source # defaultValue :: Integer Source # defaultValueDynamic :: proxy Integer -> ModelValue Source #
SupportedPrim Bool Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term Associated Types type PrimConstraint Bool Source # Methods withPrim :: proxy Bool -> (PrimConstraint Bool => a) -> a Source # termCache :: Cache (Term Bool) Source # pformatCon :: Bool -> String Source # pformatSym :: TypedSymbol Bool -> String Source # defaultValue :: Bool Source # defaultValueDynamic :: proxy Bool -> ModelValue 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 # Methods withPrim :: proxy (IntN w) -> (PrimConstraint (IntN w) => a) -> a Source # termCache :: Cache (Term (IntN w)) Source # pformatCon :: IntN w -> String Source # pformatSym :: TypedSymbol (IntN w) -> String Source # defaultValue :: IntN w Source # defaultValueDynamic :: proxy (IntN w) -> ModelValue 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 # Methods withPrim :: proxy (WordN w) -> (PrimConstraint (WordN w) => a) -> a Source # termCache :: Cache (Term (WordN w)) Source # pformatCon :: WordN w -> String Source # pformatSym :: TypedSymbol (WordN w) -> String Source # defaultValue :: WordN w Source # defaultValueDynamic :: proxy (WordN w) -> ModelValue 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.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 #

class SupportedPrim con => SymRep con Source #

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

Associated Types

type SymType con Source #

Instances

Instances details

SymRep Integer Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type SymType Integer Source #
SymRep Bool Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type SymType Bool Source #
(KnownNat n, 1 <= n) => SymRep (IntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type SymType (IntN n) Source #
(KnownNat n, 1 <= n) => SymRep (WordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type SymType (WordN n) Source #
(SymRep ca, SymRep cb) => SymRep (ca --> cb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type SymType (ca --> cb) Source #
(SymRep a, SymRep b) => SymRep (a =-> b) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type SymType (a =-> b) Source #

class ConRep sym Source #

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

Associated Types

type ConType sym Source #

Instances

Instances details

ConRep SymBool Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type ConType SymBool Source #
ConRep SymInteger Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type ConType SymInteger Source #
(KnownNat n, 1 <= n) => ConRep (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type ConType (SymIntN n) Source #
(KnownNat n, 1 <= n) => ConRep (SymWordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type ConType (SymWordN n) Source #
(ConRep a, ConRep b) => ConRep (a -~> b) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type ConType (a -~> b) Source #
(ConRep a, ConRep b) => ConRep (a =~> b) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type ConType (a =~> b) Source #

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

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

Methods

underlyingTerm :: sym -> Term con Source #

wrapTerm :: Term con -> sym Source #

Instances

Instances details

LinkedRep Integer SymInteger Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods underlyingTerm :: SymInteger -> Term Integer Source # wrapTerm :: Term Integer -> SymInteger Source #
LinkedRep Bool SymBool Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods underlyingTerm :: SymBool -> Term Bool Source # wrapTerm :: Term Bool -> SymBool Source #
(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods underlyingTerm :: SymIntN n -> Term (IntN n) Source # wrapTerm :: Term (IntN n) -> SymIntN n Source #
(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods underlyingTerm :: SymWordN n -> Term (WordN n) Source # wrapTerm :: Term (WordN n) -> SymWordN n Source #
(LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods underlyingTerm :: (sa -~> sb) -> Term (ca --> cb) Source # wrapTerm :: Term (ca --> cb) -> sa -~> sb Source #
(LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca =-> cb) (sa =~> sb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods underlyingTerm :: (sa =~> sb) -> Term (ca =-> cb) Source # wrapTerm :: Term (ca =-> cb) -> sa =~> sb Source #

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

Methods

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

pformatUnary :: tag -> Term arg -> String Source #

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

Methods

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

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

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

Methods

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

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

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 Methods emptySet :: SymbolSet Source # isEmptySet :: SymbolSet -> Bool Source # containsSymbol :: TypedSymbol a -> SymbolSet -> Bool Source # insertSymbol :: TypedSymbol a -> SymbolSet -> SymbolSet Source # intersectionSet :: SymbolSet -> SymbolSet -> SymbolSet Source # unionSet :: SymbolSet -> SymbolSet -> SymbolSet Source # differenceSet :: SymbolSet -> SymbolSet -> SymbolSet Source #
ModelOps Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods emptyModel :: Model Source # isEmptyModel :: Model -> Bool Source # modelContains :: TypedSymbol a -> Model -> Bool Source # valueOf :: TypedSymbol t -> Model -> Maybe t Source # insertValue :: TypedSymbol t -> t -> Model -> Model Source # exceptFor :: SymbolSet -> Model -> Model Source # exceptFor' :: TypedSymbol t -> Model -> Model Source # restrictTo :: SymbolSet -> Model -> Model Source # extendTo :: SymbolSet -> Model -> Model Source # exact :: SymbolSet -> Model -> Model Source #
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 Methods fromString :: String -> TypedSymbol t #
Show (TypedSymbol t) Source #
Instance details 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) 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 Methods (==) :: TypedSymbol t -> TypedSymbol t -> Bool # (/=) :: TypedSymbol t -> TypedSymbol t -> Bool #
Ord (TypedSymbol t) Source #
Instance details 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) 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 Methods buildSymbolSet :: TypedSymbol t -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b) -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c) -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) -> SymbolSet Source #
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 Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) -> SymbolSet Source #
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 Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) -> SymbolSet Source #
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 Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) -> SymbolSet Source #

data SomeTypedSymbol where Source #

Constructors

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

Instances

Instances details

Show SomeTypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term Methods showsPrec :: Int -> SomeTypedSymbol -> ShowS # show :: SomeTypedSymbol -> String # showList :: [SomeTypedSymbol] -> ShowS #
NFData SomeTypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term Methods rnf :: SomeTypedSymbol -> () #
Eq SomeTypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term Methods (==) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool # (/=) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool #
Ord SomeTypedSymbol Source #
Instance details 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 Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term Methods hashWithSalt :: Int -> SomeTypedSymbol -> Int # hash :: SomeTypedSymbol -> Int #

showUntyped :: TypedSymbol t -> String Source #

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

someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol Source #

data Term t where Source #

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
BVToSignedTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n), forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n), Typeable ubv, Typeable sbv, KnownNat n, 1 <= n, BVSignConversion (ubv n) (sbv n)) => !Id -> !(Term (ubv n)) -> Term (sbv n)
BVToUnsignedTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n), forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n), Typeable ubv, Typeable sbv, KnownNat n, 1 <= n, BVSignConversion (ubv n) (sbv n)) => !Id -> !(Term (sbv n)) -> Term (ubv n)
BVConcatTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, KnownNat a, KnownNat b, KnownNat (a + b), 1 <= a, 1 <= b, 1 <= (a + b), SizedBV bv) => !Id -> !(Term (bv a)) -> !(Term (bv b)) -> Term (bv (a + b))
BVSelectTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, 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 :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, 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

Instances details

Lift (Term t :: Type) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term Methods rnf :: Term a -> () #
SupportedPrim t => Eq (Term t) Source #
Instance details 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)) Source #
Instance details 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) Source #
Instance details 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)) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) DBVToSignedTerm :: forall (ubv :: Nat -> Type) (sbv :: Nat -> TYPE LiftedRep) (n :: Nat). !(TypeRep (ubv n), Id) -> Description (Term (sbv n)) DBVToUnsignedTerm :: forall (sbv :: Nat -> Type) (ubv :: Nat -> TYPE LiftedRep) (n :: Nat). !(TypeRep (sbv n), Id) -> Description (Term (ubv n)) 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) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term type Uninterned (Term t) = UTerm t

data UTerm t where Source #

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
UBVToSignedTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n), forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n), Typeable ubv, Typeable sbv, KnownNat n, 1 <= n, BVSignConversion (ubv n) (sbv n)) => !(Term (ubv n)) -> UTerm (sbv n)
UBVToUnsignedTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n), forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n), Typeable ubv, Typeable sbv, KnownNat n, 1 <= n, BVSignConversion (ubv n) (sbv n)) => !(Term (sbv n)) -> UTerm (ubv n)
UBVConcatTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, KnownNat a, KnownNat b, KnownNat (a + b), 1 <= a, 1 <= b, 1 <= (a + b), SizedBV bv) => !(Term (bv a)) -> !(Term (bv b)) -> UTerm (bv (a + b))
UBVSelectTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, 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 :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, 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 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))

Constructors

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

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) #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (ca --> cb)) (sa -~> sb) Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Methods toSym :: UnionM (ca --> cb) -> sa -~> sb Source #
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 #
(LinkedRep a sa, LinkedRep b sb) => Function (a --> b) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term 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 #
(SymRep ca, SymRep cb) => SymRep (ca --> cb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type SymType (ca --> cb) 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 #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Solvable (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods con :: (ca --> cb) -> sa -~> sb Source # conView :: (sa -~> sb) -> Maybe (ca --> cb) Source # ssym :: String -> sa -~> sb Source # isym :: String -> Int -> sa -~> sb Source # sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> sa -~> sb Source # iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> sa -~> sb Source #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa -~> sb) (ca --> cb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods toCon :: (sa -~> sb) -> Maybe (ca --> cb) Source #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods toSym :: (ca --> cb) -> sa -~> sb Source #
(LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods underlyingTerm :: (sa -~> sb) -> Term (ca --> cb) Source # wrapTerm :: Term (ca --> cb) -> sa -~> sb Source #
type Arg (a --> b) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term type Arg (a --> b) = SymType a
type Ret (a --> b) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term type Ret (a --> b) = SymType b
type PrimConstraint (a --> b) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term type PrimConstraint (a --> b) = (SupportedPrim a, SupportedPrim b)
type SymType (ca --> cb) Source #
Instance details 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 Source #

prettyPrintTerm :: Term t -> Doc ann Source #