| Copyright | (c) Sirui Lu 2021-2023 |
|---|---|
| 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.IR.SymPrim.Data.SymPrim
Contents
Description
Synopsis
- newtype SymBool = SymBool {}
- newtype SymInteger = SymInteger {}
- newtype SymWordN (n :: Nat) = SymWordN {
- underlyingWordNTerm :: Term (WordN n)
- newtype SymIntN (n :: Nat) = SymIntN {
- underlyingIntNTerm :: Term (IntN n)
- data SomeSymWordN where
- SomeSymWordN :: (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN
- data SomeSymIntN where
- SomeSymIntN :: (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN
- data sa =~> sb where
- data sa -~> sb where
- (-->) :: (SupportedPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedSymbol ca -> sb -> ca --> cb
- data ModelSymPair ct st where
- (:=) :: LinkedRep ct st => st -> ct -> ModelSymPair ct st
- symSize :: forall con sym. LinkedRep con sym => sym -> Int
- symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int
- data SomeSym where
- class AllSyms a where
- allSymsSize :: AllSyms a => a -> Int
- unarySomeSymIntN :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> r) -> String -> SomeSymIntN -> r
- unarySomeSymIntNR1 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n) -> String -> SomeSymIntN -> SomeSymIntN
- binSomeSymIntN :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> r) -> String -> SomeSymIntN -> SomeSymIntN -> r
- binSomeSymIntNR1 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> SymIntN n) -> String -> SomeSymIntN -> SomeSymIntN -> SomeSymIntN
- binSomeSymIntNR2 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n)) -> String -> SomeSymIntN -> SomeSymIntN -> (SomeSymIntN, SomeSymIntN)
- unarySomeSymWordN :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> r) -> String -> SomeSymWordN -> r
- unarySomeSymWordNR1 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n) -> String -> SomeSymWordN -> SomeSymWordN
- binSomeSymWordN :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> r) -> String -> SomeSymWordN -> SomeSymWordN -> r
- binSomeSymWordNR1 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> SymWordN n) -> String -> SomeSymWordN -> SomeSymWordN -> SomeSymWordN
- binSomeSymWordNR2 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n)) -> String -> SomeSymWordN -> SomeSymWordN -> (SomeSymWordN, SomeSymWordN)
Documentation
Symbolic Boolean type.
>>>:set -XOverloadedStrings>>>"a" :: SymBoola>>>"a" &&~ "b" :: SymBool(&& a b)
More symbolic operations are available. Please refer to the documentation for the type class instances.
Constructors
| SymBool | |
Fields | |
Instances
newtype SymInteger Source #
Symbolic (unbounded, mathematical) integer type.
>>>"a" + 1 :: SymInteger(+ 1 a)
More symbolic operations are available. Please refer to the documentation for the type class instances.
Constructors
| SymInteger | |
Fields | |
Instances
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 symbolic operations are available. Please refer to the documentation for the type class instances.
Constructors
| SymWordN | |
Fields
| |
Instances
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 symbolic operations are available. Please refer to the documentation for the type class instances.
Constructors
| SymIntN | |
Fields
| |
Instances
data SomeSymWordN where Source #
Symbolic unsigned bit vector type. Not indexed, but the bit width is fixed at the creation time.
A SomeSymWordN must be created by wrapping a SymWordN with the
SomeSymWordN constructor to fix the bit width:
>>>(SomeSymWordN ("a" :: SymWordN 5))a
>>>:set -XOverloadedStrings -XDataKinds -XBinaryLiterals>>>(SomeSymWordN ("a" :: SymWordN 5)) + (SomeSymWordN (5 :: SymWordN 5))(+ 0b00101 a)>>>someBVConcat (SomeSymWordN (con 0b101 :: SymWordN 3)) (SomeSymWordN (con 0b110 :: SymWordN 3))0b101110
More symbolic operations are available. Please refer to the documentation for the type class instances.
Constructors
| SomeSymWordN :: (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN |
Instances
data SomeSymIntN where Source #
Symbolic signed bit vector type. Not indexed, but the bit width is fixed at the creation time.
A SomeSymIntN must be created by wrapping a SymIntN with the
SomeSymIntN constructor to fix the bit width:
>>>(SomeSymIntN ("a" :: SymIntN 5))a
>>>:set -XOverloadedStrings -XDataKinds -XBinaryLiterals>>>(SomeSymIntN ("a" :: SymIntN 5)) + (SomeSymIntN (5 :: SymIntN 5))(+ 0b00101 a)>>>someBVConcat (SomeSymIntN (con 0b101 :: SymIntN 3)) (SomeSymIntN (con 0b110 :: SymIntN 3))0b101110
More symbolic operations are available. Please refer to the documentation for the type class instances.
Constructors
| SomeSymIntN :: (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN |
Instances
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
(-->) :: (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)
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.IR.SymPrim.Data.SymPrim Methods buildModel :: ModelSymPair ct st -> Model Source # | |
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
Some symbolic value with LinkedRep constraint.
class AllSyms a where Source #
Extract all symbolic primitive values that are represented as SMT terms.
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
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
unarySomeSymIntN :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> r) -> String -> SomeSymIntN -> r Source #
unarySomeSymIntNR1 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n) -> String -> SomeSymIntN -> SomeSymIntN Source #
binSomeSymIntN :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> r) -> String -> SomeSymIntN -> SomeSymIntN -> r Source #
binSomeSymIntNR1 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> SymIntN n) -> String -> SomeSymIntN -> SomeSymIntN -> SomeSymIntN Source #
binSomeSymIntNR2 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> (SymIntN n, SymIntN n)) -> String -> SomeSymIntN -> SomeSymIntN -> (SomeSymIntN, SomeSymIntN) Source #
unarySomeSymWordN :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> r) -> String -> SomeSymWordN -> r Source #
unarySomeSymWordNR1 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n) -> String -> SomeSymWordN -> SomeSymWordN Source #
binSomeSymWordN :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> r) -> String -> SomeSymWordN -> SomeSymWordN -> r Source #
binSomeSymWordNR1 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> SymWordN n) -> String -> SomeSymWordN -> SomeSymWordN -> SomeSymWordN Source #
binSomeSymWordNR2 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> (SymWordN n, SymWordN n)) -> String -> SomeSymWordN -> SomeSymWordN -> (SomeSymWordN, SomeSymWordN) Source #
Orphan instances
| SymRep Integer Source # | |
| SymRep Bool Source # | |
| LinkedRep Integer SymInteger Source # | |
Methods underlyingTerm :: SymInteger -> Term Integer Source # | |
| LinkedRep Bool SymBool Source # | |
| (KnownNat n, 1 <= n) => SymRep (IntN n) Source # | |
| (KnownNat n, 1 <= n) => SymRep (WordN n) Source # | |
| (KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source # | |
| (KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source # | |
| (SymRep ca, SymRep cb) => SymRep (ca --> cb) Source # | |
| (SymRep a, SymRep b) => SymRep (a =-> b) Source # | |
| (LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca --> cb) (sa -~> sb) Source # | |
| (LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca =-> cb) (sa =~> sb) Source # | |