grisette-0.5.0.1: 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 HaskellSafe-Inferred
LanguageHaskell2010

Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm

Description

 

Documentation

pevalFiniteBitsSymRotateRotateLeftTerm :: forall a. (Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) => Term a -> Term a -> Term a Source #

pevalFiniteBitsSymRotateRotateRightTerm :: forall a. (Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) => Term a -> Term a -> Term a Source #

Orphan instances

(KnownNat n, 1 <= n) => PEvalRotateTerm (IntN n) Source # 
Instance details

Methods

pevalRotateLeftTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

pevalRotateRightTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source #

withSbvRotateTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (IntN n)) => r) -> r Source #

sbvRotateLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source #

sbvRotateRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source #

(KnownNat n, 1 <= n) => PEvalRotateTerm (WordN n) Source # 
Instance details

Methods

pevalRotateLeftTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

pevalRotateRightTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source #

withSbvRotateTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (WordN n)) => r) -> r Source #

sbvRotateLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #

sbvRotateRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #