| Copyright | (c) Sirui Lu 2021-2023 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
Description
Documentation
pevalBVConcatTerm :: (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 #
pevalBVSelectTerm :: 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 #
pevalBVExtendTerm :: forall proxy l r bv. (KnownNat l, KnownNat r, 1 <= l, l <= r, SupportedPrim (bv l), SupportedPrim (bv r), SizedBV bv) => Bool -> proxy r -> Term (bv l) -> Term (bv r) Source #
pevalBVZeroExtendTerm :: forall proxy l r bv. (KnownNat l, KnownNat r, 1 <= l, l <= r, SupportedPrim (bv l), SupportedPrim (bv r), SizedBV bv) => proxy r -> Term (bv l) -> Term (bv r) Source #
pevalBVSignExtendTerm :: forall proxy l r bv. (KnownNat l, KnownNat r, 1 <= l, l <= r, SupportedPrim (bv l), SupportedPrim (bv r), SizedBV bv) => proxy r -> Term (bv l) -> Term (bv r) Source #