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	None
Language	Haskell2010

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

Contents

Orphan instances

Description

Synopsis

pevalDefaultAddNumTerm :: (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a
pevalDefaultNegNumTerm :: (PEvalNumTerm a, Eq a) => Term a -> Term a

Documentation

pevalDefaultAddNumTerm :: (PEvalNumTerm a, Eq a) => Term a -> Term a -> Term a Source #

Default partial evaluation of addition of numerical terms.

pevalDefaultNegNumTerm :: (PEvalNumTerm a, Eq a) => Term a -> Term a Source #

Default partial evaluation of negation of numerical terms.

Orphan instances

PEvalNumTerm AlgReal Source #
Instance details Methods pevalAddNumTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal Source # pevalNegNumTerm :: Term AlgReal -> Term AlgReal Source # pevalMulNumTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal Source # pevalAbsNumTerm :: Term AlgReal -> Term AlgReal Source # pevalSignumNumTerm :: Term AlgReal -> Term AlgReal Source # withSbvNumTermConstraint :: (Num (SBVType AlgReal) => r) -> r Source # sbvAddNumTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal Source # sbvNegNumTerm :: SBVType AlgReal -> SBVType AlgReal Source # sbvMulNumTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal Source # sbvAbsNumTerm :: SBVType AlgReal -> SBVType AlgReal Source # sbvSignumNumTerm :: SBVType AlgReal -> SBVType AlgReal Source #
PEvalNumTerm Integer Source #
Instance details Methods pevalAddNumTerm :: Term Integer -> Term Integer -> Term Integer Source # pevalNegNumTerm :: Term Integer -> Term Integer Source # pevalMulNumTerm :: Term Integer -> Term Integer -> Term Integer Source # pevalAbsNumTerm :: Term Integer -> Term Integer Source # pevalSignumNumTerm :: Term Integer -> Term Integer Source # withSbvNumTermConstraint :: (Num (SBVType Integer) => r) -> r Source # sbvAddNumTerm :: SBVType Integer -> SBVType Integer -> SBVType Integer Source # sbvNegNumTerm :: SBVType Integer -> SBVType Integer Source # sbvMulNumTerm :: SBVType Integer -> SBVType Integer -> SBVType Integer Source # sbvAbsNumTerm :: SBVType Integer -> SBVType Integer Source # sbvSignumNumTerm :: SBVType Integer -> SBVType Integer Source #
(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 :: (Num (SBVType (IntN n)) => r) -> r Source # sbvAddNumTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvNegNumTerm :: SBVType (IntN n) -> SBVType (IntN n) Source # sbvMulNumTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvAbsNumTerm :: SBVType (IntN n) -> SBVType (IntN n) Source # sbvSignumNumTerm :: SBVType (IntN n) -> SBVType (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 :: (Num (SBVType (WordN n)) => r) -> r Source # sbvAddNumTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvNegNumTerm :: SBVType (WordN n) -> SBVType (WordN n) Source # sbvMulNumTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvAbsNumTerm :: SBVType (WordN n) -> SBVType (WordN n) Source # sbvSignumNumTerm :: SBVType (WordN n) -> SBVType (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 :: (Num (SBVType (FP eb sb)) => r) -> r Source # sbvAddNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvNegNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvMulNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvAbsNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvSignumNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source #