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	Trustworthy
Language	Haskell2010

Grisette.Core.Data.Class.Solvable

Contents

Solvable type interface

Description

Synopsis

class IsString t => Solvable c t | t -> c where
- con :: c -> t
- conView :: t -> Maybe c
- ssym :: String -> t
- isym :: String -> Int -> t
- sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> t
- iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> t
pattern Con :: Solvable c t => c -> t

Solvable type interface

class IsString t => Solvable c t | t -> c where Source #

The class defines the creation and pattern matching of solvable type values.

Methods

con :: c -> t Source #

Wrap a concrete value in a symbolic value.

>>> con True :: SymBool
true

conView :: t -> Maybe c Source #

Extract the concrete value from a symbolic value.

>>> conView (con True :: SymBool)
Just True

>>> conView (ssym "a" :: SymBool)
Nothing

ssym :: String -> t Source #

Generate simply-named symbolic constants.

Two symbolic constants with the same name are the same symbolic constant, and will always be assigned with the same value by the solver.

>>> ssym "a" :: SymBool
a
>>> (ssym "a" :: SymBool) == ssym "a"
True
>>> (ssym "a" :: SymBool) == ssym "b"
False
>>> (ssym "a" :: SymBool) &&~ ssym "a"
a

isym :: String -> Int -> t Source #

Generate indexed symbolic constants.

Two symbolic constants with the same name but different indices are not the same symbolic constants.

>>> isym "a" 1 :: SymBool
a@1

sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> t Source #

Generate simply-named symbolic constants with some extra information for disambiguation.

Two symbolic constants with the same name but different extra information (including info with different types) are considered to be different.

>>> sinfosym "a" "someInfo" :: SymInteger
a:"someInfo"

iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> t Source #

Generate indexed symbolic constants with some extra information for disambiguation.

Two symbolic constants with the same name and index but different extra information (including info with different types) are considered to be different.

>>> iinfosym "a" 1 "someInfo" :: SymInteger
a@1:"someInfo"

Instances

Instances details

Solvable Integer SymInteger Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods con :: Integer -> SymInteger Source # conView :: SymInteger -> Maybe Integer Source # ssym :: String -> SymInteger Source # isym :: String -> Int -> SymInteger Source # sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> SymInteger Source # iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> SymInteger Source #
Solvable Bool SymBool Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods con :: Bool -> SymBool Source # conView :: SymBool -> Maybe Bool Source # ssym :: String -> SymBool Source # isym :: String -> Int -> SymBool Source # sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> SymBool Source # iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> SymBool Source #
(Solvable c t, Mergeable t) => Solvable c (UnionM t) Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Methods con :: c -> UnionM t Source # conView :: UnionM t -> Maybe c Source # ssym :: String -> UnionM t Source # isym :: String -> Int -> UnionM t Source # sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> UnionM t Source # iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> UnionM t Source #
(KnownNat n, 1 <= n) => Solvable (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods con :: IntN n -> SymIntN n Source # conView :: SymIntN n -> Maybe (IntN n) Source # ssym :: String -> SymIntN n Source # isym :: String -> Int -> SymIntN n Source # sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> SymIntN n Source # iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> SymIntN n Source #
(KnownNat n, 1 <= n) => Solvable (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods con :: WordN n -> SymWordN n Source # conView :: SymWordN n -> Maybe (WordN n) Source # ssym :: String -> SymWordN n Source # isym :: String -> Int -> SymWordN n Source # sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> SymWordN n Source # iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> SymWordN n Source #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Solvable (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods con :: (ca --> cb) -> sa -~> sb Source # conView :: (sa -~> sb) -> Maybe (ca --> cb) Source # ssym :: String -> sa -~> sb Source # isym :: String -> Int -> sa -~> sb Source # sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> sa -~> sb Source # iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> sa -~> sb Source #
(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Solvable (ca =-> cb) (sa =~> sb) Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods con :: (ca =-> cb) -> sa =~> sb Source # conView :: (sa =~> sb) -> Maybe (ca =-> cb) Source # ssym :: String -> sa =~> sb Source # isym :: String -> Int -> sa =~> sb Source # sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> sa =~> sb Source # iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> sa =~> sb Source #

pattern Con :: Solvable c t => c -> t Source #

Extract the concrete value from a solvable value with conView.

>>> case con True :: SymBool of Con v -> v
True