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

Contents

Orphan instances

Description

Synopsis

bvIsNonZeroFromGEq1 :: forall (w :: Natural) r proxy. 1 <= w => proxy w -> (BVIsNonZero w => r) -> r

Documentation

bvIsNonZeroFromGEq1 :: forall (w :: Natural) r proxy. 1 <= w => proxy w -> (BVIsNonZero w => r) -> r Source #

Construct the BVIsNonZero constraint from the proof that the width is at least 1.

Orphan instances

NonFuncSBVRep AlgReal Source #

Instance details

Associated Types

type NonFuncSBVBaseType AlgReal
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type NonFuncSBVBaseType AlgReal = AlgReal

NonFuncSBVRep FPRoundingMode Source #

Instance details

Associated Types

type NonFuncSBVBaseType FPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type NonFuncSBVBaseType FPRoundingMode = RoundingMode

NonFuncSBVRep Integer Source #

Instance details

Associated Types

type NonFuncSBVBaseType Integer
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type NonFuncSBVBaseType Integer = Integer

SBVRep AlgReal Source #

Instance details

Associated Types

type SBVType AlgReal
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type SBVType AlgReal = SBV AlgReal

SBVRep FPRoundingMode Source #

Instance details

Associated Types

type SBVType FPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type SBVType FPRoundingMode = SBV RoundingMode

SBVRep Integer Source #

Instance details

Associated Types

type SBVType Integer
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type SBVType Integer = SBV Integer

SupportedNonFuncPrim AlgReal Source #

Instance details

Methods

conNonFuncSBVTerm :: AlgReal -> SBV (NonFuncSBVBaseType AlgReal) Source #

symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType AlgReal)) Source #

withNonFuncPrim :: (NonFuncPrimConstraint AlgReal => r) -> r Source #

SupportedNonFuncPrim FPRoundingMode Source #

Instance details

Methods

conNonFuncSBVTerm :: FPRoundingMode -> SBV (NonFuncSBVBaseType FPRoundingMode) Source #

symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType FPRoundingMode)) Source #

withNonFuncPrim :: (NonFuncPrimConstraint FPRoundingMode => r) -> r Source #

SupportedNonFuncPrim Integer Source #

Instance details

Methods

conNonFuncSBVTerm :: Integer -> SBV (NonFuncSBVBaseType Integer) Source #

symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType Integer)) Source #

withNonFuncPrim :: (NonFuncPrimConstraint Integer => r) -> r Source #

SupportedPrim AlgReal Source #

Instance details

Methods

primTypeRep :: TypeRep AlgReal Source #

sameCon :: AlgReal -> AlgReal -> Bool Source #

hashConWithSalt :: Int -> AlgReal -> Int Source #

pformatCon :: AlgReal -> String Source #

defaultValue :: AlgReal Source #

pevalITETerm :: Term Bool -> Term AlgReal -> Term AlgReal -> Term AlgReal Source #

pevalEqTerm :: Term AlgReal -> Term AlgReal -> Term Bool Source #

pevalDistinctTerm :: NonEmpty (Term AlgReal) -> Term Bool Source #

conSBVTerm :: AlgReal -> SBVType AlgReal Source #

symSBVName :: TypedSymbol 'AnyKind AlgReal -> Int -> String Source #

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType AlgReal) Source #

withPrim :: ((PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal), Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) => a) -> a Source #

sbvIte :: SBV Bool -> SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal Source #

sbvEq :: SBVType AlgReal -> SBVType AlgReal -> SBV Bool Source #

sbvDistinct :: NonEmpty (SBVType AlgReal) -> SBV Bool Source #

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> AlgReal Source #

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd AlgReal -> Maybe (TypedSymbol knd' AlgReal) Source #

funcDummyConstraint :: SBVType AlgReal -> SBV Bool Source #

SupportedPrim FPRoundingMode Source #

Instance details

Methods

primTypeRep :: TypeRep FPRoundingMode Source #

sameCon :: FPRoundingMode -> FPRoundingMode -> Bool Source #

hashConWithSalt :: Int -> FPRoundingMode -> Int Source #

pformatCon :: FPRoundingMode -> String Source #

defaultValue :: FPRoundingMode Source #

pevalITETerm :: Term Bool -> Term FPRoundingMode -> Term FPRoundingMode -> Term FPRoundingMode Source #

pevalEqTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool Source #

pevalDistinctTerm :: NonEmpty (Term FPRoundingMode) -> Term Bool Source #

conSBVTerm :: FPRoundingMode -> SBVType FPRoundingMode Source #

symSBVName :: TypedSymbol 'AnyKind FPRoundingMode -> Int -> String Source #

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType FPRoundingMode) Source #

withPrim :: ((PrimConstraint FPRoundingMode, SMTDefinable (SBVType FPRoundingMode), Mergeable (SBVType FPRoundingMode), Typeable (SBVType FPRoundingMode)) => a) -> a Source #

sbvIte :: SBV Bool -> SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBVType FPRoundingMode Source #

sbvEq :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool Source #

sbvDistinct :: NonEmpty (SBVType FPRoundingMode) -> SBV Bool Source #

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FPRoundingMode Source #

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd FPRoundingMode -> Maybe (TypedSymbol knd' FPRoundingMode) Source #

funcDummyConstraint :: SBVType FPRoundingMode -> SBV Bool Source #

SupportedPrim Integer Source #

Instance details

Methods

primTypeRep :: TypeRep Integer Source #

sameCon :: Integer -> Integer -> Bool Source #

hashConWithSalt :: Int -> Integer -> Int Source #

pformatCon :: Integer -> String Source #

defaultValue :: Integer Source #

pevalITETerm :: Term Bool -> Term Integer -> Term Integer -> Term Integer Source #

pevalEqTerm :: Term Integer -> Term Integer -> Term Bool Source #

pevalDistinctTerm :: NonEmpty (Term Integer) -> Term Bool Source #

conSBVTerm :: Integer -> SBVType Integer Source #

symSBVName :: TypedSymbol 'AnyKind Integer -> Int -> String Source #

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType Integer) Source #

withPrim :: ((PrimConstraint Integer, SMTDefinable (SBVType Integer), Mergeable (SBVType Integer), Typeable (SBVType Integer)) => a) -> a Source #

sbvIte :: SBV Bool -> SBVType Integer -> SBVType Integer -> SBVType Integer Source #

sbvEq :: SBVType Integer -> SBVType Integer -> SBV Bool Source #

sbvDistinct :: NonEmpty (SBVType Integer) -> SBV Bool Source #

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> Integer Source #

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd Integer -> Maybe (TypedSymbol knd' Integer) Source #

funcDummyConstraint :: SBVType Integer -> SBV Bool Source #

SupportedPrimConstraint AlgReal Source #

Instance details

Associated Types

type PrimConstraint AlgReal
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type PrimConstraint AlgReal = ()

SupportedPrimConstraint FPRoundingMode Source #

Instance details

Associated Types

type PrimConstraint FPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type PrimConstraint FPRoundingMode = ()

SupportedPrimConstraint Integer Source #

Instance details

Associated Types

type PrimConstraint Integer
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type PrimConstraint Integer = Integral (NonFuncSBVBaseType Integer)

(KnownNat w, 1 <= w) => NonFuncSBVRep (IntN w) Source #

Instance details

Associated Types

type NonFuncSBVBaseType (IntN w)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type NonFuncSBVBaseType (IntN w) = IntN w

(KnownNat w, 1 <= w) => NonFuncSBVRep (WordN w) Source #

Instance details

Associated Types

type NonFuncSBVBaseType (WordN w)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type NonFuncSBVBaseType (WordN w) = WordN w

(KnownNat w, 1 <= w) => SBVRep (IntN w) Source #

Instance details

Associated Types

type SBVType (IntN w)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type SBVType (IntN w) = SBV (IntN w)

(KnownNat w, 1 <= w) => SBVRep (WordN w) Source #

Instance details

Associated Types

type SBVType (WordN w)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type SBVType (WordN w) = SBV (WordN w)

(KnownNat w, 1 <= w) => SupportedNonFuncPrim (IntN w) Source #

Instance details

Methods

conNonFuncSBVTerm :: IntN w -> SBV (NonFuncSBVBaseType (IntN w)) Source #

symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType (IntN w))) Source #

withNonFuncPrim :: (NonFuncPrimConstraint (IntN w) => r) -> r Source #

(KnownNat w, 1 <= w) => SupportedNonFuncPrim (WordN w) Source #

Instance details

Methods

conNonFuncSBVTerm :: WordN w -> SBV (NonFuncSBVBaseType (WordN w)) Source #

symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType (WordN w))) Source #

withNonFuncPrim :: (NonFuncPrimConstraint (WordN w) => r) -> r Source #

(KnownNat w, 1 <= w) => SupportedPrim (IntN w) Source #

Instance details

Methods

primTypeRep :: TypeRep (IntN w) Source #

sameCon :: IntN w -> IntN w -> Bool Source #

hashConWithSalt :: Int -> IntN w -> Int Source #

pformatCon :: IntN w -> String Source #

defaultValue :: IntN w Source #

pevalITETerm :: Term Bool -> Term (IntN w) -> Term (IntN w) -> Term (IntN w) Source #

pevalEqTerm :: Term (IntN w) -> Term (IntN w) -> Term Bool Source #

pevalDistinctTerm :: NonEmpty (Term (IntN w)) -> Term Bool Source #

conSBVTerm :: IntN w -> SBVType (IntN w) Source #

symSBVName :: TypedSymbol 'AnyKind (IntN w) -> Int -> String Source #

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (IntN w)) Source #

withPrim :: ((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)), Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) => a) -> a Source #

sbvIte :: SBV Bool -> SBVType (IntN w) -> SBVType (IntN w) -> SBVType (IntN w) Source #

sbvEq :: SBVType (IntN w) -> SBVType (IntN w) -> SBV Bool Source #

sbvDistinct :: NonEmpty (SBVType (IntN w)) -> SBV Bool Source #

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> IntN w Source #

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (IntN w) -> Maybe (TypedSymbol knd' (IntN w)) Source #

funcDummyConstraint :: SBVType (IntN w) -> SBV Bool Source #

(KnownNat w, 1 <= w) => SupportedPrim (WordN w) Source #

Instance details

Methods

primTypeRep :: TypeRep (WordN w) Source #

sameCon :: WordN w -> WordN w -> Bool Source #

hashConWithSalt :: Int -> WordN w -> Int Source #

pformatCon :: WordN w -> String Source #

defaultValue :: WordN w Source #

pevalITETerm :: Term Bool -> Term (WordN w) -> Term (WordN w) -> Term (WordN w) Source #

pevalEqTerm :: Term (WordN w) -> Term (WordN w) -> Term Bool Source #

pevalDistinctTerm :: NonEmpty (Term (WordN w)) -> Term Bool Source #

conSBVTerm :: WordN w -> SBVType (WordN w) Source #

symSBVName :: TypedSymbol 'AnyKind (WordN w) -> Int -> String Source #

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (WordN w)) Source #

withPrim :: ((PrimConstraint (WordN w), SMTDefinable (SBVType (WordN w)), Mergeable (SBVType (WordN w)), Typeable (SBVType (WordN w))) => a) -> a Source #

sbvIte :: SBV Bool -> SBVType (WordN w) -> SBVType (WordN w) -> SBVType (WordN w) Source #

sbvEq :: SBVType (WordN w) -> SBVType (WordN w) -> SBV Bool Source #

sbvDistinct :: NonEmpty (SBVType (WordN w)) -> SBV Bool Source #

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> WordN w Source #

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (WordN w) -> Maybe (TypedSymbol knd' (WordN w)) Source #

funcDummyConstraint :: SBVType (WordN w) -> SBV Bool Source #

(KnownNat w, 1 <= w) => SupportedPrimConstraint (IntN w) Source #

Instance details

Associated Types

type PrimConstraint (IntN w)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type PrimConstraint (IntN w) = (KnownNat w, 1 <= w, BVIsNonZero w)

(KnownNat w, 1 <= w) => SupportedPrimConstraint (WordN w) Source #

Instance details

Associated Types

type PrimConstraint (WordN w)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type PrimConstraint (WordN w) = (KnownNat w, 1 <= w, BVIsNonZero w)

ValidFP eb sb => NonFuncSBVRep (FP eb sb) Source #

Instance details

Associated Types

type NonFuncSBVBaseType (FP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type NonFuncSBVBaseType (FP eb sb) = FloatingPoint eb sb

ValidFP eb sb => SBVRep (FP eb sb) Source #

Instance details

Associated Types

type SBVType (FP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type SBVType (FP eb sb) = SBV (FloatingPoint eb sb)

ValidFP eb sb => SupportedNonFuncPrim (FP eb sb) Source #

Instance details

Methods

conNonFuncSBVTerm :: FP eb sb -> SBV (NonFuncSBVBaseType (FP eb sb)) Source #

symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType (FP eb sb))) Source #

withNonFuncPrim :: (NonFuncPrimConstraint (FP eb sb) => r) -> r Source #

ValidFP eb sb => SupportedPrim (FP eb sb) Source #

Instance details

Methods

primTypeRep :: TypeRep (FP eb sb) Source #

sameCon :: FP eb sb -> FP eb sb -> Bool Source #

hashConWithSalt :: Int -> FP eb sb -> Int Source #

pformatCon :: FP eb sb -> String Source #

defaultValue :: FP eb sb Source #

pevalITETerm :: Term Bool -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalEqTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool Source #

pevalDistinctTerm :: NonEmpty (Term (FP eb sb)) -> Term Bool Source #

conSBVTerm :: FP eb sb -> SBVType (FP eb sb) Source #

symSBVName :: TypedSymbol 'AnyKind (FP eb sb) -> Int -> String Source #

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (FP eb sb)) Source #

withPrim :: ((PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)), Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) => a) -> a Source #

sbvIte :: SBV Bool -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvEq :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool Source #

sbvDistinct :: NonEmpty (SBVType (FP eb sb)) -> SBV Bool Source #

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FP eb sb Source #

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (FP eb sb) -> Maybe (TypedSymbol knd' (FP eb sb)) Source #

funcDummyConstraint :: SBVType (FP eb sb) -> SBV Bool Source #

ValidFP eb sb => SupportedPrimConstraint (FP eb sb) Source #

Instance details

Associated Types

type PrimConstraint (FP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type PrimConstraint (FP eb sb) = ValidFP eb sb