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

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

shiftLeftTerm :: (SupportedPrim a, Integral a, FiniteBits a, SymShift a) => Term a -> Term a -> Term a

shiftRightTerm :: (SupportedPrim a, Integral a, FiniteBits a, SymShift a) => Term a -> Term a -> Term a

rotateLeftTerm :: (SupportedPrim a, Integral a, FiniteBits a, SymRotate a) => Term a -> Term a -> Term a

rotateRightTerm :: (SupportedPrim a, Integral a, FiniteBits a, SymRotate a) => Term a -> Term a -> Term a

toSignedTerm :: (SupportedPrim u, SupportedPrim s, SignConversion u s) => Term u -> Term s

toUnsignedTerm :: (SupportedPrim u, SupportedPrim s, SignConversion u s) => 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) => Term (bv a) -> Term (bv b) -> Term (bv (a + b))

bvselectTerm :: forall bv n ix w p q. (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) => p ix -> q w -> Term (bv n) -> Term (bv w)

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

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

bvzeroExtendTerm :: forall bv l r proxy. (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, 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