Documentation

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

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

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

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

notTerm :: Term Bool -> Term Bool Source #

orTerm :: Term Bool -> Term Bool -> Term Bool Source #

andTerm :: Term Bool -> Term Bool -> Term Bool Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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