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 c), KnownNat a, KnownNat b, KnownNat c, BVConcat (bv a) (bv b) (bv c)) => Term (bv a) -> Term (bv b) -> Term (bv c) Source #

bvselectTerm :: forall bv a ix w proxy. (SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a, KnownNat w, KnownNat ix, BVSelect (bv a) ix w (bv w)) => proxy ix -> proxy w -> Term (bv a) -> Term (bv w) Source #

bvextendTerm :: forall bv a n w proxy. (SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a, KnownNat n, KnownNat w, BVExtend (bv a) n (bv w)) => Bool -> proxy n -> Term (bv a) -> Term (bv w) Source #

bvsignExtendTerm :: forall bv a n w proxy. (SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a, KnownNat n, KnownNat w, BVExtend (bv a) n (bv w)) => proxy n -> Term (bv a) -> Term (bv w) Source #

bvzeroExtendTerm :: forall bv a n w proxy. (SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a, KnownNat n, KnownNat w, BVExtend (bv a) n (bv w)) => proxy n -> Term (bv a) -> Term (bv w) 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 #

divIntegerTerm :: Term Integer -> Term Integer -> Term Integer Source #

modIntegerTerm :: Term Integer -> Term Integer -> Term Integer Source #