grisette-0.3.1.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellSafe-Inferred
LanguageHaskell2010

Grisette.IR.SymPrim.Data.Prim.PartialEval.BV

Description

 

Documentation

pevalBVToSignedTerm :: (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 #

pevalBVToUnsignedTerm :: (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 #

pevalBVConcatTerm :: (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 #

pevalBVSelectTerm :: 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 #

pevalBVExtendTerm :: forall proxy l r bv. (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 #

pevalBVZeroExtendTerm :: forall proxy l r bv. (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 #

pevalBVSignExtendTerm :: forall proxy l r bv. (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 #