grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.Class.Solvable

Description

 
Synopsis

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

Solvable Bool SymBool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

(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