Copyright	(c) Sirui Lu 2021-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.Term

Contents

Supported primitive types
Partial evaluation for the terms
Typed symbols
Terms
Interning
Support for boolean type

Description

Synopsis

class SupportedPrimConstraint t where
- type PrimConstraint t :: Constraint
class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t, SupportedPrimConstraint t, SBVRep t) => SupportedPrim t where
- termCache :: Cache (Term t)
- pformatCon :: t -> String
- pformatSym :: TypedSymbol 'AnyKind t -> String
- defaultValue :: t
- defaultValueDynamic :: proxy t -> ModelValue
- pevalITETerm :: Term Bool -> Term t -> Term t -> Term t
- pevalEqTerm :: Term t -> Term t -> Term Bool
- pevalDistinctTerm :: NonEmpty (Term t) -> Term Bool
- conSBVTerm :: t -> SBVType t
- symSBVName :: TypedSymbol 'AnyKind t -> Int -> String
- symSBVTerm :: SBVFreshMonad m => String -> m (SBVType t)
- withPrim :: ((PrimConstraint t, SMTDefinable (SBVType t), Mergeable (SBVType t), Typeable (SBVType t)) => a) -> a
- sbvIte :: SBV Bool -> SBVType t -> SBVType t -> SBVType t
- sbvEq :: SBVType t -> SBVType t -> SBV Bool
- sbvDistinct :: NonEmpty (SBVType t) -> SBV Bool
- parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> t
- castTypedSymbol :: IsSymbolKind knd' => TypedSymbol knd t -> Maybe (TypedSymbol knd' t)
- isFuncType :: Bool
- funcDummyConstraint :: SBVType t -> SBV Bool
class SupportedPrim con => SymRep con where
- type SymType con
class ConRep sym where
- type ConType sym
class (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) => LinkedRep con sym | con -> sym, sym -> con where
- underlyingTerm :: sym -> Term con
- wrapTerm :: Term con -> sym
class (SupportedPrim arg, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => UnaryOp tag arg t | tag arg -> t where
- pevalUnary :: (Typeable tag, Typeable t) => tag -> Term arg -> Term t
- pformatUnary :: tag -> Term arg -> String
class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => BinaryOp tag arg1 arg2 t | tag arg1 arg2 -> t where
- pevalBinary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term t
- pformatBinary :: tag -> Term arg1 -> Term arg2 -> String
class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim arg3, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => TernaryOp tag arg1 arg2 arg3 t | tag arg1 arg2 arg3 -> t where
- pevalTernary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
- pformatTernary :: tag -> Term arg1 -> Term arg2 -> Term arg3 -> String
class (SupportedPrim f, SupportedPrim a, SupportedPrim b) => PEvalApplyTerm f a b | f -> a b where
- pevalApplyTerm :: Term f -> Term a -> Term b
- sbvApplyTerm :: SBVType f -> SBVType a -> SBVType b
class (SupportedNonFuncPrim t, Bits t) => PEvalBitwiseTerm t where
- pevalAndBitsTerm :: Term t -> Term t -> Term t
- pevalOrBitsTerm :: Term t -> Term t -> Term t
- pevalXorBitsTerm :: Term t -> Term t -> Term t
- pevalComplementBitsTerm :: Term t -> Term t
- withSbvBitwiseTermConstraint :: (Bits (SBVType t) => r) -> r
- sbvAndBitsTerm :: SBVType t -> SBVType t -> SBVType t
- sbvOrBitsTerm :: SBVType t -> SBVType t -> SBVType t
- sbvXorBitsTerm :: SBVType t -> SBVType t -> SBVType t
- sbvComplementBitsTerm :: SBVType t -> SBVType t
class (SupportedNonFuncPrim t, SymShift t) => PEvalShiftTerm t where
- pevalShiftLeftTerm :: Term t -> Term t -> Term t
- pevalShiftRightTerm :: Term t -> Term t -> Term t
- withSbvShiftTermConstraint :: (SIntegral (NonFuncSBVBaseType t) => r) -> r
- sbvShiftLeftTerm :: SBVType t -> SBVType t -> SBVType t
- sbvShiftRightTerm :: SBVType t -> SBVType t -> SBVType t
class (SupportedNonFuncPrim t, SymRotate t) => PEvalRotateTerm t where
- pevalRotateLeftTerm :: Term t -> Term t -> Term t
- pevalRotateRightTerm :: Term t -> Term t -> Term t
- withSbvRotateTermConstraint :: (SIntegral (NonFuncSBVBaseType t) => r) -> r
- sbvRotateLeftTerm :: SBVType t -> SBVType t -> SBVType t
- sbvRotateRightTerm :: SBVType t -> SBVType t -> SBVType t
class (SupportedNonFuncPrim t, Num t) => PEvalNumTerm t where
- pevalAddNumTerm :: Term t -> Term t -> Term t
- pevalNegNumTerm :: Term t -> Term t
- pevalMulNumTerm :: Term t -> Term t -> Term t
- pevalAbsNumTerm :: Term t -> Term t
- pevalSignumNumTerm :: Term t -> Term t
- withSbvNumTermConstraint :: (Num (SBVType t) => r) -> r
- sbvAddNumTerm :: SBVType t -> SBVType t -> SBVType t
- sbvNegNumTerm :: SBVType t -> SBVType t
- sbvMulNumTerm :: SBVType t -> SBVType t -> SBVType t
- sbvAbsNumTerm :: SBVType t -> SBVType t
- sbvSignumNumTerm :: SBVType t -> SBVType t
pevalSubNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a
class (SupportedNonFuncPrim t, Ord t) => PEvalOrdTerm t where
- pevalLtOrdTerm :: Term t -> Term t -> Term Bool
- pevalLeOrdTerm :: Term t -> Term t -> Term Bool
- withSbvOrdTermConstraint :: (OrdSymbolic (SBVType t) => r) -> r
- sbvLtOrdTerm :: SBVType t -> SBVType t -> SBV Bool
- sbvLeOrdTerm :: SBVType t -> SBVType t -> SBV Bool
pevalGtOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalNEqTerm :: SupportedPrim a => Term a -> Term a -> Term Bool
class (SupportedNonFuncPrim t, Integral t) => PEvalDivModIntegralTerm t where
- pevalDivIntegralTerm :: Term t -> Term t -> Term t
- pevalModIntegralTerm :: Term t -> Term t -> Term t
- pevalQuotIntegralTerm :: Term t -> Term t -> Term t
- pevalRemIntegralTerm :: Term t -> Term t -> Term t
- withSbvDivModIntegralTermConstraint :: (SDivisible (SBVType t) => r) -> r
- sbvDivIntegralTerm :: SBVType t -> SBVType t -> SBVType t
- sbvModIntegralTerm :: SBVType t -> SBVType t -> SBVType t
- sbvQuotIntegralTerm :: SBVType t -> SBVType t -> SBVType t
- sbvRemIntegralTerm :: SBVType t -> SBVType t -> SBVType t
class (SupportedNonFuncPrim a, SupportedNonFuncPrim b, BitCast a b) => PEvalBitCastTerm a b where
- pevalBitCastTerm :: Term a -> Term b
- sbvBitCast :: SBVType a -> SBVType b
class (SupportedNonFuncPrim a, SupportedNonFuncPrim b, BitCastOr a b) => PEvalBitCastOrTerm a b where
- pevalBitCastOrTerm :: Term b -> Term a -> Term b
- sbvBitCastOr :: SBVType b -> SBVType a -> SBVType b
class (forall n. (KnownNat n, 1 <= n) => SupportedNonFuncPrim (bv n), SizedBV bv, Typeable bv) => PEvalBVTerm bv where
- pevalBVConcatTerm :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (bv l) -> Term (bv r) -> Term (bv (l + r))
- pevalBVExtendTerm :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (bv l) -> Term (bv r)
- pevalBVSelectTerm :: (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (bv n) -> Term (bv w)
- sbvBVConcatTerm :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p1 l -> p2 r -> SBVType (bv l) -> SBVType (bv r) -> SBVType (bv (l + r))
- sbvBVExtendTerm :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p1 l -> p2 r -> Bool -> SBVType (bv l) -> SBVType (bv r)
- sbvBVSelectTerm :: (KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p1 ix -> p2 w -> p3 n -> SBVType (bv n) -> SBVType (bv w)
class (SupportedNonFuncPrim t, Fractional t) => PEvalFractionalTerm t where
- pevalFdivTerm :: Term t -> Term t -> Term t
- pevalRecipTerm :: Term t -> Term t
- withSbvFractionalTermConstraint :: (Fractional (SBVType t) => r) -> r
- sbvFdivTerm :: SBVType t -> SBVType t -> SBVType t
- sbvRecipTerm :: SBVType t -> SBVType t
class SupportedNonFuncPrim t => PEvalFloatingTerm t where
- pevalFloatingUnaryTerm :: FloatingUnaryOp -> Term t -> Term t
- pevalPowerTerm :: Term t -> Term t -> Term t
- withSbvFloatingTermConstraint :: (Floating (SBVType t) => r) -> r
- sbvPowerTerm :: SBVType t -> SBVType t -> SBVType t
- sbvFloatingUnaryTerm :: FloatingUnaryOp -> SBVType t -> SBVType t
class (SupportedNonFuncPrim a, SupportedNonFuncPrim b, Integral a, Num b) => PEvalFromIntegralTerm a b where
- pevalFromIntegralTerm :: Term a -> Term b
- sbvFromIntegralTerm :: SBVType a -> SBVType b
class SupportedNonFuncPrim a => PEvalIEEEFPConvertibleTerm a where
- pevalFromFPOrTerm :: ValidFP eb sb => Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
- pevalToFPTerm :: ValidFP eb sb => Term FPRoundingMode -> Term a -> Term (FP eb sb)
- sbvFromFPOrTerm :: ValidFP eb sb => SBVType a -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType a
- sbvToFPTerm :: ValidFP eb sb => SBVType FPRoundingMode -> SBVType a -> SBVType (FP eb sb)
data SymbolKind
- = ConstantKind
- | AnyKind
data TypedSymbol (knd :: SymbolKind) t where
- TypedSymbol :: (SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) => {..} -> TypedSymbol knd t
type TypedConstantSymbol = TypedSymbol 'ConstantKind
type TypedAnySymbol = TypedSymbol 'AnyKind
data SomeTypedSymbol knd where
- SomeTypedSymbol :: forall knd t. TypeRep t -> TypedSymbol knd t -> SomeTypedSymbol knd
type SomeTypedConstantSymbol = SomeTypedSymbol 'ConstantKind
type SomeTypedAnySymbol = SomeTypedSymbol 'AnyKind
class IsSymbolKind (ty :: SymbolKind) where
- type SymbolKindConstraint ty :: Type -> Constraint
- decideSymbolKind :: Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind)
showUntyped :: TypedSymbol knd t -> String
withSymbolSupported :: TypedSymbol knd t -> (SupportedPrim t => a) -> a
someTypedSymbol :: forall knd t. TypedSymbol knd t -> SomeTypedSymbol knd
eqHeteroSymbol :: forall ta a tb b. TypedSymbol ta a -> TypedSymbol tb b -> Bool
castSomeTypedSymbol :: IsSymbolKind knd' => SomeTypedSymbol knd -> Maybe (SomeTypedSymbol knd')
withSymbolKind :: TypedSymbol knd t -> (IsSymbolKind knd => a) -> a
data FPTrait
- = FPIsNaN
- | FPIsPositive
- | FPIsNegative
- | FPIsPositiveInfinite
- | FPIsNegativeInfinite
- | FPIsInfinite
- | FPIsPositiveZero
- | FPIsNegativeZero
- | FPIsZero
- | FPIsNormal
- | FPIsSubnormal
- | FPIsPoint
data FPUnaryOp
- = FPAbs
- | FPNeg
data FPBinaryOp
- = FPRem
- | FPMinimum
- | FPMinimumNumber
- | FPMaximum
- | FPMaximumNumber
data FPRoundingUnaryOp
- = FPSqrt
- | FPRoundToIntegral
data FPRoundingBinaryOp
- = FPAdd
- | FPSub
- | FPMul
- | FPDiv
data FloatingUnaryOp
- = FloatingExp
- | FloatingLog
- | FloatingSqrt
- | FloatingSin
- | FloatingCos
- | FloatingTan
- | FloatingAsin
- | FloatingAcos
- | FloatingAtan
- | FloatingSinh
- | FloatingCosh
- | FloatingTanh
- | FloatingAsinh
- | FloatingAcosh
- | FloatingAtanh
data Term t where
- ConTerm :: SupportedPrim t => !Id -> !t -> Term t
- SymTerm :: SupportedPrim t => !Id -> !(TypedSymbol 'AnyKind t) -> Term t
- ForallTerm :: SupportedNonFuncPrim t => !Id -> !(TypedSymbol 'ConstantKind t) -> !(Term Bool) -> Term Bool
- ExistsTerm :: SupportedNonFuncPrim t => !Id -> !(TypedSymbol 'ConstantKind t) -> !(Term Bool) -> Term Bool
- UnaryTerm :: UnaryOp tag arg t => !Id -> !tag -> !(Term arg) -> Term t
- BinaryTerm :: BinaryOp tag arg1 arg2 t => !Id -> !tag -> !(Term arg1) -> !(Term arg2) -> Term t
- TernaryTerm :: TernaryOp tag arg1 arg2 arg3 t => !Id -> !tag -> !(Term arg1) -> !(Term arg2) -> !(Term arg3) -> Term t
- NotTerm :: !Id -> !(Term Bool) -> Term Bool
- OrTerm :: !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
- AndTerm :: !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
- EqTerm :: SupportedNonFuncPrim t => !Id -> !(Term t) -> !(Term t) -> Term Bool
- DistinctTerm :: SupportedNonFuncPrim t => !Id -> !(NonEmpty (Term t)) -> Term Bool
- ITETerm :: SupportedPrim t => !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t
- AddNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- NegNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> Term t
- MulNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- AbsNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> Term t
- SignumNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> Term t
- LtOrdTerm :: PEvalOrdTerm t => !Id -> !(Term t) -> !(Term t) -> Term Bool
- LeOrdTerm :: PEvalOrdTerm t => !Id -> !(Term t) -> !(Term t) -> Term Bool
- AndBitsTerm :: PEvalBitwiseTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- OrBitsTerm :: PEvalBitwiseTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- XorBitsTerm :: PEvalBitwiseTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- ComplementBitsTerm :: PEvalBitwiseTerm t => !Id -> !(Term t) -> Term t
- ShiftLeftTerm :: PEvalShiftTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- ShiftRightTerm :: PEvalShiftTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- RotateLeftTerm :: PEvalRotateTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- RotateRightTerm :: PEvalRotateTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- BitCastTerm :: PEvalBitCastTerm a b => !Id -> !(Term a) -> Term b
- BitCastOrTerm :: PEvalBitCastOrTerm a b => !Id -> !(Term b) -> !(Term a) -> Term b
- BVConcatTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r)) => !Id -> !(Term (bv l)) -> !(Term (bv r)) -> Term (bv (l + r))
- BVSelectTerm :: (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => !Id -> !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv n)) -> Term (bv w)
- BVExtendTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => !Id -> !Bool -> !(TypeRep r) -> !(Term (bv l)) -> Term (bv r)
- ApplyTerm :: (SupportedPrim a, SupportedPrim b, SupportedPrim f, PEvalApplyTerm f a b) => !Id -> !(Term f) -> !(Term a) -> Term b
- DivIntegralTerm :: PEvalDivModIntegralTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- ModIntegralTerm :: PEvalDivModIntegralTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- QuotIntegralTerm :: PEvalDivModIntegralTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- RemIntegralTerm :: PEvalDivModIntegralTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- FPTraitTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => !Id -> !FPTrait -> !(Term (FP eb sb)) -> Term Bool
- FdivTerm :: PEvalFractionalTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- RecipTerm :: PEvalFractionalTerm t => !Id -> !(Term t) -> Term t
- FloatingUnaryTerm :: PEvalFloatingTerm t => !Id -> !FloatingUnaryOp -> !(Term t) -> Term t
- PowerTerm :: PEvalFloatingTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- FPUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => !Id -> !FPUnaryOp -> !(Term (FP eb sb)) -> Term (FP eb sb)
- FPBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => !Id -> !FPBinaryOp -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> Term (FP eb sb)
- FPRoundingUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !Id -> !FPRoundingUnaryOp -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> Term (FP eb sb)
- FPRoundingBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !Id -> !FPRoundingBinaryOp -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> Term (FP eb sb)
- FPFMATerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !Id -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> Term (FP eb sb)
- FromIntegralTerm :: PEvalFromIntegralTerm a b => !Id -> !(Term a) -> Term b
- FromFPOrTerm :: (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !Id -> !(Term a) -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> Term a
- ToFPTerm :: (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !Id -> !(Term FPRoundingMode) -> !(Term a) -> Proxy eb -> Proxy sb -> Term (FP eb sb)
identity :: Term t -> Id
identityWithTypeRep :: forall t. Term t -> (SomeTypeRep, Id)
introSupportedPrimConstraint :: forall t a. Term t -> (SupportedPrim t => a) -> a
pformatTerm :: forall t. SupportedPrim t => Term t -> String
data UTerm t where
- UConTerm :: SupportedPrim t => !t -> UTerm t
- USymTerm :: SupportedPrim t => !(TypedSymbol 'AnyKind t) -> UTerm t
- UForallTerm :: SupportedNonFuncPrim t => !(TypedSymbol 'ConstantKind t) -> !(Term Bool) -> UTerm Bool
- UExistsTerm :: SupportedNonFuncPrim t => !(TypedSymbol 'ConstantKind t) -> !(Term Bool) -> UTerm Bool
- UUnaryTerm :: UnaryOp tag arg t => !tag -> !(Term arg) -> UTerm t
- UBinaryTerm :: BinaryOp tag arg1 arg2 t => !tag -> !(Term arg1) -> !(Term arg2) -> UTerm t
- UTernaryTerm :: TernaryOp tag arg1 arg2 arg3 t => !tag -> !(Term arg1) -> !(Term arg2) -> !(Term arg3) -> UTerm t
- UNotTerm :: !(Term Bool) -> UTerm Bool
- UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
- UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
- UEqTerm :: SupportedNonFuncPrim t => !(Term t) -> !(Term t) -> UTerm Bool
- UDistinctTerm :: SupportedNonFuncPrim t => !(NonEmpty (Term t)) -> UTerm Bool
- UITETerm :: SupportedPrim t => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
- UAddNumTerm :: PEvalNumTerm t => !(Term t) -> !(Term t) -> UTerm t
- UNegNumTerm :: PEvalNumTerm t => !(Term t) -> UTerm t
- UMulNumTerm :: PEvalNumTerm t => !(Term t) -> !(Term t) -> UTerm t
- UAbsNumTerm :: PEvalNumTerm t => !(Term t) -> UTerm t
- USignumNumTerm :: PEvalNumTerm t => !(Term t) -> UTerm t
- ULtOrdTerm :: PEvalOrdTerm t => !(Term t) -> !(Term t) -> UTerm Bool
- ULeOrdTerm :: PEvalOrdTerm t => !(Term t) -> !(Term t) -> UTerm Bool
- UAndBitsTerm :: PEvalBitwiseTerm t => !(Term t) -> !(Term t) -> UTerm t
- UOrBitsTerm :: PEvalBitwiseTerm t => !(Term t) -> !(Term t) -> UTerm t
- UXorBitsTerm :: PEvalBitwiseTerm t => !(Term t) -> !(Term t) -> UTerm t
- UComplementBitsTerm :: PEvalBitwiseTerm t => !(Term t) -> UTerm t
- UShiftLeftTerm :: PEvalShiftTerm t => !(Term t) -> !(Term t) -> UTerm t
- UShiftRightTerm :: PEvalShiftTerm t => !(Term t) -> !(Term t) -> UTerm t
- URotateLeftTerm :: PEvalRotateTerm t => !(Term t) -> !(Term t) -> UTerm t
- URotateRightTerm :: PEvalRotateTerm t => !(Term t) -> !(Term t) -> UTerm t
- UBitCastTerm :: PEvalBitCastTerm a b => !(Term a) -> UTerm b
- UBitCastOrTerm :: PEvalBitCastOrTerm a b => !(Term b) -> !(Term a) -> UTerm b
- UBVConcatTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r)) => !(Term (bv l)) -> !(Term (bv r)) -> UTerm (bv (l + r))
- UBVSelectTerm :: (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv n)) -> UTerm (bv w)
- UBVExtendTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => !Bool -> !(TypeRep r) -> !(Term (bv l)) -> UTerm (bv r)
- UApplyTerm :: (SupportedPrim a, SupportedPrim b, SupportedPrim f, PEvalApplyTerm f a b) => Term f -> Term a -> UTerm b
- UDivIntegralTerm :: PEvalDivModIntegralTerm t => !(Term t) -> !(Term t) -> UTerm t
- UModIntegralTerm :: PEvalDivModIntegralTerm t => !(Term t) -> !(Term t) -> UTerm t
- UQuotIntegralTerm :: PEvalDivModIntegralTerm t => !(Term t) -> !(Term t) -> UTerm t
- URemIntegralTerm :: PEvalDivModIntegralTerm t => !(Term t) -> !(Term t) -> UTerm t
- UFPTraitTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => !FPTrait -> !(Term (FP eb sb)) -> UTerm Bool
- UFdivTerm :: PEvalFractionalTerm t => !(Term t) -> !(Term t) -> UTerm t
- URecipTerm :: PEvalFractionalTerm t => !(Term t) -> UTerm t
- UFloatingUnaryTerm :: PEvalFloatingTerm t => !FloatingUnaryOp -> !(Term t) -> UTerm t
- UPowerTerm :: PEvalFloatingTerm t => !(Term t) -> !(Term t) -> UTerm t
- UFPUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => !FPUnaryOp -> !(Term (FP eb sb)) -> UTerm (FP eb sb)
- UFPBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => !FPBinaryOp -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> UTerm (FP eb sb)
- UFPRoundingUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !FPRoundingUnaryOp -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> UTerm (FP eb sb)
- UFPRoundingBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !FPRoundingBinaryOp -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> UTerm (FP eb sb)
- UFPFMATerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> UTerm (FP eb sb)
- UFromIntegralTerm :: PEvalFromIntegralTerm a b => !(Term a) -> UTerm b
- UFromFPOrTerm :: (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim FPRoundingMode, SupportedPrim (FP eb sb)) => Term a -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> UTerm a
- UToFPTerm :: (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim FPRoundingMode, SupportedPrim (FP eb sb)) => !(Term FPRoundingMode) -> !(Term a) -> Proxy eb -> Proxy sb -> UTerm (FP eb sb)
prettyPrintTerm :: Term t -> Doc ann
forallTerm :: (SupportedNonFuncPrim t, Typeable t) => TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool
existsTerm :: (SupportedNonFuncPrim t, Typeable t) => TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool
constructUnary :: forall tag arg t. (SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t, Show tag) => tag -> Term arg -> Term t
constructBinary :: forall tag arg1 arg2 t. (SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term t
constructTernary :: forall tag arg1 arg2 arg3 t. (SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
conTerm :: (SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) => t -> Term t
symTerm :: forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
ssymTerm :: (SupportedPrim t, Typeable t) => Identifier -> Term t
isymTerm :: (SupportedPrim t, Typeable t) => Identifier -> Int -> Term t
notTerm :: Term Bool -> Term Bool
orTerm :: Term Bool -> Term Bool -> Term Bool
andTerm :: Term Bool -> Term Bool -> Term Bool
eqTerm :: SupportedNonFuncPrim a => Term a -> Term a -> Term Bool
distinctTerm :: SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
iteTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a
addNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a
negNumTerm :: PEvalNumTerm a => Term a -> Term a
mulNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a
absNumTerm :: PEvalNumTerm a => Term a -> Term a
signumNumTerm :: PEvalNumTerm a => Term a -> Term a
ltOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool
leOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool
andBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a -> Term a
orBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a -> Term a
xorBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a -> Term a
complementBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a
shiftLeftTerm :: PEvalShiftTerm a => Term a -> Term a -> Term a
shiftRightTerm :: PEvalShiftTerm a => Term a -> Term a -> Term a
rotateLeftTerm :: PEvalRotateTerm a => Term a -> Term a -> Term a
rotateRightTerm :: PEvalRotateTerm a => Term a -> Term a -> Term a
bitCastTerm :: PEvalBitCastTerm a b => Term a -> Term b
bitCastOrTerm :: PEvalBitCastOrTerm a b => Term b -> Term a -> Term b
bvconcatTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r)) => Term (bv l) -> Term (bv r) -> Term (bv (l + r))
bvselectTerm :: forall bv n ix w p q. (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (bv n) -> Term (bv w)
bvextendTerm :: forall bv l r proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (bv l) -> Term (bv r)
bvsignExtendTerm :: forall bv l r proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => proxy r -> Term (bv l) -> Term (bv r)
bvzeroExtendTerm :: forall bv l r proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => proxy r -> Term (bv l) -> Term (bv r)
applyTerm :: (SupportedPrim a, SupportedPrim b, SupportedPrim f, PEvalApplyTerm f a b) => Term f -> Term a -> Term b
divIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
modIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
quotIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
remIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
fpTraitTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPTrait -> Term (FP eb sb) -> Term Bool
fdivTerm :: PEvalFractionalTerm a => Term a -> Term a -> Term a
recipTerm :: PEvalFractionalTerm a => Term a -> Term a
floatingUnaryTerm :: PEvalFloatingTerm a => FloatingUnaryOp -> Term a -> Term a
powerTerm :: PEvalFloatingTerm a => Term a -> Term a -> Term a
fpUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
fpBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
fpRoundingUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
fpRoundingBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
fpFMATerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
fromIntegralTerm :: PEvalFromIntegralTerm a b => Term a -> Term b
fromFPOrTerm :: (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim FPRoundingMode, SupportedPrim (FP eb sb)) => Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
toFPTerm :: forall a eb sb. (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim FPRoundingMode, SupportedPrim (FP eb sb)) => Term FPRoundingMode -> Term a -> Term (FP eb sb)
trueTerm :: Term Bool
falseTerm :: Term Bool
pattern BoolConTerm :: Bool -> Term a
pattern TrueTerm :: Term a
pattern FalseTerm :: Term a
pattern BoolTerm :: Term Bool -> Term a
pevalNotTerm :: Term Bool -> Term Bool
pevalOrTerm :: Term Bool -> Term Bool -> Term Bool
pevalAndTerm :: Term Bool -> Term Bool -> Term Bool
pevalImplyTerm :: Term Bool -> Term Bool -> Term Bool
pevalXorTerm :: Term Bool -> Term Bool -> Term Bool
pevalITEBasic :: SupportedPrim a => Term Bool -> Term a -> Term a -> Maybe (Term a)
pevalITEBasicTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a
pevalDefaultEqTerm :: SupportedNonFuncPrim a => Term a -> Term a -> Term Bool
type NonFuncPrimConstraint a = (SymVal (NonFuncSBVBaseType a), EqSymbolic (SBVType a), Mergeable (SBVType a), SMTDefinable (SBVType a), Mergeable (SBVType a), SBVType a ~ SBV (NonFuncSBVBaseType a), PrimConstraint a)
class (SupportedPrim a, Ord a) => NonFuncSBVRep a where
- type NonFuncSBVBaseType a
class NonFuncSBVRep a => SupportedNonFuncPrim a where
- conNonFuncSBVTerm :: a -> SBV (NonFuncSBVBaseType a)
- symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType a))
- withNonFuncPrim :: (NonFuncPrimConstraint a => r) -> r
class SBVRep t where
- type SBVType t
class Monad m => SBVFreshMonad m where
- sbvFresh :: SymVal a => String -> m (SBV a)
translateTypeError :: HasCallStack => Maybe String -> TypeRep a -> b
parseSMTModelResultError :: HasCallStack => TypeRep a -> ([([CV], CV)], CV) -> a
partitionCVArg :: forall a. SupportedNonFuncPrim a => [([CV], CV)] -> [(a, [([CV], CV)])]
parseScalarSMTModelResult :: forall v r. (SatModel r, Typeable v) => (r -> v) -> ([([CV], CV)], CV) -> v

Supported primitive types

class SupportedPrimConstraint t Source #

Type class for resolving the constraint for a supported primitive type.

Associated Types

type PrimConstraint t :: Constraint Source #

type PrimConstraint _ = ()

Instances

Instances details

SupportedPrimConstraint AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type PrimConstraint AlgReal Source #
SupportedPrimConstraint FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type PrimConstraint FPRoundingMode Source #
SupportedPrimConstraint Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type PrimConstraint Integer Source #
SupportedPrimConstraint Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type PrimConstraint Bool Source #
(KnownNat w, 1 <= w) => SupportedPrimConstraint (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type PrimConstraint (IntN w) Source #
(KnownNat w, 1 <= w) => SupportedPrimConstraint (WordN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type PrimConstraint (WordN w) Source #
ValidFP eb sb => SupportedPrimConstraint (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type PrimConstraint (FP eb sb) Source #
(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Associated Types type PrimConstraint (a --> b) Source #
(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Associated Types type PrimConstraint (a =-> b) Source #

class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t, SupportedPrimConstraint t, SBVRep t) => SupportedPrim t where Source #

Indicates that a type is supported, can be represented as a symbolic term, and can be lowered to an SBV term.

Minimal complete definition

defaultValue, pevalITETerm, pevalEqTerm, pevalDistinctTerm, conSBVTerm, symSBVName, symSBVTerm, parseSMTModelResult, castTypedSymbol, isFuncType, funcDummyConstraint

Methods

termCache :: Cache (Term t) Source #

pformatCon :: t -> String Source #

default pformatCon :: Show t => t -> String Source #

pformatSym :: TypedSymbol 'AnyKind t -> String Source #

defaultValue :: t Source #

defaultValueDynamic :: proxy t -> ModelValue Source #

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

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

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

conSBVTerm :: t -> SBVType t Source #

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

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

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

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

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

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

default sbvEq :: EqSymbolic (SBVType t) => SBVType t -> SBVType t -> SBV Bool Source #

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

default sbvDistinct :: EqSymbolic (SBVType t) => NonEmpty (SBVType t) -> SBV Bool Source #

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

castTypedSymbol :: IsSymbolKind knd' => TypedSymbol knd t -> Maybe (TypedSymbol knd' t) Source #

isFuncType :: Bool Source #

funcDummyConstraint :: SBVType t -> SBV Bool Source #

Instances

Instances details

SupportedPrim AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods termCache :: Cache (Term AlgReal) Source # pformatCon :: AlgReal -> String Source # pformatSym :: TypedSymbol 'AnyKind AlgReal -> String Source # defaultValue :: AlgReal Source # defaultValueDynamic :: proxy AlgReal -> ModelValue 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 # isFuncType :: Bool Source # funcDummyConstraint :: SBVType AlgReal -> SBV Bool Source #
SupportedPrim FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods termCache :: Cache (Term FPRoundingMode) Source # pformatCon :: FPRoundingMode -> String Source # pformatSym :: TypedSymbol 'AnyKind FPRoundingMode -> String Source # defaultValue :: FPRoundingMode Source # defaultValueDynamic :: proxy FPRoundingMode -> ModelValue 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 # isFuncType :: Bool Source # funcDummyConstraint :: SBVType FPRoundingMode -> SBV Bool Source #
SupportedPrim Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods termCache :: Cache (Term Integer) Source # pformatCon :: Integer -> String Source # pformatSym :: TypedSymbol 'AnyKind Integer -> String Source # defaultValue :: Integer Source # defaultValueDynamic :: proxy Integer -> ModelValue 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 # isFuncType :: Bool Source # funcDummyConstraint :: SBVType Integer -> SBV Bool Source #
SupportedPrim Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods termCache :: Cache (Term Bool) Source # pformatCon :: Bool -> String Source # pformatSym :: TypedSymbol 'AnyKind Bool -> String Source # defaultValue :: Bool Source # defaultValueDynamic :: proxy Bool -> ModelValue Source # pevalITETerm :: Term Bool -> Term Bool -> Term Bool -> Term Bool Source # pevalEqTerm :: Term Bool -> Term Bool -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term Bool) -> Term Bool Source # conSBVTerm :: Bool -> SBVType Bool Source # symSBVName :: TypedSymbol 'AnyKind Bool -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType Bool) Source # withPrim :: ((PrimConstraint Bool, SMTDefinable (SBVType Bool), Mergeable (SBVType Bool), Typeable (SBVType Bool)) => a) -> a Source # sbvIte :: SBV Bool -> SBVType Bool -> SBVType Bool -> SBVType Bool Source # sbvEq :: SBVType Bool -> SBVType Bool -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType Bool) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> Bool Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd Bool -> Maybe (TypedSymbol knd' Bool) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType Bool -> SBV Bool Source #
(KnownNat w, 1 <= w) => SupportedPrim (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods termCache :: Cache (Term (IntN w)) Source # pformatCon :: IntN w -> String Source # pformatSym :: TypedSymbol 'AnyKind (IntN w) -> String Source # defaultValue :: IntN w Source # defaultValueDynamic :: proxy (IntN w) -> ModelValue 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 # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (IntN w) -> SBV Bool Source #
(KnownNat w, 1 <= w) => SupportedPrim (WordN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods termCache :: Cache (Term (WordN w)) Source # pformatCon :: WordN w -> String Source # pformatSym :: TypedSymbol 'AnyKind (WordN w) -> String Source # defaultValue :: WordN w Source # defaultValueDynamic :: proxy (WordN w) -> ModelValue 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 # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (WordN w) -> SBV Bool Source #
ValidFP eb sb => SupportedPrim (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods termCache :: Cache (Term (FP eb sb)) Source # pformatCon :: FP eb sb -> String Source # pformatSym :: TypedSymbol 'AnyKind (FP eb sb) -> String Source # defaultValue :: FP eb sb Source # defaultValueDynamic :: proxy (FP eb sb) -> ModelValue 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 # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (FP eb sb) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4, SupportedNonFuncPrim a5, SupportedNonFuncPrim a6, SupportedNonFuncPrim a7) => SupportedPrim (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7)))))))) Source # pformatCon :: (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> String Source # defaultValue :: a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7)))))) Source # defaultValueDynamic :: proxy (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) Source # pevalEqTerm :: Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7)))))))) -> Term Bool Source # conSBVTerm :: (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7)))))))) Source # withPrim :: ((PrimConstraint (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))), SMTDefinable (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7)))))))), Mergeable (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7)))))))), Typeable (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) Source # sbvEq :: SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7)))))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7)))))) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> Maybe (TypedSymbol knd' (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7)))))))) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> (a6 --> a7))))))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4, SupportedNonFuncPrim a5, SupportedNonFuncPrim a6) => SupportedPrim (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6))))))) Source # pformatCon :: (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> String Source # defaultValue :: a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6))))) Source # defaultValueDynamic :: proxy (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) Source # pevalEqTerm :: Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6))))))) -> Term Bool Source # conSBVTerm :: (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6))))))) Source # withPrim :: ((PrimConstraint (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))), SMTDefinable (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6))))))), Mergeable (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6))))))), Typeable (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) Source # sbvEq :: SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6))))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6))))) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> Maybe (TypedSymbol knd' (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6))))))) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> (a5 --> a6)))))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4, SupportedNonFuncPrim a5) => SupportedPrim (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5)))))) Source # pformatCon :: (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> String Source # defaultValue :: a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5)))) Source # defaultValueDynamic :: proxy (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) Source # pevalEqTerm :: Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5)))))) -> Term Bool Source # conSBVTerm :: (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5)))))) Source # withPrim :: ((PrimConstraint (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))), SMTDefinable (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5)))))), Mergeable (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5)))))), Typeable (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) Source # sbvEq :: SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5)))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5)))) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> Maybe (TypedSymbol knd' (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5)))))) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 --> (a1 --> (a2 --> (a3 --> (a4 --> a5))))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4) => SupportedPrim (a0 --> (a1 --> (a2 --> (a3 --> a4)))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a0 --> (a1 --> (a2 --> (a3 --> a4))))) Source # pformatCon :: (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> String Source # defaultValue :: a0 --> (a1 --> (a2 --> (a3 --> a4))) Source # defaultValueDynamic :: proxy (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> Term (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> Term (a0 --> (a1 --> (a2 --> (a3 --> a4)))) Source # pevalEqTerm :: Term (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> Term (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 --> (a1 --> (a2 --> (a3 --> a4))))) -> Term Bool Source # conSBVTerm :: (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> a4)))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 --> (a1 --> (a2 --> (a3 --> a4))))) Source # withPrim :: ((PrimConstraint (a0 --> (a1 --> (a2 --> (a3 --> a4)))), SMTDefinable (SBVType (a0 --> (a1 --> (a2 --> (a3 --> a4))))), Mergeable (SBVType (a0 --> (a1 --> (a2 --> (a3 --> a4))))), Typeable (SBVType (a0 --> (a1 --> (a2 --> (a3 --> a4)))))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> a4)))) Source # sbvEq :: SBVType (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> SBVType (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 --> (a1 --> (a2 --> (a3 --> a4))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 --> (a1 --> (a2 --> (a3 --> a4))) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> Maybe (TypedSymbol knd' (a0 --> (a1 --> (a2 --> (a3 --> a4))))) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 --> (a1 --> (a2 --> (a3 --> a4)))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3) => SupportedPrim (a0 --> (a1 --> (a2 --> a3))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a0 --> (a1 --> (a2 --> a3)))) Source # pformatCon :: (a0 --> (a1 --> (a2 --> a3))) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 --> (a1 --> (a2 --> a3))) -> String Source # defaultValue :: a0 --> (a1 --> (a2 --> a3)) Source # defaultValueDynamic :: proxy (a0 --> (a1 --> (a2 --> a3))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 --> (a1 --> (a2 --> a3))) -> Term (a0 --> (a1 --> (a2 --> a3))) -> Term (a0 --> (a1 --> (a2 --> a3))) Source # pevalEqTerm :: Term (a0 --> (a1 --> (a2 --> a3))) -> Term (a0 --> (a1 --> (a2 --> a3))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 --> (a1 --> (a2 --> a3)))) -> Term Bool Source # conSBVTerm :: (a0 --> (a1 --> (a2 --> a3))) -> SBVType (a0 --> (a1 --> (a2 --> a3))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 --> (a1 --> (a2 --> a3))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 --> (a1 --> (a2 --> a3)))) Source # withPrim :: ((PrimConstraint (a0 --> (a1 --> (a2 --> a3))), SMTDefinable (SBVType (a0 --> (a1 --> (a2 --> a3)))), Mergeable (SBVType (a0 --> (a1 --> (a2 --> a3)))), Typeable (SBVType (a0 --> (a1 --> (a2 --> a3))))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 --> (a1 --> (a2 --> a3))) -> SBVType (a0 --> (a1 --> (a2 --> a3))) -> SBVType (a0 --> (a1 --> (a2 --> a3))) Source # sbvEq :: SBVType (a0 --> (a1 --> (a2 --> a3))) -> SBVType (a0 --> (a1 --> (a2 --> a3))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 --> (a1 --> (a2 --> a3)))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 --> (a1 --> (a2 --> a3)) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 --> (a1 --> (a2 --> a3))) -> Maybe (TypedSymbol knd' (a0 --> (a1 --> (a2 --> a3)))) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 --> (a1 --> (a2 --> a3))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2) => SupportedPrim (a0 --> (a1 --> a2)) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a0 --> (a1 --> a2))) Source # pformatCon :: (a0 --> (a1 --> a2)) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 --> (a1 --> a2)) -> String Source # defaultValue :: a0 --> (a1 --> a2) Source # defaultValueDynamic :: proxy (a0 --> (a1 --> a2)) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 --> (a1 --> a2)) -> Term (a0 --> (a1 --> a2)) -> Term (a0 --> (a1 --> a2)) Source # pevalEqTerm :: Term (a0 --> (a1 --> a2)) -> Term (a0 --> (a1 --> a2)) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 --> (a1 --> a2))) -> Term Bool Source # conSBVTerm :: (a0 --> (a1 --> a2)) -> SBVType (a0 --> (a1 --> a2)) Source # symSBVName :: TypedSymbol 'AnyKind (a0 --> (a1 --> a2)) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 --> (a1 --> a2))) Source # withPrim :: ((PrimConstraint (a0 --> (a1 --> a2)), SMTDefinable (SBVType (a0 --> (a1 --> a2))), Mergeable (SBVType (a0 --> (a1 --> a2))), Typeable (SBVType (a0 --> (a1 --> a2)))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 --> (a1 --> a2)) -> SBVType (a0 --> (a1 --> a2)) -> SBVType (a0 --> (a1 --> a2)) Source # sbvEq :: SBVType (a0 --> (a1 --> a2)) -> SBVType (a0 --> (a1 --> a2)) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 --> (a1 --> a2))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 --> (a1 --> a2) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 --> (a1 --> a2)) -> Maybe (TypedSymbol knd' (a0 --> (a1 --> a2))) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 --> (a1 --> a2)) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1) => SupportedPrim (a0 --> a1) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a0 --> a1)) Source # pformatCon :: (a0 --> a1) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 --> a1) -> String Source # defaultValue :: a0 --> a1 Source # defaultValueDynamic :: proxy (a0 --> a1) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 --> a1) -> Term (a0 --> a1) -> Term (a0 --> a1) Source # pevalEqTerm :: Term (a0 --> a1) -> Term (a0 --> a1) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 --> a1)) -> Term Bool Source # conSBVTerm :: (a0 --> a1) -> SBVType (a0 --> a1) Source # symSBVName :: TypedSymbol 'AnyKind (a0 --> a1) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 --> a1)) Source # withPrim :: ((PrimConstraint (a0 --> a1), SMTDefinable (SBVType (a0 --> a1)), Mergeable (SBVType (a0 --> a1)), Typeable (SBVType (a0 --> a1))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 --> a1) -> SBVType (a0 --> a1) -> SBVType (a0 --> a1) Source # sbvEq :: SBVType (a0 --> a1) -> SBVType (a0 --> a1) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 --> a1)) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 --> a1 Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 --> a1) -> Maybe (TypedSymbol knd' (a0 --> a1)) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 --> a1) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4, SupportedNonFuncPrim a5, SupportedNonFuncPrim a6, SupportedNonFuncPrim a7) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))) Source # pformatCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> String Source # defaultValue :: a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))) Source # defaultValueDynamic :: proxy (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) Source # pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))) -> Term Bool Source # conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))) Source # withPrim :: ((PrimConstraint (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))), SMTDefinable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))), Mergeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))), Typeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) Source # sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7)))))))) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> (a6 =-> a7))))))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4, SupportedNonFuncPrim a5, SupportedNonFuncPrim a6) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))) Source # pformatCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> String Source # defaultValue :: a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))) Source # defaultValueDynamic :: proxy (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) Source # pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))) -> Term Bool Source # conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))) Source # withPrim :: ((PrimConstraint (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))), SMTDefinable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))), Mergeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))), Typeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) Source # sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6))))))) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> (a5 =-> a6)))))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4, SupportedNonFuncPrim a5) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))) Source # pformatCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> String Source # defaultValue :: a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))) Source # defaultValueDynamic :: proxy (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) Source # pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))) -> Term Bool Source # conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))) Source # withPrim :: ((PrimConstraint (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))), SMTDefinable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))), Mergeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))), Typeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) Source # sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5)))))) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> (a4 =-> a5))))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3, SupportedNonFuncPrim a4) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))) Source # pformatCon :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> String Source # defaultValue :: a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))) Source # defaultValueDynamic :: proxy (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) Source # pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))) -> Term Bool Source # conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))) Source # withPrim :: ((PrimConstraint (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))), SMTDefinable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))), Mergeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))), Typeable (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) Source # sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4))))) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> (a3 =-> a4)))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2, SupportedNonFuncPrim a3) => SupportedPrim (a0 =-> (a1 =-> (a2 =-> a3))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a0 =-> (a1 =-> (a2 =-> a3)))) Source # pformatCon :: (a0 =-> (a1 =-> (a2 =-> a3))) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> a3))) -> String Source # defaultValue :: a0 =-> (a1 =-> (a2 =-> a3)) Source # defaultValueDynamic :: proxy (a0 =-> (a1 =-> (a2 =-> a3))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> (a2 =-> a3))) -> Term (a0 =-> (a1 =-> (a2 =-> a3))) -> Term (a0 =-> (a1 =-> (a2 =-> a3))) Source # pevalEqTerm :: Term (a0 =-> (a1 =-> (a2 =-> a3))) -> Term (a0 =-> (a1 =-> (a2 =-> a3))) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> (a2 =-> a3)))) -> Term Bool Source # conSBVTerm :: (a0 =-> (a1 =-> (a2 =-> a3))) -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> (a2 =-> a3))) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> (a2 =-> a3)))) Source # withPrim :: ((PrimConstraint (a0 =-> (a1 =-> (a2 =-> a3))), SMTDefinable (SBVType (a0 =-> (a1 =-> (a2 =-> a3)))), Mergeable (SBVType (a0 =-> (a1 =-> (a2 =-> a3)))), Typeable (SBVType (a0 =-> (a1 =-> (a2 =-> a3))))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) Source # sbvEq :: SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> (a2 =-> a3)))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> (a2 =-> a3)) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> (a2 =-> a3))) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> (a2 =-> a3)))) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 =-> (a1 =-> (a2 =-> a3))) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1, SupportedNonFuncPrim a2) => SupportedPrim (a0 =-> (a1 =-> a2)) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a0 =-> (a1 =-> a2))) Source # pformatCon :: (a0 =-> (a1 =-> a2)) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> a2)) -> String Source # defaultValue :: a0 =-> (a1 =-> a2) Source # defaultValueDynamic :: proxy (a0 =-> (a1 =-> a2)) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 =-> (a1 =-> a2)) -> Term (a0 =-> (a1 =-> a2)) -> Term (a0 =-> (a1 =-> a2)) Source # pevalEqTerm :: Term (a0 =-> (a1 =-> a2)) -> Term (a0 =-> (a1 =-> a2)) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> (a1 =-> a2))) -> Term Bool Source # conSBVTerm :: (a0 =-> (a1 =-> a2)) -> SBVType (a0 =-> (a1 =-> a2)) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> (a1 =-> a2)) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> (a1 =-> a2))) Source # withPrim :: ((PrimConstraint (a0 =-> (a1 =-> a2)), SMTDefinable (SBVType (a0 =-> (a1 =-> a2))), Mergeable (SBVType (a0 =-> (a1 =-> a2))), Typeable (SBVType (a0 =-> (a1 =-> a2)))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 =-> (a1 =-> a2)) -> SBVType (a0 =-> (a1 =-> a2)) -> SBVType (a0 =-> (a1 =-> a2)) Source # sbvEq :: SBVType (a0 =-> (a1 =-> a2)) -> SBVType (a0 =-> (a1 =-> a2)) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> (a1 =-> a2))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> (a1 =-> a2) Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> (a1 =-> a2)) -> Maybe (TypedSymbol knd' (a0 =-> (a1 =-> a2))) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 =-> (a1 =-> a2)) -> SBV Bool Source #
(SupportedNonFuncPrim a0, SupportedNonFuncPrim a1) => SupportedPrim (a0 =-> a1) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a0 =-> a1)) Source # pformatCon :: (a0 =-> a1) -> String Source # pformatSym :: TypedSymbol 'AnyKind (a0 =-> a1) -> String Source # defaultValue :: a0 =-> a1 Source # defaultValueDynamic :: proxy (a0 =-> a1) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a0 =-> a1) -> Term (a0 =-> a1) -> Term (a0 =-> a1) Source # pevalEqTerm :: Term (a0 =-> a1) -> Term (a0 =-> a1) -> Term Bool Source # pevalDistinctTerm :: NonEmpty (Term (a0 =-> a1)) -> Term Bool Source # conSBVTerm :: (a0 =-> a1) -> SBVType (a0 =-> a1) Source # symSBVName :: TypedSymbol 'AnyKind (a0 =-> a1) -> Int -> String Source # symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (a0 =-> a1)) Source # withPrim :: ((PrimConstraint (a0 =-> a1), SMTDefinable (SBVType (a0 =-> a1)), Mergeable (SBVType (a0 =-> a1)), Typeable (SBVType (a0 =-> a1))) => a) -> a Source # sbvIte :: SBV Bool -> SBVType (a0 =-> a1) -> SBVType (a0 =-> a1) -> SBVType (a0 =-> a1) Source # sbvEq :: SBVType (a0 =-> a1) -> SBVType (a0 =-> a1) -> SBV Bool Source # sbvDistinct :: NonEmpty (SBVType (a0 =-> a1)) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a0 =-> a1 Source # castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (a0 =-> a1) -> Maybe (TypedSymbol knd' (a0 =-> a1)) Source # isFuncType :: Bool Source # funcDummyConstraint :: SBVType (a0 =-> a1) -> SBV Bool Source #

class SupportedPrim con => SymRep con Source #

Type family to resolve the symbolic type associated with a concrete type.

Associated Types

type SymType con Source #

Instances

Instances details

SymRep AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.SymAlgReal Associated Types type SymType AlgReal Source #
SymRep FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Associated Types type SymType FPRoundingMode Source #
SymRep Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Associated Types type SymType Integer Source #
SymRep Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBool Associated Types type SymType Bool Source #
(KnownNat n, 1 <= n) => SymRep (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type SymType (IntN n) Source #
(KnownNat n, 1 <= n) => SymRep (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type SymType (WordN n) Source #
ValidFP eb sb => SymRep (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Associated Types type SymType (FP eb sb) Source #
(SymRep ca, SymRep cb, SupportedPrim (ca --> cb)) => SymRep (ca --> cb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Associated Types type SymType (ca --> cb) Source #
(SymRep a, SymRep b, SupportedPrim (a =-> b)) => SymRep (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Associated Types type SymType (a =-> b) Source #

class ConRep sym Source #

Type family to resolve the concrete type associated with a symbolic type.

Associated Types

type ConType sym Source #

Instances

Instances details

ConRep SymAlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.SymAlgReal Associated Types type ConType SymAlgReal Source #
ConRep SymBool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBool Associated Types type ConType SymBool Source #
ConRep SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Associated Types type ConType SymFPRoundingMode Source #
ConRep SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Associated Types type ConType SymInteger Source #
(KnownNat n, 1 <= n) => ConRep (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type ConType (SymIntN n) Source #
(KnownNat n, 1 <= n) => ConRep (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Associated Types type ConType (SymWordN n) Source #
ConRep (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Associated Types type ConType (SymFP eb sb) Source #
(ConRep a, ConRep b) => ConRep (a -~> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Associated Types type ConType (a -~> b) Source #
(ConRep a, ConRep b) => ConRep (a =~> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Associated Types type ConType (a =~> b) Source #

class (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) => LinkedRep con sym | con -> sym, sym -> con where Source #

One-to-one mapping between symbolic types and concrete types.

Methods

underlyingTerm :: sym -> Term con Source #

wrapTerm :: Term con -> sym Source #

Instances

Instances details

LinkedRep AlgReal SymAlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.SymAlgReal Methods underlyingTerm :: SymAlgReal -> Term AlgReal Source # wrapTerm :: Term AlgReal -> SymAlgReal Source #
LinkedRep FPRoundingMode SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods underlyingTerm :: SymFPRoundingMode -> Term FPRoundingMode Source # wrapTerm :: Term FPRoundingMode -> SymFPRoundingMode Source #
LinkedRep Integer SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods underlyingTerm :: SymInteger -> Term Integer Source # wrapTerm :: Term Integer -> SymInteger Source #
LinkedRep Bool SymBool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBool Methods underlyingTerm :: SymBool -> Term Bool Source # wrapTerm :: Term Bool -> SymBool Source #
(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods underlyingTerm :: SymIntN n -> Term (IntN n) Source # wrapTerm :: Term (IntN n) -> SymIntN n Source #
(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods underlyingTerm :: SymWordN n -> Term (WordN n) Source # wrapTerm :: Term (WordN n) -> SymWordN n Source #
ValidFP eb sb => LinkedRep (FP eb sb) (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods underlyingTerm :: SymFP eb sb -> Term (FP eb sb) Source # wrapTerm :: Term (FP eb sb) -> SymFP eb sb Source #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim ca, SupportedPrim cb, SupportedPrim (ca --> cb)) => LinkedRep (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods underlyingTerm :: (sa -~> sb) -> Term (ca --> cb) Source # wrapTerm :: Term (ca --> cb) -> sa -~> sb Source #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => LinkedRep (ca =-> cb) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Methods underlyingTerm :: (sa =~> sb) -> Term (ca =-> cb) Source # wrapTerm :: Term (ca =-> cb) -> sa =~> sb Source #

Partial evaluation for the terms

class (SupportedPrim arg, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => UnaryOp tag arg t | tag arg -> t where Source #

Custom unary operator. Not used by Grisette at this time and do not use it.

Methods

pevalUnary :: (Typeable tag, Typeable t) => tag -> Term arg -> Term t Source #

pformatUnary :: tag -> Term arg -> String Source #

class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => BinaryOp tag arg1 arg2 t | tag arg1 arg2 -> t where Source #

Custom binary operator. Not used by Grisette at this time and do not use it.

Methods

pevalBinary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term t Source #

pformatBinary :: tag -> Term arg1 -> Term arg2 -> String Source #

class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim arg3, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => TernaryOp tag arg1 arg2 arg3 t | tag arg1 arg2 arg3 -> t where Source #

Custom ternary operator. Not used by Grisette at this time and do not use it.

Methods

pevalTernary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t Source #

pformatTernary :: tag -> Term arg1 -> Term arg2 -> Term arg3 -> String Source #

class (SupportedPrim f, SupportedPrim a, SupportedPrim b) => PEvalApplyTerm f a b | f -> a b where Source #

Partial evaluation and lowering for function application terms.

Methods

pevalApplyTerm :: Term f -> Term a -> Term b Source #

sbvApplyTerm :: SBVType f -> SBVType a -> SBVType b Source #

Instances

Instances details

(SupportedPrim (a --> b), SupportedNonFuncPrim a, SupportedPrim b) => PEvalApplyTerm (a --> b) a b Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods pevalApplyTerm :: Term (a --> b) -> Term a -> Term b Source # sbvApplyTerm :: SBVType (a --> b) -> SBVType a -> SBVType b Source #
(SupportedPrim a, SupportedPrim b, SupportedPrim (a =-> b)) => PEvalApplyTerm (a =-> b) a b Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods pevalApplyTerm :: Term (a =-> b) -> Term a -> Term b Source # sbvApplyTerm :: SBVType (a =-> b) -> SBVType a -> SBVType b Source #

class (SupportedNonFuncPrim t, Bits t) => PEvalBitwiseTerm t where Source #

Partial evaluation and lowering for bitwise operation terms.

Minimal complete definition

pevalAndBitsTerm, pevalOrBitsTerm, pevalXorBitsTerm, pevalComplementBitsTerm, withSbvBitwiseTermConstraint

Methods

pevalAndBitsTerm :: Term t -> Term t -> Term t Source #

pevalOrBitsTerm :: Term t -> Term t -> Term t Source #

pevalXorBitsTerm :: Term t -> Term t -> Term t Source #

pevalComplementBitsTerm :: Term t -> Term t Source #

withSbvBitwiseTermConstraint :: (Bits (SBVType t) => r) -> r Source #

sbvAndBitsTerm :: SBVType t -> SBVType t -> SBVType t Source #

sbvOrBitsTerm :: SBVType t -> SBVType t -> SBVType t Source #

sbvXorBitsTerm :: SBVType t -> SBVType t -> SBVType t Source #

sbvComplementBitsTerm :: SBVType t -> SBVType t Source #

Instances

Instances details

(KnownNat n, 1 <= n) => PEvalBitwiseTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm 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 :: (Bits (SBVType (IntN n)) => r) -> r Source # sbvAndBitsTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvOrBitsTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvXorBitsTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvComplementBitsTerm :: SBVType (IntN n) -> SBVType (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalBitwiseTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm 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 :: (Bits (SBVType (WordN n)) => r) -> r Source # sbvAndBitsTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvOrBitsTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvXorBitsTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvComplementBitsTerm :: SBVType (WordN n) -> SBVType (WordN n) Source #

class (SupportedNonFuncPrim t, SymShift t) => PEvalShiftTerm t where Source #

Partial evaluation and lowering for symbolic shifting terms.

Minimal complete definition

pevalShiftLeftTerm, pevalShiftRightTerm, withSbvShiftTermConstraint

Methods

pevalShiftLeftTerm :: Term t -> Term t -> Term t Source #

pevalShiftRightTerm :: Term t -> Term t -> Term t Source #

withSbvShiftTermConstraint :: (SIntegral (NonFuncSBVBaseType t) => r) -> r Source #

sbvShiftLeftTerm :: SBVType t -> SBVType t -> SBVType t Source #

sbvShiftRightTerm :: SBVType t -> SBVType t -> SBVType t Source #

Instances

Instances details

(KnownNat n, 1 <= n) => PEvalShiftTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm Methods pevalShiftLeftTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalShiftRightTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # withSbvShiftTermConstraint :: (SIntegral (NonFuncSBVBaseType (IntN n)) => r) -> r Source # sbvShiftLeftTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvShiftRightTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalShiftTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm Methods pevalShiftLeftTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalShiftRightTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # withSbvShiftTermConstraint :: (SIntegral (NonFuncSBVBaseType (WordN n)) => r) -> r Source # sbvShiftLeftTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvShiftRightTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

class (SupportedNonFuncPrim t, SymRotate t) => PEvalRotateTerm t where Source #

Partial evaluation and lowering for symbolic rotate terms.

Minimal complete definition

pevalRotateLeftTerm, pevalRotateRightTerm, withSbvRotateTermConstraint

Methods

pevalRotateLeftTerm :: Term t -> Term t -> Term t Source #

pevalRotateRightTerm :: Term t -> Term t -> Term t Source #

withSbvRotateTermConstraint :: (SIntegral (NonFuncSBVBaseType t) => r) -> r Source #

sbvRotateLeftTerm :: SBVType t -> SBVType t -> SBVType t Source #

sbvRotateRightTerm :: SBVType t -> SBVType t -> SBVType t Source #

Instances

Instances details

(KnownNat n, 1 <= n) => PEvalRotateTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm Methods pevalRotateLeftTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalRotateRightTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # withSbvRotateTermConstraint :: (SIntegral (NonFuncSBVBaseType (IntN n)) => r) -> r Source # sbvRotateLeftTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvRotateRightTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalRotateTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm Methods pevalRotateLeftTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalRotateRightTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # withSbvRotateTermConstraint :: (SIntegral (NonFuncSBVBaseType (WordN n)) => r) -> r Source # sbvRotateLeftTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvRotateRightTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

class (SupportedNonFuncPrim t, Num t) => PEvalNumTerm t where Source #

Partial evaluation and lowering for number terms.

Minimal complete definition

pevalAddNumTerm, pevalNegNumTerm, pevalMulNumTerm, pevalAbsNumTerm, pevalSignumNumTerm, withSbvNumTermConstraint

Methods

pevalAddNumTerm :: Term t -> Term t -> Term t Source #

pevalNegNumTerm :: Term t -> Term t Source #

pevalMulNumTerm :: Term t -> Term t -> Term t Source #

pevalAbsNumTerm :: Term t -> Term t Source #

pevalSignumNumTerm :: Term t -> Term t Source #

withSbvNumTermConstraint :: (Num (SBVType t) => r) -> r Source #

sbvAddNumTerm :: SBVType t -> SBVType t -> SBVType t Source #

sbvNegNumTerm :: SBVType t -> SBVType t Source #

sbvMulNumTerm :: SBVType t -> SBVType t -> SBVType t Source #

sbvAbsNumTerm :: SBVType t -> SBVType t Source #

sbvSignumNumTerm :: SBVType t -> SBVType t Source #

Instances

Instances details

PEvalNumTerm AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm 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 Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm 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 Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm 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 Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm 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 Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm 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 #

pevalSubNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a Source #

Partial evaluation for subtraction terms.

class (SupportedNonFuncPrim t, Ord t) => PEvalOrdTerm t where Source #

Partial evaluation and lowering for comparison terms.

Minimal complete definition

pevalLtOrdTerm, pevalLeOrdTerm, withSbvOrdTermConstraint

Methods

pevalLtOrdTerm :: Term t -> Term t -> Term Bool Source #

pevalLeOrdTerm :: Term t -> Term t -> Term Bool Source #

withSbvOrdTermConstraint :: (OrdSymbolic (SBVType t) => r) -> r Source #

sbvLtOrdTerm :: SBVType t -> SBVType t -> SBV Bool Source #

sbvLeOrdTerm :: SBVType t -> SBVType t -> SBV Bool Source #

Instances

Instances details

PEvalOrdTerm AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm Methods pevalLtOrdTerm :: Term AlgReal -> Term AlgReal -> Term Bool Source # pevalLeOrdTerm :: Term AlgReal -> Term AlgReal -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType AlgReal) => r) -> r Source # sbvLtOrdTerm :: SBVType AlgReal -> SBVType AlgReal -> SBV Bool Source # sbvLeOrdTerm :: SBVType AlgReal -> SBVType AlgReal -> SBV Bool Source #
PEvalOrdTerm FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm Methods pevalLtOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool Source # pevalLeOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType FPRoundingMode) => r) -> r Source # sbvLtOrdTerm :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool Source # sbvLeOrdTerm :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool Source #
PEvalOrdTerm Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm Methods pevalLtOrdTerm :: Term Integer -> Term Integer -> Term Bool Source # pevalLeOrdTerm :: Term Integer -> Term Integer -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType Integer) => r) -> r Source # sbvLtOrdTerm :: SBVType Integer -> SBVType Integer -> SBV Bool Source # sbvLeOrdTerm :: SBVType Integer -> SBVType Integer -> SBV Bool Source #
(KnownNat n, 1 <= n) => PEvalOrdTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm Methods pevalLtOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool Source # pevalLeOrdTerm :: Term (IntN n) -> Term (IntN n) -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType (IntN n)) => r) -> r Source # sbvLtOrdTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBV Bool Source # sbvLeOrdTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBV Bool Source #
(KnownNat n, 1 <= n) => PEvalOrdTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm Methods pevalLtOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool Source # pevalLeOrdTerm :: Term (WordN n) -> Term (WordN n) -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType (WordN n)) => r) -> r Source # sbvLtOrdTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBV Bool Source # sbvLeOrdTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBV Bool Source #
ValidFP eb sb => PEvalOrdTerm (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm Methods pevalLtOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool Source # pevalLeOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool Source # withSbvOrdTermConstraint :: (OrdSymbolic (SBVType (FP eb sb)) => r) -> r Source # sbvLtOrdTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool Source # sbvLeOrdTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool Source #

pevalGtOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool Source #

Partial evaluation for greater than terms.

pevalGeOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool Source #

Partial evaluation for greater than or equal to terms.

pevalNEqTerm :: SupportedPrim a => Term a -> Term a -> Term Bool Source #

Partial evaluation for inequality terms.

class (SupportedNonFuncPrim t, Integral t) => PEvalDivModIntegralTerm t where Source #

Partial evaluation and lowering for integer division and modulo terms.

Minimal complete definition

pevalDivIntegralTerm, pevalModIntegralTerm, pevalQuotIntegralTerm, pevalRemIntegralTerm, withSbvDivModIntegralTermConstraint

Methods

pevalDivIntegralTerm :: Term t -> Term t -> Term t Source #

pevalModIntegralTerm :: Term t -> Term t -> Term t Source #

pevalQuotIntegralTerm :: Term t -> Term t -> Term t Source #

pevalRemIntegralTerm :: Term t -> Term t -> Term t Source #

withSbvDivModIntegralTermConstraint :: (SDivisible (SBVType t) => r) -> r Source #

sbvDivIntegralTerm :: SBVType t -> SBVType t -> SBVType t Source #

sbvModIntegralTerm :: SBVType t -> SBVType t -> SBVType t Source #

sbvQuotIntegralTerm :: SBVType t -> SBVType t -> SBVType t Source #

sbvRemIntegralTerm :: SBVType t -> SBVType t -> SBVType t Source #

Instances

Instances details

PEvalDivModIntegralTerm Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm Methods pevalDivIntegralTerm :: Term Integer -> Term Integer -> Term Integer Source # pevalModIntegralTerm :: Term Integer -> Term Integer -> Term Integer Source # pevalQuotIntegralTerm :: Term Integer -> Term Integer -> Term Integer Source # pevalRemIntegralTerm :: Term Integer -> Term Integer -> Term Integer Source # withSbvDivModIntegralTermConstraint :: (SDivisible (SBVType Integer) => r) -> r Source # sbvDivIntegralTerm :: SBVType Integer -> SBVType Integer -> SBVType Integer Source # sbvModIntegralTerm :: SBVType Integer -> SBVType Integer -> SBVType Integer Source # sbvQuotIntegralTerm :: SBVType Integer -> SBVType Integer -> SBVType Integer Source # sbvRemIntegralTerm :: SBVType Integer -> SBVType Integer -> SBVType Integer Source #
(KnownNat n, 1 <= n) => PEvalDivModIntegralTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm Methods pevalDivIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalModIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalQuotIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalRemIntegralTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # withSbvDivModIntegralTermConstraint :: (SDivisible (SBVType (IntN n)) => r) -> r Source # sbvDivIntegralTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvModIntegralTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvQuotIntegralTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvRemIntegralTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalDivModIntegralTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalDivModIntegralTerm Methods pevalDivIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalModIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalQuotIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalRemIntegralTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # withSbvDivModIntegralTermConstraint :: (SDivisible (SBVType (WordN n)) => r) -> r Source # sbvDivIntegralTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvModIntegralTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvQuotIntegralTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvRemIntegralTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source #

class (SupportedNonFuncPrim a, SupportedNonFuncPrim b, BitCast a b) => PEvalBitCastTerm a b where Source #

Partial evaluation and lowering for bitcast terms.

Methods

pevalBitCastTerm :: Term a -> Term b Source #

sbvBitCast :: SBVType a -> SBVType b Source #

Instances

Instances details

PEvalBitCastTerm Bool (IntN 1) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm Methods pevalBitCastTerm :: Term Bool -> Term (IntN 1) Source # sbvBitCast :: SBVType Bool -> SBVType (IntN 1) Source #
PEvalBitCastTerm Bool (WordN 1) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm Methods pevalBitCastTerm :: Term Bool -> Term (WordN 1) Source # sbvBitCast :: SBVType Bool -> SBVType (WordN 1) Source #
PEvalBitCastTerm (IntN 1) Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm Methods pevalBitCastTerm :: Term (IntN 1) -> Term Bool Source # sbvBitCast :: SBVType (IntN 1) -> SBVType Bool Source #
PEvalBitCastTerm (WordN 1) Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm Methods pevalBitCastTerm :: Term (WordN 1) -> Term Bool Source # sbvBitCast :: SBVType (WordN 1) -> SBVType Bool Source #
(KnownNat n, 1 <= n) => PEvalBitCastTerm (IntN n) (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval Methods pevalBitCastTerm :: Term (IntN n) -> Term (WordN n) Source # sbvBitCast :: SBVType (IntN n) -> SBVType (WordN n) Source #
(KnownNat n, 1 <= n) => PEvalBitCastTerm (WordN n) (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval Methods pevalBitCastTerm :: Term (WordN n) -> Term (IntN n) Source # sbvBitCast :: SBVType (WordN n) -> SBVType (IntN n) Source #
(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastTerm (IntN n) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm 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 Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm Methods pevalBitCastTerm :: Term (WordN n) -> Term (FP eb sb) Source # sbvBitCast :: SBVType (WordN n) -> SBVType (FP eb sb) Source #

class (SupportedNonFuncPrim a, SupportedNonFuncPrim b, BitCastOr a b) => PEvalBitCastOrTerm a b where Source #

Partial evaluation and lowering for bitcast or default value terms.

Methods

pevalBitCastOrTerm :: Term b -> Term a -> Term b Source #

sbvBitCastOr :: SBVType b -> SBVType a -> SBVType b Source #

Instances

Instances details

(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastOrTerm (FP eb sb) (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm 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 Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm 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 #

class (forall n. (KnownNat n, 1 <= n) => SupportedNonFuncPrim (bv n), SizedBV bv, Typeable bv) => PEvalBVTerm bv where Source #

Partial evaluation and lowering for bit-vector terms.

Methods

pevalBVConcatTerm :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (bv l) -> Term (bv r) -> Term (bv (l + r)) Source #

pevalBVExtendTerm :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (bv l) -> Term (bv r) Source #

pevalBVSelectTerm :: (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (bv n) -> Term (bv w) Source #

sbvBVConcatTerm :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p1 l -> p2 r -> SBVType (bv l) -> SBVType (bv r) -> SBVType (bv (l + r)) Source #

sbvBVExtendTerm :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p1 l -> p2 r -> Bool -> SBVType (bv l) -> SBVType (bv r) Source #

sbvBVSelectTerm :: (KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p1 ix -> p2 w -> p3 n -> SBVType (bv n) -> SBVType (bv w) Source #

Instances

Instances details

PEvalBVTerm IntN Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval Methods pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (IntN l) -> Term (IntN r) -> Term (IntN (l + r)) Source # pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (IntN l) -> Term (IntN r) Source # pevalBVSelectTerm :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (IntN n) -> Term (IntN w) Source # sbvBVConcatTerm :: forall (l :: Nat) (r :: Nat) p1 p2. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p1 l -> p2 r -> SBVType (IntN l) -> SBVType (IntN r) -> SBVType (IntN (l + r)) Source # sbvBVExtendTerm :: forall (l :: Nat) (r :: Nat) p1 p2. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p1 l -> p2 r -> Bool -> SBVType (IntN l) -> SBVType (IntN r) Source # sbvBVSelectTerm :: forall (ix :: Nat) (w :: Nat) (n :: Nat) p1 p2 p3. (KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p1 ix -> p2 w -> p3 n -> SBVType (IntN n) -> SBVType (IntN w) Source #
PEvalBVTerm WordN Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval Methods pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (WordN l) -> Term (WordN r) -> Term (WordN (l + r)) Source # pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (WordN l) -> Term (WordN r) Source # pevalBVSelectTerm :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (WordN n) -> Term (WordN w) Source # sbvBVConcatTerm :: forall (l :: Nat) (r :: Nat) p1 p2. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p1 l -> p2 r -> SBVType (WordN l) -> SBVType (WordN r) -> SBVType (WordN (l + r)) Source # sbvBVExtendTerm :: forall (l :: Nat) (r :: Nat) p1 p2. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p1 l -> p2 r -> Bool -> SBVType (WordN l) -> SBVType (WordN r) Source # sbvBVSelectTerm :: forall (ix :: Nat) (w :: Nat) (n :: Nat) p1 p2 p3. (KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p1 ix -> p2 w -> p3 n -> SBVType (WordN n) -> SBVType (WordN w) Source #

class (SupportedNonFuncPrim t, Fractional t) => PEvalFractionalTerm t where Source #

Partial evaluation and lowering for fractional terms.

Minimal complete definition

pevalFdivTerm, pevalRecipTerm, withSbvFractionalTermConstraint

Methods

pevalFdivTerm :: Term t -> Term t -> Term t Source #

pevalRecipTerm :: Term t -> Term t Source #

withSbvFractionalTermConstraint :: (Fractional (SBVType t) => r) -> r Source #

sbvFdivTerm :: SBVType t -> SBVType t -> SBVType t Source #

sbvRecipTerm :: SBVType t -> SBVType t Source #

Instances

Instances details

PEvalFractionalTerm AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm Methods pevalFdivTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal Source # pevalRecipTerm :: Term AlgReal -> Term AlgReal Source # withSbvFractionalTermConstraint :: (Fractional (SBVType AlgReal) => r) -> r Source # sbvFdivTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal Source # sbvRecipTerm :: SBVType AlgReal -> SBVType AlgReal Source #
ValidFP eb sb => PEvalFractionalTerm (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm Methods pevalFdivTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalRecipTerm :: Term (FP eb sb) -> Term (FP eb sb) Source # withSbvFractionalTermConstraint :: (Fractional (SBVType (FP eb sb)) => r) -> r Source # sbvFdivTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvRecipTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

class SupportedNonFuncPrim t => PEvalFloatingTerm t where Source #

Partial evaluation and lowering for floating point terms.

Minimal complete definition

pevalFloatingUnaryTerm, pevalPowerTerm, withSbvFloatingTermConstraint

Methods

pevalFloatingUnaryTerm :: FloatingUnaryOp -> Term t -> Term t Source #

pevalPowerTerm :: Term t -> Term t -> Term t Source #

withSbvFloatingTermConstraint :: (Floating (SBVType t) => r) -> r Source #

sbvPowerTerm :: SBVType t -> SBVType t -> SBVType t Source #

sbvFloatingUnaryTerm :: FloatingUnaryOp -> SBVType t -> SBVType t Source #

Instances

Instances details

PEvalFloatingTerm AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm Methods pevalFloatingUnaryTerm :: FloatingUnaryOp -> Term AlgReal -> Term AlgReal Source # pevalPowerTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal Source # withSbvFloatingTermConstraint :: (Floating (SBVType AlgReal) => r) -> r Source # sbvPowerTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal Source # sbvFloatingUnaryTerm :: FloatingUnaryOp -> SBVType AlgReal -> SBVType AlgReal Source #
ValidFP eb sb => PEvalFloatingTerm (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm Methods pevalFloatingUnaryTerm :: FloatingUnaryOp -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalPowerTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # withSbvFloatingTermConstraint :: (Floating (SBVType (FP eb sb)) => r) -> r Source # sbvPowerTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvFloatingUnaryTerm :: FloatingUnaryOp -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

class (SupportedNonFuncPrim a, SupportedNonFuncPrim b, Integral a, Num b) => PEvalFromIntegralTerm a b where Source #

Partial evaluation and lowering for integral terms.

Methods

pevalFromIntegralTerm :: Term a -> Term b Source #

sbvFromIntegralTerm :: SBVType a -> SBVType b Source #

Instances

Instances details

PEvalFromIntegralTerm Integer AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term Integer -> Term AlgReal Source # sbvFromIntegralTerm :: SBVType Integer -> SBVType AlgReal Source #
(KnownNat n, 1 <= n) => PEvalFromIntegralTerm Integer (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term Integer -> Term (IntN n) Source # sbvFromIntegralTerm :: SBVType Integer -> SBVType (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalFromIntegralTerm Integer (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term Integer -> Term (WordN n) Source # sbvFromIntegralTerm :: SBVType Integer -> SBVType (WordN n) Source #
ValidFP eb sb => PEvalFromIntegralTerm Integer (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term Integer -> Term (FP eb sb) Source # sbvFromIntegralTerm :: SBVType Integer -> SBVType (FP eb sb) Source #
(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (IntN n) AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term (IntN n) -> Term AlgReal Source # sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType AlgReal Source #
(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (IntN n) Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term (IntN n) -> Term Integer Source # sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType Integer Source #
(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (WordN n) AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term (WordN n) -> Term AlgReal Source # sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType AlgReal Source #
(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (WordN n) Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term (WordN n) -> Term Integer Source # sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType Integer Source #
(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (IntN n) (IntN m) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term (IntN n) -> Term (IntN m) Source # sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (IntN m) Source #
(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (IntN n) (WordN m) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term (IntN n) -> Term (WordN m) Source # sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (WordN m) Source #
(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (WordN n) (IntN m) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term (WordN n) -> Term (IntN m) Source # sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (IntN m) Source #
(KnownNat n, 1 <= n, KnownNat m, 1 <= m) => PEvalFromIntegralTerm (WordN n) (WordN m) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term (WordN n) -> Term (WordN m) Source # sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (WordN m) Source #
(KnownNat n, 1 <= n, ValidFP eb sb) => PEvalFromIntegralTerm (IntN n) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term (IntN n) -> Term (FP eb sb) Source # sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (FP eb sb) Source #
(KnownNat n, 1 <= n, ValidFP eb sb) => PEvalFromIntegralTerm (WordN n) (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm Methods pevalFromIntegralTerm :: Term (WordN n) -> Term (FP eb sb) Source # sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (FP eb sb) Source #

class SupportedNonFuncPrim a => PEvalIEEEFPConvertibleTerm a where Source #

Partial evaluation and lowering for converting from and to IEEE floating point terms.

Methods

pevalFromFPOrTerm :: ValidFP eb sb => Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a Source #

pevalToFPTerm :: ValidFP eb sb => Term FPRoundingMode -> Term a -> Term (FP eb sb) Source #

sbvFromFPOrTerm :: ValidFP eb sb => SBVType a -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType a Source #

sbvToFPTerm :: ValidFP eb sb => SBVType FPRoundingMode -> SBVType a -> SBVType (FP eb sb) Source #

Instances

Instances details

PEvalIEEEFPConvertibleTerm AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm Methods pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term AlgReal -> Term FPRoundingMode -> Term (FP eb sb) -> Term AlgReal Source # pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term AlgReal -> Term (FP eb sb) Source # sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType AlgReal -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType AlgReal Source # sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType AlgReal -> SBVType (FP eb sb) Source #
PEvalIEEEFPConvertibleTerm Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm Methods pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term Integer -> Term FPRoundingMode -> Term (FP eb sb) -> Term Integer Source # pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term Integer -> Term (FP eb sb) Source # sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType Integer -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType Integer Source # sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType Integer -> SBVType (FP eb sb) Source #
(KnownNat n, 1 <= n) => PEvalIEEEFPConvertibleTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm Methods pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term (IntN n) -> Term FPRoundingMode -> Term (FP eb sb) -> Term (IntN n) Source # pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term (IntN n) -> Term (FP eb sb) Source # sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType (IntN n) -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (IntN n) Source # sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType (IntN n) -> SBVType (FP eb sb) Source #
(KnownNat n, 1 <= n) => PEvalIEEEFPConvertibleTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm Methods pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term (WordN n) -> Term FPRoundingMode -> Term (FP eb sb) -> Term (WordN n) Source # pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term (WordN n) -> Term (FP eb sb) Source # sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType (WordN n) -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (WordN n) Source # sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType (WordN n) -> SBVType (FP eb sb) Source #
ValidFP eb sb => PEvalIEEEFPConvertibleTerm (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm Methods pevalFromFPOrTerm :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFP eb0 sb0 => Term (FP eb sb) -> Term FPRoundingMode -> Term (FP eb0 sb0) -> Term (FP eb sb) Source # pevalToFPTerm :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFP eb0 sb0 => Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb0 sb0) Source # sbvFromFPOrTerm :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFP eb0 sb0 => SBVType (FP eb sb) -> SBVType FPRoundingMode -> SBVType (FP eb0 sb0) -> SBVType (FP eb sb) Source # sbvToFPTerm :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFP eb0 sb0 => SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb0 sb0) Source #

Typed symbols

data SymbolKind Source #

The kind of a symbol.

All symbols are AnyKind, and all symbols other than general/tabular functions are ConstantKind.

Constructors

ConstantKind
AnyKind

data TypedSymbol (knd :: SymbolKind) t where Source #

A typed symbol is a symbol that is associated with a type. Note that the same symbol bodies with different types are considered different symbols and can coexist in a term.

Simple symbols can be created with the OverloadedStrings extension:

>>> "a" :: TypedSymbol 'AnyKind Bool
a :: Bool

Constructors

TypedSymbol
Fields :: (SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) => { unTypedSymbol :: Symbol } -> TypedSymbol knd t

Instances

Instances details

ModelOps Model AnySymbolSet TypedAnySymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods emptyModel :: Model Source # isEmptyModel :: Model -> Bool Source # modelContains :: TypedAnySymbol a -> Model -> Bool Source # valueOf :: TypedAnySymbol t -> Model -> Maybe t Source # insertValue :: TypedAnySymbol t -> t -> Model -> Model Source # exceptFor :: AnySymbolSet -> Model -> Model Source # exceptFor' :: TypedAnySymbol t -> Model -> Model Source # restrictTo :: AnySymbolSet -> Model -> Model Source # extendTo :: AnySymbolSet -> Model -> Model Source # exact :: AnySymbolSet -> Model -> Model Source #
Lift (TypedSymbol knd t :: Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods lift :: Quote m => TypedSymbol knd t -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => TypedSymbol knd t -> Code m (TypedSymbol knd t) #
SymbolSetOps (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods emptySet :: SymbolSet knd Source # isEmptySet :: SymbolSet knd -> Bool Source # containsSymbol :: TypedSymbol knd a -> SymbolSet knd -> Bool Source # insertSymbol :: TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd Source # intersectionSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd Source # unionSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd Source # differenceSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd Source #
SymbolSetRep (SomeTypedSymbol knd) (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: SomeTypedSymbol knd -> SymbolSet knd Source #
SymbolSetRep [SomeTypedSymbol knd] (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: [SomeTypedSymbol knd] -> SymbolSet knd Source #
SymbolSetRep [TypedSymbol knd t] (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: [TypedSymbol knd t] -> SymbolSet knd Source #
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) => IsString (TypedSymbol knd t) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods fromString :: String -> TypedSymbol knd t #
Show (TypedSymbol knd t) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods showsPrec :: Int -> TypedSymbol knd t -> ShowS # show :: TypedSymbol knd t -> String # showList :: [TypedSymbol knd t] -> ShowS #
NFData (TypedSymbol knd t) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: TypedSymbol knd t -> () #
Eq (TypedSymbol knd t) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: TypedSymbol knd t -> TypedSymbol knd t -> Bool # (/=) :: TypedSymbol knd t -> TypedSymbol knd t -> Bool #
Ord (TypedSymbol knd t) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods compare :: TypedSymbol knd t -> TypedSymbol knd t -> Ordering # (<) :: TypedSymbol knd t -> TypedSymbol knd t -> Bool # (<=) :: TypedSymbol knd t -> TypedSymbol knd t -> Bool # (>) :: TypedSymbol knd t -> TypedSymbol knd t -> Bool # (>=) :: TypedSymbol knd t -> TypedSymbol knd t -> Bool # max :: TypedSymbol knd t -> TypedSymbol knd t -> TypedSymbol knd t # min :: TypedSymbol knd t -> TypedSymbol knd t -> TypedSymbol knd t #
PPrint (TypedSymbol knd t) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.PPrint Methods pformat :: TypedSymbol knd t -> Doc ann Source # pformatPrec :: Int -> TypedSymbol knd t -> Doc ann Source # pformatList :: [TypedSymbol knd t] -> Doc ann Source #
Hashable (TypedSymbol knd t) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> TypedSymbol knd t -> Int # hash :: TypedSymbol knd t -> Int #
SymbolSetRep (TypedSymbol knd t) (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: TypedSymbol knd t -> SymbolSet knd Source #
SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b) (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b) -> SymbolSet knd Source #
SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c) (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c) -> SymbolSet knd Source #
SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d) (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d) -> SymbolSet knd Source #
SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e) (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e) -> SymbolSet knd Source #
SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f) (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f) -> SymbolSet knd Source #
SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f, TypedSymbol knd g) (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f, TypedSymbol knd g) -> SymbolSet knd Source #
SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f, TypedSymbol knd g, TypedSymbol knd h) (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f, TypedSymbol knd g, TypedSymbol knd h) -> SymbolSet knd Source #

type TypedConstantSymbol = TypedSymbol 'ConstantKind Source #

Constant symbol

type TypedAnySymbol = TypedSymbol 'AnyKind Source #

Any symbol

data SomeTypedSymbol knd where Source #

A non-indexed symbol. Type information are checked at runtime.

Constructors

SomeTypedSymbol :: forall knd t. TypeRep t -> TypedSymbol knd t -> SomeTypedSymbol knd

Instances

Instances details

Show (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods showsPrec :: Int -> SomeTypedSymbol knd -> ShowS # show :: SomeTypedSymbol knd -> String # showList :: [SomeTypedSymbol knd] -> ShowS #
NFData (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: SomeTypedSymbol knd -> () #
Eq (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool # (/=) :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool #
Ord (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods compare :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Ordering # (<) :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool # (<=) :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool # (>) :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool # (>=) :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool # max :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> SomeTypedSymbol knd # min :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> SomeTypedSymbol knd #
PPrint (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.PPrint Methods pformat :: SomeTypedSymbol knd -> Doc ann Source # pformatPrec :: Int -> SomeTypedSymbol knd -> Doc ann Source # pformatList :: [SomeTypedSymbol knd] -> Doc ann Source #
Hashable (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> SomeTypedSymbol knd -> Int # hash :: SomeTypedSymbol knd -> Int #
SymbolSetRep (SomeTypedSymbol knd) (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: SomeTypedSymbol knd -> SymbolSet knd Source #
SymbolSetRep [SomeTypedSymbol knd] (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: [SomeTypedSymbol knd] -> SymbolSet knd Source #

type SomeTypedConstantSymbol = SomeTypedSymbol 'ConstantKind Source #

Non-indexed constant symbol

type SomeTypedAnySymbol = SomeTypedSymbol 'AnyKind Source #

Non-indexed any symbol

class IsSymbolKind (ty :: SymbolKind) where Source #

Decision procedure for symbol kinds.

Associated Types

type SymbolKindConstraint ty :: Type -> Constraint Source #

Methods

decideSymbolKind :: Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind) Source #

Instances

Instances details

IsSymbolKind 'AnyKind Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type SymbolKindConstraint 'AnyKind :: Type -> Constraint Source # Methods decideSymbolKind :: Either ('AnyKind :~~: 'ConstantKind) ('AnyKind :~~: 'AnyKind) Source #
IsSymbolKind 'ConstantKind Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type SymbolKindConstraint 'ConstantKind :: Type -> Constraint Source # Methods decideSymbolKind :: Either ('ConstantKind :~~: 'ConstantKind) ('ConstantKind :~~: 'AnyKind) Source #

showUntyped :: TypedSymbol knd t -> String Source #

Show a typed symbol without the type information.

withSymbolSupported :: TypedSymbol knd t -> (SupportedPrim t => a) -> a Source #

Introduce the SupportedPrim constraint from the TypedSymbol.

someTypedSymbol :: forall knd t. TypedSymbol knd t -> SomeTypedSymbol knd Source #

Construct a SomeTypedSymbol from a TypedSymbol.

eqHeteroSymbol :: forall ta a tb b. TypedSymbol ta a -> TypedSymbol tb b -> Bool Source #

Compare two TypedSymbols for equality.

castSomeTypedSymbol :: IsSymbolKind knd' => SomeTypedSymbol knd -> Maybe (SomeTypedSymbol knd') Source #

Cast a typed symbol to a different kind. Check if the kind is compatible.

withSymbolKind :: TypedSymbol knd t -> (IsSymbolKind knd => a) -> a Source #

Introduce the IsSymbolKind constraint from the TypedSymbol.

Terms

data FPTrait Source #

Traits for IEEE floating point numbers.

Constructors

FPIsNaN
FPIsPositive
FPIsNegative
FPIsPositiveInfinite
FPIsNegativeInfinite
FPIsInfinite
FPIsPositiveZero
FPIsNegativeZero
FPIsZero
FPIsNormal
FPIsSubnormal
FPIsPoint

Instances

Instances details

Generic FPTrait Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type Rep FPTrait :: Type -> Type # Methods from :: FPTrait -> Rep FPTrait x # to :: Rep FPTrait x -> FPTrait #
Show FPTrait Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods showsPrec :: Int -> FPTrait -> ShowS # show :: FPTrait -> String # showList :: [FPTrait] -> ShowS #
NFData FPTrait Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: FPTrait -> () #
Eq FPTrait Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: FPTrait -> FPTrait -> Bool # (/=) :: FPTrait -> FPTrait -> Bool #
Ord FPTrait Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods compare :: FPTrait -> FPTrait -> Ordering # (<) :: FPTrait -> FPTrait -> Bool # (<=) :: FPTrait -> FPTrait -> Bool # (>) :: FPTrait -> FPTrait -> Bool # (>=) :: FPTrait -> FPTrait -> Bool # max :: FPTrait -> FPTrait -> FPTrait # min :: FPTrait -> FPTrait -> FPTrait #
Hashable FPTrait Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> FPTrait -> Int # hash :: FPTrait -> Int #
Lift FPTrait Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods lift :: Quote m => FPTrait -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => FPTrait -> Code m FPTrait #
type Rep FPTrait Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type Rep FPTrait = D1 ('MetaData "FPTrait" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.8.0.0-9ziui23pS5H4p62qxsVv1c" 'False) (((C1 ('MetaCons "FPIsNaN" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPIsPositive" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPIsNegative" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "FPIsPositiveInfinite" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPIsNegativeInfinite" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPIsInfinite" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "FPIsPositiveZero" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPIsNegativeZero" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPIsZero" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "FPIsNormal" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPIsSubnormal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPIsPoint" 'PrefixI 'False) (U1 :: Type -> Type)))))

data FPUnaryOp Source #

Unary floating point operations.

Constructors

FPAbs
FPNeg

Instances

Instances details

Generic FPUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type Rep FPUnaryOp :: Type -> Type # Methods from :: FPUnaryOp -> Rep FPUnaryOp x # to :: Rep FPUnaryOp x -> FPUnaryOp #
Show FPUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods showsPrec :: Int -> FPUnaryOp -> ShowS # show :: FPUnaryOp -> String # showList :: [FPUnaryOp] -> ShowS #
NFData FPUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: FPUnaryOp -> () #
Eq FPUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: FPUnaryOp -> FPUnaryOp -> Bool # (/=) :: FPUnaryOp -> FPUnaryOp -> Bool #
Ord FPUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods compare :: FPUnaryOp -> FPUnaryOp -> Ordering # (<) :: FPUnaryOp -> FPUnaryOp -> Bool # (<=) :: FPUnaryOp -> FPUnaryOp -> Bool # (>) :: FPUnaryOp -> FPUnaryOp -> Bool # (>=) :: FPUnaryOp -> FPUnaryOp -> Bool # max :: FPUnaryOp -> FPUnaryOp -> FPUnaryOp # min :: FPUnaryOp -> FPUnaryOp -> FPUnaryOp #
Hashable FPUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> FPUnaryOp -> Int # hash :: FPUnaryOp -> Int #
Lift FPUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods lift :: Quote m => FPUnaryOp -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => FPUnaryOp -> Code m FPUnaryOp #
type Rep FPUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type Rep FPUnaryOp = D1 ('MetaData "FPUnaryOp" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.8.0.0-9ziui23pS5H4p62qxsVv1c" 'False) (C1 ('MetaCons "FPAbs" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPNeg" 'PrefixI 'False) (U1 :: Type -> Type))

data FPBinaryOp Source #

Binary floating point operations.

Constructors

FPRem
FPMinimum
FPMinimumNumber
FPMaximum
FPMaximumNumber

Instances

Instances details

Generic FPBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type Rep FPBinaryOp :: Type -> Type # Methods from :: FPBinaryOp -> Rep FPBinaryOp x # to :: Rep FPBinaryOp x -> FPBinaryOp #
Show FPBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods showsPrec :: Int -> FPBinaryOp -> ShowS # show :: FPBinaryOp -> String # showList :: [FPBinaryOp] -> ShowS #
NFData FPBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: FPBinaryOp -> () #
Eq FPBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: FPBinaryOp -> FPBinaryOp -> Bool # (/=) :: FPBinaryOp -> FPBinaryOp -> Bool #
Ord FPBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods compare :: FPBinaryOp -> FPBinaryOp -> Ordering # (<) :: FPBinaryOp -> FPBinaryOp -> Bool # (<=) :: FPBinaryOp -> FPBinaryOp -> Bool # (>) :: FPBinaryOp -> FPBinaryOp -> Bool # (>=) :: FPBinaryOp -> FPBinaryOp -> Bool # max :: FPBinaryOp -> FPBinaryOp -> FPBinaryOp # min :: FPBinaryOp -> FPBinaryOp -> FPBinaryOp #
Hashable FPBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> FPBinaryOp -> Int # hash :: FPBinaryOp -> Int #
Lift FPBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods lift :: Quote m => FPBinaryOp -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => FPBinaryOp -> Code m FPBinaryOp #
type Rep FPBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type Rep FPBinaryOp = D1 ('MetaData "FPBinaryOp" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.8.0.0-9ziui23pS5H4p62qxsVv1c" 'False) ((C1 ('MetaCons "FPRem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPMinimum" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FPMinimumNumber" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPMaximum" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPMaximumNumber" 'PrefixI 'False) (U1 :: Type -> Type))))

data FPRoundingUnaryOp Source #

Unary floating point operations with rounding modes.

Constructors

FPSqrt
FPRoundToIntegral

Instances

Instances details

Generic FPRoundingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type Rep FPRoundingUnaryOp :: Type -> Type # Methods from :: FPRoundingUnaryOp -> Rep FPRoundingUnaryOp x # to :: Rep FPRoundingUnaryOp x -> FPRoundingUnaryOp #
Show FPRoundingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods showsPrec :: Int -> FPRoundingUnaryOp -> ShowS # show :: FPRoundingUnaryOp -> String # showList :: [FPRoundingUnaryOp] -> ShowS #
NFData FPRoundingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: FPRoundingUnaryOp -> () #
Eq FPRoundingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool # (/=) :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool #
Ord FPRoundingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods compare :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Ordering # (<) :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool # (<=) :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool # (>) :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool # (>=) :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> Bool # max :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> FPRoundingUnaryOp # min :: FPRoundingUnaryOp -> FPRoundingUnaryOp -> FPRoundingUnaryOp #
Hashable FPRoundingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> FPRoundingUnaryOp -> Int # hash :: FPRoundingUnaryOp -> Int #
Lift FPRoundingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods lift :: Quote m => FPRoundingUnaryOp -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => FPRoundingUnaryOp -> Code m FPRoundingUnaryOp #
type Rep FPRoundingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type Rep FPRoundingUnaryOp = D1 ('MetaData "FPRoundingUnaryOp" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.8.0.0-9ziui23pS5H4p62qxsVv1c" 'False) (C1 ('MetaCons "FPSqrt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPRoundToIntegral" 'PrefixI 'False) (U1 :: Type -> Type))

data FPRoundingBinaryOp Source #

Binary floating point operations with rounding modes.

Constructors

FPAdd
FPSub
FPMul
FPDiv

Instances

Instances details

Generic FPRoundingBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type Rep FPRoundingBinaryOp :: Type -> Type # Methods from :: FPRoundingBinaryOp -> Rep FPRoundingBinaryOp x # to :: Rep FPRoundingBinaryOp x -> FPRoundingBinaryOp #
Show FPRoundingBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods showsPrec :: Int -> FPRoundingBinaryOp -> ShowS # show :: FPRoundingBinaryOp -> String # showList :: [FPRoundingBinaryOp] -> ShowS #
NFData FPRoundingBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: FPRoundingBinaryOp -> () #
Eq FPRoundingBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool # (/=) :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool #
Ord FPRoundingBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods compare :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Ordering # (<) :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool # (<=) :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool # (>) :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool # (>=) :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> Bool # max :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> FPRoundingBinaryOp # min :: FPRoundingBinaryOp -> FPRoundingBinaryOp -> FPRoundingBinaryOp #
Hashable FPRoundingBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> FPRoundingBinaryOp -> Int # hash :: FPRoundingBinaryOp -> Int #
Lift FPRoundingBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods lift :: Quote m => FPRoundingBinaryOp -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => FPRoundingBinaryOp -> Code m FPRoundingBinaryOp #
type Rep FPRoundingBinaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type Rep FPRoundingBinaryOp = D1 ('MetaData "FPRoundingBinaryOp" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.8.0.0-9ziui23pS5H4p62qxsVv1c" 'False) ((C1 ('MetaCons "FPAdd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPSub" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FPMul" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPDiv" 'PrefixI 'False) (U1 :: Type -> Type)))

data FloatingUnaryOp Source #

Unary floating point operations.

Constructors

FloatingExp
FloatingLog
FloatingSqrt
FloatingSin
FloatingCos
FloatingTan
FloatingAsin
FloatingAcos
FloatingAtan
FloatingSinh
FloatingCosh
FloatingTanh
FloatingAsinh
FloatingAcosh
FloatingAtanh

Instances

Instances details

Generic FloatingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type Rep FloatingUnaryOp :: Type -> Type # Methods from :: FloatingUnaryOp -> Rep FloatingUnaryOp x # to :: Rep FloatingUnaryOp x -> FloatingUnaryOp #
Show FloatingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods showsPrec :: Int -> FloatingUnaryOp -> ShowS # show :: FloatingUnaryOp -> String # showList :: [FloatingUnaryOp] -> ShowS #
NFData FloatingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: FloatingUnaryOp -> () #
Eq FloatingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: FloatingUnaryOp -> FloatingUnaryOp -> Bool # (/=) :: FloatingUnaryOp -> FloatingUnaryOp -> Bool #
Ord FloatingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods compare :: FloatingUnaryOp -> FloatingUnaryOp -> Ordering # (<) :: FloatingUnaryOp -> FloatingUnaryOp -> Bool # (<=) :: FloatingUnaryOp -> FloatingUnaryOp -> Bool # (>) :: FloatingUnaryOp -> FloatingUnaryOp -> Bool # (>=) :: FloatingUnaryOp -> FloatingUnaryOp -> Bool # max :: FloatingUnaryOp -> FloatingUnaryOp -> FloatingUnaryOp # min :: FloatingUnaryOp -> FloatingUnaryOp -> FloatingUnaryOp #
Hashable FloatingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> FloatingUnaryOp -> Int # hash :: FloatingUnaryOp -> Int #
Lift FloatingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods lift :: Quote m => FloatingUnaryOp -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => FloatingUnaryOp -> Code m FloatingUnaryOp #
type Rep FloatingUnaryOp Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type Rep FloatingUnaryOp = D1 ('MetaData "FloatingUnaryOp" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.8.0.0-9ziui23pS5H4p62qxsVv1c" 'False) (((C1 ('MetaCons "FloatingExp" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FloatingLog" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingSqrt" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FloatingSin" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingCos" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FloatingTan" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingAsin" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "FloatingAcos" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingAtan" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FloatingSinh" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingCosh" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FloatingTanh" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingAsinh" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FloatingAcosh" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingAtanh" 'PrefixI 'False) (U1 :: Type -> Type)))))

data Term t where Source #

Internal representation for Grisette symbolic terms.

Constructors

ConTerm :: SupportedPrim t => !Id -> !t -> Term t
SymTerm :: SupportedPrim t => !Id -> !(TypedSymbol 'AnyKind t) -> Term t
ForallTerm :: SupportedNonFuncPrim t => !Id -> !(TypedSymbol 'ConstantKind t) -> !(Term Bool) -> Term Bool
ExistsTerm :: SupportedNonFuncPrim t => !Id -> !(TypedSymbol 'ConstantKind t) -> !(Term Bool) -> Term Bool
UnaryTerm :: UnaryOp tag arg t => !Id -> !tag -> !(Term arg) -> Term t
BinaryTerm :: BinaryOp tag arg1 arg2 t => !Id -> !tag -> !(Term arg1) -> !(Term arg2) -> Term t
TernaryTerm :: TernaryOp tag arg1 arg2 arg3 t => !Id -> !tag -> !(Term arg1) -> !(Term arg2) -> !(Term arg3) -> Term t
NotTerm :: !Id -> !(Term Bool) -> Term Bool
OrTerm :: !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
AndTerm :: !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
EqTerm :: SupportedNonFuncPrim t => !Id -> !(Term t) -> !(Term t) -> Term Bool
DistinctTerm :: SupportedNonFuncPrim t => !Id -> !(NonEmpty (Term t)) -> Term Bool
ITETerm :: SupportedPrim t => !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t
AddNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
NegNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> Term t
MulNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
AbsNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> Term t
SignumNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> Term t
LtOrdTerm :: PEvalOrdTerm t => !Id -> !(Term t) -> !(Term t) -> Term Bool
LeOrdTerm :: PEvalOrdTerm t => !Id -> !(Term t) -> !(Term t) -> Term Bool
AndBitsTerm :: PEvalBitwiseTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
OrBitsTerm :: PEvalBitwiseTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
XorBitsTerm :: PEvalBitwiseTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
ComplementBitsTerm :: PEvalBitwiseTerm t => !Id -> !(Term t) -> Term t
ShiftLeftTerm :: PEvalShiftTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
ShiftRightTerm :: PEvalShiftTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
RotateLeftTerm :: PEvalRotateTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
RotateRightTerm :: PEvalRotateTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
BitCastTerm :: PEvalBitCastTerm a b => !Id -> !(Term a) -> Term b
BitCastOrTerm :: PEvalBitCastOrTerm a b => !Id -> !(Term b) -> !(Term a) -> Term b
BVConcatTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r)) => !Id -> !(Term (bv l)) -> !(Term (bv r)) -> Term (bv (l + r))
BVSelectTerm :: (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => !Id -> !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv n)) -> Term (bv w)
BVExtendTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => !Id -> !Bool -> !(TypeRep r) -> !(Term (bv l)) -> Term (bv r)
ApplyTerm :: (SupportedPrim a, SupportedPrim b, SupportedPrim f, PEvalApplyTerm f a b) => !Id -> !(Term f) -> !(Term a) -> Term b
DivIntegralTerm :: PEvalDivModIntegralTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
ModIntegralTerm :: PEvalDivModIntegralTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
QuotIntegralTerm :: PEvalDivModIntegralTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
RemIntegralTerm :: PEvalDivModIntegralTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
FPTraitTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => !Id -> !FPTrait -> !(Term (FP eb sb)) -> Term Bool
FdivTerm :: PEvalFractionalTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
RecipTerm :: PEvalFractionalTerm t => !Id -> !(Term t) -> Term t
FloatingUnaryTerm :: PEvalFloatingTerm t => !Id -> !FloatingUnaryOp -> !(Term t) -> Term t
PowerTerm :: PEvalFloatingTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
FPUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => !Id -> !FPUnaryOp -> !(Term (FP eb sb)) -> Term (FP eb sb)
FPBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => !Id -> !FPBinaryOp -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> Term (FP eb sb)
FPRoundingUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !Id -> !FPRoundingUnaryOp -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> Term (FP eb sb)
FPRoundingBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !Id -> !FPRoundingBinaryOp -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> Term (FP eb sb)
FPFMATerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !Id -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> Term (FP eb sb)
FromIntegralTerm :: PEvalFromIntegralTerm a b => !Id -> !(Term a) -> Term b
FromFPOrTerm :: (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !Id -> !(Term a) -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> Term a
ToFPTerm :: (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !Id -> !(Term FPRoundingMode) -> !(Term a) -> Proxy eb -> Proxy sb -> Term (FP eb sb)

Instances

Instances details

Lift (Term t :: Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods lift :: Quote m => Term t -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => Term t -> Code m (Term t) #
Show (Term ty) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods showsPrec :: Int -> Term ty -> ShowS # show :: Term ty -> String # showList :: [Term ty] -> ShowS #
NFData (Term a) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: Term a -> () #
SupportedPrim t => Eq (Term t) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: Term t -> Term t -> Bool # (/=) :: Term t -> Term t -> Bool #
SupportedPrim t => Eq (Description (Term t)) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: Description (Term t) -> Description (Term t) -> Bool # (/=) :: Description (Term t) -> Description (Term t) -> Bool #
SupportedPrim t => Hashable (Term t) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> Term t -> Int # hash :: Term t -> Int #
SupportedPrim t => Hashable (Description (Term t)) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> Description (Term t) -> Int # hash :: Description (Term t) -> Int #
SupportedPrim t => Interned (Term t) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types data Description (Term t) # type Uninterned (Term t) # Methods describe :: Uninterned (Term t) -> Description (Term t) # identify :: Id -> Uninterned (Term t) -> Term t # seedIdentity :: p (Term t) -> Id # cacheWidth :: p (Term t) -> Int # modifyAdvice :: IO (Term t) -> IO (Term t) # cache :: Cache (Term t) #
data Description (Term t) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term data Description (Term t) where DConTerm :: forall t. t -> Description (Term t) DSymTerm :: forall t. TypedSymbol 'AnyKind t -> Description (Term t) DForallTerm :: forall t1. !(TypeRep t1, TypedSymbol 'ConstantKind t1) -> !Id -> Description (Term Bool) DExistsTerm :: forall t1. !(TypeRep t1, TypedSymbol 'ConstantKind t1) -> !Id -> Description (Term Bool) DUnaryTerm :: forall tag arg t. (Eq tag, Hashable tag) => !(TypeRep tag, tag) -> !(TypeRep arg, Id) -> Description (Term t) DBinaryTerm :: forall tag arg1 arg2 t. (Eq tag, Hashable tag) => !(TypeRep tag, tag) -> !(TypeRep arg1, Id) -> !(TypeRep arg2, Id) -> Description (Term t) DTernaryTerm :: forall tag arg1 arg2 arg3 t. (Eq tag, Hashable tag) => !(TypeRep tag, tag) -> !(TypeRep arg1, Id) -> !(TypeRep arg2, Id) -> !(TypeRep arg3, Id) -> Description (Term t) DNotTerm :: !Id -> Description (Term Bool) DOrTerm :: !Id -> !Id -> Description (Term Bool) DAndTerm :: !Id -> !Id -> Description (Term Bool) DEqTerm :: forall args. TypeRep args -> !Id -> !Id -> Description (Term Bool) DDistinctTerm :: forall args. TypeRep args -> !(NonEmpty Id) -> Description (Term Bool) DITETerm :: forall t. !Id -> !Id -> !Id -> Description (Term t) DAddNumTerm :: forall t. !Id -> !Id -> Description (Term t) DNegNumTerm :: forall t. !Id -> Description (Term t) DMulNumTerm :: forall t. !Id -> !Id -> Description (Term t) DAbsNumTerm :: forall t. !Id -> Description (Term t) DSignumNumTerm :: forall t. !Id -> Description (Term t) DLtOrdTerm :: forall args. TypeRep args -> !Id -> !Id -> Description (Term Bool) DLeOrdTerm :: forall args. TypeRep args -> !Id -> !Id -> Description (Term Bool) DAndBitsTerm :: forall t. !Id -> !Id -> Description (Term t) DOrBitsTerm :: forall t. !Id -> !Id -> Description (Term t) DXorBitsTerm :: forall t. !Id -> !Id -> Description (Term t) DComplementBitsTerm :: forall t. !Id -> Description (Term t) DShiftLeftTerm :: forall t. !Id -> !Id -> Description (Term t) DShiftRightTerm :: forall t. !Id -> !Id -> Description (Term t) DRotateLeftTerm :: forall t. !Id -> !Id -> Description (Term t) DRotateRightTerm :: forall t. !Id -> !Id -> Description (Term t) DBVConcatTerm :: forall bv1 bv2 t. TypeRep bv1 -> TypeRep bv2 -> !Id -> !Id -> Description (Term t) DBitCastTerm :: forall a t. !(TypeRep a, Id) -> Description (Term t) DBitCastOrTerm :: forall a t. Id -> !(TypeRep a, Id) -> Description (Term t) DBVSelectTerm :: forall (bv :: Nat -> Type) (n :: Nat) (w :: Nat) (ix :: Nat). !(TypeRep ix) -> !(TypeRep (bv n), Id) -> Description (Term (bv w)) DBVExtendTerm :: forall (bv :: Nat -> Type) (l :: Nat) (r :: Nat). !Bool -> !(TypeRep r) -> !(TypeRep (bv l), Id) -> Description (Term (bv r)) DApplyTerm :: forall f a t. PEvalApplyTerm f a t => !(TypeRep f, Id) -> !(TypeRep a, Id) -> Description (Term t) DDivIntegralTerm :: forall t. !Id -> !Id -> Description (Term t) DModIntegralTerm :: forall t. !Id -> !Id -> Description (Term t) DQuotIntegralTerm :: forall t. !Id -> !Id -> Description (Term t) DRemIntegralTerm :: forall t. !Id -> !Id -> Description (Term t) DFPTraitTerm :: forall (eb :: Nat) (sb :: Nat). (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPTrait -> !(TypeRep (FP eb sb), Id) -> Description (Term Bool) DFdivTerm :: forall t. !Id -> !Id -> Description (Term t) DRecipTerm :: forall t. !Id -> Description (Term t) DFloatingUnaryTerm :: forall t. FloatingUnaryOp -> !Id -> Description (Term t) DPowerTerm :: forall t. !Id -> !Id -> Description (Term t) DFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat). FPUnaryOp -> !Id -> Description (Term (FP eb sb)) DFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat). FPBinaryOp -> !Id -> !Id -> Description (Term (FP eb sb)) DFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat). FPRoundingUnaryOp -> !Id -> !Id -> Description (Term (FP eb sb)) DFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat). FPRoundingBinaryOp -> !Id -> !Id -> !Id -> Description (Term (FP eb sb)) DFPFMATerm :: forall (eb :: Nat) (sb :: Nat). !Id -> !Id -> !Id -> !Id -> Description (Term (FP eb sb)) DFromIntegralTerm :: forall a t. PEvalFromIntegralTerm a t => !(TypeRep a, Id) -> Description (Term t) DFromFPOrTerm :: forall t (eb :: Nat) (sb :: Nat). (PEvalIEEEFPConvertibleTerm t, ValidFP eb sb) => !Id -> !Id -> !(TypeRep (FP eb sb), Id) -> Description (Term t) DToFPTerm :: forall a (eb :: Nat) (sb :: Nat). (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) => !Id -> !(TypeRep a, Id) -> Description (Term (FP eb sb))
type Uninterned (Term t) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type Uninterned (Term t) = UTerm t

identity :: Term t -> Id Source #

Return the ID of a term.

identityWithTypeRep :: forall t. Term t -> (SomeTypeRep, Id) Source #

Return the ID and the type representation of a term.

introSupportedPrimConstraint :: forall t a. Term t -> (SupportedPrim t => a) -> a Source #

Introduce the SupportedPrim constraint from a term.

pformatTerm :: forall t. SupportedPrim t => Term t -> String Source #

Pretty-print a term.

Interning

data UTerm t where Source #

Term without identity (before internalizing).

Constructors

UConTerm :: SupportedPrim t => !t -> UTerm t
USymTerm :: SupportedPrim t => !(TypedSymbol 'AnyKind t) -> UTerm t
UForallTerm :: SupportedNonFuncPrim t => !(TypedSymbol 'ConstantKind t) -> !(Term Bool) -> UTerm Bool
UExistsTerm :: SupportedNonFuncPrim t => !(TypedSymbol 'ConstantKind t) -> !(Term Bool) -> UTerm Bool
UUnaryTerm :: UnaryOp tag arg t => !tag -> !(Term arg) -> UTerm t
UBinaryTerm :: BinaryOp tag arg1 arg2 t => !tag -> !(Term arg1) -> !(Term arg2) -> UTerm t
UTernaryTerm :: TernaryOp tag arg1 arg2 arg3 t => !tag -> !(Term arg1) -> !(Term arg2) -> !(Term arg3) -> UTerm t
UNotTerm :: !(Term Bool) -> UTerm Bool
UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
UEqTerm :: SupportedNonFuncPrim t => !(Term t) -> !(Term t) -> UTerm Bool
UDistinctTerm :: SupportedNonFuncPrim t => !(NonEmpty (Term t)) -> UTerm Bool
UITETerm :: SupportedPrim t => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
UAddNumTerm :: PEvalNumTerm t => !(Term t) -> !(Term t) -> UTerm t
UNegNumTerm :: PEvalNumTerm t => !(Term t) -> UTerm t
UMulNumTerm :: PEvalNumTerm t => !(Term t) -> !(Term t) -> UTerm t
UAbsNumTerm :: PEvalNumTerm t => !(Term t) -> UTerm t
USignumNumTerm :: PEvalNumTerm t => !(Term t) -> UTerm t
ULtOrdTerm :: PEvalOrdTerm t => !(Term t) -> !(Term t) -> UTerm Bool
ULeOrdTerm :: PEvalOrdTerm t => !(Term t) -> !(Term t) -> UTerm Bool
UAndBitsTerm :: PEvalBitwiseTerm t => !(Term t) -> !(Term t) -> UTerm t
UOrBitsTerm :: PEvalBitwiseTerm t => !(Term t) -> !(Term t) -> UTerm t
UXorBitsTerm :: PEvalBitwiseTerm t => !(Term t) -> !(Term t) -> UTerm t
UComplementBitsTerm :: PEvalBitwiseTerm t => !(Term t) -> UTerm t
UShiftLeftTerm :: PEvalShiftTerm t => !(Term t) -> !(Term t) -> UTerm t
UShiftRightTerm :: PEvalShiftTerm t => !(Term t) -> !(Term t) -> UTerm t
URotateLeftTerm :: PEvalRotateTerm t => !(Term t) -> !(Term t) -> UTerm t
URotateRightTerm :: PEvalRotateTerm t => !(Term t) -> !(Term t) -> UTerm t
UBitCastTerm :: PEvalBitCastTerm a b => !(Term a) -> UTerm b
UBitCastOrTerm :: PEvalBitCastOrTerm a b => !(Term b) -> !(Term a) -> UTerm b
UBVConcatTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r)) => !(Term (bv l)) -> !(Term (bv r)) -> UTerm (bv (l + r))
UBVSelectTerm :: (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv n)) -> UTerm (bv w)
UBVExtendTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => !Bool -> !(TypeRep r) -> !(Term (bv l)) -> UTerm (bv r)
UApplyTerm :: (SupportedPrim a, SupportedPrim b, SupportedPrim f, PEvalApplyTerm f a b) => Term f -> Term a -> UTerm b
UDivIntegralTerm :: PEvalDivModIntegralTerm t => !(Term t) -> !(Term t) -> UTerm t
UModIntegralTerm :: PEvalDivModIntegralTerm t => !(Term t) -> !(Term t) -> UTerm t
UQuotIntegralTerm :: PEvalDivModIntegralTerm t => !(Term t) -> !(Term t) -> UTerm t
URemIntegralTerm :: PEvalDivModIntegralTerm t => !(Term t) -> !(Term t) -> UTerm t
UFPTraitTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => !FPTrait -> !(Term (FP eb sb)) -> UTerm Bool
UFdivTerm :: PEvalFractionalTerm t => !(Term t) -> !(Term t) -> UTerm t
URecipTerm :: PEvalFractionalTerm t => !(Term t) -> UTerm t
UFloatingUnaryTerm :: PEvalFloatingTerm t => !FloatingUnaryOp -> !(Term t) -> UTerm t
UPowerTerm :: PEvalFloatingTerm t => !(Term t) -> !(Term t) -> UTerm t
UFPUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => !FPUnaryOp -> !(Term (FP eb sb)) -> UTerm (FP eb sb)
UFPBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => !FPBinaryOp -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> UTerm (FP eb sb)
UFPRoundingUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !FPRoundingUnaryOp -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> UTerm (FP eb sb)
UFPRoundingBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !FPRoundingBinaryOp -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> UTerm (FP eb sb)
UFPFMATerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> !(Term (FP eb sb)) -> UTerm (FP eb sb)
UFromIntegralTerm :: PEvalFromIntegralTerm a b => !(Term a) -> UTerm b
UFromFPOrTerm :: (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim FPRoundingMode, SupportedPrim (FP eb sb)) => Term a -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> UTerm a
UToFPTerm :: (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim FPRoundingMode, SupportedPrim (FP eb sb)) => !(Term FPRoundingMode) -> !(Term a) -> Proxy eb -> Proxy sb -> UTerm (FP eb sb)

prettyPrintTerm :: Term t -> Doc ann Source #

Pretty-print a term, possibly eliding parts of it.

forallTerm :: (SupportedNonFuncPrim t, Typeable t) => TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool Source #

Construct and internalizing a ForallTerm.

existsTerm :: (SupportedNonFuncPrim t, Typeable t) => TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool Source #

Construct and internalizing a ExistsTerm.

constructUnary :: forall tag arg t. (SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t, Show tag) => tag -> Term arg -> Term t Source #

Construct and internalizing a UnaryTerm.

constructBinary :: forall tag arg1 arg2 t. (SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term t Source #

Construct and internalizing a BinaryTerm.

constructTernary :: forall tag arg1 arg2 arg3 t. (SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t Source #

Construct and internalizing a TernaryTerm.

conTerm :: (SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) => t -> Term t Source #

Construct and internalizing a ConTerm.

symTerm :: forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t Source #

Construct and internalizing a SymTerm.

ssymTerm :: (SupportedPrim t, Typeable t) => Identifier -> Term t Source #

Construct and internalizing a SymTerm with an identifier, using simple symbols.

isymTerm :: (SupportedPrim t, Typeable t) => Identifier -> Int -> Term t Source #

Construct and internalizing a SymTerm with an identifier and an index, using indexed symbols.

notTerm :: Term Bool -> Term Bool Source #

Construct and internalizing a NotTerm.

orTerm :: Term Bool -> Term Bool -> Term Bool Source #

Construct and internalizing a OrTerm.

andTerm :: Term Bool -> Term Bool -> Term Bool Source #

Construct and internalizing a AndTerm.

eqTerm :: SupportedNonFuncPrim a => Term a -> Term a -> Term Bool Source #

Construct and internalizing a EqTerm.

distinctTerm :: SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool Source #

Construct and internalizing a DistinctTerm.

iteTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a Source #

Construct and internalizing a ITETerm.

addNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a AddNumTerm.

negNumTerm :: PEvalNumTerm a => Term a -> Term a Source #

Construct and internalizing a NegNumTerm.

mulNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a MulNumTerm.

absNumTerm :: PEvalNumTerm a => Term a -> Term a Source #

Construct and internalizing a AbsNumTerm.

signumNumTerm :: PEvalNumTerm a => Term a -> Term a Source #

Construct and internalizing a SignumNumTerm.

ltOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool Source #

Construct and internalizing a LtOrdTerm.

leOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool Source #

Construct and internalizing a LeOrdTerm.

andBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a AndBitsTerm.

orBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a OrBitsTerm.

xorBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a XorBitsTerm.

complementBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a Source #

Construct and internalizing a ComplementBitsTerm.

shiftLeftTerm :: PEvalShiftTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a ShiftLeftTerm.

shiftRightTerm :: PEvalShiftTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a ShiftRightTerm.

rotateLeftTerm :: PEvalRotateTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a RotateLeftTerm.

rotateRightTerm :: PEvalRotateTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a RotateRightTerm.

bitCastTerm :: PEvalBitCastTerm a b => Term a -> Term b Source #

Construct and internalizing a BitCastTerm.

bitCastOrTerm :: PEvalBitCastOrTerm a b => Term b -> Term a -> Term b Source #

Construct and internalizing a BitCastOrTerm.

bvconcatTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r)) => Term (bv l) -> Term (bv r) -> Term (bv (l + r)) Source #

Construct and internalizing a BVConcatTerm.

bvselectTerm :: forall bv n ix w p q. (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (bv n) -> Term (bv w) Source #

Construct and internalizing a BVSelectTerm.

bvextendTerm :: forall bv l r proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (bv l) -> Term (bv r) Source #

Construct and internalizing a BVExtendTerm.

bvsignExtendTerm :: forall bv l r proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => proxy r -> Term (bv l) -> Term (bv r) Source #

Construct and internalizing a BVExtendTerm with sign extension.

bvzeroExtendTerm :: forall bv l r proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => proxy r -> Term (bv l) -> Term (bv r) Source #

Construct and internalizing a BVExtendTerm with zero extension.

applyTerm :: (SupportedPrim a, SupportedPrim b, SupportedPrim f, PEvalApplyTerm f a b) => Term f -> Term a -> Term b Source #

Construct and internalizing a ApplyTerm.

divIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a DivIntegralTerm.

modIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a ModIntegralTerm.

quotIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a QuotIntegralTerm.

remIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a RemIntegralTerm.

fpTraitTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPTrait -> Term (FP eb sb) -> Term Bool Source #

Construct and internalizing a FPTraitTerm.

fdivTerm :: PEvalFractionalTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a FdivTerm.

recipTerm :: PEvalFractionalTerm a => Term a -> Term a Source #

Construct and internalizing a RecipTerm.

floatingUnaryTerm :: PEvalFloatingTerm a => FloatingUnaryOp -> Term a -> Term a Source #

Construct and internalizing a FloatingUnaryTerm.

powerTerm :: PEvalFloatingTerm a => Term a -> Term a -> Term a Source #

Construct and internalizing a PowerTerm.

fpUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb) Source #

Construct and internalizing a FPUnaryTerm.

fpBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb)) => FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

Construct and internalizing a FPBinaryTerm.

fpRoundingUnaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) Source #

Construct and internalizing a FPRoundingUnaryTerm.

fpRoundingBinaryTerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

Construct and internalizing a FPRoundingBinaryTerm.

fpFMATerm :: (ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim FPRoundingMode) => Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

Construct and internalizing a FPFMATerm.

fromIntegralTerm :: PEvalFromIntegralTerm a b => Term a -> Term b Source #

Construct and internalizing a FromIntegralTerm.

fromFPOrTerm :: (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim FPRoundingMode, SupportedPrim (FP eb sb)) => Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a Source #

Construct and internalizing a FromFPOrTerm.

toFPTerm :: forall a eb sb. (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim FPRoundingMode, SupportedPrim (FP eb sb)) => Term FPRoundingMode -> Term a -> Term (FP eb sb) Source #

Construct and internalizing a ToFPTerm.

Support for boolean type

trueTerm :: Term Bool Source #

Construct and internalizing True term.

falseTerm :: Term Bool Source #

Construct and internalizing False term.

pattern BoolConTerm :: Bool -> Term a Source #

Pattern matcher for concrete Bool terms.

pattern TrueTerm :: Term a Source #

Pattern matcher for True term.

pattern FalseTerm :: Term a Source #

Pattern matcher for False term.

pattern BoolTerm :: Term Bool -> Term a Source #

Pattern matcher for Bool terms.

pevalNotTerm :: Term Bool -> Term Bool Source #

Partial evaluation for not terms.

pevalOrTerm :: Term Bool -> Term Bool -> Term Bool Source #

Partial evaluation for or terms.

pevalAndTerm :: Term Bool -> Term Bool -> Term Bool Source #

Partial evaluation for and terms.

pevalImplyTerm :: Term Bool -> Term Bool -> Term Bool Source #

Partial evaluation for imply terms.

pevalXorTerm :: Term Bool -> Term Bool -> Term Bool Source #

Partial evaluation for xor terms.

pevalITEBasic :: SupportedPrim a => Term Bool -> Term a -> Term a -> Maybe (Term a) Source #

Basic partial evaluation for ITE terms.

pevalITEBasicTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a Source #

Basic partial evaluation for ITE terms.

pevalDefaultEqTerm :: SupportedNonFuncPrim a => Term a -> Term a -> Term Bool Source #

Default partial evaluation for equality terms.

type NonFuncPrimConstraint a = (SymVal (NonFuncSBVBaseType a), EqSymbolic (SBVType a), Mergeable (SBVType a), SMTDefinable (SBVType a), Mergeable (SBVType a), SBVType a ~ SBV (NonFuncSBVBaseType a), PrimConstraint a) Source #

Type class for resolving the constraint for a supported non-function primitive type.

class (SupportedPrim a, Ord a) => NonFuncSBVRep a Source #

Type class for resolving the base type for the SBV type for the primitive type.

Associated Types

type NonFuncSBVBaseType a Source #

Instances

Instances details

NonFuncSBVRep AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type NonFuncSBVBaseType AlgReal Source #
NonFuncSBVRep FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type NonFuncSBVBaseType FPRoundingMode Source #
NonFuncSBVRep Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type NonFuncSBVBaseType Integer Source #
NonFuncSBVRep Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type NonFuncSBVBaseType Bool Source #
(KnownNat w, 1 <= w) => NonFuncSBVRep (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type NonFuncSBVBaseType (IntN w) Source #
(KnownNat w, 1 <= w) => NonFuncSBVRep (WordN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type NonFuncSBVBaseType (WordN w) Source #
ValidFP eb sb => NonFuncSBVRep (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type NonFuncSBVBaseType (FP eb sb) Source #

class NonFuncSBVRep a => SupportedNonFuncPrim a where Source #

Indicates that a type is supported, can be represented as a symbolic term, is not a function type, and can be lowered to an SBV term.

Methods

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

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

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

Instances

Instances details

SupportedNonFuncPrim AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim 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 Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim 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 Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods conNonFuncSBVTerm :: Integer -> SBV (NonFuncSBVBaseType Integer) Source # symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType Integer)) Source # withNonFuncPrim :: (NonFuncPrimConstraint Integer => r) -> r Source #
SupportedNonFuncPrim Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods conNonFuncSBVTerm :: Bool -> SBV (NonFuncSBVBaseType Bool) Source # symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType Bool)) Source # withNonFuncPrim :: (NonFuncPrimConstraint Bool => r) -> r Source #
(KnownNat w, 1 <= w) => SupportedNonFuncPrim (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim 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 Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim 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 #
ValidFP eb sb => SupportedNonFuncPrim (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim 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 #

class SBVRep t Source #

Type class for resolving the SBV type for the primitive type.

Associated Types

type SBVType t Source #

Instances

Instances details

SBVRep AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type SBVType AlgReal Source #
SBVRep FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type SBVType FPRoundingMode Source #
SBVRep Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type SBVType Integer Source #
SBVRep Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type SBVType Bool Source #
(KnownNat w, 1 <= w) => SBVRep (IntN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type SBVType (IntN w) Source #
(KnownNat w, 1 <= w) => SBVRep (WordN w) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type SBVType (WordN w) Source #
ValidFP eb sb => SBVRep (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type SBVType (FP eb sb) Source #
(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Associated Types type SBVType (a --> b) Source #
(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Associated Types type SBVType (a =-> b) Source #

class Monad m => SBVFreshMonad m where Source #

Monads that supports generating sbv fresh variables.

Methods

sbvFresh :: SymVal a => String -> m (SBV a) Source #

Instances

Instances details

MonadIO m => SBVFreshMonad (QueryT m) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods sbvFresh :: SymVal a => String -> QueryT m (SBV a) Source #
MonadIO m => SBVFreshMonad (SymbolicT m) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods sbvFresh :: SymVal a => String -> SymbolicT m (SBV a) Source #
SBVFreshMonad m => SBVFreshMonad (ReaderT r m) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods sbvFresh :: SymVal a => String -> ReaderT r m (SBV a) Source #
SBVFreshMonad m => SBVFreshMonad (StateT s m) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods sbvFresh :: SymVal a => String -> StateT s m (SBV a) Source #
(SBVFreshMonad m, Monoid w) => SBVFreshMonad (WriterT w m) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods sbvFresh :: SymVal a => String -> WriterT w m (SBV a) Source #
(SBVFreshMonad m, Monoid w) => SBVFreshMonad (RWST r w s m) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods sbvFresh :: SymVal a => String -> RWST r w s m (SBV a) Source #

translateTypeError :: HasCallStack => Maybe String -> TypeRep a -> b Source #

Error message for unsupported types.

parseSMTModelResultError :: HasCallStack => TypeRep a -> ([([CV], CV)], CV) -> a Source #

Error message for failure to parse the SBV model result.

partitionCVArg :: forall a. SupportedNonFuncPrim a => [([CV], CV)] -> [(a, [([CV], CV)])] Source #

Partition the list of CVs for models for functions.

parseScalarSMTModelResult :: forall v r. (SatModel r, Typeable v) => (r -> v) -> ([([CV], CV)], CV) -> v Source #

Parse the scalar model result.