grisette-0.6.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 HaskellSafe-Inferred
LanguageHaskell2010

Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm

Description

 

Documentation

Orphan instances

PEvalNumTerm Integer Source # 
Instance details

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

Methods

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

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

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

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

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

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

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

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

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

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

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

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

Methods

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

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

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

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

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

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

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

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

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

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

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

ValidFP eb sb => PEvalNumTerm (FP eb sb) Source # 
Instance details

Methods

pevalAddNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalNegNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source #

pevalMulNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalAbsNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source #

pevalSignumNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source #

withSbvNumTermConstraint :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (Num (SBVType n (FP eb sb)) => r) -> r Source #

sbvAddNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source #

sbvNegNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source #

sbvMulNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source #

sbvAbsNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source #

sbvSignumNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source #