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 #

bvToSignedTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n), forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n), Typeable ubv, Typeable sbv, KnownNat n, 1 <= n, BVSignConversion (ubv n) (sbv n)) => Term (ubv n) -> Term (sbv n) Source #

bvToUnsignedTerm :: (forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n), forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n), Typeable ubv, Typeable sbv, KnownNat n, 1 <= n, BVSignConversion (ubv n) (sbv n)) => Term (sbv n) -> Term (ubv n) Source #

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

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

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

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

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