| Copyright | (c) Sirui Lu 2021-2024 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Grisette.SymPrim
Description
Synopsis
- data IntN (n :: Nat)
- type IntN8 = IntN 8
- type IntN16 = IntN 16
- type IntN32 = IntN 32
- type IntN64 = IntN 64
- data WordN (n :: Nat)
- type WordN8 = WordN 8
- type WordN16 = WordN 16
- type WordN32 = WordN 32
- type WordN64 = WordN 64
- data SomeBV bv where
- data SomeBVException
- pattern SomeIntN :: () => (KnownNat n, 1 <= n) => IntN n -> SomeIntN
- type SomeIntN = SomeBV IntN
- pattern SomeWordN :: () => (KnownNat n, 1 <= n) => WordN n -> SomeWordN
- type SomeWordN = SomeBV WordN
- conBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv
- conBVView :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV bv -> Maybe (SomeBV cbv)
- pattern ConBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv
- symBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Symbol -> SomeBV bv
- ssymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> SomeBV bv
- isymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> Int -> SomeBV bv
- arbitraryBV :: forall bv. (forall n. (KnownNat n, 1 <= n) => Arbitrary (bv n)) => Int -> Gen (SomeBV bv)
- unsafeSomeBV :: forall bv. Int -> (forall proxy n. (KnownNat n, 1 <= n) => proxy n -> bv n) -> SomeBV bv
- unarySomeBV :: forall bv r. (forall n. (KnownNat n, 1 <= n) => bv n -> r) -> (SomeBVLit -> r) -> SomeBV bv -> r
- unarySomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n) -> (SomeBVLit -> SomeBVLit) -> SomeBV bv -> SomeBV bv
- binSomeBV :: (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> (SomeBVLit -> SomeBVLit -> r) -> SomeBV bv -> SomeBV bv -> r
- binSomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> (SomeBVLit -> SomeBVLit -> SomeBVLit) -> SomeBV bv -> SomeBV bv -> SomeBV bv
- binSomeBVR2 :: (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> (SomeBVLit -> SomeBVLit -> (SomeBVLit, SomeBVLit)) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
- binSomeBVSafe :: (MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, Mergeable r, forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) -> (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m r) -> SomeBV bv -> SomeBV bv -> m r
- binSomeBVSafeR1 :: (MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n), forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m SomeBVLit) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
- binSomeBVSafeR2 :: (MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n), forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m (SomeBVLit, SomeBVLit)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
- type ValidFP (eb :: Nat) (sb :: Nat) = ValidFloat eb sb
- data FP (eb :: Nat) (sb :: Nat)
- type FP16 = FP 5 11
- type FP32 = FP 8 24
- type FP64 = FP 11 53
- withValidFPProofs :: forall eb sb r. ValidFP eb sb => ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb), 1 <= eb, 1 <= sb) => r) -> r
- data FPRoundingMode
- allFPRoundingMode :: [FPRoundingMode]
- data AlgReal where
- AlgExactRational :: Rational -> AlgReal
- AlgInexactRational :: Rational -> AlgReal
- AlgPolyRoot :: Integer -> AlgRealPoly -> Maybe String -> AlgReal
- AlgInterval :: RealPoint -> RealPoint -> AlgReal
- newtype AlgRealPoly = AlgRealPoly [(Integer, Integer)]
- data RealPoint
- data UnsupportedAlgRealOperation = UnsupportedAlgRealOperation {}
- data a =-> b = TabularFun {
- funcTable :: [(a, b)]
- defaultFuncValue :: b
- data a --> b
- (-->) :: (SupportedNonFuncPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedConstantSymbol ca -> sb -> ca --> cb
- newtype SymBool = SymBool (Term Bool)
- newtype SymInteger = SymInteger (Term Integer)
- newtype SymWordN (n :: Nat) = SymWordN (Term (WordN n))
- type SymWordN8 = SymWordN 8
- type SymWordN16 = SymWordN 16
- type SymWordN32 = SymWordN 32
- type SymWordN64 = SymWordN 64
- newtype SymIntN (n :: Nat) = SymIntN (Term (IntN n))
- type SymIntN8 = SymIntN 8
- type SymIntN16 = SymIntN 16
- type SymIntN32 = SymIntN 32
- type SymIntN64 = SymIntN 64
- type SomeSymIntN = SomeBV SymIntN
- type SomeSymWordN = SomeBV SymWordN
- pattern SomeSymIntN :: () => (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN
- pattern SomeSymWordN :: () => (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN
- newtype SymFP eb sb = SymFP (Term (FP eb sb))
- newtype SymFPRoundingMode = SymFPRoundingMode (Term FPRoundingMode)
- type SymFP16 = SymFP 5 11
- type SymFP32 = SymFP 8 24
- type SymFP64 = SymFP 11 53
- newtype SymAlgReal = SymAlgReal (Term AlgReal)
- data sa =~> sb where
- SymTabularFun :: (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb), SupportedNonFuncPrim ca) => Term (ca =-> cb) -> sa =~> sb
- data sa -~> sb where
- SymGeneralFun :: (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => Term (ca --> cb) -> sa -~> sb
- type Prim a = (Show a, Binary a, Serial a, Serialize a, NFData a, Eq a, EvalSym a, ExtractSym a, Mergeable a, PPrint a, SubstSym a, SymEq a, SymOrd a, AllSyms a, Hashable a, Lift a, Typeable a)
- type SymPrim a = (Prim a, ITEOp a, GenSymSimple a a)
- type BasicSymPrim a = (SymPrim a, SimpleMergeable a, GenSymSimple () a, Solvable (ConType a) a, ConRep a, LinkedRep (ConType a) a, ToCon a (ConType a), ToSym (ConType a) a, Apply a, a ~ FunType a, SupportedNonFuncPrim (ConType a))
- forallSet :: ConstantSymbolSet -> SymBool -> SymBool
- forallSym :: (HasCallStack, ExtractSym a) => a -> SymBool -> SymBool
- forallFresh :: (HasCallStack, ExtractSym v, MonadFresh m, GenSym spec v, TryMerge m) => spec -> (v -> FreshT Union SymBool) -> m SymBool
- existsSet :: ConstantSymbolSet -> SymBool -> SymBool
- existsSym :: (HasCallStack, ExtractSym a) => a -> SymBool -> SymBool
- existsFresh :: (HasCallStack, ExtractSym v, MonadFresh m, GenSym spec v, TryMerge m) => spec -> (v -> FreshT Union SymBool) -> m SymBool
- class (Lift t, NFData t, Typeable t, SupportedPrimConstraint t, SBVRep t) => SupportedPrim t
- class SupportedPrim con => SymRep con where
- type SymType con
- class ConRep sym where
- type ConType sym
- class (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) => LinkedRep con sym | con -> sym, sym -> con where
- underlyingTerm :: sym -> Term con
- wrapTerm :: Term con -> sym
- data SomeSym where
- class AllSyms a where
- class (forall a. AllSyms a => AllSyms (f a)) => AllSyms1 f where
- liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym]
- allSymsS1 :: (AllSyms1 f, AllSyms a) => f a -> [SomeSym] -> [SomeSym]
- class (forall a. AllSyms a => AllSyms1 (f a)) => AllSyms2 f where
- allSymsS2 :: (AllSyms2 f, AllSyms a, AllSyms b) => f a b -> [SomeSym] -> [SomeSym]
- allSymsSize :: AllSyms a => a -> Int
- symSize :: forall con sym. LinkedRep con sym => sym -> Int
- symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int
- data family AllSymsArgs arity a :: Type
- class GAllSyms arity f where
- gallSymsS :: AllSymsArgs arity a -> f a -> [SomeSym] -> [SomeSym]
- genericAllSymsS :: (Generic a, GAllSyms Arity0 (Rep a)) => a -> [SomeSym] -> [SomeSym]
- genericLiftAllSymsS :: (Generic1 f, GAllSyms Arity1 (Rep1 f)) => (a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym]
- data SymbolKind
- class IsSymbolKind (knd :: SymbolKind) where
- type SymbolKindConstraint knd :: Type -> Constraint
- decideSymbolKind :: Either (knd :~~: 'ConstantKind) (knd :~~: 'AnyKind)
- withSymbolKindConstraint :: TypedSymbol knd t -> (SymbolKindConstraint knd t => a) -> a
- data TypedSymbol (knd :: SymbolKind) t where
- TypedSymbol :: (SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) => {..} -> TypedSymbol knd t
- typedAnySymbol :: forall t. SupportedPrim t => Symbol -> TypedSymbol 'AnyKind t
- type TypedAnySymbol = TypedSymbol 'AnyKind
- typedConstantSymbol :: forall t. SupportedNonFuncPrim t => Symbol -> TypedSymbol 'ConstantKind t
- type TypedConstantSymbol = TypedSymbol 'ConstantKind
- data SomeTypedSymbol knd where
- SomeTypedSymbol :: forall knd t. TypedSymbol knd t -> SomeTypedSymbol knd
- type SomeTypedAnySymbol = SomeTypedSymbol 'AnyKind
- type SomeTypedConstantSymbol = SomeTypedSymbol 'ConstantKind
- data SymbolSet knd
- type AnySymbolSet = SymbolSet 'AnyKind
- type ConstantSymbolSet = SymbolSet 'ConstantKind
- data Model
- data ModelValuePair t = (TypedAnySymbol t) ::= t
- data ModelSymPair ct st where
- (:=) :: LinkedRep ct st => st -> ct -> ModelSymPair ct st
- data Term t
- data SomeTerm where
- SomeTerm :: forall a. SupportedPrim a => Term a -> SomeTerm
- termSize :: Term a -> Int
- someTermSize :: SomeTerm -> Int
- termsSize :: [Term a] -> Int
- someTermsSize :: [SomeTerm] -> Int
- pattern SupportedTerm :: forall t. () => SupportedPrim t => Term t
- pattern SupportedTypedSymbol :: forall (k :: SymbolKind) t. () => (SupportedPrim t, SymbolKindConstraint k t, IsSymbolKind k) => TypedSymbol k t
- pattern SupportedConstantTypedSymbol :: forall k t. () => (SupportedPrim t, SymbolKindConstraint k t, IsSymbolKind k, k ~ 'ConstantKind) => TypedSymbol k t
- pattern ConTerm :: forall t. () => SupportedPrim t => t -> Term t
- pattern SymTerm :: forall t. () => SupportedPrim t => TypedSymbol 'AnyKind t -> Term t
- pattern ForallTerm :: forall r. () => forall t. (r ~ Bool, SupportedNonFuncPrim t) => TypedSymbol 'ConstantKind t -> Term Bool -> Term r
- pattern ExistsTerm :: forall r. () => forall t. (r ~ Bool, SupportedNonFuncPrim t) => TypedSymbol 'ConstantKind t -> Term Bool -> Term r
- pattern NotTerm :: forall r. () => r ~ Bool => Term Bool -> Term r
- pattern OrTerm :: forall r. () => r ~ Bool => Term Bool -> Term Bool -> Term r
- pattern AndTerm :: forall r. () => r ~ Bool => Term Bool -> Term Bool -> Term r
- pattern EqTerm :: forall r. () => forall t. (r ~ Bool, SupportedPrim t) => Term t -> Term t -> Term r
- pattern DistinctTerm :: forall r. () => forall t. (r ~ Bool, SupportedPrim t) => NonEmpty (Term t) -> Term r
- pattern ITETerm :: forall t. () => SupportedPrim t => Term Bool -> Term t -> Term t -> Term t
- pattern AddNumTerm :: forall t. () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t -> Term t
- pattern NegNumTerm :: forall t. () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t
- pattern MulNumTerm :: forall t. () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t -> Term t
- pattern AbsNumTerm :: forall t. () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t
- pattern SignumNumTerm :: forall t. () => (SupportedPrim t, PEvalNumTerm t) => Term t -> Term t
- pattern LtOrdTerm :: forall r. () => forall t. (r ~ Bool, SupportedPrim t, PEvalOrdTerm t) => Term t -> Term t -> Term r
- pattern LeOrdTerm :: forall r. () => forall t. (r ~ Bool, SupportedPrim t, PEvalOrdTerm t) => Term t -> Term t -> Term r
- pattern AndBitsTerm :: forall t. () => (SupportedPrim t, PEvalBitwiseTerm t) => Term t -> Term t -> Term t
- pattern OrBitsTerm :: forall t. () => (SupportedPrim t, PEvalBitwiseTerm t) => Term t -> Term t -> Term t
- pattern XorBitsTerm :: forall t. () => (SupportedPrim t, PEvalBitwiseTerm t) => Term t -> Term t -> Term t
- pattern ComplementBitsTerm :: forall t. () => (SupportedPrim t, PEvalBitwiseTerm t) => Term t -> Term t
- pattern ShiftLeftTerm :: forall t. () => (SupportedPrim t, PEvalShiftTerm t) => Term t -> Term t -> Term t
- pattern RotateLeftTerm :: forall t. () => (SupportedPrim t, PEvalRotateTerm t) => Term t -> Term t -> Term t
- pattern ShiftRightTerm :: forall t. () => (SupportedPrim t, PEvalShiftTerm t) => Term t -> Term t -> Term t
- pattern RotateRightTerm :: forall t. () => (SupportedPrim t, PEvalRotateTerm t) => Term t -> Term t -> Term t
- pattern BitCastTerm :: forall b. () => forall a. (SupportedPrim a, SupportedPrim b, PEvalBitCastTerm a b) => Term a -> Term b
- pattern BitCastOrTerm :: forall b. () => forall a. (SupportedPrim a, SupportedPrim b, PEvalBitCastOrTerm a b) => Term b -> Term a -> Term b
- pattern BVConcatTerm :: forall ret. () => forall bv l r. (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. () => forall bv w n ix. (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. () => forall bv l r. (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. () => forall f a. (PEvalApplyTerm f a b, SupportedPrim f, SupportedPrim a, SupportedPrim b) => Term f -> Term a -> Term b
- pattern DivIntegralTerm :: forall t. () => (SupportedPrim t, PEvalDivModIntegralTerm t) => Term t -> Term t -> Term t
- pattern ModIntegralTerm :: forall t. () => (SupportedPrim t, PEvalDivModIntegralTerm t) => Term t -> Term t -> Term t
- pattern QuotIntegralTerm :: forall t. () => (SupportedPrim t, PEvalDivModIntegralTerm t) => Term t -> Term t -> Term t
- pattern RemIntegralTerm :: forall t. () => (SupportedPrim t, PEvalDivModIntegralTerm t) => Term t -> Term t -> Term t
- pattern FPTraitTerm :: forall r. () => forall eb sb fp. (r ~ Bool, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPTrait -> Term (fp eb sb) -> Term r
- pattern FdivTerm :: forall t. () => (SupportedPrim t, PEvalFractionalTerm t) => Term t -> Term t -> Term t
- pattern RecipTerm :: forall t. () => (SupportedPrim t, PEvalFractionalTerm t) => Term t -> Term t
- pattern FloatingUnaryTerm :: forall t. () => (SupportedPrim t, PEvalFloatingTerm t) => FloatingUnaryOp -> Term t -> Term t
- pattern PowerTerm :: forall t. () => (SupportedPrim t, PEvalFloatingTerm t) => Term t -> Term t -> Term t
- pattern FPUnaryTerm :: forall ret. () => forall fp eb sb. (ret ~ fp eb sb, ValidFP eb sb, SupportedPrim (fp eb sb), PEvalFPTerm fp) => FPUnaryOp -> Term (fp eb sb) -> Term ret
- pattern FPBinaryTerm :: forall ret. () => forall fp eb sb. (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. () => forall fp eb sb. (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. () => forall fp eb sb. (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. () => forall fp eb sb. (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. () => forall a. (PEvalFromIntegralTerm a b, SupportedPrim a, SupportedPrim b) => Term a -> Term b
- pattern FromFPOrTerm :: forall a. () => forall eb sb. (PEvalIEEEFPConvertibleTerm a, ValidFP eb sb, SupportedPrim a) => Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
- pattern ToFPTerm :: forall ret. () => forall eb sb 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
- pattern SubTerms :: [SomeTerm] -> Term a
Documentation
Grisette introduces new primitive types:
IntNnn.WordNnn.FPeb sbebexponent bits andsbsignificand bits.AlgReal: algebraic real numbers. Can represent rational numbers. If come from solver's response, it may also represented by roots of polynomials or intervals.Bool=->BoolBool-->Bool
We also provide symbolic counterparts for these types, along with the
basic types Bool and Integer. These symbolic types can be directly
translated to constraints in the SMT solver.
SymBool(Bool, symbolic Booleans)SymInteger(Integer, symbolic unbounded integers)SymIntNnIntNnn)SymWordNnWordNnn)SymFPeb sbFPeb sbebexponent bits andsbsignificand bits)SymAlgReal: symbolic algebraic real numbers.SymBool=~>SymBoolBool=->BoolSymBool-~>SymBoolBool-->Bool
This module provides an operation to extract all primitive values from a
symbolic value, with AllSyms. The module also provides the
representation for symbols (TypedSymbolSymbolSetModelEvalSym, ExtractSym, and
SubstSym.
Extended types
Size-tagged bit-vector types
Signed bit vector type. Indexed with the bit width. Signedness affects the semantics of the operations, including comparison/extension, etc.
>>>3 + 5 :: IntN 50b01000>>>sizedBVConcat (0b101 :: IntN 3) (0b110 :: IntN 3)0b101110>>>sizedBVExt (Proxy @6) (0b101 :: IntN 3)0b111101>>>(8 :: IntN 4) < (7 :: IntN 4)True
More operations are available. Please refer to Grisette.Core for more information.
Instances
data WordN (n :: Nat) Source #
Unsigned bit vector type. Indexed with the bit width. Signedness affect the semantics of the operations, including comparison/extension, etc.
>>>3 + 5 :: WordN 50b01000>>>sizedBVConcat (0b101 :: WordN 3) (0b110 :: WordN 3)0b101110>>>sizedBVExt (Proxy @6) (0b101 :: WordN 3)0b000101>>>(8 :: WordN 4) < (7 :: WordN 4)False
More operations are available. Please refer to Grisette.Core for more information.
Instances
Runtime-sized bit-vector types
Non-indexed bitvectors.
The creation of SomeBV can be done with the bv function with a positive
bit width and a value:
>>>bv 4 0xf :: SomeBV IntN0xf
Operations on two SomeBV values require the bitwidths to be the same. So
you should check for the bit width (via finiteBitSize) before performing
operations:
>>>bv 4 0x3 + bv 4 0x3 :: SomeBV IntN0x6>>>bv 4 0x3 + bv 8 0x3 :: SomeBV IntN*** Exception: BitwidthMismatch
One exception is that the equality testing (both concrete and symbolic via
SymEq) does not require the bitwidths to be the same. Different bitwidths
means the values are not equal:
>>>(bv 4 0x3 :: SomeBV IntN) == (bv 8 0x3)False
Note: SomeBV can be constructed out of integer literals without the
bit width provided. Further binary operations will usually require at least
one operand has the bit-width, and will use that as the bit-width for the
result.
For example:
3 :: SomeBV IntN bvlit(3) >>> bv 4 0x1 + 3 :: SomeBV IntN 0x4 >>> 3 * bv 4 0x1 :: SomeBV IntN 0x3 >>> 3 * 3 :: SomeBV IntN *** Exception: UndeterminedBitwidth "(*)"
Some operations allows the literals to be used without the bit-width, such as
(+), (-), negate, toUnsigned, toSigned, .&., .|., xor,
complement, setBit, clearBit, complementBit, shiftL, and
unsafeShiftL.
>>>3 + 3 :: SomeBV IntNbvlit(6)
Instances
data SomeBVException Source #
An exception that would be thrown when operations are performed on incompatible bit widths.
Constructors
| BitwidthMismatch | |
| UndeterminedBitwidth Text |
Instances
pattern SomeIntN :: () => (KnownNat n, 1 <= n) => IntN n -> SomeIntN Source #
Pattern synonym for SomeBV for concrete signed bitvectors.
pattern SomeWordN :: () => (KnownNat n, 1 <= n) => WordN n -> SomeWordN Source #
Pattern synonym for SomeBV for concrete unsigned bitvectors.
conBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv Source #
conBVView :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV bv -> Maybe (SomeBV cbv) Source #
pattern ConBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => SomeBV cbv -> SomeBV bv Source #
symBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Symbol -> SomeBV bv Source #
ssymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> SomeBV bv Source #
isymBV :: forall cbv bv. (forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n), Solvable (cbv 1) (bv 1)) => Int -> Identifier -> Int -> SomeBV bv Source #
arbitraryBV :: forall bv. (forall n. (KnownNat n, 1 <= n) => Arbitrary (bv n)) => Int -> Gen (SomeBV bv) Source #
Generate an arbitrary SomeBV with a given run-time bitwidth.
Some low-level helpers for writing instances for SomeBV
The functions here will check the bitwidths of the input bit-vectors
and raise BitwidthMismatch if they do not match.
unsafeSomeBV :: forall bv. Int -> (forall proxy n. (KnownNat n, 1 <= n) => proxy n -> bv n) -> SomeBV bv Source #
Construct a SomeBV with a given run-time bitwidth and a polymorphic
value for the underlying bitvector.
unarySomeBV :: forall bv r. (forall n. (KnownNat n, 1 <= n) => bv n -> r) -> (SomeBVLit -> r) -> SomeBV bv -> r Source #
Lift a unary operation on sized bitvectors that returns anything to
SomeBV.
unarySomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n) -> (SomeBVLit -> SomeBVLit) -> SomeBV bv -> SomeBV bv Source #
binSomeBV :: (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> (SomeBVLit -> SomeBVLit -> r) -> SomeBV bv -> SomeBV bv -> r Source #
Lift a binary operation on sized bitvectors that returns anything to
SomeBV. Crash if the bitwidths do not match.
binSomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> (SomeBVLit -> SomeBVLit -> SomeBVLit) -> SomeBV bv -> SomeBV bv -> SomeBV bv Source #
binSomeBVR2 :: (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> (SomeBVLit -> SomeBVLit -> (SomeBVLit, SomeBVLit)) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv) Source #
binSomeBVSafe :: (MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, Mergeable r, forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) -> (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m r) -> SomeBV bv -> SomeBV bv -> m r Source #
Lift a binary operation on sized bitvectors that returns anything wrapped
with ExceptT to SomeBV. If the bitwidths do not match, throw an
BitwidthMismatch error to the monadic context.
binSomeBVSafeR1 :: (MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n), forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m SomeBVLit) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source #
Lift a binary operation on sized bitvectors that returns a bitvector
wrapped with ExceptT to SomeBV. The result will also be wrapped with
SomeBV.
If the bitwidths do not match, throw an BitwidthMismatch error to the
monadic context.
binSomeBVSafeR2 :: (MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n), forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m (SomeBVLit, SomeBVLit)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv) Source #
Lift a binary operation on sized bitvectors that returns two bitvectors
wrapped with ExceptT to SomeBV. The results will also be wrapped with
SomeBV.
If the bitwidths do not match, throw an BitwidthMismatch error to the
monadic context.
Floating point
type ValidFP (eb :: Nat) (sb :: Nat) = ValidFloat eb sb Source #
A type-level proof that the given bit-widths are valid for a floating-point number.
data FP (eb :: Nat) (sb :: Nat) Source #
IEEE 754 floating-point number with eb exponent bits and sb significand
bits.
>>>1.0 + 2.0 :: FP 11 533.0
More operations are available. Please refer to Grisette.Core for more information.
Instances
withValidFPProofs :: forall eb sb r. ValidFP eb sb => ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb), 1 <= eb, 1 <= sb) => r) -> r Source #
Some type-level witnesses that could be derived from ValidFP.
data FPRoundingMode Source #
Rounding mode for floating-point operations.
Constructors
| RNE | Round to nearest, ties to even. |
| RNA | Round to nearest, ties to away from zero. |
| RTP | Round towards positive infinity. |
| RTN | Round towards negative infinity. |
| RTZ | Round towards zero. |
Instances
allFPRoundingMode :: [FPRoundingMode] Source #
All IEEE 754 rounding modes.
Algebraic real numbers
Algebraic real numbers. The representation can be abstract for roots-of-polynomials or intervals.
Constructors
| AlgExactRational :: Rational -> AlgReal | Exact rational number. |
| AlgInexactRational :: Rational -> AlgReal | Inexact rational numbers. SMT-solver return it with ? at the end. |
| AlgPolyRoot | Algebraic real number as a root of a polynomial. |
Fields
| |
| AlgInterval | Interval with low and high bounds. |
Instances
newtype AlgRealPoly Source #
A univariate polynomial with integer coefficients.
For instance, 5x^3+2x-5 is represented as
AlgRealPoly [(5, 3), (2, 1), (-5, 0)]
Constructors
| AlgRealPoly [(Integer, Integer)] |
Instances
Boundary point for real intervals.
Constructors
| OpenPoint Rational | Open point. |
| ClosedPoint Rational | Closed point. |
Instances
data UnsupportedAlgRealOperation Source #
Exception for unsupported operations on algebraic real numbers.
We only support operations on exact rationals.
Constructors
| UnsupportedAlgRealOperation | |
Instances
| Exception UnsupportedAlgRealOperation Source # | |
| Show UnsupportedAlgRealOperation Source # | |
Defined in Grisette.Internal.SymPrim.AlgReal Methods showsPrec :: Int -> UnsupportedAlgRealOperation -> ShowS # show :: UnsupportedAlgRealOperation -> String # showList :: [UnsupportedAlgRealOperation] -> ShowS # | |
Functions
data a =-> b infixr 0 Source #
Functions as a table. Use the # operator to apply the function.
>>>let f = TabularFun [(1, 2), (3, 4)] 0 :: Int =-> Int>>>f # 12>>>f # 20>>>f # 34
Constructors
| TabularFun | |
Fields
| |
Instances
data a --> b infixr 0 Source #
General symbolic function type. Use the # operator to apply the function.
Note that this function should be applied to symbolic values only. It is by
itself already a symbolic value, but can be considered partially concrete
as the function body is specified. Use -~>
for uninterpreted general symbolic functions.
The result would be partially evaluated.
>>>let f = ("x" :: TypedConstantSymbol Integer) --> ("x" + 1 + "y" :: SymInteger) :: Integer --> Integer>>>f # 1 -- 1 has the type SymInteger(+ 2 y)>>>f # "a" -- "a" has the type SymInteger(+ 1 (+ a y))
Instances
| Lift (a --> b :: Type) Source # | |
| (SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => ToSym (Union (ca --> cb)) (sa -~> sb) Source # | |
| Show (a --> b) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g, GeneralFunArg h, GeneralFunArg i) => Binary (a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i)))))))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g, GeneralFunArg h) => Binary (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g) => Binary (a --> (b --> (c --> (d --> (e --> (f --> g)))))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f) => Binary (a --> (b --> (c --> (d --> (e --> f))))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e) => Binary (a --> (b --> (c --> (d --> e)))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d) => Binary (a --> (b --> (c --> d))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c) => Binary (a --> (b --> c)) Source # | |
| (GeneralFunArg a, GeneralFunArg b) => Binary (a --> b) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g, GeneralFunArg h, GeneralFunArg i) => Serial (a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i)))))))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g, GeneralFunArg h) => Serial (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g) => Serial (a --> (b --> (c --> (d --> (e --> (f --> g)))))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f) => Serial (a --> (b --> (c --> (d --> (e --> f))))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e) => Serial (a --> (b --> (c --> (d --> e)))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d) => Serial (a --> (b --> (c --> d))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c) => Serial (a --> (b --> c)) Source # | |
| (GeneralFunArg a, GeneralFunArg b) => Serial (a --> b) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g, GeneralFunArg h, GeneralFunArg i) => Serialize (a --> (b --> (c --> (d --> (e --> (f --> (g --> (h --> i)))))))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g, GeneralFunArg h) => Serialize (a --> (b --> (c --> (d --> (e --> (f --> (g --> h))))))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f, GeneralFunArg g) => Serialize (a --> (b --> (c --> (d --> (e --> (f --> g)))))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e, GeneralFunArg f) => Serialize (a --> (b --> (c --> (d --> (e --> f))))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d, GeneralFunArg e) => Serialize (a --> (b --> (c --> (d --> e)))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c, GeneralFunArg d) => Serialize (a --> (b --> (c --> d))) Source # | |
| (GeneralFunArg a, GeneralFunArg b, GeneralFunArg c) => Serialize (a --> (b --> c)) Source # | |
| (GeneralFunArg a, GeneralFunArg b) => Serialize (a --> b) Source # | |
| NFData (a --> b) Source # | |
Defined in Grisette.Internal.SymPrim.GeneralFun | |
| Eq (a --> b) Source # | |
| (Apply st, LinkedRep ca sa, LinkedRep ct st) => Apply (ca --> ct) Source # | |
| ITEOp (a --> b) Source # | |
| EvalSym (SymType b) => EvalSym (a --> b) Source # | |
| ExtractSym (SymType b) => ExtractSym (a --> b) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym Methods extractSym :: (a --> b) -> AnySymbolSet Source # extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => (a --> b) -> Maybe (SymbolSet knd) Source # | |
| Mergeable (a --> b) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy (a --> b) Source # sortIndices :: (a --> b) -> [DynamicSortedIdx] Source # | |
| PPrint (a --> b) Source # | |
| SimpleMergeable (a --> b) Source # | |
| SubstSym (SymType b) => SubstSym (a --> b) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym Methods substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> (a --> b) -> a --> b Source # | |
| (SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a --> b) Source # | |
Defined in Grisette.Internal.SymPrim.GeneralFun | |
| (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 # | |
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 # | |
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 # | |
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 # | |
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 # | |
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 # | |
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 # | |
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 a, SupportedPrim b) => SupportedPrimConstraint (a --> b) Source # | |
Defined in Grisette.Internal.SymPrim.GeneralFun Associated Types type PrimConstraint (a --> b) Source # | |
| (SymRep ca, SymRep cb, SupportedPrim (ca --> cb)) => SymRep (ca --> cb) Source # | |
Defined in Grisette.Internal.SymPrim.SymGeneralFun | |
| Hashable (a --> b) Source # | |
Defined in Grisette.Internal.SymPrim.GeneralFun | |
| (LinkedRep a sa, LinkedRep b sb) => Function (a --> b) sa sb Source # | |
Defined in Grisette.Internal.SymPrim.GeneralFun | |
| (SupportedPrim (a --> b), SupportedNonFuncPrim a, SupportedPrim b) => PEvalApplyTerm (a --> b) a b Source # | |
Defined in Grisette.Internal.SymPrim.GeneralFun | |
| (SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb)) => Solvable (ca --> cb) (sa -~> sb) Source # | |
| ToCon (a --> b) (a --> b) Source # | |
| (LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa -~> sb) (ca --> cb) Source # | |
| ToSym (a --> b) (a --> b) Source # | |
| (SupportedPrim (ca --> cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca --> cb) (sa -~> sb) Source # | |
| (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim cb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => LinkedRep (ca --> cb) (sa -~> sb) Source # | |
| type FunType (ca --> ct) Source # | |
| type PrimConstraint (a --> b) Source # | |
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)) | |
| type SBVType (a --> b) Source # | |
Defined in Grisette.Internal.SymPrim.GeneralFun | |
| type SymType (ca --> cb) Source # | |
(-->) :: (SupportedNonFuncPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedConstantSymbol ca -> sb -> ca --> cb infixr 0 Source #
Construction of general symbolic functions.
>>>f = "a" --> "a" + 1 :: Integer --> Integer>>>f\(arg@0 :: Integer) -> (+ 1 arg@0)
This general symbolic function needs to be applied to symbolic values:
>>>f # ("a" :: SymInteger)(+ 1 a)>>>f # (2 :: SymInteger)3
Symbolic types
Symbolic bool and integer types
Symbolic Boolean type.
>>>"a" :: SymBoola>>>"a" .&& "b" :: SymBool(&& a b)
More operations are available. Please refer to Grisette.Core for more information.
Instances
newtype SymInteger Source #
Symbolic (unbounded, mathematical) integer type.
>>>"a" + 1 :: SymInteger(+ 1 a)
More operations are available. Please refer to Grisette.Core for more information.
Constructors
| SymInteger (Term Integer) |
Instances
Symbolic bit-vector types
newtype SymWordN (n :: Nat) Source #
Symbolic unsigned bit vector type. Indexed with the bit width. Signedness affects the semantics of the operations, including comparison/extension, etc.
>>>"a" + 5 :: SymWordN 5(+ 0b00101 a)>>>sizedBVConcat (con 0b101 :: SymWordN 3) (con 0b110 :: SymWordN 3)0b101110>>>sizedBVExt (Proxy @6) (con 0b101 :: SymWordN 3)0b000101>>>(8 :: SymWordN 4) .< (7 :: SymWordN 4)false
More operations are available. Please refer to Grisette.Core for more information.
Instances
type SymWordN16 = SymWordN 16 Source #
Symbolic 16-bit unsigned bit-vector.
type SymWordN32 = SymWordN 32 Source #
Symbolic 32-bit unsigned bit-vector.
type SymWordN64 = SymWordN 64 Source #
Symbolic 64-bit unsigned bit-vector.
newtype SymIntN (n :: Nat) Source #
Symbolic signed bit vector type. Indexed with the bit width. Signedness affects the semantics of the operations, including comparison/extension, etc.
>>>"a" + 5 :: SymIntN 5(+ 0b00101 a)>>>sizedBVConcat (con 0b101 :: SymIntN 3) (con 0b110 :: SymIntN 3)0b101110>>>sizedBVExt (Proxy @6) (con 0b101 :: SymIntN 3)0b111101>>>(8 :: SymIntN 4) .< (7 :: SymIntN 4)true
More operations are available. Please refer to Grisette.Core for more information.
Instances
type SomeSymWordN = SomeBV SymWordN Source #
Type synonym for SomeBV for symbolic unsigned bitvectors.
pattern SomeSymIntN :: () => (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN Source #
Pattern synonym for SomeBV for symbolic signed bitvectors.
pattern SomeSymWordN :: () => (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN Source #
Pattern synonym for SomeBV for symbolic unsigned bitvectors.
Symbolic floating point
Symbolic IEEE 754 floating-point number with eb exponent bits and sb
significand bits.
>>>"a" + 2.0 :: SymFP 11 53(+ a 2.0)>>>fpAdd rne "a" 2.0 :: SymFP 11 53(fp.add rne a 2.0)
More operations are available. Please refer to Grisette.Core for more information.
Instances
newtype SymFPRoundingMode Source #
Symbolic floating-point rounding mode.
Constructors
| SymFPRoundingMode (Term FPRoundingMode) |
Instances
Symbolic algebraic real numbers
newtype SymAlgReal Source #
Symbolic representation of algebraic real numbers.
Constructors
| SymAlgReal (Term AlgReal) |
Instances
Symbolic function, possibly uninterpreted
data sa =~> sb where infixr 0 Source #
Symbolic tabular function type.
>>>f' = "f" :: SymInteger =~> SymInteger>>>f = (f' #)>>>f 1(apply f 1)
>>>f' = con (TabularFun [(1, 2), (2, 3)] 4) :: SymInteger =~> SymInteger>>>f = (f' #)>>>f 12>>>f 23>>>f 34>>>f "b"(ite (= b 1) 2 (ite (= b 2) 3 4))
Constructors
| SymTabularFun :: (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb), SupportedNonFuncPrim ca) => Term (ca =-> cb) -> sa =~> sb |
Instances
data sa -~> sb where infixr 0 Source #
Symbolic general function type.
>>>f' = "f" :: SymInteger -~> SymInteger>>>f = (f' #)>>>f 1(apply f 1)
>>>f' = con ("a" --> "a" + 1) :: SymInteger -~> SymInteger>>>f'\(arg@0 :: Integer) -> (+ 1 arg@0)>>>f = (f' #)>>>f 12>>>f 23>>>f 34>>>f "b"(+ 1 b)
Constructors
| SymGeneralFun :: (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb), SupportedNonFuncPrim ca) => Term (ca --> cb) -> sa -~> sb |
Instances
Shared constraints
type Prim a = (Show a, Binary a, Serial a, Serialize a, NFData a, Eq a, EvalSym a, ExtractSym a, Mergeable a, PPrint a, SubstSym a, SymEq a, SymOrd a, AllSyms a, Hashable a, Lift a, Typeable a) Source #
A type that is used as a constraint for all the primitive types (including concrete primitives) in Grisette.
type SymPrim a = (Prim a, ITEOp a, GenSymSimple a a) Source #
A type that is used as a constraint for all the symbolic primitive types in Grisette.
type BasicSymPrim a = (SymPrim a, SimpleMergeable a, GenSymSimple () a, Solvable (ConType a) a, ConRep a, LinkedRep (ConType a) a, ToCon a (ConType a), ToSym (ConType a) a, Apply a, a ~ FunType a, SupportedNonFuncPrim (ConType a)) Source #
A type that is used as a constraint for all the basic symbolic primitive types in Grisette.
SomeSymWordN is not considered as a basic symbolic
primitive type.
Quantifiers
forallSet :: ConstantSymbolSet -> SymBool -> SymBool Source #
Forall quantifier over a set of constant symbols. Quantifier over functions is not supported.
>>>let xsym = "x" :: TypedConstantSymbol Integer>>>let ysym = "y" :: TypedConstantSymbol Integer>>>let x = "x" :: SymInteger>>>let y = "y" :: SymInteger>>>forallSet (buildSymbolSet [xsym, ysym]) (x .== y)(forall x :: Integer (forall y :: Integer (= x y)))
Only available with SBV 10.1.0 or later.
forallSym :: (HasCallStack, ExtractSym a) => a -> SymBool -> SymBool Source #
Forall quantifier over all symbolic constants in a value. Quantifier over functions is not supported.
>>>let a = ["x", "y"] :: [SymInteger]>>>forallSym a $ sum a .== 0(forall x :: Integer (forall y :: Integer (= (+ x y) 0)))
Only available with sbv 10.1.0 or later.
forallFresh :: (HasCallStack, ExtractSym v, MonadFresh m, GenSym spec v, TryMerge m) => spec -> (v -> FreshT Union SymBool) -> m SymBool Source #
Forall quantifier over symbolic constants in a freshly generated value. Quantifier over functions is not supported.
>>>:{x :: Fresh SymBool x = forallFresh () $ \(a :: SymBool) -> existsFresh () $ \(b :: SymBool) -> mrgReturn $ a .== b :}
>>>runFresh x "x"(forall x@0 :: Bool (exists x@1 :: Bool (= x@0 x@1)))
Only available with sbv 10.1.0 or later.
existsSet :: ConstantSymbolSet -> SymBool -> SymBool Source #
Exists quantifier over a set of constant symbols. Quantifier over functions is not supported.
>>>let xsym = "x" :: TypedConstantSymbol Integer>>>let ysym = "y" :: TypedConstantSymbol Integer>>>let x = "x" :: SymInteger>>>let y = "y" :: SymInteger>>>existsSet (buildSymbolSet [xsym, ysym]) (x .== y)(exists x :: Integer (exists y :: Integer (= x y)))
Only available with SBV 10.1.0 or later.
existsSym :: (HasCallStack, ExtractSym a) => a -> SymBool -> SymBool Source #
Exists quantifier over all symbolic constants in a value. Quantifier over functions is not supported.
>>>let a = ["x", "y"] :: [SymInteger]>>>existsSym a $ sum a .== 0(exists x :: Integer (exists y :: Integer (= (+ x y) 0)))
Only available with sbv 10.1.0 or later.
existsFresh :: (HasCallStack, ExtractSym v, MonadFresh m, GenSym spec v, TryMerge m) => spec -> (v -> FreshT Union SymBool) -> m SymBool Source #
Exists quantifier over symbolic constants in a freshly generated value. Quantifier over functions is not supported.
>>>:{x :: Fresh SymBool x = forallFresh () $ \(a :: SymBool) -> existsFresh () $ \(b :: SymBool) -> mrgReturn $ a .== b :}
>>>runFresh x "x"(forall x@0 :: Bool (exists x@1 :: Bool (= x@0 x@1)))
Only available with sbv 10.1.0 or later.
Basic constraints
class (Lift t, NFData t, Typeable t, SupportedPrimConstraint t, SBVRep t) => SupportedPrim t 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
Instances
class SupportedPrim con => SymRep con Source #
Type family to resolve the symbolic type associated with a concrete type.
Instances
| SymRep AlgReal Source # | |
Defined in Grisette.Internal.SymPrim.SymAlgReal | |
| SymRep FPRoundingMode Source # | |
Defined in Grisette.Internal.SymPrim.SymFP Associated Types type SymType FPRoundingMode Source # | |
| SymRep Integer Source # | |
Defined in Grisette.Internal.SymPrim.SymInteger | |
| SymRep Bool Source # | |
Defined in Grisette.Internal.SymPrim.SymBool | |
| (KnownNat n, 1 <= n) => SymRep (IntN n) Source # | |
Defined in Grisette.Internal.SymPrim.SymBV | |
| (KnownNat n, 1 <= n) => SymRep (WordN n) Source # | |
Defined in Grisette.Internal.SymPrim.SymBV | |
| ValidFP eb sb => SymRep (FP eb sb) Source # | |
Defined in Grisette.Internal.SymPrim.SymFP | |
| (SymRep ca, SymRep cb, SupportedPrim (ca --> cb)) => SymRep (ca --> cb) Source # | |
Defined in Grisette.Internal.SymPrim.SymGeneralFun | |
| (SymRep a, SymRep b, SupportedPrim (a =-> b)) => SymRep (a =-> b) Source # | |
Defined in Grisette.Internal.SymPrim.SymTabularFun | |
Type family to resolve the concrete type associated with a symbolic type.
Instances
| ConRep SymAlgReal Source # | |
Defined in Grisette.Internal.SymPrim.SymAlgReal Associated Types type ConType SymAlgReal Source # | |
| ConRep SymBool Source # | |
Defined in Grisette.Internal.SymPrim.SymBool | |
| ConRep SymFPRoundingMode Source # | |
Defined in Grisette.Internal.SymPrim.SymFP Associated Types type ConType SymFPRoundingMode Source # | |
| ConRep SymInteger Source # | |
Defined in Grisette.Internal.SymPrim.SymInteger Associated Types type ConType SymInteger Source # | |
| (KnownNat n, 1 <= n) => ConRep (SymIntN n) Source # | |
Defined in Grisette.Internal.SymPrim.SymBV | |
| (KnownNat n, 1 <= n) => ConRep (SymWordN n) Source # | |
Defined in Grisette.Internal.SymPrim.SymBV | |
| ConRep (SymFP eb sb) Source # | |
Defined in Grisette.Internal.SymPrim.SymFP | |
| (ConRep a, ConRep b) => ConRep (a -~> b) Source # | |
Defined in Grisette.Internal.SymPrim.SymGeneralFun | |
| (ConRep a, ConRep b) => ConRep (a =~> b) Source # | |
Defined in Grisette.Internal.SymPrim.SymTabularFun | |
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.
Instances
Extract symbolic values
Some symbolic value with LinkedRep constraint.
class AllSyms a where Source #
Extract all symbolic primitive values that are represented as SMT terms.
>>>allSyms (["a" + 1 :: SymInteger, -"b"], "c" :: SymBool)[(+ 1 a),(- b),c]
This is usually used for getting a statistical summary of the size of
a symbolic value with allSymsSize.
Note: This type class can be derived for algebraic data types. You may
need the DerivingVia and DerivingStrategies extenstions.
data X = ... deriving Generic deriving AllSyms via (Default X)
Methods
allSymsS :: a -> [SomeSym] -> [SomeSym] Source #
Convert a value to a list of symbolic primitive values. It should prepend to an existing list of symbolic primitive values.
allSyms :: a -> [SomeSym] Source #
Specialized allSymsS that prepends to an empty list.
Instances
class (forall a. AllSyms a => AllSyms (f a)) => AllSyms1 f where Source #
Lifting of the AllSyms class to unary type constructors.
Methods
liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym] Source #
Lift the allSymsS function to unary type constructors.
Instances
allSymsS1 :: (AllSyms1 f, AllSyms a) => f a -> [SomeSym] -> [SomeSym] Source #
Lift the standard allSymsS function to unary type constructors.
class (forall a. AllSyms a => AllSyms1 (f a)) => AllSyms2 f where Source #
Lifting of the AllSyms class to binary type constructors.
Methods
liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> f a b -> [SomeSym] -> [SomeSym] Source #
Lift the allSymsS function to binary type constructors.
Instances
allSymsS2 :: (AllSyms2 f, AllSyms a, AllSyms b) => f a b -> [SomeSym] -> [SomeSym] Source #
Lift the standard allSymsS function to binary type constructors.
allSymsSize :: AllSyms a => a -> Int Source #
Get the total size of symbolic terms in a value. Duplicate sub-terms are counted for only once.
>>>allSymsSize ("a" :: SymInteger, "a" + "b" :: SymInteger, ("a" + "b") * "c" :: SymInteger)5
The 5 terms are a, b, (+ a b), c, and (* (+ a b) c).
symSize :: forall con sym. LinkedRep con sym => sym -> Int Source #
Get the size of a symbolic term. Duplicate sub-terms are counted for only once.
>>>symSize (1 :: SymInteger)1>>>symSize ("a" :: SymInteger)1>>>symSize ("a" + 1 :: SymInteger)3>>>symSize (("a" + 1) * ("a" + 1) :: SymInteger)4
symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int Source #
Get the sum of the sizes of a list of symbolic terms. Duplicate sub-terms are counted for only once.
>>>symsSize [1, "a" :: SymInteger, "a" + 1 :: SymInteger]3
Generic AllSyms
data family AllSymsArgs arity a :: Type Source #
The arguments to the generic AllSyms function.
Instances
| data AllSymsArgs Arity0 _ Source # | |
| newtype AllSymsArgs Arity1 a Source # | |
class GAllSyms arity f where Source #
The class of types that can generically extract all symbolic primitives.
Instances
| GAllSyms Arity1 Par1 Source # | |
| GAllSyms arity (U1 :: Type -> Type) Source # | |
| GAllSyms arity (V1 :: Type -> Type) Source # | |
| AllSyms1 f => GAllSyms Arity1 (Rec1 f) Source # | |
| (GAllSyms arity a, GAllSyms arity b) => GAllSyms arity (a :*: b) Source # | |
| (GAllSyms arity a, GAllSyms arity b) => GAllSyms arity (a :+: b) Source # | |
| AllSyms c => GAllSyms arity (K1 i c :: Type -> Type) Source # | |
| (AllSyms1 f, GAllSyms Arity1 g) => GAllSyms Arity1 (f :.: g) Source # | |
| GAllSyms arity a => GAllSyms arity (M1 i c a) Source # | |
genericAllSymsS :: (Generic a, GAllSyms Arity0 (Rep a)) => a -> [SomeSym] -> [SomeSym] Source #
Generic allSymsS function.
genericLiftAllSymsS :: (Generic1 f, GAllSyms Arity1 (Rep1 f)) => (a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym] Source #
Generic liftAllSymsS function.
Symbolic constant sets and models
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 |
class IsSymbolKind (knd :: SymbolKind) where Source #
Decision procedure for symbol kinds.
Associated Types
type SymbolKindConstraint knd :: Type -> Constraint Source #
Methods
decideSymbolKind :: Either (knd :~~: 'ConstantKind) (knd :~~: 'AnyKind) Source #
withSymbolKindConstraint :: TypedSymbol knd t -> (SymbolKindConstraint knd t => a) -> a Source #
Instances
| IsSymbolKind 'AnyKind Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type SymbolKindConstraint 'AnyKind :: Type -> Constraint Source # Methods decideSymbolKind :: Either ('AnyKind :~~: 'ConstantKind) ('AnyKind :~~: 'AnyKind) Source # withSymbolKindConstraint :: TypedSymbol 'AnyKind t -> (SymbolKindConstraint 'AnyKind t => a) -> a Source # | |
| IsSymbolKind 'ConstantKind Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.Term Associated Types type SymbolKindConstraint 'ConstantKind :: Type -> Constraint Source # Methods decideSymbolKind :: Either ('ConstantKind :~~: 'ConstantKind) ('ConstantKind :~~: 'AnyKind) Source # withSymbolKindConstraint :: TypedSymbol 'ConstantKind t -> (SymbolKindConstraint 'ConstantKind t => a) -> a Source # | |
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 Boola :: Bool
Constructors
| TypedSymbol | |
Fields
| |
Instances
typedAnySymbol :: forall t. SupportedPrim t => Symbol -> TypedSymbol 'AnyKind t Source #
Create a typed symbol with any kinds.
type TypedAnySymbol = TypedSymbol 'AnyKind Source #
Any symbol
typedConstantSymbol :: forall t. SupportedNonFuncPrim t => Symbol -> TypedSymbol 'ConstantKind t Source #
Create a typed symbol with constant kinds.
type TypedConstantSymbol = TypedSymbol 'ConstantKind Source #
Constant symbol
data SomeTypedSymbol knd where Source #
A non-indexed symbol. Type information are checked at runtime.
Constructors
| SomeTypedSymbol :: forall knd t. TypedSymbol knd t -> SomeTypedSymbol knd |
Instances
type SomeTypedAnySymbol = SomeTypedSymbol 'AnyKind Source #
Non-indexed any symbol
type SomeTypedConstantSymbol = SomeTypedSymbol 'ConstantKind Source #
Non-indexed constant symbol
Set of symbols.
Check SymbolSetOps for operations, and
SymbolSetRep for manual constructions.
Instances
type AnySymbolSet = SymbolSet 'AnyKind Source #
Set of any symbols.
type ConstantSymbolSet = SymbolSet 'ConstantKind Source #
Set of constant symbols. Excluding unintepreted functions.
Instances
data ModelValuePair t Source #
A type used for building a model by hand.
>>>buildModel ("x" ::= (1 :: Integer), "y" ::= True) :: ModelModel {x -> 1 :: Integer, y -> true :: Bool}
Constructors
| (TypedAnySymbol t) ::= t |
Instances
| Show t => Show (ModelValuePair t) Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Model Methods showsPrec :: Int -> ModelValuePair t -> ShowS # show :: ModelValuePair t -> String # showList :: [ModelValuePair t] -> ShowS # | |
| ModelRep (ModelValuePair t) Model Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildModel :: ModelValuePair t -> Model Source # | |
data ModelSymPair ct st where Source #
A pair of a symbolic constant and its value. This is used to build a model from a list of symbolic constants and their values.
>>>buildModel ("a" := (1 :: Integer), "b" := True) :: ModelModel {a -> 1 :: Integer, b -> true :: Bool}
Constructors
| (:=) :: LinkedRep ct st => st -> ct -> ModelSymPair ct st |
Instances
| ModelRep (ModelSymPair ct st) Model Source # | |
Defined in Grisette.Internal.SymPrim.ModelRep Methods buildModel :: ModelSymPair ct st -> Model Source # | |
Analysis on the terms
Internal representation for Grisette symbolic terms.
Instances
Existential wrapper for symbolic Grisette terms.
Constructors
| SomeTerm :: forall a. SupportedPrim a => Term a -> SomeTerm |
someTermSize :: SomeTerm -> Int Source #
Compute the size of a list of terms. Do not count the same term twice.
termsSize :: [Term a] -> Int Source #
Compute the size of a list of terms. Do not count the same term twice.
someTermsSize :: [SomeTerm] -> Int Source #
Compute the size of a list of terms. Do not count the same term twice.
pattern SupportedTerm :: forall t. () => SupportedPrim t => Term t Source #
Pattern synonym to introduce the SupportedPrim constraint.
pattern SupportedTypedSymbol :: forall (k :: SymbolKind) t. () => (SupportedPrim t, SymbolKindConstraint k t, IsSymbolKind k) => TypedSymbol k t Source #
Pattern synonym to introduce constraints from a TypedSymbol.
pattern SupportedConstantTypedSymbol :: forall k t. () => (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 :: forall t. () => SupportedPrim t => t -> Term t Source #
pattern SymTerm :: forall t. () => SupportedPrim t => TypedSymbol 'AnyKind t -> Term t Source #
pattern ForallTerm :: forall r. () => forall 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. () => forall 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 EqTerm :: forall r. () => forall t. (r ~ Bool, SupportedPrim t) => Term t -> Term t -> Term r Source #
pattern DistinctTerm :: forall r. () => forall 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 :: forall t. () => SupportedPrim t => Term Bool -> Term t -> Term t -> Term t Source #
pattern AddNumTerm :: forall t. () => (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 :: forall t. () => (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 :: forall t. () => (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 :: forall t. () => (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 :: forall t. () => (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. () => forall 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. () => forall 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 :: forall t. () => (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 :: forall t. () => (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 :: forall t. () => (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 :: forall t. () => (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 :: forall t. () => (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 :: forall t. () => (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 :: forall t. () => (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 :: forall t. () => (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. () => forall 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 :: forall b. () => forall a. (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. () => forall bv l r. (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. () => forall bv w n ix. (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. () => forall bv l r. (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. () => forall 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 :: forall t. () => (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 :: forall t. () => (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 :: forall t. () => (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 :: forall t. () => (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. () => forall eb sb 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 :: forall t. () => (SupportedPrim t, PEvalFractionalTerm t) => Term t -> Term t -> Term t Source #
pattern RecipTerm :: forall t. () => (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 :: forall t. () => (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 :: forall t. () => (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. () => forall fp eb sb. (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. () => forall fp eb sb. (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. () => forall fp eb sb. (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. () => forall fp eb sb. (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. () => forall fp eb sb. (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. () => forall 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. () => forall eb sb. (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. () => forall eb sb 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 #