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

Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm

Description

 
Synopsis

Documentation

pevalFiniteBitsSymShiftShiftLeftTerm :: forall bv (n :: Nat). (forall (m :: Nat). (KnownNat m, 1 <= m) => Integral (bv m), forall (m :: Nat). (KnownNat m, 1 <= m) => SymShift (bv m), forall (m :: Nat). (KnownNat m, 1 <= m) => SupportedPrim (bv m), forall (m :: Nat). (KnownNat m, 1 <= m) => PEvalShiftTerm (bv m), PEvalBVTerm bv, KnownNat n, 1 <= n) => Term (bv n) -> Term (bv n) -> Term (bv n) Source #

Partial evaluation of symbolic shift left term for finite bits types.

pevalFiniteBitsSymShiftShiftRightTerm :: forall bv (n :: Nat). (forall (m :: Nat). (KnownNat m, 1 <= m) => Integral (bv m), forall (m :: Nat). (KnownNat m, 1 <= m) => SymShift (bv m), forall (m :: Nat). (KnownNat m, 1 <= m) => SupportedPrim (bv m), forall (m :: Nat). (KnownNat m, 1 <= m) => PEvalShiftTerm (bv m), PEvalBVTerm bv, KnownNat n, 1 <= n) => Term (bv n) -> Term (bv n) -> Term (bv n) Source #

Partial evaluation of symbolic shift right term for finite bits types.

Orphan instances