Copyright	(c) Sirui Lu 2024
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.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm

Contents

Orphan instances

Description

Orphan instances

(KnownNat n, 1 <= n) => PEvalBitwiseTerm (IntN n) Source #
Instance details Methods pevalAndBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalOrBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalXorBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalComplementBitsTerm :: Term (IntN n) -> Term (IntN n) Source # withSbvBitwiseTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Bits (SBVType n0 (IntN n)) => r) -> r Source # sbvAndBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvOrBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvXorBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvComplementBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalBitwiseTerm (WordN n) Source #
Instance details Methods pevalAndBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalOrBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalXorBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalComplementBitsTerm :: Term (WordN n) -> Term (WordN n) Source # withSbvBitwiseTermConstraint :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Bits (SBVType n0 (WordN n)) => r) -> r Source # sbvAndBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvOrBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvXorBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvComplementBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #