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