| 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
Description
Synopsis
- data IntN (n :: Nat)
- data WordN (n :: Nat)
- data SomeWordN where
- data SomeIntN where
- data a =-> b = TabularFun {
- funcTable :: [(a, b)]
- defaultFuncValue :: b
- data a --> b
- (-->) :: (SupportedPrim ca, SupportedPrim cb, LinkedRep cb sb) => TypedSymbol ca -> sb -> ca --> cb
- class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData 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
- 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
- data TypedSymbol t where
- SimpleSymbol :: SupportedPrim t => String -> TypedSymbol t
- IndexedSymbol :: SupportedPrim t => String -> Int -> TypedSymbol t
- WithInfo :: forall t a. (SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => TypedSymbol t -> a -> TypedSymbol t
- symSize :: forall con sym. LinkedRep con sym => sym -> Int
- symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int
- class AllSyms a where
- allSymsSize :: AllSyms a => a -> Int
- newtype SymbolSet = SymbolSet {}
- newtype Model = Model {}
- data ModelValuePair t = (TypedSymbol t) ::= t
- data ModelSymPair ct st where
- (:=) :: LinkedRep ct st => st -> ct -> ModelSymPair ct st
Symbolic type implementation
Extended types
Symbolic signed bit vectors.
Instances
data WordN (n :: Nat) Source #
Symbolic unsigned bit vectors.
Instances
A non-indexed version of WordN.
Instances
A non-indexed version of IntN.
Instances
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)
Symbolic types
class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t Source #
Indicates that a type is supported and can be represented as a symbolic term.
Minimal complete definition
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.IR.SymPrim.Data.SymPrim | |
| SymRep Bool Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim | |
| (KnownNat n, 1 <= n) => SymRep (IntN n) Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim | |
| (KnownNat n, 1 <= n) => SymRep (WordN n) Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim | |
| (SymRep ca, SymRep cb) => SymRep (ca --> cb) Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim | |
| (SymRep a, SymRep b) => SymRep (a =-> b) Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim | |
Type family to resolve the concrete type associated with a symbolic type.
Instances
| ConRep SymBool Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim | |
| ConRep SymInteger Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim Associated Types type ConType SymInteger Source # | |
| (KnownNat n, 1 <= n) => ConRep (SymIntN n) Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim | |
| (KnownNat n, 1 <= n) => ConRep (SymWordN n) Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim | |
| (ConRep a, ConRep b) => ConRep (a -~> b) Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim | |
| (ConRep a, ConRep b) => ConRep (a =~> b) Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim | |
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 Integer SymInteger Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim 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 # | |
| (LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca --> cb) (sa -~> sb) Source # | |
| (LinkedRep ca sa, LinkedRep cb sb) => LinkedRep (ca =-> cb) (sa =~> sb) Source # | |
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
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
| SimpleSymbol :: SupportedPrim t => String -> TypedSymbol t | |
| IndexedSymbol :: SupportedPrim t => String -> Int -> TypedSymbol t | |
| WithInfo :: forall t a. (SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => TypedSymbol t -> a -> TypedSymbol t |
Instances
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
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
Symbolic constant sets and models
Symbolic constant set.
Constructors
| SymbolSet | |
Fields | |
Instances
Model returned by the solver.
Constructors
| Model | |
Fields | |
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.IR.SymPrim.Data.Prim.Model Methods showsPrec :: Int -> ModelValuePair t -> ShowS # show :: ModelValuePair t -> String # showList :: [ModelValuePair t] -> ShowS # | |
| ModelRep (ModelValuePair t) Model Source # | |
Defined in Grisette.IR.SymPrim.Data.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.IR.SymPrim.Data.SymPrim Methods buildModel :: ModelSymPair ct st -> Model Source # | |