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.Internal.IR.SymPrim

Description

Synopsis

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 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
- ShiftLeftTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymShift t) => !Id -> !(Term t) -> !(Term t) -> Term t
- ShiftRightTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymShift t) => !Id -> !(Term t) -> !(Term t) -> Term t
- RotateLeftTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymRotate t) => !Id -> !(Term t) -> !(Term t) -> Term t
- RotateRightTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymRotate t) => !Id -> !(Term t) -> !(Term t) -> Term t
- ToSignedTerm :: (SupportedPrim u, SupportedPrim s, SignConversion u s) => !Id -> !(Term u) -> Term s
- ToUnsignedTerm :: (SupportedPrim u, SupportedPrim s, SignConversion u s) => !Id -> !(Term s) -> Term u
- 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
showUntyped :: TypedSymbol t -> String
withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a
data SomeTypedSymbol where
- SomeTypedSymbol :: forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol
someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol
evaluateTerm :: forall a. SupportedPrim a => Bool -> Model -> Term a -> Term a
introSupportedPrimConstraint :: forall t a. Term t -> (SupportedPrim t => a) -> a
data SomeTerm where
- SomeTerm :: forall a. SupportedPrim a => Term a -> SomeTerm
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
castTerm :: forall a b. Typeable b => Term a -> Maybe (Term b)
identity :: Term t -> Id
identityWithTypeRep :: forall t. Term t -> (TypeRep, Id)
pformat :: forall t. SupportedPrim t => Term t -> String
constructUnary :: forall tag arg t. (SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t, Show tag) => tag -> Term arg -> Term t
constructBinary :: forall tag arg1 arg2 t. (SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term t
constructTernary :: forall tag arg1 arg2 arg3 t. (SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
conTerm :: (SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) => t -> Term t
symTerm :: forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
ssymTerm :: (SupportedPrim t, Typeable t) => Text -> Term t
isymTerm :: (SupportedPrim t, Typeable t) => Text -> Int -> Term t
sinfosymTerm :: (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => Text -> a -> Term t
iinfosymTerm :: (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => Text -> Int -> a -> Term t
termSize :: Term a -> Int
termsSize :: [Term a] -> Int
extractSymbolicsTerm :: SupportedPrim a => Term a -> HashSet SomeTypedSymbol
trueTerm :: Term Bool
falseTerm :: Term Bool
pattern BoolConTerm :: Bool -> Term a
pattern TrueTerm :: Term a
pattern FalseTerm :: Term a
pattern BoolTerm :: Term Bool -> Term a
pevalNotTerm :: Term Bool -> Term Bool
pevalEqvTerm :: forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalNotEqvTerm :: SupportedPrim a => Term a -> Term a -> Term Bool
pevalOrTerm :: Term Bool -> Term Bool -> Term Bool
pevalAndTerm :: Term Bool -> Term Bool -> Term Bool
pevalITETerm :: forall a. SupportedPrim a => Term Bool -> Term a -> Term a -> Term a
pevalImplyTerm :: Term Bool -> Term Bool -> Term Bool
pevalXorTerm :: Term Bool -> Term Bool -> Term Bool
unaryUnfoldOnce :: forall a b. (Typeable a, SupportedPrim b) => PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
binaryUnfoldOnce :: forall a b c. (Typeable a, Typeable b, SupportedPrim c) => PartialRuleBinary a b c -> TotalRuleBinary a b c -> TotalRuleBinary a b c
pattern UnaryTermPatt :: forall a b tag. (Typeable tag, Typeable b) => tag -> Term b -> Term a
pattern BinaryTermPatt :: forall a b c tag. (Typeable tag, Typeable b, Typeable c) => tag -> Term b -> Term c -> Term a
pattern TernaryTermPatt :: forall a b c d tag. (Typeable tag, Typeable b, Typeable c, Typeable d) => tag -> Term b -> Term c -> Term d -> Term a
type PartialFun a b = a -> Maybe b
type PartialRuleUnary a b = PartialFun (Term a) (Term b)
type TotalRuleUnary a b = Term a -> Term b
type PartialRuleBinary a b c = Term a -> PartialFun (Term b) (Term c)
type TotalRuleBinary a b c = Term a -> Term b -> Term c
totalize :: PartialFun a b -> (a -> b) -> a -> b
totalize2 :: (a -> PartialFun b c) -> (a -> b -> c) -> a -> b -> c
class UnaryPartialStrategy tag a b | tag a -> b where
- extractor :: tag -> Term a -> Maybe a
- constantHandler :: tag -> a -> Maybe (Term b)
- nonConstantHandler :: tag -> Term a -> Maybe (Term b)
unaryPartial :: forall tag a b. UnaryPartialStrategy tag a b => tag -> PartialRuleUnary a b
class BinaryCommPartialStrategy tag a c | tag a -> c where
- singleConstantHandler :: tag -> a -> Term a -> Maybe (Term c)
class BinaryPartialStrategy tag a b c | tag a b -> c where
- extractora :: tag -> Term a -> Maybe a
- extractorb :: tag -> Term b -> Maybe b
- allConstantHandler :: tag -> a -> b -> Maybe (Term c)
- leftConstantHandler :: tag -> a -> Term b -> Maybe (Term c)
- rightConstantHandler :: tag -> Term a -> b -> Maybe (Term c)
- nonBinaryConstantHandler :: tag -> Term a -> Term b -> Maybe (Term c)
binaryPartial :: forall tag a b c. BinaryPartialStrategy tag a b c => tag -> PartialRuleBinary a b c
pattern NumConTerm :: forall b a. (Num b, Typeable b) => b -> Term a
pattern NumOrdConTerm :: forall b a. (Num b, Ord b, Typeable b) => b -> Term a
pevalAddNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalMinusNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalUMinusNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a
pevalAbsNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a
pevalSignumNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a
pevalTimesNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalLtNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool
pevalLeNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool
pevalGtNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool
pevalGeNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool
pevalTabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a =-> b) -> Term a -> Term b
pevalGeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> Term b
pevalDivIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
pevalModIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
pevalQuotIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
pevalRemIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a

Documentation

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 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
ShiftLeftTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymShift t) => !Id -> !(Term t) -> !(Term t) -> Term t
ShiftRightTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymShift t) => !Id -> !(Term t) -> !(Term t) -> Term t
RotateLeftTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymRotate t) => !Id -> !(Term t) -> !(Term t) -> Term t
RotateRightTerm :: (SupportedPrim t, Integral t, FiniteBits t, SymRotate t) => !Id -> !(Term t) -> !(Term t) -> Term t
ToSignedTerm :: (SupportedPrim u, SupportedPrim s, SignConversion u s) => !Id -> !(Term u) -> Term s
ToUnsignedTerm :: (SupportedPrim u, SupportedPrim s, SignConversion u s) => !Id -> !(Term s) -> Term u
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) DShiftLeftTerm :: forall t. !Id -> !Id -> Description (Term t) DShiftRightTerm :: forall t. !Id -> !Id -> Description (Term t) DRotateLeftTerm :: forall t. !Id -> !Id -> Description (Term t) DRotateRightTerm :: forall t. !Id -> !Id -> Description (Term t) DBVConcatTerm :: forall bv1 bv2 t. TypeRep bv1 -> TypeRep bv2 -> !Id -> !Id -> Description (Term t) DToSignedTerm :: forall u t. !(TypeRep u, Id) -> Description (Term t) DToUnsignedTerm :: forall s t. !(TypeRep s, Id) -> Description (Term t) DBVSelectTerm :: forall (bv :: Nat -> Type) (n :: Nat) (w :: Nat) (ix :: Nat). !(TypeRep ix) -> !(TypeRep (bv n), Id) -> Description (Term (bv w)) DBVExtendTerm :: forall (bv :: Nat -> Type) (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

showUntyped :: TypedSymbol t -> String Source #

withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a 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 #

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

evaluateTerm :: forall a. SupportedPrim a => Bool -> Model -> Term a -> Term a Source #

introSupportedPrimConstraint :: forall t a. Term t -> (SupportedPrim t => a) -> a Source #

data SomeTerm where Source #

Constructors

SomeTerm :: forall a. SupportedPrim a => Term a -> SomeTerm

Instances

Instances details

Show SomeTerm Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm Methods showsPrec :: Int -> SomeTerm -> ShowS # show :: SomeTerm -> String # showList :: [SomeTerm] -> ShowS #
Eq SomeTerm Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm Methods (==) :: SomeTerm -> SomeTerm -> Bool # (/=) :: SomeTerm -> SomeTerm -> Bool #
Hashable SomeTerm Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm Methods hashWithSalt :: Int -> SomeTerm -> Int # hash :: SomeTerm -> Int #

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 #

castTerm :: forall a b. Typeable b => Term a -> Maybe (Term b) Source #

identity :: Term t -> Id Source #

identityWithTypeRep :: forall t. Term t -> (TypeRep, Id) Source #

pformat :: forall t. SupportedPrim t => Term t -> String Source #

constructUnary :: forall tag arg t. (SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t, Show tag) => tag -> Term arg -> Term t Source #

constructBinary :: forall tag arg1 arg2 t. (SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term t Source #

constructTernary :: forall tag arg1 arg2 arg3 t. (SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t Source #

conTerm :: (SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) => t -> Term t Source #

symTerm :: forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t Source #

ssymTerm :: (SupportedPrim t, Typeable t) => Text -> Term t Source #

isymTerm :: (SupportedPrim t, Typeable t) => Text -> Int -> Term t Source #

sinfosymTerm :: (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => Text -> a -> Term t Source #

iinfosymTerm :: (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => Text -> Int -> a -> Term t Source #

termSize :: Term a -> Int Source #

termsSize :: [Term a] -> Int Source #

extractSymbolicsTerm :: SupportedPrim a => Term a -> HashSet SomeTypedSymbol Source #

trueTerm :: Term Bool Source #

falseTerm :: Term Bool Source #

pattern BoolConTerm :: Bool -> Term a Source #

pattern TrueTerm :: Term a Source #

pattern FalseTerm :: Term a Source #

pattern BoolTerm :: Term Bool -> Term a Source #

pevalNotTerm :: Term Bool -> Term Bool Source #

pevalEqvTerm :: forall a. SupportedPrim a => Term a -> Term a -> Term Bool Source #

pevalNotEqvTerm :: SupportedPrim a => Term a -> Term a -> Term Bool Source #

pevalOrTerm :: Term Bool -> Term Bool -> Term Bool Source #

pevalAndTerm :: Term Bool -> Term Bool -> Term Bool Source #

pevalITETerm :: forall a. SupportedPrim a => Term Bool -> Term a -> Term a -> Term a Source #

pevalImplyTerm :: Term Bool -> Term Bool -> Term Bool Source #

pevalXorTerm :: Term Bool -> Term Bool -> Term Bool Source #

unaryUnfoldOnce :: forall a b. (Typeable a, SupportedPrim b) => PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b Source #

binaryUnfoldOnce :: forall a b c. (Typeable a, Typeable b, SupportedPrim c) => PartialRuleBinary a b c -> TotalRuleBinary a b c -> TotalRuleBinary a b c Source #

pattern UnaryTermPatt :: forall a b tag. (Typeable tag, Typeable b) => tag -> Term b -> Term a Source #

pattern BinaryTermPatt :: forall a b c tag. (Typeable tag, Typeable b, Typeable c) => tag -> Term b -> Term c -> Term a Source #

pattern TernaryTermPatt :: forall a b c d tag. (Typeable tag, Typeable b, Typeable c, Typeable d) => tag -> Term b -> Term c -> Term d -> Term a Source #

type PartialFun a b = a -> Maybe b Source #

type PartialRuleUnary a b = PartialFun (Term a) (Term b) Source #

type TotalRuleUnary a b = Term a -> Term b Source #

type PartialRuleBinary a b c = Term a -> PartialFun (Term b) (Term c) Source #

type TotalRuleBinary a b c = Term a -> Term b -> Term c Source #

totalize :: PartialFun a b -> (a -> b) -> a -> b Source #

totalize2 :: (a -> PartialFun b c) -> (a -> b -> c) -> a -> b -> c Source #

class UnaryPartialStrategy tag a b | tag a -> b where Source #

Methods

extractor :: tag -> Term a -> Maybe a Source #

constantHandler :: tag -> a -> Maybe (Term b) Source #

nonConstantHandler :: tag -> Term a -> Maybe (Term b) Source #

unaryPartial :: forall tag a b. UnaryPartialStrategy tag a b => tag -> PartialRuleUnary a b Source #

class BinaryCommPartialStrategy tag a c | tag a -> c where Source #

Methods

singleConstantHandler :: tag -> a -> Term a -> Maybe (Term c) Source #

class BinaryPartialStrategy tag a b c | tag a b -> c where Source #

Minimal complete definition

extractora, extractorb, allConstantHandler, nonBinaryConstantHandler

Methods

extractora :: tag -> Term a -> Maybe a Source #

extractorb :: tag -> Term b -> Maybe b Source #

allConstantHandler :: tag -> a -> b -> Maybe (Term c) Source #

leftConstantHandler :: tag -> a -> Term b -> Maybe (Term c) Source #

default leftConstantHandler :: (a ~ b, BinaryCommPartialStrategy tag a c) => tag -> a -> Term b -> Maybe (Term c) Source #

rightConstantHandler :: tag -> Term a -> b -> Maybe (Term c) Source #

default rightConstantHandler :: (a ~ b, BinaryCommPartialStrategy tag a c) => tag -> Term a -> b -> Maybe (Term c) Source #

nonBinaryConstantHandler :: tag -> Term a -> Term b -> Maybe (Term c) Source #

binaryPartial :: forall tag a b c. BinaryPartialStrategy tag a b c => tag -> PartialRuleBinary a b c Source #

pattern NumConTerm :: forall b a. (Num b, Typeable b) => b -> Term a Source #

pattern NumOrdConTerm :: forall b a. (Num b, Ord b, Typeable b) => b -> Term a Source #

pevalAddNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a Source #

pevalMinusNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a -> Term a Source #

pevalUMinusNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a Source #

pevalAbsNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a Source #

pevalSignumNumTerm :: (Num a, SupportedPrim a) => Term a -> Term a Source #

pevalTimesNumTerm :: forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a Source #

pevalLtNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool Source #

pevalLeNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool Source #

pevalGtNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool Source #

pevalGeNumTerm :: (Num a, Ord a, SupportedPrim a) => Term a -> Term a -> Term Bool Source #

pevalTabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a =-> b) -> Term a -> Term b Source #

pevalGeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> Term b Source #

pevalDivIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a Source #

pevalModIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a Source #

pevalQuotIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a Source #

pevalRemIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a Source #