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) -> (Integer -> r) -> SomeBV bv -> r
- unarySomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => bv n -> bv n) -> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
- binSomeBV :: (forall n. (KnownNat n, 1 <= n) => Num (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> (Integer -> Integer -> r) -> SomeBV bv -> SomeBV bv -> r
- binSomeBVR1 :: (forall n. (KnownNat n, 1 <= n) => Num (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> (Integer -> Integer -> Integer) -> SomeBV bv -> SomeBV bv -> SomeBV bv
- binSomeBVR2 :: (forall n. (KnownNat n, 1 <= n) => Num (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> (Integer -> Integer -> (Integer, Integer)) -> 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)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) -> (Integer -> Integer -> 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)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> (Integer -> Integer -> ExceptT (Either SomeBVException e) m Integer) -> 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)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> (Integer -> Integer -> ExceptT (Either SomeBVException e) m (Integer, Integer)) -> 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
- data sa -~> sb where
- 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, 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 SymbolKind
- class IsSymbolKind (ty :: SymbolKind) where
- type SymbolKindConstraint ty :: Type -> Constraint
- decideSymbolKind :: Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind)
- data TypedSymbol (knd :: SymbolKind) t where
- TypedSymbol :: (SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) => {..} -> TypedSymbol knd t
- type TypedAnySymbol = TypedSymbol 'AnyKind
- type TypedConstantSymbol = TypedSymbol 'ConstantKind
- data SomeTypedSymbol knd where
- SomeTypedSymbol :: forall knd t. TypeRep 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
Documentation
Grisette introduces new primitive types:
: signed bit vectors of bit widthIntN
nn
.
: unsigned bit vectors of bit widthWordN
nn
.
: IEEE-754 floating point numbers withFP
eb sbeb
exponent bits andsb
significand 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.
: functions represented as a table for the input-output relations.Bool
=->
Bool
: functions represented as a formula over some bound variables.Bool
-->
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)
(SymIntN
n
, symbolic signed bit vectors of bit widthIntN
nn
)
(SymWordN
n
, symbolic unsigned bit vectors of bit widthWordN
nn
)
(SymFP
eb sb
, symbolic IEEE-754 floating point numbers withFP
eb sbeb
exponent bits andsb
significand bits)SymAlgReal
: symbolic algebraic real numbers.
(SymBool
=~>
SymBool
, symbolic functions, uninterpreted or represented as a table for the input-output relations).Bool
=->
Bool
(SymBool
-~>
SymBool
, symbolic functions, uninterpreted or represented as a formula over some bound variables).Bool
-->
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 (
), symbol sets
(TypedSymbol
), and models (SymbolSet
). They are useful when working
with Model
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.
>>>
3 + 5 :: IntN 5
0b01000>>>
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 5
0b01000>>>
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 IntN
0xf
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 IntN
0x6>>>
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 IntN
bvlit(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) -> (Integer -> 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) -> (Integer -> Integer) -> SomeBV bv -> SomeBV bv Source #
binSomeBV :: (forall n. (KnownNat n, 1 <= n) => Num (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) -> (Integer -> Integer -> 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)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) -> (Integer -> Integer -> Integer) -> SomeBV bv -> SomeBV bv -> SomeBV bv Source #
binSomeBVR2 :: (forall n. (KnownNat n, 1 <= n) => Num (bv n)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) -> (Integer -> Integer -> (Integer, Integer)) -> 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)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) -> (Integer -> Integer -> 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)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) -> (Integer -> Integer -> ExceptT (Either SomeBVException e) m Integer) -> 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)) => (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n, bv n)) -> (Integer -> Integer -> ExceptT (Either SomeBVException e) m (Integer, Integer)) -> 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 53
3.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
Generic RealPoint Source # | |
NFData RealPoint Source # | |
Defined in Grisette.Internal.SymPrim.AlgReal | |
Eq RealPoint Source # | |
Mergeable RealPoint Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods | |
Hashable RealPoint Source # | |
Defined in Grisette.Internal.SymPrim.AlgReal | |
Lift RealPoint Source # | |
type Rep RealPoint Source # | |
Defined in Grisette.Internal.SymPrim.AlgReal type Rep RealPoint = D1 ('MetaData "RealPoint" "Grisette.Internal.SymPrim.AlgReal" "grisette-0.8.0.0-9ziui23pS5H4p62qxsVv1c" 'False) (C1 ('MetaCons "OpenPoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational)) :+: C1 ('MetaCons "ClosedPoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational))) |
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 # 1
2>>>
f # 2
0>>>
f # 3
4
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
(-->) :: (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
\(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.
>>>
"a" :: SymBool
a>>>
"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 1
2>>>
f 2
3>>>
f 3
4>>>
f "b"
(ite (= b 1) 2 (ite (= b 2) 3 4))
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'
\(a:ARG :: Integer) -> (+ 1 a:ARG)>>>
f = (f' #)
>>>
f 1
2>>>
f 2
3>>>
f 3
4>>>
f "b"
(+ 1 b)
Instances
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, 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, pevalDistinctTerm, conSBVTerm, symSBVName, symSBVTerm, parseSMTModelResult, castTypedSymbol, isFuncType, 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 Source #
One-to-one mapping between symbolic types and concrete types.
Minimal complete definition
Instances
LinkedRep AlgReal SymAlgReal Source # | |
Defined in Grisette.Internal.SymPrim.SymAlgReal Methods underlyingTerm :: SymAlgReal -> Term AlgReal Source # | |
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 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 (ty :: SymbolKind) where Source #
Decision procedure for symbol kinds.
Associated Types
type SymbolKindConstraint ty :: Type -> Constraint Source #
Methods
decideSymbolKind :: Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind) 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 # | |
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 # |
data TypedSymbol (knd :: SymbolKind) t where Source #
A typed symbol is a symbol that is associated with a type. Note that the same symbol bodies with different types are considered different symbols and can coexist in a term.
Simple symbols can be created with the OverloadedStrings
extension:
>>>
"a" :: TypedSymbol 'AnyKind Bool
a :: Bool
Constructors
TypedSymbol | |
Fields
|
Instances
type TypedAnySymbol = TypedSymbol 'AnyKind Source #
Any symbol
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. TypeRep 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) :: Model
Model {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) :: Model
Model {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 # |