Grisette.Core.Data.Class.Solvable

Solvable type interface

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

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

Methods

con :: c -> t

Wrap a concrete value in a symbolic value.

>>> con True :: SymBool
true

conView :: t -> Maybe c

Extract the concrete value from a symbolic value.

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

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

ssym :: String -> t

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

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

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

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

Solvable Integer SymInteger

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: Integer -> SymInteger

conView :: SymInteger -> Maybe Integer

ssym :: String -> SymInteger

isym :: String -> Int -> SymInteger

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

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

Solvable Bool SymBool

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: Bool -> SymBool

conView :: SymBool -> Maybe Bool

ssym :: String -> SymBool

isym :: String -> Int -> SymBool

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

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

(Solvable c t, Mergeable t) => Solvable c (UnionM t)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

con :: c -> UnionM t

conView :: UnionM t -> Maybe c

ssym :: String -> UnionM t

isym :: String -> Int -> UnionM t

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

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

(KnownNat n, 1 <= n) => Solvable (IntN n) (SymIntN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: IntN n -> SymIntN n

conView :: SymIntN n -> Maybe (IntN n)

ssym :: String -> SymIntN n

isym :: String -> Int -> SymIntN n

sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> SymIntN n

iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> SymIntN n

(KnownNat n, 1 <= n) => Solvable (WordN n) (SymWordN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: WordN n -> SymWordN n

conView :: SymWordN n -> Maybe (WordN n)

ssym :: String -> SymWordN n

isym :: String -> Int -> SymWordN n

sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> SymWordN n

iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> SymWordN n

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Solvable (ca --> cb) (sa -~> sb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: (ca --> cb) -> sa -~> sb

conView :: (sa -~> sb) -> Maybe (ca --> cb)

ssym :: String -> sa -~> sb

isym :: String -> Int -> sa -~> sb

sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> sa -~> sb

iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> sa -~> sb

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Solvable (ca =-> cb) (sa =~> sb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: (ca =-> cb) -> sa =~> sb

conView :: (sa =~> sb) -> Maybe (ca =-> cb)

ssym :: String -> sa =~> sb

isym :: String -> Int -> sa =~> sb

sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> sa =~> sb

iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> sa =~> sb

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

Extract the concrete value from a solvable value with conView.

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