| 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 a =-> b = TabularFun {
- funcTable :: [(a, b)]
- defaultFuncValue :: b
- data a --> b
- (-->) :: (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Sym b -> a --> b
- class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t
- data Sym a
- 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 :: Sym a -> Int
- symsSize :: [Sym a] -> Int
- type SymBool = Sym Bool
- type SymInteger = Sym Integer
- type SymIntN n = Sym (IntN n)
- type SymWordN n = Sym (WordN n)
- type (=~>) a b = Sym (a =-> b)
- type (-~>) a b = Sym (a --> b)
- newtype SymbolSet = SymbolSet {}
- newtype Model = Model {}
- data ModelValuePair t = (TypedSymbol t) ::= t
Symbolic type implementation
Extended types
Symbolic signed bit vectors.
Instances
data WordN (n :: Nat) Source #
Symbolic unsigned bit vectors.
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 a, SupportedPrim b) => TypedSymbol a -> Sym b -> a --> b Source #
Construction of general symbolic functions.
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
Symbolic primitive type.
Symbolic Boolean, integer, and bit vector types are supported.
>>>:set -XOverloadedStrings>>>"a" :: Sym Boola>>>"a" &&~ "b" :: Sym Bool(&& a b)>>>"i" + 1 :: Sym Integer(+ 1 i)
For more symbolic operations, please refer to the documentation of the grisette-core package.
Grisette also supports uninterpreted functions. You can use the -->
(general function) or =-> (tabular function) types to define uninterpreted
functions. The following code shows the examples
>>>:set -XTypeOperators>>>let ftab = "ftab" :: Sym (Integer =-> Integer)>>>ftab # "x"(apply ftab x)
>>> solve (UnboundedReasoning z3) (ftab # 1 ==~ 2 &&~ ftab # 2 ==~ 3 &&~ ftab # 3 ==~ 4)
Right (Model {
ftab ->
TabularFun {funcTable = [(3,4),(2,3)], defaultFuncValue = 2}
:: (=->) Integer Integer
}) -- possible result (reformatted)>>>let fgen = "fgen" :: Sym (Integer --> Integer)>>>fgen # "x"(apply fgen x)
>>> solve (UnboundedReasoning z3) (fgen # 1 ==~ 2 &&~ fgen # 2 ==~ 3 &&~ fgen # 3 ==~ 4)
Right (Model {
fgen ->
\(arg@0:FuncArg :: Integer) ->
(ite (= arg@0:FuncArg 2) 3 (ite (= arg@0:FuncArg 3) 4 2))
:: (-->) Integer Integer
}) -- possible result (reformatted)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 :: Sym a -> Int Source #
Get the size of a symbolic term. Duplicate sub-terms are counted for only once.
symsSize :: [Sym a] -> Int Source #
Get the sum of the sizes of a list of symbolic terms. Duplicate sub-terms are counted for only once.
Symbolic type synonyms
type SymInteger = Sym Integer Source #
Symbolic integer type (unbounded, mathematical integer).
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 |