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.PEvalBitCastTerm

Contents

Orphan instances

Description

Synopsis

doPevalBitCast :: (PEvalBitCastTerm a b, SupportedPrim b) => Term a -> Maybe (Term b)

Documentation

doPevalBitCast :: (PEvalBitCastTerm a b, SupportedPrim b) => Term a -> Maybe (Term b) Source #

Partially evaluate a bitcast term. If no reduction is performed, return Nothing.

Orphan instances

PEvalBitCastTerm Bool (IntN 1) Source #
Instance details Methods pevalBitCastTerm :: Term Bool -> Term (IntN 1) Source # sbvBitCast :: SBVType Bool -> SBVType (IntN 1) Source #
PEvalBitCastTerm Bool (WordN 1) Source #
Instance details Methods pevalBitCastTerm :: Term Bool -> Term (WordN 1) Source # sbvBitCast :: SBVType Bool -> SBVType (WordN 1) Source #
PEvalBitCastTerm (IntN 1) Bool Source #
Instance details Methods pevalBitCastTerm :: Term (IntN 1) -> Term Bool Source # sbvBitCast :: SBVType (IntN 1) -> SBVType Bool Source #
PEvalBitCastTerm (WordN 1) Bool Source #
Instance details Methods pevalBitCastTerm :: Term (WordN 1) -> Term Bool Source # sbvBitCast :: SBVType (WordN 1) -> SBVType Bool Source #
(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastTerm (IntN n) (FP eb sb) Source #
Instance details Methods pevalBitCastTerm :: Term (IntN n) -> Term (FP eb sb) Source # sbvBitCast :: SBVType (IntN n) -> SBVType (FP eb sb) Source #
(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastTerm (WordN n) (FP eb sb) Source #
Instance details Methods pevalBitCastTerm :: Term (WordN n) -> Term (FP eb sb) Source # sbvBitCast :: SBVType (WordN n) -> SBVType (FP eb sb) Source #
(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastOrTerm (FP eb sb) (IntN n) Source #
Instance details Methods pevalBitCastOrTerm :: Term (IntN n) -> Term (FP eb sb) -> Term (IntN n) Source # sbvBitCastOr :: SBVType (IntN n) -> SBVType (FP eb sb) -> SBVType (IntN n) Source #
(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastOrTerm (FP eb sb) (WordN n) Source #
Instance details Methods pevalBitCastOrTerm :: Term (WordN n) -> Term (FP eb sb) -> Term (WordN n) Source # sbvBitCastOr :: SBVType (WordN n) -> SBVType (FP eb sb) -> SBVType (WordN n) Source #