| Copyright | (c) Sirui Lu 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.Internal.SymPrim.AllSyms
Description
Synopsis
- 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]
Get all symbolic primitive values in a value
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 | |