Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors

Documentation

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) => String -> Term t

isymTerm :: (SupportedPrim t, Typeable t) => String -> Int -> Term t

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

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

notTerm :: Term Bool -> Term Bool

orTerm :: Term Bool -> Term Bool -> Term Bool

andTerm :: Term Bool -> Term Bool -> Term Bool

eqvTerm :: SupportedPrim a => Term a -> Term a -> Term Bool

iteTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a

addNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a -> Term a

uminusNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a

timesNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a -> Term a

absNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a

signumNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a

ltNumTerm :: (SupportedPrim a, Num a, Ord a) => Term a -> Term a -> Term Bool

leNumTerm :: (SupportedPrim a, Num a, Ord a) => Term a -> Term a -> Term Bool

andBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a -> Term a

orBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a -> Term a

xorBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a -> Term a

complementBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a

shiftBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Int -> Term a

rotateBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Int -> Term a

bvconcatTerm :: (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) -> Term (bv (a + b))

bvselectTerm :: forall bv n ix w proxy. (SupportedPrim (bv n), SupportedPrim (bv w), KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n, SizedBV bv) => proxy ix -> proxy w -> Term (bv n) -> Term (bv w)

bvextendTerm :: forall bv l r proxy. (SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l, KnownNat r, 1 <= l, l <= r, SizedBV bv) => Bool -> proxy r -> Term (bv l) -> Term (bv r)

bvsignExtendTerm :: forall bv l r proxy. (SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l, KnownNat r, 1 <= l, l <= r, SizedBV bv) => proxy r -> Term (bv l) -> Term (bv r)

bvzeroExtendTerm :: forall bv l r proxy. (SupportedPrim (bv l), SupportedPrim (bv r), KnownNat l, KnownNat r, 1 <= l, l <= r, SizedBV bv) => proxy r -> Term (bv l) -> Term (bv r)

tabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a =-> b) -> Term a -> Term b

generalFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> Term b

divIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a

modIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a

quotIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a

remIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a

divBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a

modBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a

quotBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a

remBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a