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 |
Synopsis
- class SupportedPrimConstraint t where
- type PrimConstraint (n :: Nat) t :: Constraint
- class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t, SupportedPrimConstraint t, SBVRep t) => SupportedPrim t where
- termCache :: Cache (Term t)
- pformatCon :: t -> String
- pformatSym :: TypedSymbol t -> String
- defaultValue :: t
- defaultValueDynamic :: proxy t -> ModelValue
- pevalITETerm :: Term Bool -> Term t -> Term t -> Term t
- pevalEqTerm :: Term t -> Term t -> Term Bool
- conSBVTerm :: KnownIsZero n => proxy n -> t -> SBVType n t
- symSBVName :: TypedSymbol t -> Int -> String
- symSBVTerm :: (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n t)
- withPrim :: KnownIsZero n => p n -> ((PrimConstraint n t, SMTDefinable (SBVType n t), Mergeable (SBVType n t), Typeable (SBVType n t)) => a) -> a
- sbvIte :: KnownIsZero n => proxy n -> SBV Bool -> SBVType n t -> SBVType n t -> SBVType n t
- sbvEq :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBV Bool
- parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> t
- class SupportedPrim con => SymRep con where
- type SymType con
- class ConRep sym where
- type ConType sym
- class (ConRep sym, SymRep con, sym ~ SymType con, con ~ ConType sym) => LinkedRep con sym | con -> sym, sym -> con where
- underlyingTerm :: sym -> Term con
- wrapTerm :: Term con -> sym
- class (SupportedPrim arg, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => UnaryOp tag arg t | tag arg -> t where
- pevalUnary :: (Typeable tag, Typeable t) => tag -> Term arg -> Term t
- pformatUnary :: tag -> Term arg -> String
- class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => BinaryOp tag arg1 arg2 t | tag arg1 arg2 -> t where
- pevalBinary :: (Typeable tag, Typeable t) => tag -> Term arg1 -> Term arg2 -> Term t
- pformatBinary :: tag -> Term arg1 -> Term arg2 -> String
- class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim arg3, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => TernaryOp tag arg1 arg2 arg3 t | tag arg1 arg2 arg3 -> t where
- class (SupportedPrim f, SupportedPrim a, SupportedPrim b) => PEvalApplyTerm f a b | f -> a b where
- pevalApplyTerm :: Term f -> Term a -> Term b
- sbvApplyTerm :: KnownIsZero n => proxy n -> SBVType n f -> SBVType n a -> SBVType n b
- class (SupportedPrim t, Bits t) => PEvalBitwiseTerm t where
- pevalAndBitsTerm :: Term t -> Term t -> Term t
- pevalOrBitsTerm :: Term t -> Term t -> Term t
- pevalXorBitsTerm :: Term t -> Term t -> Term t
- pevalComplementBitsTerm :: Term t -> Term t
- withSbvBitwiseTermConstraint :: KnownIsZero n => proxy n -> (Bits (SBVType n t) => r) -> r
- sbvAndBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvOrBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvXorBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvComplementBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t
- class (SupportedNonFuncPrim t, SymShift t) => PEvalShiftTerm t where
- pevalShiftLeftTerm :: Term t -> Term t -> Term t
- pevalShiftRightTerm :: Term t -> Term t -> Term t
- withSbvShiftTermConstraint :: KnownIsZero n => proxy n -> (SIntegral (NonFuncSBVBaseType n t) => r) -> r
- sbvShiftLeftTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvShiftRightTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- class (SupportedNonFuncPrim t, SymRotate t) => PEvalRotateTerm t where
- pevalRotateLeftTerm :: Term t -> Term t -> Term t
- pevalRotateRightTerm :: Term t -> Term t -> Term t
- withSbvRotateTermConstraint :: KnownIsZero n => proxy n -> (SIntegral (NonFuncSBVBaseType n t) => r) -> r
- sbvRotateLeftTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvRotateRightTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- class (SupportedPrim t, Num t) => PEvalNumTerm t where
- pevalAddNumTerm :: Term t -> Term t -> Term t
- pevalNegNumTerm :: Term t -> Term t
- pevalMulNumTerm :: Term t -> Term t -> Term t
- pevalAbsNumTerm :: Term t -> Term t
- pevalSignumNumTerm :: Term t -> Term t
- withSbvNumTermConstraint :: KnownIsZero n => proxy n -> (Num (SBVType n t) => r) -> r
- sbvAddNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvNegNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t
- sbvMulNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvAbsNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t
- sbvSignumNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t
- pevalSubNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a
- class (SupportedPrim t, Ord t) => PEvalOrdTerm t where
- pevalLtOrdTerm :: Term t -> Term t -> Term Bool
- pevalLeOrdTerm :: Term t -> Term t -> Term Bool
- withSbvOrdTermConstraint :: KnownIsZero n => proxy n -> (OrdSymbolic (SBVType n t) => r) -> r
- sbvLtOrdTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBV Bool
- sbvLeOrdTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBV Bool
- pevalGtOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool
- pevalGeOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool
- pevalNEqTerm :: SupportedPrim a => Term a -> Term a -> Term Bool
- class (SupportedPrim t, Integral t) => PEvalDivModIntegralTerm t where
- pevalDivIntegralTerm :: Term t -> Term t -> Term t
- pevalModIntegralTerm :: Term t -> Term t -> Term t
- pevalQuotIntegralTerm :: Term t -> Term t -> Term t
- pevalRemIntegralTerm :: Term t -> Term t -> Term t
- withSbvDivModIntegralTermConstraint :: KnownIsZero n => proxy n -> (SDivisible (SBVType n t) => r) -> r
- sbvDivIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvModIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvQuotIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- sbvRemIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t
- class (PEvalBVTerm s, PEvalBVTerm u, forall n. (KnownNat n, 1 <= n) => SupportedNonFuncPrim (u n), forall n. (KnownNat n, 1 <= n) => SupportedNonFuncPrim (s n), forall n. (KnownNat n, 1 <= n) => SignConversion (u n) (s n)) => PEvalBVSignConversionTerm u s | u -> s, s -> u where
- pevalBVToSignedTerm :: (KnownNat n, 1 <= n) => Term (u n) -> Term (s n)
- pevalBVToUnsignedTerm :: (KnownNat n, 1 <= n) => Term (s n) -> Term (u n)
- withSbvSignConversionTermConstraint :: forall n integerBitwidth p q r. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => p n -> q integerBitwidth -> ((Integral (NonFuncSBVBaseType integerBitwidth (u n)), Integral (NonFuncSBVBaseType integerBitwidth (s n))) => r) -> r
- sbvToSigned :: forall n integerBitwidth o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o u -> p n -> q integerBitwidth -> SBVType integerBitwidth (u n) -> SBVType integerBitwidth (s n)
- sbvToUnsigned :: forall n integerBitwidth o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o s -> p n -> q integerBitwidth -> SBVType integerBitwidth (s n) -> SBVType integerBitwidth (u n)
- class (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), SizedBV bv, Typeable bv) => PEvalBVTerm bv where
- pevalBVConcatTerm :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (bv l) -> Term (bv r) -> Term (bv (l + r))
- pevalBVExtendTerm :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (bv l) -> Term (bv r)
- pevalBVSelectTerm :: (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (bv n) -> Term (bv w)
- sbvBVConcatTerm :: (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (bv l) -> SBVType n (bv r) -> SBVType n (bv (l + r))
- sbvBVExtendTerm :: (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (bv l) -> SBVType n (bv r)
- sbvBVSelectTerm :: (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (bv n) -> SBVType int (bv w)
- data TypedSymbol t where
- TypedSymbol :: SupportedPrim t => {..} -> TypedSymbol t
- data SomeTypedSymbol where
- SomeTypedSymbol :: forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol
- showUntyped :: TypedSymbol t -> String
- withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a
- someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol
- data Term t where
- ConTerm :: SupportedPrim t => !Id -> !t -> Term t
- SymTerm :: SupportedPrim t => !Id -> !(TypedSymbol t) -> Term t
- UnaryTerm :: UnaryOp tag arg t => !Id -> !tag -> !(Term arg) -> Term t
- BinaryTerm :: BinaryOp tag arg1 arg2 t => !Id -> !tag -> !(Term arg1) -> !(Term arg2) -> Term t
- TernaryTerm :: TernaryOp tag arg1 arg2 arg3 t => !Id -> !tag -> !(Term arg1) -> !(Term arg2) -> !(Term arg3) -> Term t
- NotTerm :: !Id -> !(Term Bool) -> Term Bool
- OrTerm :: !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
- AndTerm :: !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool
- EqTerm :: SupportedPrim t => !Id -> !(Term t) -> !(Term t) -> Term Bool
- ITETerm :: SupportedPrim t => !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t
- AddNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- NegNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> Term t
- MulNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- AbsNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> Term t
- SignumNumTerm :: PEvalNumTerm t => !Id -> !(Term t) -> Term t
- LtOrdTerm :: PEvalOrdTerm t => !Id -> !(Term t) -> !(Term t) -> Term Bool
- LeOrdTerm :: PEvalOrdTerm t => !Id -> !(Term t) -> !(Term t) -> Term Bool
- AndBitsTerm :: PEvalBitwiseTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- OrBitsTerm :: PEvalBitwiseTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- XorBitsTerm :: PEvalBitwiseTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- ComplementBitsTerm :: PEvalBitwiseTerm t => !Id -> !(Term t) -> Term t
- ShiftLeftTerm :: PEvalShiftTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- ShiftRightTerm :: PEvalShiftTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- RotateLeftTerm :: PEvalRotateTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- RotateRightTerm :: PEvalRotateTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- ToSignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => !Id -> !(Term (u n)) -> Term (s n)
- ToUnsignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => !Id -> !(Term (s n)) -> Term (u n)
- BVConcatTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r)) => !Id -> !(Term (bv l)) -> !(Term (bv r)) -> Term (bv (l + r))
- BVSelectTerm :: (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => !Id -> !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv n)) -> Term (bv w)
- BVExtendTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => !Id -> !Bool -> !(TypeRep r) -> !(Term (bv l)) -> Term (bv r)
- ApplyTerm :: (SupportedPrim a, SupportedPrim b, SupportedPrim f, PEvalApplyTerm f a b) => !Id -> !(Term f) -> !(Term a) -> Term b
- DivIntegralTerm :: PEvalDivModIntegralTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- ModIntegralTerm :: PEvalDivModIntegralTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- QuotIntegralTerm :: PEvalDivModIntegralTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- RemIntegralTerm :: PEvalDivModIntegralTerm t => !Id -> !(Term t) -> !(Term t) -> Term t
- identity :: Term t -> Id
- identityWithTypeRep :: forall t. Term t -> (SomeTypeRep, Id)
- introSupportedPrimConstraint :: forall t a. Term t -> (SupportedPrim t => a) -> a
- pformat :: forall t. SupportedPrim t => Term t -> String
- data UTerm t where
- UConTerm :: SupportedPrim t => !t -> UTerm t
- USymTerm :: SupportedPrim t => !(TypedSymbol t) -> UTerm t
- UUnaryTerm :: UnaryOp tag arg t => !tag -> !(Term arg) -> UTerm t
- UBinaryTerm :: BinaryOp tag arg1 arg2 t => !tag -> !(Term arg1) -> !(Term arg2) -> UTerm t
- UTernaryTerm :: TernaryOp tag arg1 arg2 arg3 t => !tag -> !(Term arg1) -> !(Term arg2) -> !(Term arg3) -> UTerm t
- UNotTerm :: !(Term Bool) -> UTerm Bool
- UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
- UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool
- UEqTerm :: SupportedPrim t => !(Term t) -> !(Term t) -> UTerm Bool
- UITETerm :: SupportedPrim t => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t
- UAddNumTerm :: PEvalNumTerm t => !(Term t) -> !(Term t) -> UTerm t
- UNegNumTerm :: PEvalNumTerm t => !(Term t) -> UTerm t
- UMulNumTerm :: PEvalNumTerm t => !(Term t) -> !(Term t) -> UTerm t
- UAbsNumTerm :: PEvalNumTerm t => !(Term t) -> UTerm t
- USignumNumTerm :: PEvalNumTerm t => !(Term t) -> UTerm t
- ULtOrdTerm :: PEvalOrdTerm t => !(Term t) -> !(Term t) -> UTerm Bool
- ULeOrdTerm :: PEvalOrdTerm t => !(Term t) -> !(Term t) -> UTerm Bool
- UAndBitsTerm :: PEvalBitwiseTerm t => !(Term t) -> !(Term t) -> UTerm t
- UOrBitsTerm :: PEvalBitwiseTerm t => !(Term t) -> !(Term t) -> UTerm t
- UXorBitsTerm :: PEvalBitwiseTerm t => !(Term t) -> !(Term t) -> UTerm t
- UComplementBitsTerm :: PEvalBitwiseTerm t => !(Term t) -> UTerm t
- UShiftLeftTerm :: PEvalShiftTerm t => !(Term t) -> !(Term t) -> UTerm t
- UShiftRightTerm :: PEvalShiftTerm t => !(Term t) -> !(Term t) -> UTerm t
- URotateLeftTerm :: PEvalRotateTerm t => !(Term t) -> !(Term t) -> UTerm t
- URotateRightTerm :: PEvalRotateTerm t => !(Term t) -> !(Term t) -> UTerm t
- UToSignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => !(Term (u n)) -> UTerm (s n)
- UToUnsignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => !(Term (s n)) -> UTerm (u n)
- UBVConcatTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r)) => !(Term (bv l)) -> !(Term (bv r)) -> UTerm (bv (l + r))
- UBVSelectTerm :: (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => !(TypeRep ix) -> !(TypeRep w) -> !(Term (bv n)) -> UTerm (bv w)
- UBVExtendTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => !Bool -> !(TypeRep r) -> !(Term (bv l)) -> UTerm (bv r)
- UApplyTerm :: (SupportedPrim a, SupportedPrim b, SupportedPrim f, PEvalApplyTerm f a b) => Term f -> Term a -> UTerm b
- UDivIntegralTerm :: PEvalDivModIntegralTerm t => !(Term t) -> !(Term t) -> UTerm t
- UModIntegralTerm :: PEvalDivModIntegralTerm t => !(Term t) -> !(Term t) -> UTerm t
- UQuotIntegralTerm :: PEvalDivModIntegralTerm t => !(Term t) -> !(Term t) -> UTerm t
- URemIntegralTerm :: PEvalDivModIntegralTerm t => !(Term t) -> !(Term t) -> UTerm t
- prettyPrintTerm :: Term t -> Doc ann
- constructUnary :: forall tag arg t. (SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t, Show tag) => tag -> Term arg -> Term t
- constructBinary :: forall tag arg1 arg2 t. (SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term t
- constructTernary :: forall tag arg1 arg2 arg3 t. (SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
- conTerm :: (SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) => t -> Term t
- symTerm :: forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
- ssymTerm :: (SupportedPrim t, Typeable t) => Identifier -> Term t
- isymTerm :: (SupportedPrim t, Typeable t) => Identifier -> Int -> Term t
- notTerm :: Term Bool -> Term Bool
- orTerm :: Term Bool -> Term Bool -> Term Bool
- andTerm :: Term Bool -> Term Bool -> Term Bool
- eqTerm :: SupportedPrim a => Term a -> Term a -> Term Bool
- iteTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a
- addNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a
- negNumTerm :: PEvalNumTerm a => Term a -> Term a
- mulNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a
- absNumTerm :: PEvalNumTerm a => Term a -> Term a
- signumNumTerm :: PEvalNumTerm a => Term a -> Term a
- ltOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool
- leOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool
- andBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a -> Term a
- orBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a -> Term a
- xorBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a -> Term a
- complementBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a
- shiftLeftTerm :: PEvalShiftTerm a => Term a -> Term a -> Term a
- shiftRightTerm :: PEvalShiftTerm a => Term a -> Term a -> Term a
- rotateLeftTerm :: PEvalRotateTerm a => Term a -> Term a -> Term a
- rotateRightTerm :: PEvalRotateTerm a => Term a -> Term a -> Term a
- toSignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => Term (u n) -> Term (s n)
- toUnsignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => Term (s n) -> Term (u n)
- bvconcatTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r)) => Term (bv l) -> Term (bv r) -> Term (bv (l + r))
- bvselectTerm :: forall bv n ix w p q. (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (bv n) -> Term (bv w)
- bvextendTerm :: forall bv l r proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (bv l) -> Term (bv r)
- bvsignExtendTerm :: forall bv l r proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => proxy r -> Term (bv l) -> Term (bv r)
- bvzeroExtendTerm :: forall bv l r proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => proxy r -> Term (bv l) -> Term (bv r)
- applyTerm :: (SupportedPrim a, SupportedPrim b, SupportedPrim f, PEvalApplyTerm f a b) => Term f -> Term a -> Term b
- divIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
- modIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
- quotIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
- remIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a
- trueTerm :: Term Bool
- falseTerm :: Term Bool
- pattern BoolConTerm :: Bool -> Term a
- pattern TrueTerm :: Term a
- pattern FalseTerm :: Term a
- pattern BoolTerm :: Term Bool -> Term a
- pevalNotTerm :: Term Bool -> Term Bool
- pevalOrTerm :: Term Bool -> Term Bool -> Term Bool
- pevalAndTerm :: Term Bool -> Term Bool -> Term Bool
- pevalImplyTerm :: Term Bool -> Term Bool -> Term Bool
- pevalXorTerm :: Term Bool -> Term Bool -> Term Bool
- pevalITEBasic :: SupportedPrim a => Term Bool -> Term a -> Term a -> Maybe (Term a)
- pevalITEBasicTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a
- pevalDefaultEqTerm :: SupportedPrim a => Term a -> Term a -> Term Bool
- class (SupportedPrim a, Ord a) => NonFuncSBVRep a where
- type NonFuncSBVBaseType (n :: Nat) a
- class NonFuncSBVRep a => SupportedNonFuncPrim a where
- conNonFuncSBVTerm :: KnownIsZero n => proxy n -> a -> SBV (NonFuncSBVBaseType n a)
- symNonFuncSBVTerm :: (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n a))
- withNonFuncPrim :: KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a), Mergeable (SBVType n a), SMTDefinable (SBVType n a), Mergeable (SBVType n a), SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) => r) -> r
- class SBVRep t where
- class Monad m => SBVFreshMonad m where
- translateTypeError :: HasCallStack => Maybe String -> TypeRep a -> b
- parseSMTModelResultError :: TypeRep a -> ([([CV], CV)], CV) -> a
- partitionCVArg :: forall a. SupportedNonFuncPrim a => [([CV], CV)] -> [(a, [([CV], CV)])]
Supported primitive types
class SupportedPrimConstraint t Source #
type PrimConstraint (n :: Nat) t :: Constraint Source #
type PrimConstraint _ _ = ()
Instances
SupportedPrimConstraint Integer Source # | |
SupportedPrimConstraint Bool Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type PrimConstraint n Bool Source # | |
(KnownNat w, 1 <= w) => SupportedPrimConstraint (IntN w) Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type PrimConstraint n (IntN w) Source # | |
(KnownNat w, 1 <= w) => SupportedPrimConstraint (WordN w) Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type PrimConstraint n (WordN w) Source # | |
(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a --> b) Source # | |
Defined in Grisette.Internal.SymPrim.GeneralFun type PrimConstraint n (a --> b) Source # | |
(SupportedNonFuncPrim a, SupportedPrim b) => SupportedPrimConstraint (a =-> b) Source # | |
Defined in Grisette.Internal.SymPrim.TabularFun type PrimConstraint n (a =-> b) Source # |
class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t, SupportedPrimConstraint t, SBVRep t) => SupportedPrim t where Source #
Indicates that a type is supported and can be represented as a symbolic term.
termCache :: Cache (Term t) Source #
pformatCon :: t -> String Source #
default pformatCon :: Show t => t -> String Source #
pformatSym :: TypedSymbol t -> String Source #
defaultValue :: t Source #
defaultValueDynamic :: proxy t -> ModelValue Source #
pevalITETerm :: Term Bool -> Term t -> Term t -> Term t Source #
pevalEqTerm :: Term t -> Term t -> Term Bool Source #
conSBVTerm :: KnownIsZero n => proxy n -> t -> SBVType n t Source #
symSBVName :: TypedSymbol t -> Int -> String Source #
symSBVTerm :: (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBVType n t) Source #
withPrim :: KnownIsZero n => p n -> ((PrimConstraint n t, SMTDefinable (SBVType n t), Mergeable (SBVType n t), Typeable (SBVType n t)) => a) -> a Source #
default withPrim :: (PrimConstraint n t, SMTDefinable (SBVType n t), Mergeable (SBVType n t), Typeable (SBVType n t), KnownIsZero n) => p n -> ((PrimConstraint n t, SMTDefinable (SBVType n t), Mergeable (SBVType n t), Typeable (SBVType n t)) => a) -> a Source #
sbvIte :: KnownIsZero n => proxy n -> SBV Bool -> SBVType n t -> SBVType n t -> SBVType n t Source #
sbvEq :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBV Bool Source #
default sbvEq :: (KnownIsZero n, EqSymbolic (SBVType n t)) => proxy n -> SBVType n t -> SBVType n t -> SBV Bool Source #
parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> t Source #
Instances
class SupportedPrim con => SymRep con Source #
Type family to resolve the symbolic type associated with a concrete type.
Instances
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 | |
(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 SymBool Source # | |
Defined in Grisette.Internal.SymPrim.SymBool | |
ConRep SymInteger Source # | |
Defined in Grisette.Internal.SymPrim.SymInteger 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 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
LinkedRep Integer SymInteger Source # | |
Defined in Grisette.Internal.SymPrim.SymInteger underlyingTerm :: SymInteger -> Term Integer Source # | |
LinkedRep Bool SymBool Source # | |
(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source # | |
(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source # | |
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim ca, SupportedPrim cb, SupportedPrim (ca --> cb)) => LinkedRep (ca --> cb) (sa -~> sb) Source # | |
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => LinkedRep (ca =-> cb) (sa =~> sb) Source # | |
Partial evaluation for the terms
class (SupportedPrim arg, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => UnaryOp tag arg t | tag arg -> t where Source #
class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => BinaryOp tag arg1 arg2 t | tag arg1 arg2 -> t where Source #
class (SupportedPrim arg1, SupportedPrim arg2, SupportedPrim arg3, SupportedPrim t, Lift tag, NFData tag, Show tag, Typeable tag, Eq tag, Hashable tag) => TernaryOp tag arg1 arg2 arg3 t | tag arg1 arg2 arg3 -> t where Source #
class (SupportedPrim f, SupportedPrim a, SupportedPrim b) => PEvalApplyTerm f a b | f -> a b where Source #
pevalApplyTerm :: Term f -> Term a -> Term b Source #
sbvApplyTerm :: KnownIsZero n => proxy n -> SBVType n f -> SBVType n a -> SBVType n b Source #
Instances
(SupportedPrim (a --> b), SupportedNonFuncPrim a, SupportedPrim b) => PEvalApplyTerm (a --> b) a b Source # | |
Defined in Grisette.Internal.SymPrim.GeneralFun | |
(SupportedPrim a, SupportedPrim b, SupportedPrim (a =-> b)) => PEvalApplyTerm (a =-> b) a b Source # | |
Defined in Grisette.Internal.SymPrim.TabularFun |
class (SupportedPrim t, Bits t) => PEvalBitwiseTerm t where Source #
pevalAndBitsTerm, pevalOrBitsTerm, pevalXorBitsTerm, pevalComplementBitsTerm, withSbvBitwiseTermConstraint
pevalAndBitsTerm :: Term t -> Term t -> Term t Source #
pevalOrBitsTerm :: Term t -> Term t -> Term t Source #
pevalXorBitsTerm :: Term t -> Term t -> Term t Source #
pevalComplementBitsTerm :: Term t -> Term t Source #
withSbvBitwiseTermConstraint :: KnownIsZero n => proxy n -> (Bits (SBVType n t) => r) -> r Source #
sbvAndBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
sbvOrBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
sbvXorBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
sbvComplementBitsTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t Source #
Instances
class (SupportedNonFuncPrim t, SymShift t) => PEvalShiftTerm t where Source #
pevalShiftLeftTerm :: Term t -> Term t -> Term t Source #
pevalShiftRightTerm :: Term t -> Term t -> Term t Source #
withSbvShiftTermConstraint :: KnownIsZero n => proxy n -> (SIntegral (NonFuncSBVBaseType n t) => r) -> r Source #
sbvShiftLeftTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
sbvShiftRightTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
Instances
class (SupportedNonFuncPrim t, SymRotate t) => PEvalRotateTerm t where Source #
pevalRotateLeftTerm :: Term t -> Term t -> Term t Source #
pevalRotateRightTerm :: Term t -> Term t -> Term t Source #
withSbvRotateTermConstraint :: KnownIsZero n => proxy n -> (SIntegral (NonFuncSBVBaseType n t) => r) -> r Source #
sbvRotateLeftTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
sbvRotateRightTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
Instances
class (SupportedPrim t, Num t) => PEvalNumTerm t where Source #
pevalAddNumTerm, pevalNegNumTerm, pevalMulNumTerm, pevalAbsNumTerm, pevalSignumNumTerm, withSbvNumTermConstraint
pevalAddNumTerm :: Term t -> Term t -> Term t Source #
pevalNegNumTerm :: Term t -> Term t Source #
pevalMulNumTerm :: Term t -> Term t -> Term t Source #
pevalAbsNumTerm :: Term t -> Term t Source #
pevalSignumNumTerm :: Term t -> Term t Source #
withSbvNumTermConstraint :: KnownIsZero n => proxy n -> (Num (SBVType n t) => r) -> r Source #
sbvAddNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
sbvNegNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t Source #
sbvMulNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
sbvAbsNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t Source #
sbvSignumNumTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t Source #
Instances
pevalSubNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a Source #
class (SupportedPrim t, Ord t) => PEvalOrdTerm t where Source #
pevalLtOrdTerm :: Term t -> Term t -> Term Bool Source #
pevalLeOrdTerm :: Term t -> Term t -> Term Bool Source #
withSbvOrdTermConstraint :: KnownIsZero n => proxy n -> (OrdSymbolic (SBVType n t) => r) -> r Source #
sbvLtOrdTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBV Bool Source #
sbvLeOrdTerm :: KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBV Bool Source #
Instances
pevalGtOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool Source #
pevalGeOrdTerm :: PEvalOrdTerm a => Term a -> Term a -> Term Bool Source #
pevalNEqTerm :: SupportedPrim a => Term a -> Term a -> Term Bool Source #
class (SupportedPrim t, Integral t) => PEvalDivModIntegralTerm t where Source #
pevalDivIntegralTerm, pevalModIntegralTerm, pevalQuotIntegralTerm, pevalRemIntegralTerm, withSbvDivModIntegralTermConstraint
pevalDivIntegralTerm :: Term t -> Term t -> Term t Source #
pevalModIntegralTerm :: Term t -> Term t -> Term t Source #
pevalQuotIntegralTerm :: Term t -> Term t -> Term t Source #
pevalRemIntegralTerm :: Term t -> Term t -> Term t Source #
withSbvDivModIntegralTermConstraint :: KnownIsZero n => proxy n -> (SDivisible (SBVType n t) => r) -> r Source #
sbvDivIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
sbvModIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
sbvQuotIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
sbvRemIntegralTerm :: forall proxy n. KnownIsZero n => proxy n -> SBVType n t -> SBVType n t -> SBVType n t Source #
Instances
class (PEvalBVTerm s, PEvalBVTerm u, forall n. (KnownNat n, 1 <= n) => SupportedNonFuncPrim (u n), forall n. (KnownNat n, 1 <= n) => SupportedNonFuncPrim (s n), forall n. (KnownNat n, 1 <= n) => SignConversion (u n) (s n)) => PEvalBVSignConversionTerm u s | u -> s, s -> u where Source #
pevalBVToSignedTerm :: (KnownNat n, 1 <= n) => Term (u n) -> Term (s n) Source #
pevalBVToUnsignedTerm :: (KnownNat n, 1 <= n) => Term (s n) -> Term (u n) Source #
withSbvSignConversionTermConstraint :: forall n integerBitwidth p q r. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => p n -> q integerBitwidth -> ((Integral (NonFuncSBVBaseType integerBitwidth (u n)), Integral (NonFuncSBVBaseType integerBitwidth (s n))) => r) -> r Source #
sbvToSigned :: forall n integerBitwidth o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o u -> p n -> q integerBitwidth -> SBVType integerBitwidth (u n) -> SBVType integerBitwidth (s n) Source #
sbvToUnsigned :: forall n integerBitwidth o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o s -> p n -> q integerBitwidth -> SBVType integerBitwidth (s n) -> SBVType integerBitwidth (u n) Source #
Instances
PEvalBVSignConversionTerm WordN IntN Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval pevalBVToSignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (WordN n) -> Term (IntN n) Source # pevalBVToUnsignedTerm :: forall (n :: Nat). (KnownNat n, 1 <= n) => Term (IntN n) -> Term (WordN n) Source # withSbvSignConversionTermConstraint :: forall (n :: Nat) (integerBitwidth :: Nat) p q r. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => p n -> q integerBitwidth -> ((Integral (NonFuncSBVBaseType integerBitwidth (WordN n)), Integral (NonFuncSBVBaseType integerBitwidth (IntN n))) => r) -> r Source # sbvToSigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o WordN -> p n -> q integerBitwidth -> SBVType integerBitwidth (WordN n) -> SBVType integerBitwidth (IntN n) Source # sbvToUnsigned :: forall (n :: Nat) (integerBitwidth :: Nat) o p q. (KnownIsZero integerBitwidth, KnownNat n, 1 <= n) => o IntN -> p n -> q integerBitwidth -> SBVType integerBitwidth (IntN n) -> SBVType integerBitwidth (WordN n) Source # |
class (forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n), SizedBV bv, Typeable bv) => PEvalBVTerm bv where Source #
pevalBVConcatTerm :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (bv l) -> Term (bv r) -> Term (bv (l + r)) Source #
pevalBVExtendTerm :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (bv l) -> Term (bv r) Source #
pevalBVSelectTerm :: (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (bv n) -> Term (bv w) Source #
sbvBVConcatTerm :: (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (bv l) -> SBVType n (bv r) -> SBVType n (bv (l + r)) Source #
sbvBVExtendTerm :: (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (bv l) -> SBVType n (bv r) Source #
sbvBVSelectTerm :: (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (bv n) -> SBVType int (bv w) Source #
Instances
PEvalBVTerm IntN Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (IntN l) -> Term (IntN r) -> Term (IntN (l + r)) Source # pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (IntN l) -> Term (IntN r) Source # pevalBVSelectTerm :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (IntN n) -> Term (IntN w) Source # sbvBVConcatTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (IntN l) -> SBVType n (IntN r) -> SBVType n (IntN (l + r)) Source # sbvBVExtendTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (IntN l) -> SBVType n (IntN r) Source # sbvBVSelectTerm :: forall (int :: Nat) (ix :: Nat) (w :: Nat) (n :: Nat) p0 p1 p2 p3. (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (IntN n) -> SBVType int (IntN w) Source # | |
PEvalBVTerm WordN Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.BVPEval pevalBVConcatTerm :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => Term (WordN l) -> Term (WordN r) -> Term (WordN (l + r)) Source # pevalBVExtendTerm :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (WordN l) -> Term (WordN r) Source # pevalBVSelectTerm :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (WordN n) -> Term (WordN w) Source # sbvBVConcatTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r) => p0 n -> p1 l -> p2 r -> SBVType n (WordN l) -> SBVType n (WordN r) -> SBVType n (WordN (l + r)) Source # sbvBVExtendTerm :: forall (n :: Nat) (l :: Nat) (r :: Nat) p0 p1 p2. (KnownIsZero n, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => p0 n -> p1 l -> p2 r -> Bool -> SBVType n (WordN l) -> SBVType n (WordN r) Source # sbvBVSelectTerm :: forall (int :: Nat) (ix :: Nat) (w :: Nat) (n :: Nat) p0 p1 p2 p3. (KnownIsZero int, KnownNat ix, KnownNat w, KnownNat n, 1 <= n, 1 <= w, (ix + w) <= n) => p0 int -> p1 ix -> p2 w -> p3 n -> SBVType int (WordN n) -> SBVType int (WordN w) Source # |
Typed symbols
data TypedSymbol t where Source #
A typed symbol is a symbol that is associated with a type. Note that the same symbol bodies with different types are considered different symbols and can coexist in a term.
Simple symbols can be created with the OverloadedStrings
extension:
>>>
:set -XOverloadedStrings
>>>
"a" :: TypedSymbol Bool
a :: Bool
TypedSymbol | |
|
Instances
data SomeTypedSymbol where Source #
SomeTypedSymbol :: forall t. TypeRep t -> TypedSymbol t -> SomeTypedSymbol |
Instances
showUntyped :: TypedSymbol t -> String Source #
withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a Source #
someTypedSymbol :: forall t. TypedSymbol t -> SomeTypedSymbol Source #
Terms
Instances
identityWithTypeRep :: forall t. Term t -> (SomeTypeRep, Id) Source #
introSupportedPrimConstraint :: forall t a. Term t -> (SupportedPrim t => a) -> a Source #
Interning
prettyPrintTerm :: Term t -> Doc ann Source #
constructUnary :: forall tag arg t. (SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t, Show tag) => tag -> Term arg -> Term t Source #
constructBinary :: forall tag arg1 arg2 t. (SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term t Source #
constructTernary :: forall tag arg1 arg2 arg3 t. (SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t, Show tag) => tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t Source #
ssymTerm :: (SupportedPrim t, Typeable t) => Identifier -> Term t Source #
isymTerm :: (SupportedPrim t, Typeable t) => Identifier -> Int -> Term t Source #
addNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a Source #
negNumTerm :: PEvalNumTerm a => Term a -> Term a Source #
mulNumTerm :: PEvalNumTerm a => Term a -> Term a -> Term a Source #
absNumTerm :: PEvalNumTerm a => Term a -> Term a Source #
signumNumTerm :: PEvalNumTerm a => Term a -> Term a Source #
andBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a -> Term a Source #
orBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a -> Term a Source #
xorBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a -> Term a Source #
complementBitsTerm :: PEvalBitwiseTerm a => Term a -> Term a Source #
shiftLeftTerm :: PEvalShiftTerm a => Term a -> Term a -> Term a Source #
shiftRightTerm :: PEvalShiftTerm a => Term a -> Term a -> Term a Source #
rotateLeftTerm :: PEvalRotateTerm a => Term a -> Term a -> Term a Source #
rotateRightTerm :: PEvalRotateTerm a => Term a -> Term a -> Term a Source #
toSignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => Term (u n) -> Term (s n) Source #
toUnsignedTerm :: (PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) => Term (s n) -> Term (u n) Source #
bvconcatTerm :: (PEvalBVTerm bv, KnownNat l, KnownNat r, KnownNat (l + r), 1 <= l, 1 <= r, 1 <= (l + r)) => Term (bv l) -> Term (bv r) -> Term (bv (l + r)) Source #
bvselectTerm :: forall bv n ix w p q. (PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> Term (bv n) -> Term (bv w) Source #
bvextendTerm :: forall bv l r proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => Bool -> proxy r -> Term (bv l) -> Term (bv r) Source #
bvsignExtendTerm :: forall bv l r proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => proxy r -> Term (bv l) -> Term (bv r) Source #
bvzeroExtendTerm :: forall bv l r proxy. (PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) => proxy r -> Term (bv l) -> Term (bv r) Source #
applyTerm :: (SupportedPrim a, SupportedPrim b, SupportedPrim f, PEvalApplyTerm f a b) => Term f -> Term a -> Term b Source #
divIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a Source #
modIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a Source #
quotIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a Source #
remIntegralTerm :: PEvalDivModIntegralTerm a => Term a -> Term a -> Term a Source #
Support for boolean type
pattern BoolConTerm :: Bool -> Term a Source #
pevalITEBasic :: SupportedPrim a => Term Bool -> Term a -> Term a -> Maybe (Term a) Source #
pevalITEBasicTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a Source #
pevalDefaultEqTerm :: SupportedPrim a => Term a -> Term a -> Term Bool Source #
class (SupportedPrim a, Ord a) => NonFuncSBVRep a Source #
type NonFuncSBVBaseType (n :: Nat) a Source #
Instances
NonFuncSBVRep Integer Source # | |
NonFuncSBVRep Bool Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.Term type NonFuncSBVBaseType n Bool Source # | |
(KnownNat w, 1 <= w) => NonFuncSBVRep (IntN w) Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type NonFuncSBVBaseType n (IntN w) Source # | |
(KnownNat w, 1 <= w) => NonFuncSBVRep (WordN w) Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type NonFuncSBVBaseType n (WordN w) Source # |
class NonFuncSBVRep a => SupportedNonFuncPrim a where Source #
conNonFuncSBVTerm :: KnownIsZero n => proxy n -> a -> SBV (NonFuncSBVBaseType n a) Source #
symNonFuncSBVTerm :: (SBVFreshMonad m, KnownIsZero n) => proxy n -> String -> m (SBV (NonFuncSBVBaseType n a)) Source #
withNonFuncPrim :: KnownIsZero n => proxy n -> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a), Mergeable (SBVType n a), SMTDefinable (SBVType n a), Mergeable (SBVType n a), SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) => r) -> r Source #
Instances
Instances
SBVRep Integer Source # | |
SBVRep Bool Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Internal.Term | |
(KnownNat w, 1 <= w) => SBVRep (IntN w) Source # | |
(KnownNat w, 1 <= w) => SBVRep (WordN w) Source # | |
(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a --> b) Source # | |
Defined in Grisette.Internal.SymPrim.GeneralFun | |
(SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a =-> b) Source # | |
Defined in Grisette.Internal.SymPrim.TabularFun |
class Monad m => SBVFreshMonad m where Source #
Instances
MonadIO m => SBVFreshMonad (QueryT m) Source # | |
MonadIO m => SBVFreshMonad (SymbolicT m) Source # | |
SBVFreshMonad m => SBVFreshMonad (ReaderT r m) Source # | |
SBVFreshMonad m => SBVFreshMonad (StateT s m) Source # | |
translateTypeError :: HasCallStack => Maybe String -> TypeRep a -> b Source #
partitionCVArg :: forall a. SupportedNonFuncPrim a => [([CV], CV)] -> [(a, [([CV], CV)])] Source #