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.Internal.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
- sym :: Symbol -> t
- ssym :: Identifier -> t
- isym :: Identifier -> Int -> t
pattern Con :: Solvable c t => c -> t
slocsym :: Solvable c s => Text -> SpliceQ s
ilocsym :: Solvable c s => Text -> Int -> SpliceQ s

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.

Minimal complete definition

con, conView, sym

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

sym :: Symbol -> t Source #

Generate symbolic constants.

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

>>> sym "a" :: SymBool
a
>>> (sym "a" :: SymBool) == sym "a"
True
>>> (sym "a" :: SymBool) == sym "b"
False
>>> (sym "a" :: SymBool) .&& sym "a"
a
>>> (sym "a" :: SymBool) == isym "a" 1
False

ssym :: Identifier -> t Source #

Generate simply-named symbolic constants.

Two symbolic constants with the same identifier 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 :: Identifier -> Int -> t Source #

Generate indexed symbolic constants.

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

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

Instances

Instances details

Solvable AlgReal SymAlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.SymAlgReal Methods con :: AlgReal -> SymAlgReal Source # conView :: SymAlgReal -> Maybe AlgReal Source # sym :: Symbol -> SymAlgReal Source # ssym :: Identifier -> SymAlgReal Source # isym :: Identifier -> Int -> SymAlgReal Source #
Solvable FPRoundingMode SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods con :: FPRoundingMode -> SymFPRoundingMode Source # conView :: SymFPRoundingMode -> Maybe FPRoundingMode Source # sym :: Symbol -> SymFPRoundingMode Source # ssym :: Identifier -> SymFPRoundingMode Source # isym :: Identifier -> Int -> SymFPRoundingMode Source #
Solvable Integer SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods con :: Integer -> SymInteger Source # conView :: SymInteger -> Maybe Integer Source # sym :: Symbol -> SymInteger Source # ssym :: Identifier -> SymInteger Source # isym :: Identifier -> Int -> SymInteger Source #
Solvable Bool SymBool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBool Methods con :: Bool -> SymBool Source # conView :: SymBool -> Maybe Bool Source # sym :: Symbol -> SymBool Source # ssym :: Identifier -> SymBool Source # isym :: Identifier -> Int -> SymBool Source #
(Solvable c t, Mergeable t) => Solvable c (Union t) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.Core.Control.Monad.Union Methods con :: c -> Union t Source # conView :: Union t -> Maybe c Source # sym :: Symbol -> Union t Source # ssym :: Identifier -> Union t Source # isym :: Identifier -> Int -> Union t Source #
(KnownNat n, 1 <= n) => Solvable (IntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods con :: IntN n -> SymIntN n Source # conView :: SymIntN n -> Maybe (IntN n) Source # sym :: Symbol -> SymIntN n Source # ssym :: Identifier -> SymIntN n Source # isym :: Identifier -> Int -> SymIntN n Source #
(KnownNat n, 1 <= n) => Solvable (WordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods con :: WordN n -> SymWordN n Source # conView :: SymWordN n -> Maybe (WordN n) Source # sym :: Symbol -> SymWordN n Source # ssym :: Identifier -> SymWordN n Source # isym :: Identifier -> Int -> SymWordN n Source #
ValidFP eb sb => Solvable (FP eb sb) (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods con :: FP eb sb -> SymFP eb sb Source # conView :: SymFP eb sb -> Maybe (FP eb sb) Source # sym :: Symbol -> SymFP eb sb Source # ssym :: Identifier -> SymFP eb sb Source # isym :: Identifier -> Int -> SymFP eb sb Source #
(SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb)) => Solvable (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods con :: (ca --> cb) -> sa -~> sb Source # conView :: (sa -~> sb) -> Maybe (ca --> cb) Source # sym :: Symbol -> sa -~> sb Source # ssym :: Identifier -> sa -~> sb Source # isym :: Identifier -> Int -> sa -~> sb Source #
(LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb), SupportedNonFuncPrim ca) => Solvable (ca =-> cb) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Methods con :: (ca =-> cb) -> sa =~> sb Source # conView :: (sa =~> sb) -> Maybe (ca =-> cb) Source # sym :: Symbol -> sa =~> sb Source # ssym :: Identifier -> sa =~> sb Source # isym :: Identifier -> Int -> 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

slocsym :: Solvable c s => Text -> SpliceQ s Source #

Generate simply-named symbolic variables. The file location will be attached to the identifier.

>>> $$(slocsym "a") :: SymBool
a:[grisette-file-location <interactive>...]

Calling slocsym with the same name at different location will always generate different symbolic constants. Calling slocsym at the same location for multiple times will generate the same symbolic constants.

>>> ($$(slocsym "a") :: SymBool) == $$(slocsym "a")
False
>>> let f _ = $$(slocsym "a") :: SymBool
>>> f () == f ()
True

ilocsym :: Solvable c s => Text -> Int -> SpliceQ s Source #

Generate indexed symbolic variables. The file location will be attached to the identifier.

>>> $$(ilocsym "a" 1) :: SymBool
a:[grisette-file-location <interactive>...]@1

Calling ilocsym with the same name and index at different location will always generate different symbolic constants. Calling slocsym at the same location for multiple times will generate the same symbolic constants.