| 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 BitwidthMismatch = BitwidthMismatch
- 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) -> SomeBV bv -> r
- unarySomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n) -> SomeBV bv -> SomeBV bv
- binSomeBV :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> SomeBV bv -> SomeBV bv -> r
- binSomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> SomeBV bv -> SomeBV bv -> SomeBV bv
- binSomeBVR2 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
- binSomeBVSafe :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, Mergeable r) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) -> SomeBV bv -> SomeBV bv -> m r
- binSomeBVSafeR1 :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
- binSomeBVSafeR2 :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> 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 a =-> b = TabularFun {
- funcTable :: [(a, b)]
- defaultFuncValue :: b
- data a --> b
- (-->) :: (SupportedPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedSymbol 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
- data sa =~> sb where
- data sa -~> sb where
- class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData 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
- 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 TypedSymbol t where
- TypedSymbol :: SupportedPrim t => {..} -> TypedSymbol t
- data SymbolSet
- data Model
- data ModelValuePair t = (TypedSymbol t) ::= t
- data ModelSymPair ct st where
- (:=) :: LinkedRep ct st => st -> ct -> ModelSymPair ct st
Documentation
Grisette introduces new primitive types:
IntNnn.WordNnn.FPeb sbebexponent bits andsbsignificand bits.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)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 (TypedSymbol), symbol sets (SymbolSet),
and models (Model). They are useful when working with
EvalSym, 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.
>>>:set -XOverloadedStrings -XDataKinds -XBinaryLiterals>>>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.
>>>:set -XOverloadedStrings -XDataKinds -XBinaryLiterals>>>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
Instances
data BitwidthMismatch Source #
An exception that would be thrown when operations are performed on incompatible bit widths.
Constructors
| BitwidthMismatch |
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) -> 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) -> SomeBV bv -> SomeBV bv Source #
binSomeBV :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> 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) => bv n -> bv n -> bv n) -> SomeBV bv -> SomeBV bv -> SomeBV bv Source #
binSomeBVR2 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv) Source #
binSomeBVSafe :: (MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e, Mergeable r) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT 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 BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> 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 BitwidthMismatch e) m, TryMerge m, Mergeable e, forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> 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.
>>>:set -XDataKinds>>>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.
Functions
data a =-> b infixr 0 Source #
Functions as a table. Use the # operator to apply the function.
>>>:set -XTypeOperators>>>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.
>>>:set -XOverloadedStrings>>>:set -XTypeOperators>>>let f = ("x" :: TypedSymbol 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
(-->) :: (SupportedPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedSymbol ca -> sb -> ca --> cb infixr 0 Source #
Construction of general symbolic functions.
>>>f = "a" --> "a" + 1 :: Integer --> Integer>>>f\(a:ARG :: Integer) -> (+ 1 a:ARG)
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.
>>>:set -XOverloadedStrings>>>"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.
>>>:set -XOverloadedStrings -XDataKinds -XBinaryLiterals>>>"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.
>>>:set -XOverloadedStrings -XDataKinds -XBinaryLiterals>>>"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.
>>>:set -XOverloadedStrings -XDataKinds>>>"a" + 2.0 :: SymFP 11 53(+ a 2.0)>>>symFpAdd 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 function, possibly uninterpreted
data sa =~> sb where infixr 0 Source #
Symbolic tabular function type.
>>>:set -XTypeOperators -XOverloadedStrings>>>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))
Instances
data sa -~> sb where infixr 0 Source #
Symbolic general function type.
>>>:set -XTypeOperators -XOverloadedStrings>>>f' = "f" :: SymInteger -~> SymInteger>>>f = (f' #)>>>f 1(apply f 1)
>>>f' = con ("a" --> "a" + 1) :: SymInteger -~> SymInteger>>>f'\(a:ARG :: Integer) -> (+ 1 a:ARG)>>>f = (f' #)>>>f 12>>>f 23>>>f 34>>>f "b"(+ 1 b)
Instances
Basic constraints
class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData 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, conSBVTerm, symSBVName, symSBVTerm, parseSMTModelResult
Instances
class SupportedPrim con => SymRep con Source #
Type family to resolve the symbolic type associated with a concrete type.
Instances
| 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 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 Source #
One-to-one mapping between symbolic types and concrete types.
Minimal complete definition
Instances
| LinkedRep FPRoundingMode SymFPRoundingMode Source # | |
Defined in Grisette.Internal.SymPrim.SymFP Methods underlyingTerm :: SymFPRoundingMode -> Term FPRoundingMode Source # wrapTerm :: Term FPRoundingMode -> SymFPRoundingMode Source # | |
| LinkedRep Integer SymInteger Source # | |
Defined in Grisette.Internal.SymPrim.SymInteger Methods 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 # | |
| ValidFP eb sb => LinkedRep (FP eb sb) (SymFP eb sb) Source # | |
| (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim ca, SupportedPrim cb, SupportedPrim (ca --> cb)) => LinkedRep (ca --> cb) (sa -~> sb) Source # | |
| (LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => LinkedRep (ca =-> cb) (sa =~> sb) Source # | |
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.
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 # | |
Defined in Grisette.Internal.SymPrim.AllSyms | |
| newtype AllSymsArgs Arity1 a Source # | |
Defined in Grisette.Internal.SymPrim.AllSyms | |
class GAllSyms arity f where Source #
The class of types that can generically extract all symbolic primitives.
Instances
| GAllSyms Arity1 Par1 Source # | |
Defined in Grisette.Internal.SymPrim.AllSyms | |
| GAllSyms arity (U1 :: Type -> Type) Source # | |
Defined in Grisette.Internal.SymPrim.AllSyms | |
| GAllSyms arity (V1 :: Type -> Type) Source # | |
Defined in Grisette.Internal.SymPrim.AllSyms | |
| AllSyms1 f => GAllSyms Arity1 (Rec1 f) Source # | |
Defined in Grisette.Internal.SymPrim.AllSyms | |
| (GAllSyms arity a, GAllSyms arity b) => GAllSyms arity (a :*: b) Source # | |
Defined in Grisette.Internal.SymPrim.AllSyms | |
| (GAllSyms arity a, GAllSyms arity b) => GAllSyms arity (a :+: b) Source # | |
Defined in Grisette.Internal.SymPrim.AllSyms | |
| AllSyms c => GAllSyms arity (K1 i c :: Type -> Type) Source # | |
Defined in Grisette.Internal.SymPrim.AllSyms | |
| (AllSyms1 f, GAllSyms Arity1 g) => GAllSyms Arity1 (f :.: g) Source # | |
Defined in Grisette.Internal.SymPrim.AllSyms | |
| GAllSyms arity a => GAllSyms arity (M1 i c a) Source # | |
Defined in Grisette.Internal.SymPrim.AllSyms | |
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 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 Boola :: Bool
Constructors
| TypedSymbol | |
Fields
| |
Instances
Set of symbols.
Check SymbolSetOps for operations, and
SymbolSetRep for manual constructions.
Instances
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
| (TypedSymbol 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 # | |