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

Grisette.Internal.SymPrim.Prim.Internal.Term

Contents

Supported primitive types
Partial evaluation for the terms
Typed symbols
Terms
Interning
Interned constructors
Patterns
Support for boolean type
Orphan instances

Description

Synopsis

class SupportedPrimConstraint t where
- type PrimConstraint t
class (Lift t, NFData t, Typeable t, SupportedPrimConstraint t, SBVRep t) => SupportedPrim t where
- primTypeRep :: TypeRep t
- sameCon :: t -> t -> Bool
- hashConWithSalt :: Int -> t -> Int
- pformatCon :: t -> String
- defaultValue :: t
- pevalITETerm :: Term Bool -> Term t -> Term t -> Term t
- pevalEqTerm :: Term t -> Term t -> Term Bool
- pevalDistinctTerm :: NonEmpty (Term t) -> Term Bool
- conSBVTerm :: t -> SBVType t
- symSBVName :: TypedSymbol 'AnyKind t -> Int -> String
- symSBVTerm :: SBVFreshMonad m => String -> m (SBVType t)
- withPrim :: ((PrimConstraint t, SMTDefinable (SBVType t), Mergeable (SBVType t), Typeable (SBVType t)) => a) -> a
- sbvIte :: SBV Bool -> SBVType t -> SBVType t -> SBVType t
- sbvEq :: SBVType t -> SBVType t -> SBV Bool
- sbvDistinct :: NonEmpty (SBVType t) -> SBV Bool
- parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> t
- castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd t -> Maybe (TypedSymbol knd' t)
- funcDummyConstraint :: SBVType t -> SBV Bool
class SupportedPrim con => SymRep con where
- type SymType con
class ConRep sym where
- type ConType sym
class (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) => LinkedRep con sym | con -> sym, sym -> con where
- underlyingTerm :: sym -> Term con
- wrapTerm :: Term con -> sym
class PEvalApplyTerm f a b | f -> a b where
- pevalApplyTerm :: Term f -> Term a -> Term b
- sbvApplyTerm :: SBVType f -> SBVType a -> SBVType b
class PEvalBitwiseTerm t where
- pevalAndBitsTerm :: Term t -> Term t -> Term t
- pevalOrBitsTerm :: Term t -> Term t -> Term t
- pevalXorBitsTerm :: Term t -> Term t -> Term t
- pevalComplementBitsTerm :: Term t -> Term t
- withSbvBitwiseTermConstraint :: (Bits (SBVType t) => r) -> r
- sbvAndBitsTerm :: SBVType t -> SBVType t -> SBVType t
- sbvOrBitsTerm :: SBVType t -> SBVType t -> SBVType t
- sbvXorBitsTerm :: SBVType t -> SBVType t -> SBVType t
- sbvComplementBitsTerm :: SBVType t -> SBVType t
class PEvalShiftTerm t where
- pevalShiftLeftTerm :: Term t -> Term t -> Term t
- pevalShiftRightTerm :: Term t -> Term t -> Term t
- withSbvShiftTermConstraint :: (SIntegral (NonFuncSBVBaseType t) => r) -> r
- sbvShiftLeftTerm :: SBVType t -> SBVType t -> SBVType t
- sbvShiftRightTerm :: SBVType t -> SBVType t -> SBVType t
class PEvalRotateTerm t where
- pevalRotateLeftTerm :: Term t -> Term t -> Term t
- pevalRotateRightTerm :: Term t -> Term t -> Term t
- withSbvRotateTermConstraint :: (SIntegral (NonFuncSBVBaseType t) => r) -> r
- sbvRotateLeftTerm :: SBVType t -> SBVType t -> SBVType t
- sbvRotateRightTerm :: SBVType t -> SBVType t -> SBVType t
class Num t => PEvalNumTerm t where
- pevalAddNumTerm :: Term t -> Term t -> Term t
- pevalNegNumTerm :: Term t -> Term t
- pevalMulNumTerm :: Term t -> Term t -> Term t
- pevalAbsNumTerm :: Term t -> Term t
- pevalSignumNumTerm :: Term t -> Term t
- withSbvNumTermConstraint :: (Num (SBVType t) => r) -> r
- sbvAddNumTerm :: SBVType t -> SBVType t -> SBVType t
- sbvNegNumTerm :: SBVType t -> SBVType t
- sbvMulNumTerm :: SBVType t -> SBVType t -> SBVType t
- sbvAbsNumTerm :: SBVType t -> SBVType t
- sbvSignumNumTerm :: SBVType t -> SBVType t
pevalSubNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a
class PEvalOrdTerm t where
- pevalLtOrdTerm :: Term t -> Term t -> Term Bool
- pevalLeOrdTerm :: Term t -> Term t -> Term Bool
- withSbvOrdTermConstraint :: (OrdSymbolic (SBVType t) => r) -> r
- sbvLtOrdTerm :: SBVType t -> SBVType t -> SBV Bool
- sbvLeOrdTerm :: SBVType t -> SBVType t -> SBV Bool
pevalGtOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalNEqTerm :: SupportedPrim a => Term a -> Term a -> Term Bool
class PEvalDivModIntegralTerm t where
- pevalDivIntegralTerm :: Term t -> Term t -> Term t
- pevalModIntegralTerm :: Term t -> Term t -> Term t
- pevalQuotIntegralTerm :: Term t -> Term t -> Term t
- pevalRemIntegralTerm :: Term t -> Term t -> Term t
- withSbvDivModIntegralTermConstraint :: (SDivisible (SBVType t) => r) -> r
- sbvDivIntegralTerm :: SBVType t -> SBVType t -> SBVType t
- sbvModIntegralTerm :: SBVType t -> SBVType t -> SBVType t
- sbvQuotIntegralTerm :: SBVType t -> SBVType t -> SBVType t
- sbvRemIntegralTerm :: SBVType t -> SBVType t -> SBVType t
class BitCast a b => PEvalBitCastTerm a b where
- pevalBitCastTerm :: Term a -> Term b
- sbvBitCast :: SBVType a -> SBVType b
class BitCastOr a b => PEvalBitCastOrTerm a b where
- pevalBitCastOrTerm :: Term b -> Term a -> Term b
- sbvBitCastOr :: SBVType b -> SBVType a -> SBVType b
class SizedBV bv => PEvalBVTerm (bv :: Natural -> Type) where
- pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (bv l) -> Term (bv r) -> Term (bv (l + r))
- pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (bv l) -> Term (bv r)
- 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 (bv n) -> Term (bv w)
- sbvBVConcatTerm :: forall (l :: Nat) (r :: Nat) p1 p2. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p1 l -> p2 r -> SBVType (bv l) -> SBVType (bv r) -> SBVType (bv (l + r))
- sbvBVExtendTerm :: forall (l :: Nat) (r :: Nat) p1 p2. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p1 l -> p2 r -> Bool -> SBVType (bv l) -> SBVType (bv r)
- sbvBVSelectTerm :: forall (ix :: Nat) (w :: Nat) (n :: Nat) p1 p2 p3. (KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p1 ix -> p2 w -> p3 n -> SBVType (bv n) -> SBVType (bv w)
class Fractional t => PEvalFractionalTerm t where
- pevalFdivTerm :: Term t -> Term t -> Term t
- pevalRecipTerm :: Term t -> Term t
- withSbvFractionalTermConstraint :: (Fractional (SBVType t) => r) -> r
- sbvFdivTerm :: SBVType t -> SBVType t -> SBVType t
- sbvRecipTerm :: SBVType t -> SBVType t
class PEvalFPTerm (fp :: Nat -> Nat -> Type) where
- pevalFPTraitTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPTrait -> Term (fp eb sb) -> Term Bool
- pevalFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPUnaryOp -> Term (fp eb sb) -> Term (fp eb sb)
- pevalFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPBinaryOp -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb)
- pevalFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb)
- pevalFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb)
- pevalFPFMATerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb)
- sbvFPTraitTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPTrait -> SBVType (fp eb sb) -> SBVType Bool
- sbvFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPUnaryOp -> SBVType (fp eb sb) -> SBVType (fp eb sb)
- sbvFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPBinaryOp -> SBVType (fp eb sb) -> SBVType (fp eb sb) -> SBVType (fp eb sb)
- sbvFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingUnaryOp -> SBVType FPRoundingMode -> SBVType (fp eb sb) -> SBVType (fp eb sb)
- sbvFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingBinaryOp -> SBVType FPRoundingMode -> SBVType (fp eb sb) -> SBVType (fp eb sb) -> SBVType (fp eb sb)
- sbvFPFMATerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType (fp eb sb) -> SBVType (fp eb sb) -> SBVType (fp eb sb) -> SBVType (fp eb sb)
class PEvalFloatingTerm t where
- pevalFloatingUnaryTerm :: FloatingUnaryOp -> Term t -> Term t
- pevalPowerTerm :: Term t -> Term t -> Term t
- withSbvFloatingTermConstraint :: (Floating (SBVType t) => r) -> r
- sbvPowerTerm :: SBVType t -> SBVType t -> SBVType t
- sbvFloatingUnaryTerm :: FloatingUnaryOp -> SBVType t -> SBVType t
class (Integral a, Num b) => PEvalFromIntegralTerm a b where
- pevalFromIntegralTerm :: Term a -> Term b
- sbvFromIntegralTerm :: SBVType a -> SBVType b
class PEvalIEEEFPConvertibleTerm a where
- pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
- pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term a -> Term (FP eb sb)
- sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType a -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType a
- sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType a -> SBVType (FP eb sb)
data SymbolKind
- = ConstantKind
- | AnyKind
data TypedSymbol (knd :: SymbolKind) t where
- TypedSymbol :: forall t (knd :: SymbolKind). (SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) => {..} -> TypedSymbol knd t
typedConstantSymbol :: SupportedNonFuncPrim t => Symbol -> TypedSymbol 'ConstantKind t
typedAnySymbol :: SupportedPrim t => Symbol -> TypedSymbol 'AnyKind t
type TypedConstantSymbol = TypedSymbol 'ConstantKind
type TypedAnySymbol = TypedSymbol 'AnyKind
data SomeTypedSymbol (knd :: SymbolKind) where
- SomeTypedSymbol :: forall (knd :: SymbolKind) t. TypedSymbol knd t -> SomeTypedSymbol knd
type SomeTypedConstantSymbol = SomeTypedSymbol 'ConstantKind
type SomeTypedAnySymbol = SomeTypedSymbol 'AnyKind
class IsSymbolKind (knd :: SymbolKind) where
- type SymbolKindConstraint (knd :: SymbolKind) :: Type -> Constraint
- decideSymbolKind :: Either (knd :~~: 'ConstantKind) (knd :~~: 'AnyKind)
- withSymbolKindConstraint :: TypedSymbol knd t -> (SymbolKindConstraint knd t => a) -> a
showUntyped :: forall (knd :: SymbolKind) t. TypedSymbol knd t -> String
someTypedSymbol :: forall (knd :: SymbolKind) t. TypedSymbol knd t -> SomeTypedSymbol knd
eqHeteroSymbol :: forall (ta :: SymbolKind) a (tb :: SymbolKind) b. TypedSymbol ta a -> TypedSymbol tb b -> Bool
castSomeTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => SomeTypedSymbol knd -> Maybe (SomeTypedSymbol knd')
data FPTrait
- = FPIsNaN
- | FPIsPositive
- | FPIsNegative
- | FPIsPositiveInfinite
- | FPIsNegativeInfinite
- | FPIsInfinite
- | FPIsPositiveZero
- | FPIsNegativeZero
- | FPIsZero
- | FPIsNormal
- | FPIsSubnormal
- | FPIsPoint
data FPUnaryOp
- = FPAbs
- | FPNeg
data FPBinaryOp
- = FPRem
- | FPMinimum
- | FPMinimumNumber
- | FPMaximum
- | FPMaximumNumber
data FPRoundingUnaryOp
- = FPSqrt
- | FPRoundToIntegral
data FPRoundingBinaryOp
- = FPAdd
- | FPSub
- | FPMul
- | FPDiv
data FloatingUnaryOp
- = FloatingExp
- | FloatingLog
- | FloatingSqrt
- | FloatingSin
- | FloatingCos
- | FloatingTan
- | FloatingAsin
- | FloatingAcos
- | FloatingAtan
- | FloatingSinh
- | FloatingCosh
- | FloatingTanh
- | FloatingAsinh
- | FloatingAcosh
- | FloatingAtanh
data Term t where
- ConTerm' :: forall t. SupportedPrim t => !CachedInfo -> !t -> Term t
- SymTerm' :: forall t. !CachedInfo -> !(TypedSymbol 'AnyKind t) -> Term t
- ForallTerm' :: forall t1. !CachedInfo -> !(TypedSymbol 'ConstantKind t1) -> !(Term Bool) -> Term Bool
- ExistsTerm' :: forall t1. !CachedInfo -> !(TypedSymbol 'ConstantKind t1) -> !(Term Bool) -> Term Bool
- NotTerm' :: !CachedInfo -> !(Term Bool) -> Term Bool
- OrTerm' :: !CachedInfo -> !(Term Bool) -> !(Term Bool) -> Term Bool
- AndTerm' :: !CachedInfo -> !(Term Bool) -> !(Term Bool) -> Term Bool
- EqTerm' :: forall t1. !CachedInfo -> !(Term t1) -> !(Term t1) -> Term Bool
- DistinctTerm' :: forall t1. !CachedInfo -> !(NonEmpty (Term t1)) -> Term Bool
- ITETerm' :: forall t. SupportedPrim t => !CachedInfo -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t
- AddNumTerm' :: forall t. (SupportedPrim t, PEvalNumTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- NegNumTerm' :: forall t. (SupportedPrim t, PEvalNumTerm t) => !CachedInfo -> !(Term t) -> Term t
- MulNumTerm' :: forall t. (SupportedPrim t, PEvalNumTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- AbsNumTerm' :: forall t. (SupportedPrim t, PEvalNumTerm t) => !CachedInfo -> !(Term t) -> Term t
- SignumNumTerm' :: forall t. (SupportedPrim t, PEvalNumTerm t) => !CachedInfo -> !(Term t) -> Term t
- LtOrdTerm' :: forall t1. (SupportedPrim t1, PEvalOrdTerm t1) => !CachedInfo -> !(Term t1) -> !(Term t1) -> Term Bool
- LeOrdTerm' :: forall t1. (SupportedPrim t1, PEvalOrdTerm t1) => !CachedInfo -> !(Term t1) -> !(Term t1) -> Term Bool
- AndBitsTerm' :: forall t. (SupportedPrim t, PEvalBitwiseTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- OrBitsTerm' :: forall t. (SupportedPrim t, PEvalBitwiseTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- XorBitsTerm' :: forall t. (SupportedPrim t, PEvalBitwiseTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- ComplementBitsTerm' :: forall t. (SupportedPrim t, PEvalBitwiseTerm t) => !CachedInfo -> !(Term t) -> Term t
- ShiftLeftTerm' :: forall t. (SupportedPrim t, PEvalShiftTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- ShiftRightTerm' :: forall t. (SupportedPrim t, PEvalShiftTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- RotateLeftTerm' :: forall t. (SupportedPrim t, PEvalRotateTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- RotateRightTerm' :: forall t. (SupportedPrim t, PEvalRotateTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- BitCastTerm' :: forall t a. (SupportedPrim t, PEvalBitCastTerm a t) => !CachedInfo -> !(Term a) -> Term t
- BitCastOrTerm' :: forall t a. (SupportedPrim t, PEvalBitCastOrTerm a t) => !CachedInfo -> !(Term t) -> !(Term a) -> Term t
- BVConcatTerm' :: forall (bv :: Natural -> Type) (l :: Nat) (r :: Nat). (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r), SupportedPrim (bv (l + r))) => !CachedInfo -> !(Term (bv l)) -> !(Term (bv r)) -> Term (bv (l + r))
- BVSelectTerm' :: forall (bv :: Natural -> Type) (n :: Nat) (ix :: Nat) (w :: Nat). (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n, SupportedPrim (bv w)) => !CachedInfo -> !(Proxy ix) -> !(Proxy w) -> !(Term (bv n)) -> Term (bv w)
- BVExtendTerm' :: forall (bv :: Natural -> Type) (l :: Nat) (r :: Nat). (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r, SupportedPrim (bv r)) => !CachedInfo -> !Bool -> !(Proxy r) -> !(Term (bv l)) -> Term (bv r)
- ApplyTerm' :: forall f a t. (PEvalApplyTerm f a t, SupportedPrim t) => !CachedInfo -> !(Term f) -> !(Term a) -> Term t
- DivIntegralTerm' :: forall t. (SupportedPrim t, PEvalDivModIntegralTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- ModIntegralTerm' :: forall t. (SupportedPrim t, PEvalDivModIntegralTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- QuotIntegralTerm' :: forall t. (SupportedPrim t, PEvalDivModIntegralTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- RemIntegralTerm' :: forall t. (SupportedPrim t, PEvalDivModIntegralTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- FPTraitTerm' :: forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> Type). (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => !CachedInfo -> !FPTrait -> !(Term (fp eb sb)) -> Term Bool
- FdivTerm' :: forall t. (SupportedPrim t, PEvalFractionalTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- RecipTerm' :: forall t. (SupportedPrim t, PEvalFractionalTerm t) => !CachedInfo -> !(Term t) -> Term t
- FloatingUnaryTerm' :: forall t. (SupportedPrim t, PEvalFloatingTerm t) => !CachedInfo -> !FloatingUnaryOp -> !(Term t) -> Term t
- PowerTerm' :: forall t. (SupportedPrim t, PEvalFloatingTerm t) => !CachedInfo -> !(Term t) -> !(Term t) -> Term t
- FPUnaryTerm' :: forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> Type). (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => !CachedInfo -> !FPUnaryOp -> !(Term (fp eb sb)) -> Term (fp eb sb)
- FPBinaryTerm' :: forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> Type). (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => !CachedInfo -> !FPBinaryOp -> !(Term (fp eb sb)) -> !(Term (fp eb sb)) -> Term (fp eb sb)
- FPRoundingUnaryTerm' :: forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> Type). (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => !CachedInfo -> !FPRoundingUnaryOp -> !(Term FPRoundingMode) -> !(Term (fp eb sb)) -> Term (fp eb sb)
- FPRoundingBinaryTerm' :: forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> Type). (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => !CachedInfo -> !FPRoundingBinaryOp -> !(Term FPRoundingMode) -> !(Term (fp eb sb)) -> !(Term (fp eb sb)) -> Term (fp eb sb)
- FPFMATerm' :: forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> Type). (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => !CachedInfo -> !(Term FPRoundingMode) -> !(Term (fp eb sb)) -> !(Term (fp eb sb)) -> !(Term (fp eb sb)) -> Term (fp eb sb)
- FromIntegralTerm' :: forall a t. (PEvalFromIntegralTerm a t, SupportedPrim t) => !CachedInfo -> !(Term a) -> Term t
- FromFPOrTerm' :: forall t (eb :: Nat) (sb :: Nat). (PEvalIEEEFPConvertibleTerm t, ValidFP eb sb, SupportedPrim t) => !CachedInfo -> !(Term t) -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> Term t
- ToFPTerm' :: forall a (eb :: Nat) (sb :: Nat). (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim (FP eb sb)) => !CachedInfo -> !(Term FPRoundingMode) -> !(Term a) -> Proxy eb -> Proxy sb -> Term (FP eb sb)
defaultValueDynamic :: SupportedPrim t => proxy t -> ModelValue
pattern DynTerm :: SupportedPrim a => Term a -> Term b
toCurThread :: Term t -> IO (Term t)
data CachedInfo = CachedInfo {
- cachedThreadId :: !WeakThreadId
- cachedDigest :: !Digest
- cachedId :: !Id
- cachedStableIdent :: !StableIdent
}
termInfo :: Term t -> CachedInfo
termThreadId :: Term t -> WeakThreadId
termDigest :: Term t -> Digest
termId :: Term t -> Id
termStableIdent :: Term t -> StableIdent
pformatTerm :: Term t -> String
data ModelValue where
- ModelValue :: forall v. SupportedPrim v => v -> ModelValue
toModelValue :: SupportedPrim a => a -> ModelValue
unsafeFromModelValue :: Typeable a => ModelValue -> a
data UTerm t where
- UConTerm :: forall t. SupportedPrim t => !t -> UTerm t
- USymTerm :: forall t. !(TypedSymbol 'AnyKind t) -> UTerm t
- UForallTerm :: forall t1. !(TypedSymbol 'ConstantKind t1) -> !(Term Bool) -> UTerm Bool
- UExistsTerm :: forall t1. !(TypedSymbol 'ConstantKind t1) -> !(Term Bool) -> UTerm Bool
- UNotTerm :: !(Term Bool) -> UTerm Bool
- UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
- UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
- UEqTerm :: forall t1. !(Term t1) -> !(Term t1) -> UTerm Bool
- UDistinctTerm :: forall t1. !(NonEmpty (Term t1)) -> UTerm Bool
- UITETerm :: forall t. SupportedPrim t => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
- UAddNumTerm :: forall t. (SupportedPrim t, PEvalNumTerm t) => !(Term t) -> !(Term t) -> UTerm t
- UNegNumTerm :: forall t. (SupportedPrim t, PEvalNumTerm t) => !(Term t) -> UTerm t
- UMulNumTerm :: forall t. (SupportedPrim t, PEvalNumTerm t) => !(Term t) -> !(Term t) -> UTerm t
- UAbsNumTerm :: forall t. (SupportedPrim t, PEvalNumTerm t) => !(Term t) -> UTerm t
- USignumNumTerm :: forall t. (SupportedPrim t, PEvalNumTerm t) => !(Term t) -> UTerm t
- ULtOrdTerm :: forall t1. (SupportedPrim t1, PEvalOrdTerm t1) => !(Term t1) -> !(Term t1) -> UTerm Bool
- ULeOrdTerm :: forall t1. (SupportedPrim t1, PEvalOrdTerm t1) => !(Term t1) -> !(Term t1) -> UTerm Bool
- UAndBitsTerm :: forall t. (SupportedPrim t, PEvalBitwiseTerm t) => !(Term t) -> !(Term t) -> UTerm t
- UOrBitsTerm :: forall t. (SupportedPrim t, PEvalBitwiseTerm t) => !(Term t) -> !(Term t) -> UTerm t
- UXorBitsTerm :: forall t. (SupportedPrim t, PEvalBitwiseTerm t) => !(Term t) -> !(Term t) -> UTerm t
- UComplementBitsTerm :: forall t. (SupportedPrim t, PEvalBitwiseTerm t) => !(Term t) -> UTerm t
- UShiftLeftTerm :: forall t. (SupportedPrim t, PEvalShiftTerm t) => !(Term t) -> !(Term t) -> UTerm t
- UShiftRightTerm :: forall t. (SupportedPrim t, PEvalShiftTerm t) => !(Term t) -> !(Term t) -> UTerm t
- URotateLeftTerm :: forall t. (SupportedPrim t, PEvalRotateTerm t) => !(Term t) -> !(Term t) -> UTerm t
- URotateRightTerm :: forall t. (SupportedPrim t, PEvalRotateTerm t) => !(Term t) -> !(Term t) -> UTerm t
- UBitCastTerm :: forall t a. (SupportedPrim t, PEvalBitCastTerm a t) => !(Term a) -> UTerm t
- UBitCastOrTerm :: forall t a. (SupportedPrim t, PEvalBitCastOrTerm a t) => !(Term t) -> !(Term a) -> UTerm t
- UBVConcatTerm :: forall (bv :: Natural -> Type) (l :: Nat) (r :: Nat). (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r), SupportedPrim (bv (l + r))) => !(Term (bv l)) -> !(Term (bv r)) -> UTerm (bv (l + r))
- UBVSelectTerm :: forall (bv :: Natural -> Type) (n :: Nat) (ix :: Nat) (w :: Nat). (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n, SupportedPrim (bv w)) => !(Proxy ix) -> !(Proxy w) -> !(Term (bv n)) -> UTerm (bv w)
- UBVExtendTerm :: forall (bv :: Natural -> Type) (l :: Nat) (r :: Nat). (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r, SupportedPrim (bv r)) => !Bool -> !(Proxy r) -> !(Term (bv l)) -> UTerm (bv r)
- UApplyTerm :: forall f a t. (PEvalApplyTerm f a t, SupportedPrim t) => Term f -> Term a -> UTerm t
- UDivIntegralTerm :: forall t. (SupportedPrim t, PEvalDivModIntegralTerm t) => !(Term t) -> !(Term t) -> UTerm t
- UModIntegralTerm :: forall t. (SupportedPrim t, PEvalDivModIntegralTerm t) => !(Term t) -> !(Term t) -> UTerm t
- UQuotIntegralTerm :: forall t. (SupportedPrim t, PEvalDivModIntegralTerm t) => !(Term t) -> !(Term t) -> UTerm t
- URemIntegralTerm :: forall t. (SupportedPrim t, PEvalDivModIntegralTerm t) => !(Term t) -> !(Term t) -> UTerm t
- UFPTraitTerm :: forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> Type). (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => !FPTrait -> !(Term (fp eb sb)) -> UTerm Bool
- UFdivTerm :: forall t. (SupportedPrim t, PEvalFractionalTerm t) => !(Term t) -> !(Term t) -> UTerm t
- URecipTerm :: forall t. (SupportedPrim t, PEvalFractionalTerm t) => !(Term t) -> UTerm t
- UFloatingUnaryTerm :: forall t. (SupportedPrim t, PEvalFloatingTerm t) => !FloatingUnaryOp -> !(Term t) -> UTerm t
- UPowerTerm :: forall t. (SupportedPrim t, PEvalFloatingTerm t) => !(Term t) -> !(Term t) -> UTerm t
- UFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> Type). (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => !FPUnaryOp -> !(Term (fp eb sb)) -> UTerm (fp eb sb)
- UFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> Type). (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => !FPBinaryOp -> !(Term (fp eb sb)) -> !(Term (fp eb sb)) -> UTerm (fp eb sb)
- UFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> Type). (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => !FPRoundingUnaryOp -> !(Term FPRoundingMode) -> !(Term (fp eb sb)) -> UTerm (fp eb sb)
- UFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> Type). (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => !FPRoundingBinaryOp -> !(Term FPRoundingMode) -> !(Term (fp eb sb)) -> !(Term (fp eb sb)) -> UTerm (fp eb sb)
- UFPFMATerm :: forall (eb :: Nat) (sb :: Nat) (fp :: Nat -> Nat -> Type). (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => !(Term FPRoundingMode) -> !(Term (fp eb sb)) -> !(Term (fp eb sb)) -> !(Term (fp eb sb)) -> UTerm (fp eb sb)
- UFromIntegralTerm :: forall a t. (PEvalFromIntegralTerm a t, SupportedPrim t) => !(Term a) -> UTerm t
- UFromFPOrTerm :: forall t (eb :: Nat) (sb :: Nat). (PEvalIEEEFPConvertibleTerm t, SupportedPrim t, ValidFP eb sb) => Term t -> !(Term FPRoundingMode) -> !(Term (FP eb sb)) -> UTerm t
- UToFPTerm :: forall a (eb :: Nat) (sb :: Nat). (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim (FP eb sb)) => !(Term FPRoundingMode) -> !(Term a) -> Proxy eb -> Proxy sb -> UTerm (FP eb sb)
prettyPrintTerm :: Term t -> Doc ann
conTerm :: SupportedPrim t => t -> Term t
symTerm :: forall (knd :: SymbolKind) t. TypedSymbol knd t -> Term t
ssymTerm :: SupportedPrim t => Identifier -> Term t
isymTerm :: SupportedPrim t => Identifier -> Int -> Term t
forallTerm :: TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool
existsTerm :: TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool
notTerm :: Term Bool -> Term Bool
orTerm :: Term Bool -> Term Bool -> Term Bool
andTerm :: Term Bool -> Term Bool -> Term Bool
eqTerm :: Term a -> Term a -> Term Bool
distinctTerm :: NonEmpty (Term a) -> Term Bool
iteTerm :: 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
rotateLeftTerm :: PEvalRotateTerm a => Term a -> Term a -> Term a
shiftRightTerm :: PEvalShiftTerm a => Term a -> Term a -> Term a
rotateRightTerm :: PEvalRotateTerm a => Term a -> Term a -> Term a
bitCastTerm :: (PEvalBitCastTerm a b, SupportedPrim b) => Term a -> Term b
bitCastOrTerm :: PEvalBitCastOrTerm a b => Term b -> Term a -> Term b
bvConcatTerm :: forall bv (l :: Nat) (r :: Nat). (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r), SupportedPrim (bv (l + r))) => Term (bv l) -> Term (bv r) -> Term (bv (l + r))
bvSelectTerm :: forall bv (n :: Nat) (ix :: Nat) (w :: Nat) p q. (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n, SupportedPrim (bv w)) => p ix -> q w -> Term (bv n) -> Term (bv w)
bvExtendTerm :: forall bv (l :: Nat) (r :: Nat) proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r, SupportedPrim (bv r)) => Bool -> proxy r -> Term (bv l) -> Term (bv r)
bvsignExtendTerm :: forall bv (l :: Nat) (r :: Nat) proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r, SupportedPrim (bv r)) => proxy r -> Term (bv l) -> Term (bv r)
bvzeroExtendTerm :: forall bv (l :: Nat) (r :: Nat) proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r, SupportedPrim (bv r)) => proxy r -> Term (bv l) -> Term (bv r)
applyTerm :: (PEvalApplyTerm f a b, SupportedPrim 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 :: forall (eb :: Nat) (sb :: Nat) fp. (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPTrait -> Term (fp eb sb) -> Term Bool
fdivTerm :: PEvalFractionalTerm a => Term a -> Term a -> Term a
recipTerm :: PEvalFractionalTerm a => Term a -> Term a
floatingUnaryTerm :: PEvalFloatingTerm a => FloatingUnaryOp -> Term a -> Term a
powerTerm :: PEvalFloatingTerm a => Term a -> Term a -> Term a
fpUnaryTerm :: forall (eb :: Nat) (sb :: Nat) fp. (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPUnaryOp -> Term (fp eb sb) -> Term (fp eb sb)
fpBinaryTerm :: forall (eb :: Nat) (sb :: Nat) fp. (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPBinaryOp -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb)
fpRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat) fp. (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb)
fpRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat) fp. (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb)
fpFMATerm :: forall (eb :: Nat) (sb :: Nat) fp. (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb)
fromIntegralTerm :: (PEvalFromIntegralTerm a b, SupportedPrim b) => Term a -> Term b
fromFPOrTerm :: forall a (eb :: Nat) (sb :: Nat). (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) => Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
toFPTerm :: forall a (eb :: Nat) (sb :: Nat). (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim (FP eb sb)) => Term FPRoundingMode -> Term a -> Term (FP eb sb)
pattern SupportedTerm :: () => SupportedPrim t => Term t
pattern SupportedTypedSymbol :: () => (SupportedPrim t, SymbolKindConstraint k t, IsSymbolKind k) => TypedSymbol k t
pattern SupportedConstantTypedSymbol :: () => (SupportedPrim t, SymbolKindConstraint k t, IsSymbolKind k, k ~ 'ConstantKind) => TypedSymbol k t
pattern ConTerm :: () => SupportedPrim t => t -> Term t
pattern SymTerm :: () => SupportedPrim t => TypedSymbol 'AnyKind t -> Term t
pattern ForallTerm :: forall r t. () => (r ~ Bool, SupportedNonFuncPrim t) => TypedSymbol 'ConstantKind t -> Term Bool -> Term r
pattern ExistsTerm :: forall r t. () => (r ~ Bool, SupportedNonFuncPrim t) => TypedSymbol 'ConstantKind t -> Term Bool -> Term r
pattern NotTerm :: () => r ~ Bool => Term Bool -> Term r
pattern OrTerm :: () => r ~ Bool => Term Bool -> Term Bool -> Term r
pattern AndTerm :: () => r ~ Bool => Term Bool -> Term Bool -> Term r
pattern EqTerm :: forall r t. () => (r ~ Bool, SupportedPrim t) => Term t -> Term t -> Term r
pattern DistinctTerm :: forall r t. () => (r ~ Bool, SupportedPrim t) => NonEmpty (Term t) -> Term r
pattern ITETerm :: () => SupportedPrim t => Term Bool -> Term t -> Term t -> Term t
pattern AddNumTerm :: () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t -> Term t
pattern NegNumTerm :: () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t
pattern MulNumTerm :: () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t -> Term t
pattern AbsNumTerm :: () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t
pattern SignumNumTerm :: () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t
pattern LtOrdTerm :: forall r t. () => (r ~ Bool, SupportedPrim t, PEvalOrdTerm t) => Term t -> Term t -> Term r
pattern LeOrdTerm :: forall r t. () => (r ~ Bool, SupportedPrim t, PEvalOrdTerm t) => Term t -> Term t -> Term r
pattern AndBitsTerm :: () => (SupportedPrim t, PEvalBitwiseTerm t) => Term t -> Term t -> Term t
pattern OrBitsTerm :: () => (SupportedPrim t, PEvalBitwiseTerm t) => Term t -> Term t -> Term t
pattern XorBitsTerm :: () => (SupportedPrim t, PEvalBitwiseTerm t) => Term t -> Term t -> Term t
pattern ComplementBitsTerm :: () => (SupportedPrim t, PEvalBitwiseTerm t) => Term t -> Term t
pattern ShiftLeftTerm :: () => (SupportedPrim t, PEvalShiftTerm t) => Term t -> Term t -> Term t
pattern RotateLeftTerm :: () => (SupportedPrim t, PEvalRotateTerm t) => Term t -> Term t -> Term t
pattern ShiftRightTerm :: () => (SupportedPrim t, PEvalShiftTerm t) => Term t -> Term t -> Term t
pattern RotateRightTerm :: () => (SupportedPrim t, PEvalRotateTerm t) => Term t -> Term t -> Term t
pattern BitCastTerm :: forall b a. () => (SupportedPrim a, SupportedPrim b, PEvalBitCastTerm a b) => Term a -> Term b
pattern BitCastOrTerm :: () => (SupportedPrim a, SupportedPrim b, PEvalBitCastOrTerm a b) => Term b -> Term a -> Term b
pattern BVConcatTerm :: forall ret bv (l :: Nat) (r :: Nat). () => (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r), SupportedPrim (bv l), SupportedPrim (bv r), SupportedPrim (bv (l + r)), ret ~ bv (l + r)) => Term (bv l) -> Term (bv r) -> Term ret
pattern BVSelectTerm :: forall ret bv (w :: Nat) (n :: Nat) (ix :: Nat). () => (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n, SupportedPrim (bv n), SupportedPrim (bv w), ret ~ bv w) => Proxy ix -> Proxy w -> Term (bv n) -> Term ret
pattern BVExtendTerm :: forall ret bv (l :: Nat) (r :: Nat). () => (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r, SupportedPrim (bv l), SupportedPrim (bv r), ret ~ bv r) => Bool -> Proxy r -> Term (bv l) -> Term ret
pattern ApplyTerm :: forall b f a. () => (PEvalApplyTerm f a b, SupportedPrim f, SupportedPrim a, SupportedPrim b) => Term f -> Term a -> Term b
pattern DivIntegralTerm :: () => (SupportedPrim t, PEvalDivModIntegralTerm t) => Term t -> Term t -> Term t
pattern ModIntegralTerm :: () => (SupportedPrim t, PEvalDivModIntegralTerm t) => Term t -> Term t -> Term t
pattern QuotIntegralTerm :: () => (SupportedPrim t, PEvalDivModIntegralTerm t) => Term t -> Term t -> Term t
pattern RemIntegralTerm :: () => (SupportedPrim t, PEvalDivModIntegralTerm t) => Term t -> Term t -> Term t
pattern FPTraitTerm :: forall r (eb :: Nat) (sb :: Nat) fp. () => (r ~ Bool, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPTrait -> Term (fp eb sb) -> Term r
pattern FdivTerm :: () => (SupportedPrim t, PEvalFractionalTerm t) => Term t -> Term t -> Term t
pattern RecipTerm :: () => (SupportedPrim t, PEvalFractionalTerm t) => Term t -> Term t
pattern FloatingUnaryTerm :: () => (SupportedPrim t, PEvalFloatingTerm t) => FloatingUnaryOp -> Term t -> Term t
pattern PowerTerm :: () => (SupportedPrim t, PEvalFloatingTerm t) => Term t -> Term t -> Term t
pattern FPUnaryTerm :: forall ret fp (eb :: Nat) (sb :: Nat). () => (ret ~ fp eb sb, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPUnaryOp -> Term (fp eb sb) -> Term ret
pattern FPBinaryTerm :: forall ret fp (eb :: Nat) (sb :: Nat). () => (ret ~ fp eb sb, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPBinaryOp -> Term (fp eb sb) -> Term (fp eb sb) -> Term ret
pattern FPRoundingUnaryTerm :: forall ret fp (eb :: Nat) (sb :: Nat). () => (ret ~ fp eb sb, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (fp eb sb) -> Term ret
pattern FPRoundingBinaryTerm :: forall ret fp (eb :: Nat) (sb :: Nat). () => (ret ~ fp eb sb, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) -> Term ret
pattern FPFMATerm :: forall ret fp (eb :: Nat) (sb :: Nat). () => (ret ~ fp eb sb, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb) -> Term ret
pattern FromIntegralTerm :: forall b a. () => (PEvalFromIntegralTerm a b, SupportedPrim a, SupportedPrim b) => Term a -> Term b
pattern FromFPOrTerm :: forall a (eb :: Nat) (sb :: Nat). () => (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim a) => Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
pattern ToFPTerm :: forall ret (eb :: Nat) (sb :: Nat) a. () => (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim a, ret ~ FP eb sb) => Term FPRoundingMode -> Term a -> Proxy eb -> Proxy sb -> Term ret
trueTerm :: Term Bool
falseTerm :: Term Bool
pattern BoolConTerm :: Bool -> Term a
pattern TrueTerm :: Term a
pattern FalseTerm :: Term a
pattern BoolTerm :: Term Bool -> Term a
pevalNotTerm :: Term Bool -> Term Bool
pevalOrTerm :: Term Bool -> Term Bool -> Term Bool
pevalAndTerm :: Term Bool -> Term Bool -> Term Bool
pevalImplyTerm :: Term Bool -> Term Bool -> Term Bool
pevalXorTerm :: Term Bool -> Term Bool -> Term Bool
pevalITEBasic :: SupportedPrim a => Term Bool -> Term a -> Term a -> Maybe (Term a)
pevalITEBasicTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a
pevalDefaultEqTerm :: SupportedNonFuncPrim a => Term a -> Term a -> Term Bool
type NonFuncPrimConstraint a = (SymVal (NonFuncSBVBaseType a), EqSymbolic (SBVType a), Mergeable (SBVType a), SMTDefinable (SBVType a), Mergeable (SBVType a), SBVType a ~ SBV (NonFuncSBVBaseType a), PrimConstraint a)
class (SupportedPrim a, Ord a, Eq a, Show a, Hashable a, Typeable a) => NonFuncSBVRep a where
- type NonFuncSBVBaseType a
class NonFuncSBVRep a => SupportedNonFuncPrim a where
- conNonFuncSBVTerm :: a -> SBV (NonFuncSBVBaseType a)
- symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType a))
- withNonFuncPrim :: (NonFuncPrimConstraint a => r) -> r
class SBVRep t where
- type SBVType t
class MonadIO m => SBVFreshMonad (m :: Type -> Type) where
- sbvFresh :: SymVal a => String -> m (SBV a)
translateTypeError :: HasCallStack => Maybe String -> TypeRep a -> b
parseSMTModelResultError :: HasCallStack => TypeRep a -> ([([CV], CV)], CV) -> a
partitionCVArg :: SupportedNonFuncPrim a => [([CV], CV)] -> [(a, [([CV], CV)])]
parseScalarSMTModelResult :: forall v r. (SatModel r, Typeable v) => (r -> v) -> ([([CV], CV)], CV) -> v

Supported primitive types

class SupportedPrimConstraint t Source #

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

Associated Types

type PrimConstraint t Source #

type PrimConstraint t = ()

Instances

Instances details

SupportedPrimConstraint AlgReal Source #

Instance details

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

Associated Types

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

SupportedPrimConstraint FPRoundingMode Source #

Instance details

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

Associated Types

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

SupportedPrimConstraint Integer Source #

Instance details

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

Associated Types

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

SupportedPrimConstraint Bool Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

type PrimConstraint Bool
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type PrimConstraint Bool = ()

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

Instance details

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

Associated Types

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

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

Instance details

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

Associated Types

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

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

Instance details

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

Associated Types

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

(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a --> b) Source #

Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

Associated Types

type PrimConstraint (a --> b)
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun type PrimConstraint (a --> b) = (SupportedNonFuncPrim a, SupportedPrim b, NonFuncPrimConstraint a, PrimConstraint b, SBVType (a --> b) ~ (SBV (NonFuncSBVBaseType a) -> SBVType b))

(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a =-> b) Source #

Instance details

Defined in Grisette.Internal.SymPrim.TabularFun

Associated Types

type PrimConstraint (a =-> b)
Instance details Defined in Grisette.Internal.SymPrim.TabularFun type PrimConstraint (a =-> b) = (SupportedNonFuncPrim a, SupportedPrim b, NonFuncPrimConstraint a, PrimConstraint b)

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

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

Minimal complete definition

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

Methods

primTypeRep :: TypeRep t Source #

default primTypeRep :: Typeable t => TypeRep t Source #

sameCon :: t -> t -> Bool Source #

default sameCon :: Eq t => t -> t -> Bool Source #

hashConWithSalt :: Int -> t -> Int Source #

default hashConWithSalt :: Hashable t => Int -> t -> Int Source #

pformatCon :: t -> String Source #

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

defaultValue :: t Source #

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

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

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

conSBVTerm :: t -> SBVType t Source #

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

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

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

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

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

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

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

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

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

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

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

funcDummyConstraint :: SBVType t -> SBV Bool Source #

Instances

Instances details

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

class SupportedPrim con => SymRep con Source #

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

Associated Types

type SymType con Source #

Instances

Instances details

SymRep AlgReal Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Associated Types

type SymType AlgReal
Instance details Defined in Grisette.Internal.SymPrim.SymAlgReal type SymType AlgReal = SymAlgReal

SymRep FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type SymType FPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.SymFP type SymType FPRoundingMode = SymFPRoundingMode

SymRep Integer Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Associated Types

type SymType Integer
Instance details Defined in Grisette.Internal.SymPrim.SymInteger type SymType Integer = SymInteger

SymRep Bool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Associated Types

type SymType Bool
Instance details Defined in Grisette.Internal.SymPrim.SymBool type SymType Bool = SymBool

(KnownNat n, 1 <= n) => SymRep (IntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type SymType (IntN n)
Instance details Defined in Grisette.Internal.SymPrim.SymBV type SymType (IntN n) = SymIntN n

(KnownNat n, 1 <= n) => SymRep (WordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type SymType (WordN n)
Instance details Defined in Grisette.Internal.SymPrim.SymBV type SymType (WordN n) = SymWordN n

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

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type SymType (FP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.SymFP type SymType (FP eb sb) = SymFP eb sb

(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)
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun type SymType (ca --> cb) = SymType ca -~> SymType cb

(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)
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun type SymType (a =-> b) = SymType a =~> SymType b

class ConRep sym Source #

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

Associated Types

type ConType sym Source #

Instances

Instances details

ConRep SymAlgReal Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Associated Types

type ConType SymAlgReal
Instance details Defined in Grisette.Internal.SymPrim.SymAlgReal type ConType SymAlgReal = AlgReal

ConRep SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Associated Types

type ConType SymBool
Instance details Defined in Grisette.Internal.SymPrim.SymBool type ConType SymBool = Bool

ConRep SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type ConType SymFPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.SymFP type ConType SymFPRoundingMode = FPRoundingMode

ConRep SymInteger Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Associated Types

type ConType SymInteger
Instance details Defined in Grisette.Internal.SymPrim.SymInteger type ConType SymInteger = Integer

(KnownNat n, 1 <= n) => ConRep (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type ConType (SymIntN n)
Instance details Defined in Grisette.Internal.SymPrim.SymBV type ConType (SymIntN n) = IntN n

(KnownNat n, 1 <= n) => ConRep (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Associated Types

type ConType (SymWordN n)
Instance details Defined in Grisette.Internal.SymPrim.SymBV type ConType (SymWordN n) = WordN n

ConRep (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type ConType (SymFP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.SymFP type ConType (SymFP eb sb) = FP eb sb

(ConRep a, ConRep b) => ConRep (a -~> b) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymGeneralFun

Associated Types

type ConType (a -~> b)
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun type ConType (a -~> b) = ConType a --> ConType b

(ConRep a, ConRep b) => ConRep (a =~> b) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymTabularFun

Associated Types

type ConType (a =~> b)
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun type ConType (a =~> b) = ConType a =-> ConType b

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

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

Methods

underlyingTerm :: sym -> Term con Source #

wrapTerm :: Term con -> sym Source #

Instances

Instances details

LinkedRep AlgReal SymAlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.SymAlgReal Methods underlyingTerm :: SymAlgReal -> Term AlgReal Source # wrapTerm :: Term AlgReal -> SymAlgReal Source #
LinkedRep FPRoundingMode SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods underlyingTerm :: SymFPRoundingMode -> Term FPRoundingMode Source # wrapTerm :: Term FPRoundingMode -> SymFPRoundingMode Source #
LinkedRep Integer SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods underlyingTerm :: SymInteger -> Term Integer Source # wrapTerm :: Term Integer -> SymInteger Source #
LinkedRep Bool SymBool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBool Methods underlyingTerm :: SymBool -> Term Bool Source # wrapTerm :: Term Bool -> SymBool Source #
(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods underlyingTerm :: SymIntN n -> Term (IntN n) Source # wrapTerm :: Term (IntN n) -> SymIntN n Source #
(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods underlyingTerm :: SymWordN n -> Term (WordN n) Source # wrapTerm :: Term (WordN n) -> SymWordN n Source #
ValidFP eb sb => LinkedRep (FP eb sb) (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods underlyingTerm :: SymFP eb sb -> Term (FP eb sb) Source # wrapTerm :: Term (FP eb sb) -> SymFP eb sb Source #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim cb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => 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), SupportedNonFuncPrim ca) => 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 PEvalApplyTerm f a b | f -> a b where Source #

Partial evaluation and lowering for function application terms.

Methods

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

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

Instances

Instances details

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

class PEvalBitwiseTerm t where Source #

Partial evaluation and lowering for bitwise operation terms.

Minimal complete definition

pevalAndBitsTerm, pevalOrBitsTerm, pevalXorBitsTerm, pevalComplementBitsTerm, withSbvBitwiseTermConstraint

Methods

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

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

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

pevalComplementBitsTerm :: Term t -> Term t Source #

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

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

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

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

sbvComplementBitsTerm :: SBVType t -> SBVType t Source #

Instances

Instances details

(KnownNat n, 1 <= n) => PEvalBitwiseTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm Methods pevalAndBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalOrBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalXorBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalComplementBitsTerm :: Term (IntN n) -> Term (IntN n) Source # withSbvBitwiseTermConstraint :: (Bits (SBVType (IntN n)) => r) -> r Source # sbvAndBitsTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvOrBitsTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvXorBitsTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvComplementBitsTerm :: SBVType (IntN n) -> SBVType (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalBitwiseTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm Methods pevalAndBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalOrBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalXorBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalComplementBitsTerm :: Term (WordN n) -> Term (WordN n) Source # withSbvBitwiseTermConstraint :: (Bits (SBVType (WordN n)) => r) -> r Source # sbvAndBitsTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvOrBitsTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvXorBitsTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvComplementBitsTerm :: SBVType (WordN n) -> SBVType (WordN n) Source #

class PEvalShiftTerm t where Source #

Partial evaluation and lowering for symbolic shifting terms.

Minimal complete definition

pevalShiftLeftTerm, pevalShiftRightTerm, withSbvShiftTermConstraint

Methods

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

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

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

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

default sbvShiftLeftTerm :: SupportedNonFuncPrim t => SBVType t -> SBVType t -> SBVType t Source #

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

default sbvShiftRightTerm :: SupportedNonFuncPrim t => SBVType t -> SBVType t -> SBVType t Source #

Instances

Instances details

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

class PEvalRotateTerm t where Source #

Partial evaluation and lowering for symbolic rotate terms.

Minimal complete definition

pevalRotateLeftTerm, pevalRotateRightTerm, withSbvRotateTermConstraint

Methods

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

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

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

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

default sbvRotateLeftTerm :: SupportedNonFuncPrim t => SBVType t -> SBVType t -> SBVType t Source #

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

default sbvRotateRightTerm :: SupportedNonFuncPrim t => SBVType t -> SBVType t -> SBVType t Source #

Instances

Instances details

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

class Num t => PEvalNumTerm t where Source #

Partial evaluation and lowering for number terms.

Minimal complete definition

pevalAddNumTerm, pevalNegNumTerm, pevalMulNumTerm, pevalAbsNumTerm, pevalSignumNumTerm, withSbvNumTermConstraint

Methods

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

pevalNegNumTerm :: Term t -> Term t Source #

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

pevalAbsNumTerm :: Term t -> Term t Source #

pevalSignumNumTerm :: Term t -> Term t Source #

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

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

sbvNegNumTerm :: SBVType t -> SBVType t Source #

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

sbvAbsNumTerm :: SBVType t -> SBVType t Source #

sbvSignumNumTerm :: SBVType t -> SBVType t Source #

Instances

Instances details

PEvalNumTerm AlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm Methods pevalAddNumTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal Source # pevalNegNumTerm :: Term AlgReal -> Term AlgReal Source # pevalMulNumTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal Source # pevalAbsNumTerm :: Term AlgReal -> Term AlgReal Source # pevalSignumNumTerm :: Term AlgReal -> Term AlgReal Source # withSbvNumTermConstraint :: (Num (SBVType AlgReal) => r) -> r Source # sbvAddNumTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal Source # sbvNegNumTerm :: SBVType AlgReal -> SBVType AlgReal Source # sbvMulNumTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal Source # sbvAbsNumTerm :: SBVType AlgReal -> SBVType AlgReal Source # sbvSignumNumTerm :: SBVType AlgReal -> SBVType AlgReal Source #
PEvalNumTerm Integer Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm Methods pevalAddNumTerm :: Term Integer -> Term Integer -> Term Integer Source # pevalNegNumTerm :: Term Integer -> Term Integer Source # pevalMulNumTerm :: Term Integer -> Term Integer -> Term Integer Source # pevalAbsNumTerm :: Term Integer -> Term Integer Source # pevalSignumNumTerm :: Term Integer -> Term Integer Source # withSbvNumTermConstraint :: (Num (SBVType Integer) => r) -> r Source # sbvAddNumTerm :: SBVType Integer -> SBVType Integer -> SBVType Integer Source # sbvNegNumTerm :: SBVType Integer -> SBVType Integer Source # sbvMulNumTerm :: SBVType Integer -> SBVType Integer -> SBVType Integer Source # sbvAbsNumTerm :: SBVType Integer -> SBVType Integer Source # sbvSignumNumTerm :: SBVType Integer -> SBVType Integer Source #
(KnownNat n, 1 <= n) => PEvalNumTerm (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm Methods pevalAddNumTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalNegNumTerm :: Term (IntN n) -> Term (IntN n) Source # pevalMulNumTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n) Source # pevalAbsNumTerm :: Term (IntN n) -> Term (IntN n) Source # pevalSignumNumTerm :: Term (IntN n) -> Term (IntN n) Source # withSbvNumTermConstraint :: (Num (SBVType (IntN n)) => r) -> r Source # sbvAddNumTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvNegNumTerm :: SBVType (IntN n) -> SBVType (IntN n) Source # sbvMulNumTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n) Source # sbvAbsNumTerm :: SBVType (IntN n) -> SBVType (IntN n) Source # sbvSignumNumTerm :: SBVType (IntN n) -> SBVType (IntN n) Source #
(KnownNat n, 1 <= n) => PEvalNumTerm (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm Methods pevalAddNumTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalNegNumTerm :: Term (WordN n) -> Term (WordN n) Source # pevalMulNumTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n) Source # pevalAbsNumTerm :: Term (WordN n) -> Term (WordN n) Source # pevalSignumNumTerm :: Term (WordN n) -> Term (WordN n) Source # withSbvNumTermConstraint :: (Num (SBVType (WordN n)) => r) -> r Source # sbvAddNumTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvNegNumTerm :: SBVType (WordN n) -> SBVType (WordN n) Source # sbvMulNumTerm :: SBVType (WordN n) -> SBVType (WordN n) -> SBVType (WordN n) Source # sbvAbsNumTerm :: SBVType (WordN n) -> SBVType (WordN n) Source # sbvSignumNumTerm :: SBVType (WordN n) -> SBVType (WordN n) Source #
ValidFP eb sb => PEvalNumTerm (FP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm Methods pevalAddNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalNegNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source # pevalMulNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source # pevalAbsNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source # pevalSignumNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source # withSbvNumTermConstraint :: (Num (SBVType (FP eb sb)) => r) -> r Source # sbvAddNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvNegNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvMulNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvAbsNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source # sbvSignumNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

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

Partial evaluation for subtraction terms.

class PEvalOrdTerm t where Source #

Partial evaluation and lowering for comparison terms.

Minimal complete definition

pevalLtOrdTerm, pevalLeOrdTerm, withSbvOrdTermConstraint

Methods

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

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

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

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

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

Instances

Instances details

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

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

Partial evaluation for greater than terms.

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

Partial evaluation for greater than or equal to terms.

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

Partial evaluation for inequality terms.

class PEvalDivModIntegralTerm t where Source #

Partial evaluation and lowering for integer division and modulo terms.

Minimal complete definition

pevalDivIntegralTerm, pevalModIntegralTerm, pevalQuotIntegralTerm, pevalRemIntegralTerm, withSbvDivModIntegralTermConstraint

Methods

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

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

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

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

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

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

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

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

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

Instances

Instances details

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

class BitCast a b => PEvalBitCastTerm a b where Source #

Partial evaluation and lowering for bitcast terms.

Methods

pevalBitCastTerm :: Term a -> Term b Source #

sbvBitCast :: SBVType a -> SBVType b Source #

Instances

Instances details

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

class BitCastOr a b => PEvalBitCastOrTerm a b where Source #

Partial evaluation and lowering for bitcast or default value terms.

Methods

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

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

Instances

Instances details

(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastOrTerm (FP eb sb) (IntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm Methods pevalBitCastOrTerm :: Term (IntN n) -> Term (FP eb sb) -> Term (IntN n) Source # sbvBitCastOr :: SBVType (IntN n) -> SBVType (FP eb sb) -> SBVType (IntN n) Source #
(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastOrTerm (FP eb sb) (WordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm Methods pevalBitCastOrTerm :: Term (WordN n) -> Term (FP eb sb) -> Term (WordN n) Source # sbvBitCastOr :: SBVType (WordN n) -> SBVType (FP eb sb) -> SBVType (WordN n) Source #

class SizedBV bv => PEvalBVTerm (bv :: Natural -> Type) where Source #

Partial evaluation and lowering for bit-vector terms.

Methods

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

pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (bv l) -> Term (bv 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 (bv n) -> Term (bv w) Source #

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

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

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

Instances

Instances details

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

class Fractional t => PEvalFractionalTerm t where Source #

Partial evaluation and lowering for fractional terms.

Minimal complete definition

pevalFdivTerm, pevalRecipTerm, withSbvFractionalTermConstraint

Methods

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

pevalRecipTerm :: Term t -> Term t Source #

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

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

sbvRecipTerm :: SBVType t -> SBVType t Source #

Instances

Instances details

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

class PEvalFPTerm (fp :: Nat -> Nat -> Type) where Source #

Partial evaluation and lowering for floating point terms.

Methods

pevalFPTraitTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPTrait -> Term (fp eb sb) -> Term Bool Source #

pevalFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPUnaryOp -> Term (fp eb sb) -> Term (fp eb sb) Source #

pevalFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPBinaryOp -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb) Source #

pevalFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) Source #

pevalFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb) Source #

pevalFPFMATerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb) Source #

sbvFPTraitTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPTrait -> SBVType (fp eb sb) -> SBVType Bool Source #

sbvFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPUnaryOp -> SBVType (fp eb sb) -> SBVType (fp eb sb) Source #

sbvFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPBinaryOp -> SBVType (fp eb sb) -> SBVType (fp eb sb) -> SBVType (fp eb sb) Source #

sbvFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingUnaryOp -> SBVType FPRoundingMode -> SBVType (fp eb sb) -> SBVType (fp eb sb) Source #

sbvFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingBinaryOp -> SBVType FPRoundingMode -> SBVType (fp eb sb) -> SBVType (fp eb sb) -> SBVType (fp eb sb) Source #

sbvFPFMATerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType (fp eb sb) -> SBVType (fp eb sb) -> SBVType (fp eb sb) -> SBVType (fp eb sb) Source #

Instances

Instances details

PEvalFPTerm FP Source #

Instance details

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

Methods

pevalFPTraitTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPTrait -> Term (FP eb sb) -> Term Bool Source #

pevalFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalFPFMATerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

sbvFPTraitTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPTrait -> SBVType (FP eb sb) -> SBVType Bool Source #

sbvFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPUnaryOp -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPBinaryOp -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingUnaryOp -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingBinaryOp -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvFPFMATerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

class PEvalFloatingTerm t where Source #

Partial evaluation and lowering for floating point terms.

Minimal complete definition

pevalFloatingUnaryTerm, pevalPowerTerm, withSbvFloatingTermConstraint

Methods

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

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

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

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

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

Instances

Instances details

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

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

Partial evaluation and lowering for integral terms.

Methods

pevalFromIntegralTerm :: Term a -> Term b Source #

sbvFromIntegralTerm :: SBVType a -> SBVType b Source #

Instances

Instances details

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

class PEvalIEEEFPConvertibleTerm a where Source #

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

Methods

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

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

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

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

Instances

Instances details

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

Typed symbols

data SymbolKind Source #

The kind of a symbol.

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

Constructors

ConstantKind
AnyKind

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

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

Simple symbols can be created with the OverloadedStrings extension:

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

Constructors

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

Instances

Instances details

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

typedConstantSymbol :: SupportedNonFuncPrim t => Symbol -> TypedSymbol 'ConstantKind t Source #

Create a typed symbol with constant kinds.

typedAnySymbol :: SupportedPrim t => Symbol -> TypedSymbol 'AnyKind t Source #

Create a typed symbol with any kinds.

type TypedConstantSymbol = TypedSymbol 'ConstantKind Source #

Constant symbol

type TypedAnySymbol = TypedSymbol 'AnyKind Source #

Any symbol

data SomeTypedSymbol (knd :: SymbolKind) where Source #

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

Constructors

SomeTypedSymbol :: forall (knd :: SymbolKind) t. TypedSymbol knd t -> SomeTypedSymbol knd

Instances

Instances details

Lift (SomeTypedSymbol knd :: Type) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods lift :: Quote m => SomeTypedSymbol knd -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => SomeTypedSymbol knd -> Code m (SomeTypedSymbol knd) #
IsSymbolKind knd => Binary (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize Methods put :: SomeTypedSymbol knd -> Put # get :: Get (SomeTypedSymbol knd) # putList :: [SomeTypedSymbol knd] -> Put #
IsSymbolKind knd => Serial (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize Methods serialize :: MonadPut m => SomeTypedSymbol knd -> m () # deserialize :: MonadGet m => m (SomeTypedSymbol knd) #
IsSymbolKind knd => Serialize (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize Methods put :: Putter (SomeTypedSymbol knd) # get :: Get (SomeTypedSymbol knd) #
NFData (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: SomeTypedSymbol knd -> () #
Show (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods showsPrec :: Int -> SomeTypedSymbol knd -> ShowS # show :: SomeTypedSymbol knd -> String # showList :: [SomeTypedSymbol knd] -> ShowS #
Eq (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool # (/=) :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool #
Ord (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods compare :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Ordering # (<) :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool # (<=) :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool # (>) :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool # (>=) :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> Bool # max :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> SomeTypedSymbol knd # min :: SomeTypedSymbol knd -> SomeTypedSymbol knd -> SomeTypedSymbol knd #
PPrint (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint Methods pformat :: SomeTypedSymbol knd -> Doc ann Source # pformatPrec :: Int -> SomeTypedSymbol knd -> Doc ann Source # pformatList :: [SomeTypedSymbol knd] -> Doc ann Source #
Hashable (SomeTypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> SomeTypedSymbol knd -> Int # hash :: SomeTypedSymbol knd -> Int #
SymbolSetRep (SomeTypedSymbol knd) (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: SomeTypedSymbol knd -> SymbolSet knd Source #
SymbolSetRep [SomeTypedSymbol knd] (SymbolSet knd) (TypedSymbol knd) Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: [SomeTypedSymbol knd] -> SymbolSet knd Source #

type SomeTypedConstantSymbol = SomeTypedSymbol 'ConstantKind Source #

Non-indexed constant symbol

type SomeTypedAnySymbol = SomeTypedSymbol 'AnyKind Source #

Non-indexed any symbol

class IsSymbolKind (knd :: SymbolKind) where Source #

Decision procedure for symbol kinds.

Associated Types

type SymbolKindConstraint (knd :: SymbolKind) :: Type -> Constraint Source #

Methods

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

withSymbolKindConstraint :: TypedSymbol knd t -> (SymbolKindConstraint knd t => a) -> a Source #

Instances

Instances details

IsSymbolKind 'AnyKind Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

type SymbolKindConstraint 'AnyKind
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type SymbolKindConstraint 'AnyKind = SupportedPrim

Methods

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

withSymbolKindConstraint :: TypedSymbol 'AnyKind t -> (SymbolKindConstraint 'AnyKind t => a) -> a Source #

IsSymbolKind 'ConstantKind Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

type SymbolKindConstraint 'ConstantKind
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type SymbolKindConstraint 'ConstantKind = SupportedNonFuncPrim

Methods

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

withSymbolKindConstraint :: TypedSymbol 'ConstantKind t -> (SymbolKindConstraint 'ConstantKind t => a) -> a Source #

showUntyped :: forall (knd :: SymbolKind) t. TypedSymbol knd t -> String Source #

Show a typed symbol without the type information.

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

Construct a SomeTypedSymbol from a TypedSymbol.

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

Compare two TypedSymbols for equality.

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

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

Terms

data FPTrait Source #

Traits for IEEE floating point numbers.

Constructors

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

Instances

Instances details

Binary FPTrait Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

put :: FPTrait -> Put #

get :: Get FPTrait #

putList :: [FPTrait] -> Put #

Serial FPTrait Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

serialize :: MonadPut m => FPTrait -> m () #

deserialize :: MonadGet m => m FPTrait #

Serialize FPTrait Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

put :: Putter FPTrait #

get :: Get FPTrait #

NFData FPTrait Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

rnf :: FPTrait -> () #

Generic FPTrait Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

type Rep FPTrait

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

type Rep FPTrait = D1 ('MetaData "FPTrait" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" '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)))))

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 #

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.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (((C1 ('MetaCons "FPIsNaN" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPIsPositive" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPIsNegative" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "FPIsPositiveInfinite" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPIsNegativeInfinite" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPIsInfinite" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "FPIsPositiveZero" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPIsNegativeZero" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPIsZero" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "FPIsNormal" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPIsSubnormal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPIsPoint" 'PrefixI 'False) (U1 :: Type -> Type)))))

data FPUnaryOp Source #

Unary floating point operations.

Constructors

FPAbs
FPNeg

Instances

Instances details

Binary FPUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

put :: FPUnaryOp -> Put #

get :: Get FPUnaryOp #

putList :: [FPUnaryOp] -> Put #

Serial FPUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

serialize :: MonadPut m => FPUnaryOp -> m () #

deserialize :: MonadGet m => m FPUnaryOp #

Serialize FPUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

put :: Putter FPUnaryOp #

get :: Get FPUnaryOp #

NFData FPUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

rnf :: FPUnaryOp -> () #

Generic FPUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

type Rep FPUnaryOp
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type Rep FPUnaryOp = D1 ('MetaData "FPUnaryOp" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "FPAbs" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPNeg" 'PrefixI 'False) (U1 :: 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 #

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

data FPBinaryOp Source #

Binary floating point operations.

Constructors

FPRem
FPMinimum
FPMinimumNumber
FPMaximum
FPMaximumNumber

Instances

Instances details

Binary FPBinaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

put :: FPBinaryOp -> Put #

get :: Get FPBinaryOp #

putList :: [FPBinaryOp] -> Put #

Serial FPBinaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

serialize :: MonadPut m => FPBinaryOp -> m () #

deserialize :: MonadGet m => m FPBinaryOp #

Serialize FPBinaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

put :: Putter FPBinaryOp #

get :: Get FPBinaryOp #

NFData FPBinaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

rnf :: FPBinaryOp -> () #

Generic FPBinaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

type Rep FPBinaryOp

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

type Rep FPBinaryOp = D1 ('MetaData "FPBinaryOp" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) ((C1 ('MetaCons "FPRem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPMinimum" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FPMinimumNumber" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPMaximum" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPMaximumNumber" 'PrefixI 'False) (U1 :: Type -> Type))))

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 #

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.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) ((C1 ('MetaCons "FPRem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPMinimum" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FPMinimumNumber" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPMaximum" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPMaximumNumber" 'PrefixI 'False) (U1 :: Type -> Type))))

data FPRoundingUnaryOp Source #

Unary floating point operations with rounding modes.

Constructors

FPSqrt
FPRoundToIntegral

Instances

Instances details

Binary FPRoundingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

put :: FPRoundingUnaryOp -> Put #

get :: Get FPRoundingUnaryOp #

putList :: [FPRoundingUnaryOp] -> Put #

Serial FPRoundingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

serialize :: MonadPut m => FPRoundingUnaryOp -> m () #

deserialize :: MonadGet m => m FPRoundingUnaryOp #

Serialize FPRoundingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

put :: Putter FPRoundingUnaryOp #

get :: Get FPRoundingUnaryOp #

NFData FPRoundingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

rnf :: FPRoundingUnaryOp -> () #

Generic FPRoundingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

type Rep FPRoundingUnaryOp
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type Rep FPRoundingUnaryOp = D1 ('MetaData "FPRoundingUnaryOp" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "FPSqrt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPRoundToIntegral" 'PrefixI 'False) (U1 :: 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 #

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

data FPRoundingBinaryOp Source #

Binary floating point operations with rounding modes.

Constructors

FPAdd
FPSub
FPMul
FPDiv

Instances

Instances details

Binary FPRoundingBinaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

put :: FPRoundingBinaryOp -> Put #

get :: Get FPRoundingBinaryOp #

putList :: [FPRoundingBinaryOp] -> Put #

Serial FPRoundingBinaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

serialize :: MonadPut m => FPRoundingBinaryOp -> m () #

deserialize :: MonadGet m => m FPRoundingBinaryOp #

Serialize FPRoundingBinaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

put :: Putter FPRoundingBinaryOp #

get :: Get FPRoundingBinaryOp #

NFData FPRoundingBinaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

rnf :: FPRoundingBinaryOp -> () #

Generic FPRoundingBinaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

type Rep FPRoundingBinaryOp

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

type Rep FPRoundingBinaryOp = D1 ('MetaData "FPRoundingBinaryOp" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" '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)))

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 #

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.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) ((C1 ('MetaCons "FPAdd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPSub" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FPMul" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPDiv" 'PrefixI 'False) (U1 :: Type -> Type)))

data FloatingUnaryOp Source #

Unary floating point operations.

Constructors

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

Instances

Instances details

Binary FloatingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

put :: FloatingUnaryOp -> Put #

get :: Get FloatingUnaryOp #

putList :: [FloatingUnaryOp] -> Put #

Serial FloatingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

serialize :: MonadPut m => FloatingUnaryOp -> m () #

deserialize :: MonadGet m => m FloatingUnaryOp #

Serialize FloatingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

put :: Putter FloatingUnaryOp #

get :: Get FloatingUnaryOp #

NFData FloatingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

rnf :: FloatingUnaryOp -> () #

Generic FloatingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

type Rep FloatingUnaryOp

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

type Rep FloatingUnaryOp = D1 ('MetaData "FloatingUnaryOp" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (((C1 ('MetaCons "FloatingExp" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FloatingLog" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingSqrt" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FloatingSin" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingCos" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FloatingTan" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingAsin" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "FloatingAcos" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingAtan" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FloatingSinh" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingCosh" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FloatingTanh" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingAsinh" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FloatingAcosh" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingAtanh" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: FloatingUnaryOp -> Rep FloatingUnaryOp x #

to :: Rep FloatingUnaryOp x -> FloatingUnaryOp #

Show FloatingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

showsPrec :: Int -> FloatingUnaryOp -> ShowS #

show :: FloatingUnaryOp -> String #

showList :: [FloatingUnaryOp] -> ShowS #

Eq FloatingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

(==) :: FloatingUnaryOp -> FloatingUnaryOp -> Bool #

(/=) :: FloatingUnaryOp -> FloatingUnaryOp -> Bool #

Ord FloatingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

compare :: FloatingUnaryOp -> FloatingUnaryOp -> Ordering #

(<) :: FloatingUnaryOp -> FloatingUnaryOp -> Bool #

(<=) :: FloatingUnaryOp -> FloatingUnaryOp -> Bool #

(>) :: FloatingUnaryOp -> FloatingUnaryOp -> Bool #

(>=) :: FloatingUnaryOp -> FloatingUnaryOp -> Bool #

max :: FloatingUnaryOp -> FloatingUnaryOp -> FloatingUnaryOp #

min :: FloatingUnaryOp -> FloatingUnaryOp -> FloatingUnaryOp #

Hashable FloatingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

hashWithSalt :: Int -> FloatingUnaryOp -> Int #

hash :: FloatingUnaryOp -> Int #

Lift FloatingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

lift :: Quote m => FloatingUnaryOp -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => FloatingUnaryOp -> Code m FloatingUnaryOp #

type Rep FloatingUnaryOp Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

type Rep FloatingUnaryOp = D1 ('MetaData "FloatingUnaryOp" "Grisette.Internal.SymPrim.Prim.Internal.Term" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (((C1 ('MetaCons "FloatingExp" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FloatingLog" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingSqrt" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FloatingSin" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingCos" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FloatingTan" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingAsin" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "FloatingAcos" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingAtan" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FloatingSinh" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingCosh" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FloatingTanh" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingAsinh" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FloatingAcosh" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FloatingAtanh" 'PrefixI 'False) (U1 :: Type -> Type)))))

data Term t where Source #

Internal representation for Grisette symbolic terms.

Constructors

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

Instances

Instances details

Lift (Term t :: Type) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

lift :: Quote m => Term t -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => Term t -> Code m (Term t) #

SupportedPrim a => Binary (Term a) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: Term a -> Put #

get :: Get (Term a) #

putList :: [Term a] -> Put #

SupportedPrim a => Serial (Term a) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

serialize :: MonadPut m => Term a -> m () #

deserialize :: MonadGet m => m (Term a) #

SupportedPrim a => Serialize (Term a) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize

Methods

put :: Putter (Term a) #

get :: Get (Term a) #

NFData (Term a) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

rnf :: Term a -> () #

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 #

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 => 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 #

PPrint (Term t) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: Term t -> Doc ann Source #

pformatPrec :: Int -> Term t -> Doc ann Source #

pformatList :: [Term t] -> Doc ann Source #

Interned (Term t) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

data Description (Term t)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term data Description (Term t) where DConTerm :: forall t. (t -> t -> Bool) -> !Digest -> t -> Description (Term t) DSymTerm :: forall t. !Digest -> TypedSymbol 'AnyKind t -> Description (Term t) DForallTerm :: forall t1. !Digest -> !(TypedSymbol 'ConstantKind t1) -> !HashId -> Description (Term Bool) DExistsTerm :: forall t1. !Digest -> !(TypedSymbol 'ConstantKind t1) -> !HashId -> Description (Term Bool) DNotTerm :: !Digest -> !HashId -> Description (Term Bool) DOrTerm :: !Digest -> !HashId -> !HashId -> Description (Term Bool) DAndTerm :: !Digest -> !HashId -> !HashId -> Description (Term Bool) DEqTerm :: !Digest -> Fingerprint -> !HashId -> !HashId -> Description (Term Bool) DDistinctTerm :: !Digest -> Fingerprint -> !(NonEmpty HashId) -> Description (Term Bool) DITETerm :: forall t. !Digest -> !HashId -> !HashId -> !HashId -> Description (Term t) DAddNumTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DNegNumTerm :: forall t. !Digest -> !HashId -> Description (Term t) DMulNumTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DAbsNumTerm :: forall t. !Digest -> !HashId -> Description (Term t) DSignumNumTerm :: forall t. !Digest -> !HashId -> Description (Term t) DLtOrdTerm :: !Digest -> !Fingerprint -> !HashId -> !HashId -> Description (Term Bool) DLeOrdTerm :: !Digest -> !Fingerprint -> !HashId -> !HashId -> Description (Term Bool) DAndBitsTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DOrBitsTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DXorBitsTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DComplementBitsTerm :: forall t. !Digest -> !HashId -> Description (Term t) DShiftLeftTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DShiftRightTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DRotateLeftTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DRotateRightTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DBVConcatTerm :: forall t. !Digest -> !TypeHashId -> !TypeHashId -> Description (Term t) DBitCastTerm :: forall t. !Digest -> !TypeHashId -> Description (Term t) DBitCastOrTerm :: forall t. !Digest -> !HashId -> !TypeHashId -> Description (Term t) DBVSelectTerm :: forall (bv :: Nat -> Type) (w :: Nat). !Digest -> !Fingerprint -> !TypeHashId -> Description (Term (bv w)) DBVExtendTerm :: forall (bv :: Nat -> Type) (r :: Nat). !Digest -> !Bool -> !(Proxy r) -> !TypeHashId -> Description (Term (bv r)) DApplyTerm :: forall t. !Digest -> !TypeHashId -> !TypeHashId -> Description (Term t) DDivIntegralTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DModIntegralTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DQuotIntegralTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DRemIntegralTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DFPTraitTerm :: !Digest -> FPTrait -> !TypeHashId -> Description (Term Bool) DFdivTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DRecipTerm :: forall t. !Digest -> !HashId -> Description (Term t) DFloatingUnaryTerm :: forall t. !Digest -> FloatingUnaryOp -> !HashId -> Description (Term t) DPowerTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t) DFPUnaryTerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> FPUnaryOp -> !HashId -> Description (Term (fp eb sb)) DFPBinaryTerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> FPBinaryOp -> !HashId -> !HashId -> Description (Term (fp eb sb)) DFPRoundingUnaryTerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> FPRoundingUnaryOp -> !HashId -> !HashId -> Description (Term (fp eb sb)) DFPRoundingBinaryTerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> FPRoundingBinaryOp -> !HashId -> !HashId -> !HashId -> Description (Term (fp eb sb)) DFPFMATerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> !HashId -> !HashId -> !HashId -> !HashId -> Description (Term (fp eb sb)) DFromIntegralTerm :: forall t. !Digest -> !TypeHashId -> Description (Term t) DFromFPOrTerm :: forall t. !Digest -> !HashId -> !HashId -> !TypeHashId -> Description (Term t) DToFPTerm :: forall (eb :: Nat) (sb :: Nat). !Digest -> !HashId -> !TypeHashId -> Description (Term (FP eb sb))
type Uninterned (Term t)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type Uninterned (Term t) = UTerm t

Methods

describe :: Uninterned (Term t) -> Description (Term t) Source #

identify :: CachedInfo -> Uninterned (Term t) -> Term t Source #

threadId :: Term t -> WeakThreadId Source #

descriptionDigest :: Description (Term t) -> Digest Source #

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 => Hashable (Term t) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Methods

hashWithSalt :: Int -> Term t -> Int #

hash :: Term t -> Int #

data Description (Term t) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

data Description (Term t) where

DConTerm :: forall t. (t -> t -> Bool) -> !Digest -> t -> Description (Term t)
DSymTerm :: forall t. !Digest -> TypedSymbol 'AnyKind t -> Description (Term t)
DForallTerm :: forall t1. !Digest -> !(TypedSymbol 'ConstantKind t1) -> !HashId -> Description (Term Bool)
DExistsTerm :: forall t1. !Digest -> !(TypedSymbol 'ConstantKind t1) -> !HashId -> Description (Term Bool)
DNotTerm :: !Digest -> !HashId -> Description (Term Bool)
DOrTerm :: !Digest -> !HashId -> !HashId -> Description (Term Bool)
DAndTerm :: !Digest -> !HashId -> !HashId -> Description (Term Bool)
DEqTerm :: !Digest -> Fingerprint -> !HashId -> !HashId -> Description (Term Bool)
DDistinctTerm :: !Digest -> Fingerprint -> !(NonEmpty HashId) -> Description (Term Bool)
DITETerm :: forall t. !Digest -> !HashId -> !HashId -> !HashId -> Description (Term t)
DAddNumTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DNegNumTerm :: forall t. !Digest -> !HashId -> Description (Term t)
DMulNumTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DAbsNumTerm :: forall t. !Digest -> !HashId -> Description (Term t)
DSignumNumTerm :: forall t. !Digest -> !HashId -> Description (Term t)
DLtOrdTerm :: !Digest -> !Fingerprint -> !HashId -> !HashId -> Description (Term Bool)
DLeOrdTerm :: !Digest -> !Fingerprint -> !HashId -> !HashId -> Description (Term Bool)
DAndBitsTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DOrBitsTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DXorBitsTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DComplementBitsTerm :: forall t. !Digest -> !HashId -> Description (Term t)
DShiftLeftTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DShiftRightTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DRotateLeftTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DRotateRightTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DBVConcatTerm :: forall t. !Digest -> !TypeHashId -> !TypeHashId -> Description (Term t)
DBitCastTerm :: forall t. !Digest -> !TypeHashId -> Description (Term t)
DBitCastOrTerm :: forall t. !Digest -> !HashId -> !TypeHashId -> Description (Term t)
DBVSelectTerm :: forall (bv :: Nat -> Type) (w :: Nat). !Digest -> !Fingerprint -> !TypeHashId -> Description (Term (bv w))
DBVExtendTerm :: forall (bv :: Nat -> Type) (r :: Nat). !Digest -> !Bool -> !(Proxy r) -> !TypeHashId -> Description (Term (bv r))
DApplyTerm :: forall t. !Digest -> !TypeHashId -> !TypeHashId -> Description (Term t)
DDivIntegralTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DModIntegralTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DQuotIntegralTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DRemIntegralTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DFPTraitTerm :: !Digest -> FPTrait -> !TypeHashId -> Description (Term Bool)
DFdivTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DRecipTerm :: forall t. !Digest -> !HashId -> Description (Term t)
DFloatingUnaryTerm :: forall t. !Digest -> FloatingUnaryOp -> !HashId -> Description (Term t)
DPowerTerm :: forall t. !Digest -> !HashId -> !HashId -> Description (Term t)
DFPUnaryTerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> FPUnaryOp -> !HashId -> Description (Term (fp eb sb))
DFPBinaryTerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> FPBinaryOp -> !HashId -> !HashId -> Description (Term (fp eb sb))
DFPRoundingUnaryTerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> FPRoundingUnaryOp -> !HashId -> !HashId -> Description (Term (fp eb sb))
DFPRoundingBinaryTerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> FPRoundingBinaryOp -> !HashId -> !HashId -> !HashId -> Description (Term (fp eb sb))
DFPFMATerm :: forall (fp :: Nat -> Nat -> Type) (eb :: Nat) (sb :: Nat). !Digest -> !HashId -> !HashId -> !HashId -> !HashId -> Description (Term (fp eb sb))
DFromIntegralTerm :: forall t. !Digest -> !TypeHashId -> Description (Term t)
DFromFPOrTerm :: forall t. !Digest -> !HashId -> !HashId -> !TypeHashId -> Description (Term t)
DToFPTerm :: forall (eb :: Nat) (sb :: Nat). !Digest -> !HashId -> !TypeHashId -> 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

defaultValueDynamic :: SupportedPrim t => proxy t -> ModelValue Source #

The default value in a dynamic ModelValue.

pattern DynTerm :: SupportedPrim a => Term a -> Term b Source #

Pattern for term with dynamic typing.

toCurThread :: Term t -> IO (Term t) Source #

Convert a term to the current thread.

data CachedInfo Source #

Information about a cached term.

Constructors

CachedInfo
Fields cachedThreadId :: !WeakThreadId cachedDigest :: !Digest cachedId :: !Id cachedStableIdent :: !StableIdent

Instances

Instances details

NFData CachedInfo Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: CachedInfo -> () #

termInfo :: Term t -> CachedInfo Source #

Get the cached information for a term.

termThreadId :: Term t -> WeakThreadId Source #

Get the thread ID for a term.

termDigest :: Term t -> Digest Source #

Get the digest for a term.

termId :: Term t -> Id Source #

Get the ID for a term.

termStableIdent :: Term t -> StableIdent Source #

Get the stable identifier for a term.

pformatTerm :: Term t -> String Source #

Pretty-print a term.

data ModelValue where Source #

A value with its type information.

Constructors

ModelValue :: forall v. SupportedPrim v => v -> ModelValue

Instances

Instances details

Binary ModelValue Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize Methods put :: ModelValue -> Put # get :: Get ModelValue # putList :: [ModelValue] -> Put #
Serial ModelValue Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize Methods serialize :: MonadPut m => ModelValue -> m () # deserialize :: MonadGet m => m ModelValue #
Serialize ModelValue Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Serialize Methods put :: Putter ModelValue # get :: Get ModelValue #
NFData ModelValue Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods rnf :: ModelValue -> () #
Show ModelValue Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods showsPrec :: Int -> ModelValue -> ShowS # show :: ModelValue -> String # showList :: [ModelValue] -> ShowS #
Eq ModelValue Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods (==) :: ModelValue -> ModelValue -> Bool # (/=) :: ModelValue -> ModelValue -> Bool #
PPrint ModelValue Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint Methods pformat :: ModelValue -> Doc ann Source # pformatPrec :: Int -> ModelValue -> Doc ann Source # pformatList :: [ModelValue] -> Doc ann Source #
Hashable ModelValue Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods hashWithSalt :: Int -> ModelValue -> Int # hash :: ModelValue -> Int #
Lift ModelValue Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Methods lift :: Quote m => ModelValue -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => ModelValue -> Code m ModelValue #

toModelValue :: SupportedPrim a => a -> ModelValue Source #

Convert to a model value.

unsafeFromModelValue :: Typeable a => ModelValue -> a Source #

Convert from a model value. Crashes if the types does not match.

Interning

data UTerm t where Source #

Term without identity (before internalizing).

Constructors

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

prettyPrintTerm :: Term t -> Doc ann Source #

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

Interned constructors

conTerm :: SupportedPrim t => t -> Term t Source #

Construct and internalizing a ConTerm.

symTerm :: forall (knd :: SymbolKind) t. TypedSymbol knd t -> Term t Source #

Construct and internalizing a SymTerm.

ssymTerm :: SupportedPrim t => Identifier -> Term t Source #

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

isymTerm :: SupportedPrim t => Identifier -> Int -> Term t Source #

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

forallTerm :: TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool Source #

Construct and internalizing a ForallTerm.

existsTerm :: TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool Source #

Construct and internalizing a ExistsTerm.

notTerm :: Term Bool -> Term Bool Source #

Construct and internalizing a NotTerm.

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

Construct and internalizing a OrTerm.

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

Construct and internalizing a AndTerm.

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

Construct and internalizing a EqTerm.

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

Construct and internalizing a DistinctTerm.

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

Construct and internalizing a ITETerm.

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

Construct and internalizing a AddNumTerm.

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

Construct and internalizing a NegNumTerm.

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

Construct and internalizing a MulNumTerm.

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

Construct and internalizing a AbsNumTerm.

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

Construct and internalizing a SignumNumTerm.

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

Construct and internalizing a LtOrdTerm.

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

Construct and internalizing a LeOrdTerm.

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

Construct and internalizing a AndBitsTerm.

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

Construct and internalizing a OrBitsTerm.

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

Construct and internalizing a XorBitsTerm.

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

Construct and internalizing a ComplementBitsTerm.

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

Construct and internalizing a ShiftLeftTerm.

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

Construct and internalizing a RotateLeftTerm.

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

Construct and internalizing a ShiftRightTerm.

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

Construct and internalizing a RotateRightTerm.

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

Construct and internalizing a BitCastTerm.

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

Construct and internalizing a BitCastOrTerm.

bvConcatTerm :: forall bv (l :: Nat) (r :: Nat). (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r), SupportedPrim (bv (l + r))) => Term (bv l) -> Term (bv r) -> Term (bv (l + r)) Source #

Construct and internalizing a BVConcatTerm.

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

Construct and internalizing a BVSelectTerm.

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

Construct and internalizing a BVExtendTerm.

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

Construct and internalizing a BVExtendTerm with sign extension.

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

Construct and internalizing a BVExtendTerm with zero extension.

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

Construct and internalizing a ApplyTerm.

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

Construct and internalizing a DivIntegralTerm.

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

Construct and internalizing a ModIntegralTerm.

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

Construct and internalizing a QuotIntegralTerm.

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

Construct and internalizing a RemIntegralTerm.

fpTraitTerm :: forall (eb :: Nat) (sb :: Nat) fp. (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPTrait -> Term (fp eb sb) -> Term Bool Source #

Construct and internalizing a FPTraitTerm.

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

Construct and internalizing a FdivTerm.

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

Construct and internalizing a RecipTerm.

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

Construct and internalizing a FloatingUnaryTerm.

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

Construct and internalizing a PowerTerm.

fpUnaryTerm :: forall (eb :: Nat) (sb :: Nat) fp. (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPUnaryOp -> Term (fp eb sb) -> Term (fp eb sb) Source #

Construct and internalizing a FPUnaryTerm.

fpBinaryTerm :: forall (eb :: Nat) (sb :: Nat) fp. (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPBinaryOp -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb) Source #

Construct and internalizing a FPBinaryTerm.

fpRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat) fp. (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) Source #

Construct and internalizing a FPRoundingUnaryTerm.

fpRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat) fp. (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb) Source #

Construct and internalizing a FPRoundingBinaryTerm.

fpFMATerm :: forall (eb :: Nat) (sb :: Nat) fp. (ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb) Source #

Construct and internalizing a FPFMATerm.

fromIntegralTerm :: (PEvalFromIntegralTerm a b, SupportedPrim b) => Term a -> Term b Source #

Construct and internalizing a FromIntegralTerm.

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

Construct and internalizing a FromFPOrTerm.

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

Construct and internalizing a ToFPTerm.

Patterns

pattern SupportedTerm :: () => SupportedPrim t => Term t Source #

Pattern synonym to introduce the SupportedPrim constraint.

pattern SupportedTypedSymbol :: () => (SupportedPrim t, SymbolKindConstraint k t, IsSymbolKind k) => TypedSymbol k t Source #

Pattern synonym to introduce constraints from a TypedSymbol.

pattern SupportedConstantTypedSymbol :: () => (SupportedPrim t, SymbolKindConstraint k t, IsSymbolKind k, k ~ 'ConstantKind) => TypedSymbol k t Source #

Pattern synonym to introduce constraints from a TypedSymbol. Also checks that the symbol kind is ConstantKind.

pattern ConTerm :: () => SupportedPrim t => t -> Term t Source #

Pattern synonym for ConTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern SymTerm :: () => SupportedPrim t => TypedSymbol 'AnyKind t -> Term t Source #

Pattern synonym for SymTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern ForallTerm :: forall r t. () => (r ~ Bool, SupportedNonFuncPrim t) => TypedSymbol 'ConstantKind t -> Term Bool -> Term r Source #

Pattern synonym for ForallTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern ExistsTerm :: forall r t. () => (r ~ Bool, SupportedNonFuncPrim t) => TypedSymbol 'ConstantKind t -> Term Bool -> Term r Source #

Pattern synonym for ExistsTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern NotTerm :: () => r ~ Bool => Term Bool -> Term r Source #

Pattern synonym for NotTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern OrTerm :: () => r ~ Bool => Term Bool -> Term Bool -> Term r Source #

Pattern synonym for OrTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern AndTerm :: () => r ~ Bool => Term Bool -> Term Bool -> Term r Source #

Pattern synonym for AndTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern EqTerm :: forall r t. () => (r ~ Bool, SupportedPrim t) => Term t -> Term t -> Term r Source #

Pattern synonym for EqTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern DistinctTerm :: forall r t. () => (r ~ Bool, SupportedPrim t) => NonEmpty (Term t) -> Term r Source #

Pattern synonym for DistinctTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern ITETerm :: () => SupportedPrim t => Term Bool -> Term t -> Term t -> Term t Source #

Pattern synonym for ITETerm'. Note that using this pattern to construct a Term will do term simplification.

pattern AddNumTerm :: () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for AddNumTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern NegNumTerm :: () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t Source #

Pattern synonym for NegNumTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern MulNumTerm :: () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for MulNumTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern AbsNumTerm :: () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t Source #

Pattern synonym for AbsNumTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern SignumNumTerm :: () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t Source #

Pattern synonym for SignumNumTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern LtOrdTerm :: forall r t. () => (r ~ Bool, SupportedPrim t, PEvalOrdTerm t) => Term t -> Term t -> Term r Source #

Pattern synonym for LtOrdTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern LeOrdTerm :: forall r t. () => (r ~ Bool, SupportedPrim t, PEvalOrdTerm t) => Term t -> Term t -> Term r Source #

Pattern synonym for LeOrdTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern AndBitsTerm :: () => (SupportedPrim t, PEvalBitwiseTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for AndBitsTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern OrBitsTerm :: () => (SupportedPrim t, PEvalBitwiseTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for OrBitsTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern XorBitsTerm :: () => (SupportedPrim t, PEvalBitwiseTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for XorBitsTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern ComplementBitsTerm :: () => (SupportedPrim t, PEvalBitwiseTerm t) => Term t -> Term t Source #

Pattern synonym for ComplementBitsTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern ShiftLeftTerm :: () => (SupportedPrim t, PEvalShiftTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for ShiftLeftTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern RotateLeftTerm :: () => (SupportedPrim t, PEvalRotateTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for RotateLeftTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern ShiftRightTerm :: () => (SupportedPrim t, PEvalShiftTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for ShiftRightTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern RotateRightTerm :: () => (SupportedPrim t, PEvalRotateTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for RotateRightTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern BitCastTerm :: forall b a. () => (SupportedPrim a, SupportedPrim b, PEvalBitCastTerm a b) => Term a -> Term b Source #

Pattern synonym for BitCastTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern BitCastOrTerm :: () => (SupportedPrim a, SupportedPrim b, PEvalBitCastOrTerm a b) => Term b -> Term a -> Term b Source #

Pattern synonym for BitCastOrTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern BVConcatTerm :: forall ret bv (l :: Nat) (r :: Nat). () => (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r), SupportedPrim (bv l), SupportedPrim (bv r), SupportedPrim (bv (l + r)), ret ~ bv (l + r)) => Term (bv l) -> Term (bv r) -> Term ret Source #

Pattern synonym for BVConcatTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern BVSelectTerm :: forall ret bv (w :: Nat) (n :: Nat) (ix :: Nat). () => (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n, SupportedPrim (bv n), SupportedPrim (bv w), ret ~ bv w) => Proxy ix -> Proxy w -> Term (bv n) -> Term ret Source #

Pattern synonym for BVSelectTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern BVExtendTerm :: forall ret bv (l :: Nat) (r :: Nat). () => (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r, SupportedPrim (bv l), SupportedPrim (bv r), ret ~ bv r) => Bool -> Proxy r -> Term (bv l) -> Term ret Source #

Pattern synonym for BVExtendTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern ApplyTerm :: forall b f a. () => (PEvalApplyTerm f a b, SupportedPrim f, SupportedPrim a, SupportedPrim b) => Term f -> Term a -> Term b Source #

Pattern synonym for ApplyTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern DivIntegralTerm :: () => (SupportedPrim t, PEvalDivModIntegralTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for DivIntegralTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern ModIntegralTerm :: () => (SupportedPrim t, PEvalDivModIntegralTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for ModIntegralTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern QuotIntegralTerm :: () => (SupportedPrim t, PEvalDivModIntegralTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for QuotIntegralTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern RemIntegralTerm :: () => (SupportedPrim t, PEvalDivModIntegralTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for RemIntegralTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern FPTraitTerm :: forall r (eb :: Nat) (sb :: Nat) fp. () => (r ~ Bool, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPTrait -> Term (fp eb sb) -> Term r Source #

Pattern synonym for FPTraitTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern FdivTerm :: () => (SupportedPrim t, PEvalFractionalTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for FdivTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern RecipTerm :: () => (SupportedPrim t, PEvalFractionalTerm t) => Term t -> Term t Source #

Pattern synonym for RecipTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern FloatingUnaryTerm :: () => (SupportedPrim t, PEvalFloatingTerm t) => FloatingUnaryOp -> Term t -> Term t Source #

Pattern synonym for FloatingUnaryTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern PowerTerm :: () => (SupportedPrim t, PEvalFloatingTerm t) => Term t -> Term t -> Term t Source #

Pattern synonym for PowerTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern FPUnaryTerm :: forall ret fp (eb :: Nat) (sb :: Nat). () => (ret ~ fp eb sb, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPUnaryOp -> Term (fp eb sb) -> Term ret Source #

Pattern synonym for FPUnaryTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern FPBinaryTerm :: forall ret fp (eb :: Nat) (sb :: Nat). () => (ret ~ fp eb sb, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPBinaryOp -> Term (fp eb sb) -> Term (fp eb sb) -> Term ret Source #

Pattern synonym for FPBinaryTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern FPRoundingUnaryTerm :: forall ret fp (eb :: Nat) (sb :: Nat). () => (ret ~ fp eb sb, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (fp eb sb) -> Term ret Source #

Pattern synonym for FPRoundingUnaryTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern FPRoundingBinaryTerm :: forall ret fp (eb :: Nat) (sb :: Nat). () => (ret ~ fp eb sb, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) -> Term ret Source #

Pattern synonym for FPRoundingBinaryTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern FPFMATerm :: forall ret fp (eb :: Nat) (sb :: Nat). () => (ret ~ fp eb sb, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => Term FPRoundingMode -> Term (fp eb sb) -> Term (fp eb sb) -> Term (fp eb sb) -> Term ret Source #

Pattern synonym for FPFMATerm'. Note that using this pattern to construct a Term will do term simplification.

pattern FromIntegralTerm :: forall b a. () => (PEvalFromIntegralTerm a b, SupportedPrim a, SupportedPrim b) => Term a -> Term b Source #

Pattern synonym for FromIntegralTerm'. Note that using this pattern to construct a Term will do term simplification.

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

Pattern synonym for FromFPOrTerm'. Note that using this pattern to construct a Term will do term simplification.

pattern ToFPTerm :: forall ret (eb :: Nat) (sb :: Nat) a. () => (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim (FP eb sb), SupportedPrim a, ret ~ FP eb sb) => Term FPRoundingMode -> Term a -> Proxy eb -> Proxy sb -> Term ret Source #

Pattern synonym for ToFPTerm'. Note that using this pattern to construct a Term will do term simplification.

Support for boolean type

trueTerm :: Term Bool Source #

Construct and internalizing True term.

falseTerm :: Term Bool Source #

Construct and internalizing False term.

pattern BoolConTerm :: Bool -> Term a Source #

Pattern matcher for concrete Bool terms.

pattern TrueTerm :: Term a Source #

Pattern matcher for True term.

pattern FalseTerm :: Term a Source #

Pattern matcher for False term.

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

Pattern matcher for Bool terms.

pevalNotTerm :: Term Bool -> Term Bool Source #

Partial evaluation for not terms.

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

Partial evaluation for or terms.

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

Partial evaluation for and terms.

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

Partial evaluation for imply terms.

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

Partial evaluation for xor terms.

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

Basic partial evaluation for ITE terms.

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

Basic partial evaluation for ITE terms.

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

Default partial evaluation for equality terms.

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

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

class (SupportedPrim a, Ord a, Eq a, Show a, Hashable a, Typeable a) => NonFuncSBVRep a Source #

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

Associated Types

type NonFuncSBVBaseType a Source #

Instances

Instances details

NonFuncSBVRep AlgReal Source #

Instance details

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

Associated Types

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

NonFuncSBVRep FPRoundingMode Source #

Instance details

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

Associated Types

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

NonFuncSBVRep Integer Source #

Instance details

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

Associated Types

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

NonFuncSBVRep Bool Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

type NonFuncSBVBaseType Bool
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type NonFuncSBVBaseType Bool = Bool

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

Instance details

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

Associated Types

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

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

Instance details

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

Associated Types

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

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

Instance details

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

Associated Types

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

class NonFuncSBVRep a => SupportedNonFuncPrim a where Source #

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

Methods

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

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

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

Instances

Instances details

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

class SBVRep t Source #

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

Associated Types

type SBVType t Source #

Instances

Instances details

SBVRep AlgReal Source #

Instance details

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

Associated Types

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

SBVRep FPRoundingMode Source #

Instance details

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

Associated Types

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

SBVRep Integer Source #

Instance details

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

Associated Types

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

SBVRep Bool Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Term

Associated Types

type SBVType Bool
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type SBVType Bool = SBV Bool

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

Instance details

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

Associated Types

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

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

Instance details

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

Associated Types

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

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

Instance details

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

Associated Types

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

(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a --> b) Source #

Instance details

Defined in Grisette.Internal.SymPrim.GeneralFun

Associated Types

type SBVType (a --> b)
Instance details Defined in Grisette.Internal.SymPrim.GeneralFun type SBVType (a --> b) = SBV (NonFuncSBVBaseType a) -> SBVType b

(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a =-> b) Source #

Instance details

Defined in Grisette.Internal.SymPrim.TabularFun

Associated Types

type SBVType (a =-> b)
Instance details Defined in Grisette.Internal.SymPrim.TabularFun type SBVType (a =-> b) = SBV (NonFuncSBVBaseType a) -> SBVType b

class MonadIO m => SBVFreshMonad (m :: Type -> Type) where Source #

Monads that supports generating sbv fresh variables.

Methods

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

Instances

Instances details

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

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

Error message for unsupported types.

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

Error message for failure to parse the SBV model result.

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

Partition the list of CVs for models for functions.

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

Parse the scalar model result.

Orphan instances

NFData CachedInfo Source #
Instance details Methods rnf :: CachedInfo -> () #