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 (n :: Nat) 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 t -> String
- defaultValue :: t
- defaultValueDynamic :: proxy t -> ModelValue
- pevalITETerm :: Term Bool -> Term t -> Term t -> Term t
- pevalEqTerm :: Term t -> Term t -> Term Bool
- conSBVTerm :: KnownIsZero n => proxy n -> t -> SBVType n t
- symSBVName :: TypedSymbol t -> Int -> String
- symSBVTerm :: (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n t)
- withPrim :: KnownIsZero n => p n -> ((PrimConstraint n t, SMTDefinable (SBVType n t), Mergeable (SBVType n t), Typeable (SBVType n t)) => a) -> a
- sbvIte :: KnownIsZero n => proxy n -> SBV Bool -> SBVType n t -> SBVType n t -> SBVType n t
- sbvEq :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBV Bool
- parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> t
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 :: KnownIsZero n => proxy n -> SBVType n f -> SBVType n a -> SBVType n b
class (SupportedPrim 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 :: KnownIsZero n => proxy n -> (Bits (SBVType n t) => r) -> r
- sbvAndBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvOrBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvXorBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvComplementBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t
class (SupportedNonFuncPrim t, SymShift t) => PEvalShiftTerm t where
- pevalShiftLeftTerm :: Term t -> Term t -> Term t
- pevalShiftRightTerm :: Term t -> Term t -> Term t
- withSbvShiftTermConstraint :: KnownIsZero n => proxy n -> (SIntegral (NonFuncSBVBaseType n t) => r) -> r
- sbvShiftLeftTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvShiftRightTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
class (SupportedNonFuncPrim t, SymRotate t) => PEvalRotateTerm t where
- pevalRotateLeftTerm :: Term t -> Term t -> Term t
- pevalRotateRightTerm :: Term t -> Term t -> Term t
- withSbvRotateTermConstraint :: KnownIsZero n => proxy n -> (SIntegral (NonFuncSBVBaseType n t) => r) -> r
- sbvRotateLeftTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvRotateRightTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
class (SupportedPrim 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 :: KnownIsZero n => proxy n -> (Num (SBVType n t) => r) -> r
- sbvAddNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvNegNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t
- sbvMulNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvAbsNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t
- sbvSignumNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t
pevalSubNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a
class (SupportedPrim t, Ord t) => PEvalOrdTerm t where
- pevalLtOrdTerm :: Term t -> Term t -> Term Bool
- pevalLeOrdTerm :: Term t -> Term t -> Term Bool
- withSbvOrdTermConstraint :: KnownIsZero n => proxy n -> (OrdSymbolic (SBVType n t) => r) -> r
- sbvLtOrdTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBV Bool
- sbvLeOrdTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n 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 (SupportedPrim 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 :: KnownIsZero n => proxy n -> (SDivisible (SBVType n t) => r) -> r
- sbvDivIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvModIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvQuotIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvRemIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
class (PEvalBVTerm s, PEvalBVTerm u, forall n. (KnownNat n, 1 <= n) => SupportedNonFuncPrim (u n), forall n. (KnownNat n, 1 <= n) => SupportedNonFuncPrim (s n), forall n. (KnownNat n, 1 <= n) => SignConversion (u n) (s n)) => PEvalBVSignConversionTerm u s | u -> s, s -> u where
- pevalBVToSignedTerm :: (KnownNat n, 1 <= n) => Term (u n) -> Term (s n)
- pevalBVToUnsignedTerm :: (KnownNat n, 1 <= n) => Term (s n) -> Term (u n)
- withSbvSignConversionTermConstraint :: forall n integerBitwidth p q r. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => p n -> q integerBitwidth -> ((Integral (NonFuncSBVBaseType integerBitwidth (u n)), Integral (NonFuncSBVBaseType integerBitwidth (s n))) => r) -> r
- sbvToSigned :: forall n integerBitwidth o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o u -> p n -> q integerBitwidth -> SBVType integerBitwidth (u n) -> SBVType integerBitwidth (s n)
- sbvToUnsigned :: forall n integerBitwidth o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o s -> p n -> q integerBitwidth -> SBVType integerBitwidth (s n) -> SBVType integerBitwidth (u n)
class (forall n. (KnownNat n, 1 <= n) => SupportedPrim (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 :: (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (bv l) -> SBVType n (bv r) -> SBVType n (bv (l + r))
- sbvBVExtendTerm :: (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (bv l) -> SBVType n (bv r)
- sbvBVSelectTerm :: (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (bv n) -> SBVType int (bv w)
class (SupportedPrim t, Fractional t) => PEvalFractionalTerm t where
- pevalFdivTerm :: Term t -> Term t -> Term t
- pevalRecipTerm :: Term t -> Term t
- withSbvFractionalTermConstraint :: KnownIsZero n => proxy n -> (Fractional (SBVType n t) => r) -> r
- sbvFdivTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvRecipTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t
class (SupportedPrim t, Floating t) => PEvalFloatingTerm t where
- pevalSqrtTerm :: Term t -> Term t
- withSbvFloatingTermConstraint :: KnownIsZero n => proxy n -> (Floating (SBVType n t) => r) -> r
- sbvSqrtTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t
data TypedSymbol t where
- TypedSymbol :: SupportedPrim t => {..} -> TypedSymbol t
data SomeTypedSymbol where
- SomeTypedSymbol :: forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol
showUntyped :: TypedSymbol t -> String
withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a
someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol
data FPTrait
- = FPIsNaN
- | FPIsPositive
- | FPIsNegative
- | FPIsPositiveInfinite
- | FPIsNegativeInfinite
- | FPIsInfinite
- | FPIsPositiveZero
- | FPIsNegativeZero
- | FPIsZero
- | FPIsNormal
- | FPIsSubnormal
- | FPIsPoint
data FPUnaryOp
- = FPAbs
- | FPNeg
data FPBinaryOp
- = FPRem
- | FPMin
- | FPMax
data FPRoundingUnaryOp
- = FPSqrt
- | FPRoundToIntegral
data FPRoundingBinaryOp
- = FPAdd
- | FPSub
- | FPMul
- | FPDiv
data Term t where
- ConTerm :: SupportedPrim t => !Id -> !t -> Term t
- SymTerm :: SupportedPrim t => !Id -> !(TypedSymbol t) -> Term t
- 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 :: SupportedPrim t => !Id -> !(Term t) -> !(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
- ToSignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => !Id -> !(Term (u n)) -> Term (s n)
- ToUnsignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => !Id -> !(Term (s n)) -> Term (u n)
- 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
- SqrtTerm :: PEvalFloatingTerm t => !Id -> !(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)
identity :: Term t -> Id
identityWithTypeRep :: forall t. Term t -> (SomeTypeRep, Id)
introSupportedPrimConstraint :: forall t a. Term t -> (SupportedPrim t => a) -> a
pformat :: forall t. SupportedPrim t => Term t -> String
data UTerm t where
- UConTerm :: SupportedPrim t => !t -> UTerm t
- USymTerm :: SupportedPrim t => !(TypedSymbol t) -> UTerm t
- 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 :: SupportedPrim t => !(Term t) -> !(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
- UToSignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => !(Term (u n)) -> UTerm (s n)
- UToUnsignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => !(Term (s n)) -> UTerm (u n)
- 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
- USqrtTerm :: PEvalFloatingTerm 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)
prettyPrintTerm :: Term t -> Doc ann
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 :: SupportedPrim a => Term a -> 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
toSignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => Term (u n) -> Term (s n)
toUnsignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => Term (s n) -> Term (u n)
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
sqrtTerm :: PEvalFloatingTerm 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)
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 :: SupportedPrim a => Term a -> Term a -> Term Bool
class (SupportedPrim a, Ord a) => NonFuncSBVRep a where
- type NonFuncSBVBaseType (n :: Nat) a
class NonFuncSBVRep a => SupportedNonFuncPrim a where
- conNonFuncSBVTerm :: KnownIsZero n => proxy n -> a -> SBV (NonFuncSBVBaseType n a)
- symNonFuncSBVTerm :: (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n a))
- withNonFuncPrim :: KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a), Mergeable (SBVType n a), SMTDefinable (SBVType n a), Mergeable (SBVType n a), SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) => r) -> r
class SBVRep t where
- type SBVType (n :: Nat) 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)])]

Supported primitive types

class SupportedPrimConstraint t Source #

Associated Types

type PrimConstraint (n :: Nat) t :: Constraint Source #

type PrimConstraint _ _ = ()

Instances

Instances details

SupportedPrimConstraint FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type PrimConstraint n FPRoundingMode Source #
SupportedPrimConstraint Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type PrimConstraint n Integer Source #
SupportedPrimConstraint Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type PrimConstraint n 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 n (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 n (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 n (FP eb sb) Source #
(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Associated Types type PrimConstraint n (a --> b) Source #
(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Associated Types type PrimConstraint n (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, conSBVTerm, symSBVName, symSBVTerm, parseSMTModelResult

Methods

termCache :: Cache (Term t) Source #

pformatCon :: t -> String Source #

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

pformatSym :: TypedSymbol 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 #

conSBVTerm :: KnownIsZero n => proxy n -> t -> SBVType n t Source #

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

symSBVTerm :: (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n t) Source #

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

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

sbvIte :: KnownIsZero n => proxy n -> SBV Bool -> SBVType n t -> SBVType n t -> SBVType n t Source #

sbvEq :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBV Bool Source #

default sbvEq :: (KnownIsZero n, EqSymbolic (SBVType n t)) => proxy n -> SBVType n t -> SBVType n t -> SBV Bool Source #

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

Instances

Instances details

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 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 # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> FPRoundingMode -> SBVType n FPRoundingMode Source # symSBVName :: TypedSymbol FPRoundingMode -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n FPRoundingMode) Source # withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n FPRoundingMode, SMTDefinable (SBVType n FPRoundingMode), Mergeable (SBVType n FPRoundingMode), Typeable (SBVType n FPRoundingMode)) => a) -> a Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n FPRoundingMode -> SBVType n FPRoundingMode -> SBVType n FPRoundingMode Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n FPRoundingMode -> SBVType n FPRoundingMode -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FPRoundingMode 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 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 # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> Integer -> SBVType n Integer Source # symSBVName :: TypedSymbol Integer -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n Integer) Source # withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n Integer, SMTDefinable (SBVType n Integer), Mergeable (SBVType n Integer), Typeable (SBVType n Integer)) => a) -> a Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> Integer 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 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 # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> Bool -> SBVType n Bool Source # symSBVName :: TypedSymbol Bool -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n Bool) Source # withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n Bool, SMTDefinable (SBVType n Bool), Mergeable (SBVType n Bool), Typeable (SBVType n Bool)) => a) -> a Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n Bool -> SBVType n Bool -> SBVType n Bool Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n Bool -> SBVType n Bool -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> 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 (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 # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> IntN w -> SBVType n (IntN w) Source # symSBVName :: TypedSymbol (IntN w) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (IntN w)) Source # withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n (IntN w), SMTDefinable (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)), Typeable (SBVType n (IntN w))) => a) -> a Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (IntN w) -> SBVType n (IntN w) -> SBVType n (IntN w) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (IntN w) -> SBVType n (IntN w) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> IntN w 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 (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 # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> WordN w -> SBVType n (WordN w) Source # symSBVName :: TypedSymbol (WordN w) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (WordN w)) Source # withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n (WordN w), SMTDefinable (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)), Typeable (SBVType n (WordN w))) => a) -> a Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (WordN w) -> SBVType n (WordN w) -> SBVType n (WordN w) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (WordN w) -> SBVType n (WordN w) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> WordN w 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 (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 # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> FP eb sb -> SBVType n (FP eb sb) Source # symSBVName :: TypedSymbol (FP eb sb) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (FP eb sb)) Source # withPrim :: forall (n :: Nat) p a. KnownIsZero n => p n -> ((PrimConstraint n (FP eb sb), SMTDefinable (SBVType n (FP eb sb)), Mergeable (SBVType n (FP eb sb)), Typeable (SBVType n (FP eb sb))) => a) -> a Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FP eb sb Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedNonFuncPrim h, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g, SupportedPrim h) => SupportedPrim (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))) Source # pformatCon :: (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> String Source # pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> String Source # defaultValue :: a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))) Source # defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) Source # pevalEqTerm :: Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) Source # symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))))), Typeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> (e --> (f --> (g --> h)))))) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g) => SupportedPrim (a --> (b --> (c --> (d --> (e --> (f --> g)))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> (b --> (c --> (d --> (e --> (f --> g))))))) Source # pformatCon :: (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> String Source # pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> String Source # defaultValue :: a --> (b --> (c --> (d --> (e --> (f --> g))))) Source # defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) Source # pevalEqTerm :: Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) Source # symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> (e --> (f --> g)))))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g))))))), Typeable (SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> (f --> g)))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> (e --> (f --> g))))) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f) => SupportedPrim (a --> (b --> (c --> (d --> (e --> f))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> (b --> (c --> (d --> (e --> f)))))) Source # pformatCon :: (a --> (b --> (c --> (d --> (e --> f))))) -> String Source # pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> (e --> f))))) -> String Source # defaultValue :: a --> (b --> (c --> (d --> (e --> f)))) Source # defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> (e --> f))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term (a --> (b --> (c --> (d --> (e --> f))))) Source # pevalEqTerm :: Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term (a --> (b --> (c --> (d --> (e --> f))))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) Source # symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> (e --> f))))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> (e --> f)))))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> (e --> f))))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> (e --> f)))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> (e --> f)))))), Typeable (SBVType n (a --> (b --> (c --> (d --> (e --> f))))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBVType n (a --> (b --> (c --> (d --> (e --> f))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> (e --> f)))) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e) => SupportedPrim (a --> (b --> (c --> (d --> e)))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> (b --> (c --> (d --> e))))) Source # pformatCon :: (a --> (b --> (c --> (d --> e)))) -> String Source # pformatSym :: TypedSymbol (a --> (b --> (c --> (d --> e)))) -> String Source # defaultValue :: a --> (b --> (c --> (d --> e))) Source # defaultValueDynamic :: proxy (a --> (b --> (c --> (d --> e)))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> (d --> e)))) -> Term (a --> (b --> (c --> (d --> e)))) -> Term (a --> (b --> (c --> (d --> e)))) Source # pevalEqTerm :: Term (a --> (b --> (c --> (d --> e)))) -> Term (a --> (b --> (c --> (d --> e)))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e)))) Source # symSBVName :: TypedSymbol (a --> (b --> (c --> (d --> e)))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> (d --> e))))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> (d --> e)))), SMTDefinable (SBVType n (a --> (b --> (c --> (d --> e))))), Mergeable (SBVType n (a --> (b --> (c --> (d --> e))))), Typeable (SBVType n (a --> (b --> (c --> (d --> e)))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e)))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBVType n (a --> (b --> (c --> (d --> e)))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> (d --> e))) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d) => SupportedPrim (a --> (b --> (c --> d))) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> (b --> (c --> d)))) Source # pformatCon :: (a --> (b --> (c --> d))) -> String Source # pformatSym :: TypedSymbol (a --> (b --> (c --> d))) -> String Source # defaultValue :: a --> (b --> (c --> d)) Source # defaultValueDynamic :: proxy (a --> (b --> (c --> d))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> (b --> (c --> d))) -> Term (a --> (b --> (c --> d))) -> Term (a --> (b --> (c --> d))) Source # pevalEqTerm :: Term (a --> (b --> (c --> d))) -> Term (a --> (b --> (c --> d))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d))) Source # symSBVName :: TypedSymbol (a --> (b --> (c --> d))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> (c --> d)))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> (c --> d))), SMTDefinable (SBVType n (a --> (b --> (c --> d)))), Mergeable (SBVType n (a --> (b --> (c --> d)))), Typeable (SBVType n (a --> (b --> (c --> d))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> (c --> d))) -> SBVType n (a --> (b --> (c --> d))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> (c --> d)) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedPrim a, SupportedPrim b, SupportedPrim c) => SupportedPrim (a --> (b --> c)) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> (b --> c))) Source # pformatCon :: (a --> (b --> c)) -> String Source # pformatSym :: TypedSymbol (a --> (b --> c)) -> String Source # defaultValue :: a --> (b --> c) Source # defaultValueDynamic :: proxy (a --> (b --> c)) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> (b --> c)) -> Term (a --> (b --> c)) -> Term (a --> (b --> c)) Source # pevalEqTerm :: Term (a --> (b --> c)) -> Term (a --> (b --> c)) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> (b --> c)) -> SBVType n (a --> (b --> c)) Source # symSBVName :: TypedSymbol (a --> (b --> c)) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> (b --> c))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> (b --> c)), SMTDefinable (SBVType n (a --> (b --> c))), Mergeable (SBVType n (a --> (b --> c))), Typeable (SBVType n (a --> (b --> c)))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> (b --> c)) -> SBVType n (a --> (b --> c)) -> SBVType n (a --> (b --> c)) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> (b --> c)) -> SBVType n (a --> (b --> c)) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> (b --> c) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b) => SupportedPrim (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Methods termCache :: Cache (Term (a --> b)) Source # pformatCon :: (a --> b) -> String Source # pformatSym :: TypedSymbol (a --> b) -> String Source # defaultValue :: a --> b Source # defaultValueDynamic :: proxy (a --> b) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a --> b) -> Term (a --> b) -> Term (a --> b) Source # pevalEqTerm :: Term (a --> b) -> Term (a --> b) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a --> b) -> SBVType n (a --> b) Source # symSBVName :: TypedSymbol (a --> b) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a --> b)) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a --> b), SMTDefinable (SBVType n (a --> b)), Mergeable (SBVType n (a --> b)), Typeable (SBVType n (a --> b))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a --> b) -> SBVType n (a --> b) -> SBVType n (a --> b) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> b) -> SBVType n (a --> b) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a --> b Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedNonFuncPrim h, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g, SupportedPrim h) => SupportedPrim (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))) Source # pformatCon :: (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> String Source # pformatSym :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> String Source # defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))) Source # defaultValueDynamic :: proxy (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) Source # pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) Source # symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))), Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))))), Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h))))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> (g =-> h)))))) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedNonFuncPrim g, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f, SupportedPrim g) => SupportedPrim (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))) Source # pformatCon :: (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> String Source # pformatSym :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> String Source # defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))) Source # defaultValueDynamic :: proxy (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) Source # pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) Source # symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))), Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))))), Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g)))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> (f =-> g))))) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedNonFuncPrim f, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e, SupportedPrim f) => SupportedPrim (a =-> (b =-> (c =-> (d =-> (e =-> f))))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a =-> (b =-> (c =-> (d =-> (e =-> f)))))) Source # pformatCon :: (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> String Source # pformatSym :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> String Source # defaultValue :: a =-> (b =-> (c =-> (d =-> (e =-> f)))) Source # defaultValueDynamic :: proxy (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) Source # pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) Source # symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> (e =-> f))))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))), Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f)))))), Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBVType n (a =-> (b =-> (c =-> (d =-> (e =-> f))))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> (e =-> f)))) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedNonFuncPrim e, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d, SupportedPrim e) => SupportedPrim (a =-> (b =-> (c =-> (d =-> e)))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a =-> (b =-> (c =-> (d =-> e))))) Source # pformatCon :: (a =-> (b =-> (c =-> (d =-> e)))) -> String Source # pformatSym :: TypedSymbol (a =-> (b =-> (c =-> (d =-> e)))) -> String Source # defaultValue :: a =-> (b =-> (c =-> (d =-> e))) Source # defaultValueDynamic :: proxy (a =-> (b =-> (c =-> (d =-> e)))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term (a =-> (b =-> (c =-> (d =-> e)))) Source # pevalEqTerm :: Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term (a =-> (b =-> (c =-> (d =-> e)))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> (d =-> e)))) -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) Source # symSBVName :: TypedSymbol (a =-> (b =-> (c =-> (d =-> e)))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> (d =-> e))))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> (d =-> e)))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))), Mergeable (SBVType n (a =-> (b =-> (c =-> (d =-> e))))), Typeable (SBVType n (a =-> (b =-> (c =-> (d =-> e)))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) -> SBVType n (a =-> (b =-> (c =-> (d =-> e)))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> (d =-> e))) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedNonFuncPrim d, SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d) => SupportedPrim (a =-> (b =-> (c =-> d))) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a =-> (b =-> (c =-> d)))) Source # pformatCon :: (a =-> (b =-> (c =-> d))) -> String Source # pformatSym :: TypedSymbol (a =-> (b =-> (c =-> d))) -> String Source # defaultValue :: a =-> (b =-> (c =-> d)) Source # defaultValueDynamic :: proxy (a =-> (b =-> (c =-> d))) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a =-> (b =-> (c =-> d))) -> Term (a =-> (b =-> (c =-> d))) -> Term (a =-> (b =-> (c =-> d))) Source # pevalEqTerm :: Term (a =-> (b =-> (c =-> d))) -> Term (a =-> (b =-> (c =-> d))) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d))) Source # symSBVName :: TypedSymbol (a =-> (b =-> (c =-> d))) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> (c =-> d)))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> (c =-> d))), SMTDefinable (SBVType n (a =-> (b =-> (c =-> d)))), Mergeable (SBVType n (a =-> (b =-> (c =-> d)))), Typeable (SBVType n (a =-> (b =-> (c =-> d))))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d))) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> (c =-> d))) -> SBVType n (a =-> (b =-> (c =-> d))) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> (c =-> d)) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b, SupportedNonFuncPrim c, SupportedPrim a, SupportedPrim b, SupportedPrim c) => SupportedPrim (a =-> (b =-> c)) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a =-> (b =-> c))) Source # pformatCon :: (a =-> (b =-> c)) -> String Source # pformatSym :: TypedSymbol (a =-> (b =-> c)) -> String Source # defaultValue :: a =-> (b =-> c) Source # defaultValueDynamic :: proxy (a =-> (b =-> c)) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c)) Source # pevalEqTerm :: Term (a =-> (b =-> c)) -> Term (a =-> (b =-> c)) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c)) Source # symSBVName :: TypedSymbol (a =-> (b =-> c)) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> (b =-> c))) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> (b =-> c)), SMTDefinable (SBVType n (a =-> (b =-> c))), Mergeable (SBVType n (a =-> (b =-> c))), Typeable (SBVType n (a =-> (b =-> c)))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c)) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> (b =-> c)) -> SBVType n (a =-> (b =-> c)) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> (b =-> c) Source #
(SupportedNonFuncPrim a, SupportedNonFuncPrim b) => SupportedPrim (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Methods termCache :: Cache (Term (a =-> b)) Source # pformatCon :: (a =-> b) -> String Source # pformatSym :: TypedSymbol (a =-> b) -> String Source # defaultValue :: a =-> b Source # defaultValueDynamic :: proxy (a =-> b) -> ModelValue Source # pevalITETerm :: Term Bool -> Term (a =-> b) -> Term (a =-> b) -> Term (a =-> b) Source # pevalEqTerm :: Term (a =-> b) -> Term (a =-> b) -> Term Bool Source # conSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> (a =-> b) -> SBVType n (a =-> b) Source # symSBVName :: TypedSymbol (a =-> b) -> Int -> String Source # symSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n (a =-> b)) Source # withPrim :: forall (n :: Nat) p a0. KnownIsZero n => p n -> ((PrimConstraint n (a =-> b), SMTDefinable (SBVType n (a =-> b)), Mergeable (SBVType n (a =-> b)), Typeable (SBVType n (a =-> b))) => a0) -> a0 Source # sbvIte :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBV Bool -> SBVType n (a =-> b) -> SBVType n (a =-> b) -> SBVType n (a =-> b) Source # sbvEq :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> b) -> SBVType n (a =-> b) -> SBV Bool Source # parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> a =-> b 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 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 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 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 #

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 #

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 #

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 #

Methods

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

sbvApplyTerm :: KnownIsZero n => proxy n -> SBVType n f -> SBVType n a -> SBVType n 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 :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a --> b) -> SBVType n a -> SBVType n 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 :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (a =-> b) -> SBVType n a -> SBVType n b Source #

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

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 :: KnownIsZero n => proxy n -> (Bits (SBVType n t) => r) -> r Source #

sbvAndBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #

sbvOrBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #

sbvXorBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #

sbvComplementBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n 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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Bits (SBVType n0 (IntN n)) => r) -> r Source # sbvAndBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvOrBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvXorBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvComplementBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Bits (SBVType n0 (WordN n)) => r) -> r Source # sbvAndBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvOrBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvXorBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvComplementBitsTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #

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

Minimal complete definition

pevalShiftLeftTerm, pevalShiftRightTerm, withSbvShiftTermConstraint

Methods

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

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

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

sbvShiftLeftTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #

sbvShiftRightTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n 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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (IntN n)) => r) -> r Source # sbvShiftLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvShiftRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (WordN n)) => r) -> r Source # sbvShiftLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvShiftRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #

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

Minimal complete definition

pevalRotateLeftTerm, pevalRotateRightTerm, withSbvRotateTermConstraint

Methods

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

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

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

sbvRotateLeftTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #

sbvRotateRightTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n 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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (IntN n)) => r) -> r Source # sbvRotateLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvRotateRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SIntegral (NonFuncSBVBaseType n0 (WordN n)) => r) -> r Source # sbvRotateLeftTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvRotateRightTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #

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

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 :: KnownIsZero n => proxy n -> (Num (SBVType n t) => r) -> r Source #

sbvAddNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #

sbvNegNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t Source #

sbvMulNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #

sbvAbsNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t Source #

sbvSignumNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t Source #

Instances

Instances details

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 :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (Num (SBVType n Integer) => r) -> r Source # sbvAddNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source # sbvNegNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer Source # sbvMulNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source # sbvAbsNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer Source # sbvSignumNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n 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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Num (SBVType n0 (IntN n)) => r) -> r Source # sbvAddNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvNegNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvMulNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvAbsNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvSignumNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalNumTerm (WordN n) Source #
Instance details 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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (Num (SBVType n0 (WordN n)) => r) -> r Source # sbvAddNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvNegNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvMulNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvAbsNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvSignumNumTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #
ValidFP eb sb => PEvalNumTerm (FP eb sb) Source #
Instance details 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 :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (Num (SBVType n (FP eb sb)) => r) -> r Source # sbvAddNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source # sbvNegNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source # sbvMulNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source # sbvAbsNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source # sbvSignumNumTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) Source #

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

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

Minimal complete definition

pevalLtOrdTerm, pevalLeOrdTerm, withSbvOrdTermConstraint

Methods

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

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

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

sbvLtOrdTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBV Bool Source #

sbvLeOrdTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBV Bool Source #

Instances

Instances details

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 :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (OrdSymbolic (SBVType n FPRoundingMode) => r) -> r Source # sbvLtOrdTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n FPRoundingMode -> SBVType n FPRoundingMode -> SBV Bool Source # sbvLeOrdTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n FPRoundingMode -> SBVType n 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 :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (OrdSymbolic (SBVType n Integer) => r) -> r Source # sbvLtOrdTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBV Bool Source # sbvLeOrdTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n 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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (OrdSymbolic (SBVType n0 (IntN n)) => r) -> r Source # sbvLtOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBV Bool Source # sbvLeOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (OrdSymbolic (SBVType n0 (WordN n)) => r) -> r Source # sbvLtOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBV Bool Source # sbvLeOrdTerm :: forall (n0 :: Nat) proxy. KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (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 :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (OrdSymbolic (SBVType n (FP eb sb)) => r) -> r Source # sbvLtOrdTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBV Bool Source # sbvLeOrdTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> SBVType n (FP eb sb) -> SBVType n (FP eb sb) -> SBV Bool Source #

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

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

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

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

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 :: KnownIsZero n => proxy n -> (SDivisible (SBVType n t) => r) -> r Source #

sbvDivIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #

sbvModIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #

sbvQuotIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #

sbvRemIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n 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 :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (SDivisible (SBVType n Integer) => r) -> r Source # sbvDivIntegralTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source # sbvModIntegralTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source # sbvQuotIntegralTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBVType n Integer Source # sbvRemIntegralTerm :: forall proxy (n :: Nat). KnownIsZero n => proxy n -> SBVType n Integer -> SBVType n Integer -> SBVType n 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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SDivisible (SBVType n0 (IntN n)) => r) -> r Source # sbvDivIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvModIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvQuotIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) Source # sbvRemIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (IntN n) -> SBVType n0 (IntN n) -> SBVType n0 (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 :: forall (n0 :: Nat) proxy r. KnownIsZero n0 => proxy n0 -> (SDivisible (SBVType n0 (WordN n)) => r) -> r Source # sbvDivIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvModIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvQuotIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source # sbvRemIntegralTerm :: forall proxy (n0 :: Nat). KnownIsZero n0 => proxy n0 -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) -> SBVType n0 (WordN n) Source #

class (PEvalBVTerm s, PEvalBVTerm u, forall n. (KnownNat n, 1 <= n) => SupportedNonFuncPrim (u n), forall n. (KnownNat n, 1 <= n) => SupportedNonFuncPrim (s n), forall n. (KnownNat n, 1 <= n) => SignConversion (u n) (s n)) => PEvalBVSignConversionTerm u s | u -> s, s -> u where Source #

Minimal complete definition

pevalBVToSignedTerm, pevalBVToUnsignedTerm, withSbvSignConversionTermConstraint

Methods

pevalBVToSignedTerm :: (KnownNat n, 1 <= n) => Term (u n) -> Term (s n) Source #

pevalBVToUnsignedTerm :: (KnownNat n, 1 <= n) => Term (s n) -> Term (u n) Source #

withSbvSignConversionTermConstraint :: forall n integerBitwidth p q r. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => p n -> q integerBitwidth -> ((Integral (NonFuncSBVBaseType integerBitwidth (u n)), Integral (NonFuncSBVBaseType integerBitwidth (s n))) => r) -> r Source #

sbvToSigned :: forall n integerBitwidth o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o u -> p n -> q integerBitwidth -> SBVType integerBitwidth (u n) -> SBVType integerBitwidth (s n) Source #

sbvToUnsigned :: forall n integerBitwidth o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o s -> p n -> q integerBitwidth -> SBVType integerBitwidth (s n) -> SBVType integerBitwidth (u n) Source #

Instances

Instances details

PEvalBVSignConversionTerm WordN IntN Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval

Methods

pevalBVToSignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (WordN n) -> Term (IntN n) Source #

pevalBVToUnsignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (IntN n) -> Term (WordN n) Source #

withSbvSignConversionTermConstraint :: forall (n :: Nat) (integerBitwidth :: Nat) p q r. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => p n -> q integerBitwidth -> ((Integral (NonFuncSBVBaseType integerBitwidth (WordN n)), Integral (NonFuncSBVBaseType integerBitwidth (IntN n))) => r) -> r Source #

sbvToSigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o WordN -> p n -> q integerBitwidth -> SBVType integerBitwidth (WordN n) -> SBVType integerBitwidth (IntN n) Source #

sbvToUnsigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o IntN -> p n -> q integerBitwidth -> SBVType integerBitwidth (IntN n) -> SBVType integerBitwidth (WordN n) Source #

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

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 :: (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (bv l) -> SBVType n (bv r) -> SBVType n (bv (l + r)) Source #

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

sbvBVSelectTerm :: (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (bv n) -> SBVType int (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 (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (IntN l) -> SBVType n (IntN r) -> SBVType n (IntN (l + r)) Source # sbvBVExtendTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (IntN l) -> SBVType n (IntN r) Source # sbvBVSelectTerm :: forall (int :: Nat) (ix :: Nat) (w :: Nat) (n :: Nat) p0 p1 p2 p3. (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (IntN n) -> SBVType int (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 (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (WordN l) -> SBVType n (WordN r) -> SBVType n (WordN (l + r)) Source # sbvBVExtendTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (WordN l) -> SBVType n (WordN r) Source # sbvBVSelectTerm :: forall (int :: Nat) (ix :: Nat) (w :: Nat) (n :: Nat) p0 p1 p2 p3. (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (WordN n) -> SBVType int (WordN w) Source #

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

Minimal complete definition

pevalFdivTerm, pevalRecipTerm, withSbvFractionalTermConstraint

Methods

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

pevalRecipTerm :: Term t -> Term t Source #

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

sbvFdivTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #

sbvRecipTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t Source #

Instances

Instances details

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 :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> (Fractional (SBVType n (FP eb sb)) => r) -> r Source #

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

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

class (SupportedPrim t, Floating t) => PEvalFloatingTerm t where Source #

Minimal complete definition

pevalSqrtTerm, withSbvFloatingTermConstraint

Methods

pevalSqrtTerm :: Term t -> Term t Source #

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

sbvSqrtTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t Source #

Instances

Instances details

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

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm

Methods

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

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

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

Typed symbols

data TypedSymbol 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:

>>> :set -XOverloadedStrings
>>> "a" :: TypedSymbol Bool
a :: Bool

Constructors

TypedSymbol
Fields :: SupportedPrim t => { unTypedSymbol :: Symbol } -> TypedSymbol t

Instances

Instances details

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

data SomeTypedSymbol where Source #

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

Constructors

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

Instances

Instances details

Show SomeTypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods showsPrec :: Int -> SomeTypedSymbol -> ShowS # show :: SomeTypedSymbol -> String # showList :: [SomeTypedSymbol] -> ShowS #
NFData SomeTypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: SomeTypedSymbol -> () #
Eq SomeTypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool # (/=) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool #
Ord SomeTypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods compare :: SomeTypedSymbol -> SomeTypedSymbol -> Ordering # (<) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool # (<=) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool # (>) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool # (>=) :: SomeTypedSymbol -> SomeTypedSymbol -> Bool # max :: SomeTypedSymbol -> SomeTypedSymbol -> SomeTypedSymbol # min :: SomeTypedSymbol -> SomeTypedSymbol -> SomeTypedSymbol #
Hashable SomeTypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> SomeTypedSymbol -> Int # hash :: SomeTypedSymbol -> Int #

showUntyped :: TypedSymbol t -> String Source #

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

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

Terms

data FPTrait Source #

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.7.0.0-3DYM4wcz8TiF8sSQ1gvVO8" '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 #

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.7.0.0-3DYM4wcz8TiF8sSQ1gvVO8" 'False) (C1 ('MetaCons "FPAbs" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPNeg" 'PrefixI 'False) (U1 :: Type -> Type))

data FPBinaryOp Source #

Constructors

FPRem
FPMin
FPMax

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.7.0.0-3DYM4wcz8TiF8sSQ1gvVO8" 'False) (C1 ('MetaCons "FPRem" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPMin" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPMax" 'PrefixI 'False) (U1 :: Type -> Type)))

data FPRoundingUnaryOp Source #

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.7.0.0-3DYM4wcz8TiF8sSQ1gvVO8" 'False) (C1 ('MetaCons "FPSqrt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPRoundToIntegral" 'PrefixI 'False) (U1 :: Type -> Type))

data FPRoundingBinaryOp Source #

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.7.0.0-3DYM4wcz8TiF8sSQ1gvVO8" '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 Term t where Source #

Constructors

ConTerm :: SupportedPrim t => !Id -> !t -> Term t
SymTerm :: SupportedPrim t => !Id -> !(TypedSymbol t) -> Term t
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 :: SupportedPrim t => !Id -> !(Term t) -> !(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
ToSignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => !Id -> !(Term (u n)) -> Term (s n)
ToUnsignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => !Id -> !(Term (s n)) -> Term (u n)
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
SqrtTerm :: PEvalFloatingTerm t => !Id -> !(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)

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 t -> Description (Term t) 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) 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) DToSignedTerm :: forall u t. !(TypeRep u, Id) -> Description (Term t) DToUnsignedTerm :: forall s t. !(TypeRep s, 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 :: FPTrait -> !Id -> Description (Term Bool) DFdivTerm :: forall t. !Id -> !Id -> Description (Term t) DRecipTerm :: forall t. !Id -> Description (Term t) DSqrtTerm :: forall t. !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))
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 #

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

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

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

Interning

data UTerm t where Source #

Constructors

UConTerm :: SupportedPrim t => !t -> UTerm t
USymTerm :: SupportedPrim t => !(TypedSymbol t) -> UTerm t
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 :: SupportedPrim t => !(Term t) -> !(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
UToSignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => !(Term (u n)) -> UTerm (s n)
UToUnsignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => !(Term (s n)) -> UTerm (u n)
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
USqrtTerm :: PEvalFloatingTerm 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)

prettyPrintTerm :: Term t -> Doc ann Source #

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

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 #

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 #

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

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

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

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

notTerm :: Term Bool -> Term Bool Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

toSignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => Term (u n) -> Term (s n) Source #

toUnsignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => Term (s n) -> Term (u n) Source #

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 #

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 #

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 #

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 #

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 #

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

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

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

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

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

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

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

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

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

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

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

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

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 #

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 #

Support for boolean type

trueTerm :: Term Bool Source #

falseTerm :: Term Bool Source #

pattern BoolConTerm :: Bool -> Term a Source #

pattern TrueTerm :: Term a Source #

pattern FalseTerm :: Term a Source #

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

pevalNotTerm :: Term Bool -> Term Bool Source #

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

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

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

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

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

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

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

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

Associated Types

type NonFuncSBVBaseType (n :: Nat) a Source #

Instances

Instances details

NonFuncSBVRep FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type NonFuncSBVBaseType n FPRoundingMode Source #
NonFuncSBVRep Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type NonFuncSBVBaseType n Integer Source #
NonFuncSBVRep Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type NonFuncSBVBaseType n 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 n (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 n (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 n (FP eb sb) Source #

class NonFuncSBVRep a => SupportedNonFuncPrim a where Source #

Methods

conNonFuncSBVTerm :: KnownIsZero n => proxy n -> a -> SBV (NonFuncSBVBaseType n a) Source #

symNonFuncSBVTerm :: (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n a)) Source #

withNonFuncPrim :: KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a), Mergeable (SBVType n a), SMTDefinable (SBVType n a), Mergeable (SBVType n a), SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) => r) -> r Source #

Instances

Instances details

SupportedNonFuncPrim FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> FPRoundingMode -> SBV (NonFuncSBVBaseType n FPRoundingMode) Source # symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n FPRoundingMode)) Source # withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n FPRoundingMode), EqSymbolic (SBVType n FPRoundingMode), Mergeable (SBVType n FPRoundingMode), SMTDefinable (SBVType n FPRoundingMode), Mergeable (SBVType n FPRoundingMode), SBVType n FPRoundingMode ~ SBV (NonFuncSBVBaseType n FPRoundingMode), PrimConstraint n FPRoundingMode) => r) -> r Source #
SupportedNonFuncPrim Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Methods conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> Integer -> SBV (NonFuncSBVBaseType n Integer) Source # symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n Integer)) Source # withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n Integer), EqSymbolic (SBVType n Integer), Mergeable (SBVType n Integer), SMTDefinable (SBVType n Integer), Mergeable (SBVType n Integer), SBVType n Integer ~ SBV (NonFuncSBVBaseType n Integer), PrimConstraint n Integer) => r) -> r Source #
SupportedNonFuncPrim Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods conNonFuncSBVTerm :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> Bool -> SBV (NonFuncSBVBaseType n Bool) Source # symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n Bool)) Source # withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n Bool), EqSymbolic (SBVType n Bool), Mergeable (SBVType n Bool), SMTDefinable (SBVType n Bool), Mergeable (SBVType n Bool), SBVType n Bool ~ SBV (NonFuncSBVBaseType n Bool), PrimConstraint n 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 :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> IntN w -> SBV (NonFuncSBVBaseType n (IntN w)) Source # symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n (IntN w))) Source # withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n (IntN w)), EqSymbolic (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)), SMTDefinable (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)), SBVType n (IntN w) ~ SBV (NonFuncSBVBaseType n (IntN w)), PrimConstraint n (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 :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> WordN w -> SBV (NonFuncSBVBaseType n (WordN w)) Source # symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n (WordN w))) Source # withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n (WordN w)), EqSymbolic (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)), SMTDefinable (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)), SBVType n (WordN w) ~ SBV (NonFuncSBVBaseType n (WordN w)), PrimConstraint n (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 :: forall (n :: Nat) proxy. KnownIsZero n => proxy n -> FP eb sb -> SBV (NonFuncSBVBaseType n (FP eb sb)) Source # symNonFuncSBVTerm :: forall m (n :: Nat) proxy. (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n (FP eb sb))) Source # withNonFuncPrim :: forall (n :: Nat) proxy r. KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n (FP eb sb)), EqSymbolic (SBVType n (FP eb sb)), Mergeable (SBVType n (FP eb sb)), SMTDefinable (SBVType n (FP eb sb)), Mergeable (SBVType n (FP eb sb)), SBVType n (FP eb sb) ~ SBV (NonFuncSBVBaseType n (FP eb sb)), PrimConstraint n (FP eb sb)) => r) -> r Source #

class SBVRep t Source #

Associated Types

type SBVType (n :: Nat) t Source #

Instances

Instances details

SBVRep FPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type SBVType n FPRoundingMode Source #
SBVRep Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim Associated Types type SBVType n Integer Source #
SBVRep Bool Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type SBVType n 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 n (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 n (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 n (FP eb sb) Source #
(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a --> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun Associated Types type SBVType n (a --> b) Source #
(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a =-> b) Source #
Instance details Defined in Grisette.Internal.SymPrim.TabularFun Associated Types type SBVType n (a =-> b) Source #

class Monad m => SBVFreshMonad m where Source #

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 #

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

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

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