grisette-0.1.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.Internal.Core

Description

 
Synopsis

The UnionBase type

data Union a Source #

The default union implementation.

Constructors

Single a

A single value

If

A if value

Fields

  • a

    Cached leftmost value

  • !Bool

    Is merged invariant already maintained?

  • !SymBool

    If condition

  • (Union a)

    True branch

  • (Union a)

    False branch

Instances

Instances details
Eq1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

liftEq :: (a -> b -> Bool) -> Union a -> Union b -> Bool #

Show1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Union a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Union a] -> ShowS #

NFData1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

liftRnf :: (a -> ()) -> Union a -> () #

Mergeable1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

SimpleMergeable1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> Union a -> Union a -> Union a Source #

UnionLike Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

UnionPrjOp Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Lift a => Lift (Union a :: Type) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

lift :: Quote m => Union a -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => Union a -> Code m (Union a) #

Generic (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Associated Types

type Rep (Union a) :: Type -> Type #

Methods

from :: Union a -> Rep (Union a) x #

to :: Rep (Union a) x -> Union a #

Show a => Show (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

showsPrec :: Int -> Union a -> ShowS #

show :: Union a -> String #

showList :: [Union a] -> ShowS #

NFData a => NFData (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

rnf :: Union a -> () #

Eq a => Eq (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

(==) :: Union a -> Union a -> Bool #

(/=) :: Union a -> Union a -> Bool #

Mergeable a => Mergeable (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Mergeable a => SimpleMergeable (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

mrgIte :: SymBool -> Union a -> Union a -> Union a Source #

Hashable a => Hashable (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

Methods

hashWithSalt :: Int -> Union a -> Int #

hash :: Union a -> Int #

Generic1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

Associated Types

type Rep1 Union :: k -> Type #

Methods

from1 :: forall (a :: k). Union a -> Rep1 Union a #

to1 :: forall (a :: k). Rep1 Union a -> Union a #

type Rep (Union a) Source # 
Instance details

Defined in Grisette.Core.Data.Union

type Rep1 Union Source # 
Instance details

Defined in Grisette.Core.Data.Union

ifWithLeftMost :: Bool -> SymBool -> Union a -> Union a -> Union a Source #

Build If with leftmost cache correctly maintained.

Usually you should never directly try to build a If with its constructor.

ifWithStrategy :: MergingStrategy a -> SymBool -> Union a -> Union a -> Union a Source #

Use a specific strategy to build a If value.

The merged invariant will be maintained in the result.

fullReconstruct :: MergingStrategy a -> Union a -> Union a Source #

Fully reconstruct a Union to maintain the merged invariant.

The UnionMBase type

data UnionM a where Source #

UnionM is the Union container (hidden) enhanced with MergingStrategy knowledge propagation.

The Union models the underlying semantics evaluation semantics for unsolvable types with the nested if-then-else tree semantics, and can be viewed as the following structure:

data Union a
  = Single a
  | If bool (Union a) (Union a)

The Single constructor is for a single value with the path condition true, and the If constructor is the if operator in an if-then-else tree. For clarity, when printing a UnionM value, we will omit the Single constructor. The following two representations has the same semantics.

If      c1    (If c11 v11 (If c12 v12 v13))
  (If   c2    v2
              v3)

\[ \left\{\begin{aligned}&t_1&&\mathrm{if}&&c_1\\&v_2&&\mathrm{else if}&&c_2\\&v_3&&\mathrm{otherwise}&&\end{aligned}\right.\hspace{2em}\mathrm{where}\hspace{2em}t_1 = \left\{\begin{aligned}&v_{11}&&\mathrm{if}&&c_{11}\\&v_{12}&&\mathrm{else if}&&c_{12}\\&v_{13}&&\mathrm{otherwise}&&\end{aligned}\right. \]

To reduce the size of the if-then-else tree to reduce the number of paths to execute, Grisette would merge the branches in a Union container and maintain a representation invariant for them. To perform this merging procedure, Grisette relies on a type class called Mergeable and the merging strategy defined by it.

Union is a monad, so we can easily write code with the do-notation and monadic combinators. However, the standard monadic operators cannot resolve any extra constraints, including the Mergeable constraint (see The constrained-monad problem by Sculthorpe et al.). This prevents the standard do-notations to merge the results automatically, and would result in bad performance or very verbose code.

To reduce this boilerplate, Grisette provide another monad, UnionM that would try to cache the merging strategy. The UnionM has two data constructors (hidden intentionally), UAny and UMrg. The UAny data constructor (printed as <...>) wraps an arbitrary (probably unmerged) Union. It is constructed when no Mergeable knowledge is available (for example, when constructed with Haskell's return). The UMrg data constructor (printed as {...}) wraps a merged UnionM along with the Mergeable constraint. This constraint can be propagated to the contexts without Mergeable knowledge, and helps the system to merge the resulting Union.

Examples:

return cannot resolve the Mergeable constraint.

>>> return 1 :: UnionM Integer
<1>

mrgReturn can resolve the Mergeable constraint.

>>> import Grisette.Lib.Base
>>> mrgReturn 1 :: UnionM Integer
{1}

unionIf cannot resolve the Mergeable constraint.

>>> unionIf "a" (return 1) (unionIf "b" (return 1) (return 2)) :: UnionM Integer
<If a 1 (If b 1 2)>

But unionIf is able to merge the result if some of the branches are merged:

>>> unionIf "a" (return 1) (unionIf "b" (mrgReturn 1) (return 2)) :: UnionM Integer
{If (|| a b) 1 2}

The >>= operator uses unionIf internally. When the final statement in a do-block merges the values, the system can then merge the final result.

>>> :{
  do
    x <- unionIf (ssym "a") (return 1) (unionIf (ssym "b") (return 1) (return 2))
    mrgSingle $ x + 1 :: UnionM Integer
:}
{If (|| a b) 2 3}

Calling a function that merges a result at the last line of a do-notation will also merge the whole block. If you stick to these mrg* combinators and all the functions will merge the results, the whole program can be symbolically evaluated efficiently.

>>> f x y = mrgIf "c" x y
>>> :{
  do
    x <- unionIf (ssym "a") (return 1) (unionIf (ssym "b") (return 1) (return 2))
    f x (x + 1) :: UnionM Integer
:}
{If (&& c (|| a b)) 1 (If (|| a (|| b c)) 2 3)}

In Grisette.Lib.Base, Grisette.Lib.Mtl, we also provided more mrg* variants of other combinators. You should stick to these combinators to ensure efficient merging by Grisette.

Constructors

UAny

UnionM with no Mergeable knowledge.

Fields

UMrg

UnionM with Mergeable knowledge.

Fields

Instances

Instances details
Eq1 UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

liftEq :: (a -> b -> Bool) -> UnionM a -> UnionM b -> Bool #

Show1 UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> UnionM a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [UnionM a] -> ShowS #

Applicative UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

pure :: a -> UnionM a #

(<*>) :: UnionM (a -> b) -> UnionM a -> UnionM b #

liftA2 :: (a -> b -> c) -> UnionM a -> UnionM b -> UnionM c #

(*>) :: UnionM a -> UnionM b -> UnionM b #

(<*) :: UnionM a -> UnionM b -> UnionM a #

Functor UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

fmap :: (a -> b) -> UnionM a -> UnionM b #

(<$) :: a -> UnionM b -> UnionM a #

Monad UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

(>>=) :: UnionM a -> (a -> UnionM b) -> UnionM b #

(>>) :: UnionM a -> UnionM b -> UnionM b #

return :: a -> UnionM a #

NFData1 UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

liftRnf :: (a -> ()) -> UnionM a -> () #

Mergeable1 UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

SimpleMergeable1 UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> UnionM a -> UnionM a -> UnionM a Source #

UnionLike UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

UnionPrjOp UnionM Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

(GenSym spec a, Mergeable a) => GenSym spec (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

fresh :: MonadFresh m => spec -> m (UnionM (UnionM a)) Source #

GenSym spec a => GenSymSimple spec (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

simpleFresh :: MonadFresh m => spec -> m (UnionM a) 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 #

(ToSym a b, Mergeable b) => ToSym a (UnionM b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: a -> UnionM b Source #

Lift a => Lift (UnionM a :: Type) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

lift :: Quote m => UnionM a -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => UnionM a -> Code m (UnionM a) #

(IsString a, Mergeable a) => IsString (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

fromString :: String -> UnionM a #

(Num a, Mergeable a) => Num (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

(+) :: UnionM a -> UnionM a -> UnionM a #

(-) :: UnionM a -> UnionM a -> UnionM a #

(*) :: UnionM a -> UnionM a -> UnionM a #

negate :: UnionM a -> UnionM a #

abs :: UnionM a -> UnionM a #

signum :: UnionM a -> UnionM a #

fromInteger :: Integer -> UnionM a #

Show a => Show (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

showsPrec :: Int -> UnionM a -> ShowS #

show :: UnionM a -> String #

showList :: [UnionM a] -> ShowS #

NFData a => NFData (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

rnf :: UnionM a -> () #

Eq a => Eq (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

(==) :: UnionM a -> UnionM a -> Bool #

(/=) :: UnionM a -> UnionM a -> Bool #

(ITEOp a, Mergeable a) => ITEOp (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

ites :: SymBool -> UnionM a -> UnionM a -> UnionM a Source #

(LogicalOp a, Mergeable a) => LogicalOp (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

(||~) :: UnionM a -> UnionM a -> UnionM a Source #

(&&~) :: UnionM a -> UnionM a -> UnionM a Source #

nots :: UnionM a -> UnionM a Source #

xors :: UnionM a -> UnionM a -> UnionM a Source #

implies :: UnionM a -> UnionM a -> UnionM a Source #

SEq a => SEq (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

(==~) :: UnionM a -> UnionM a -> SymBool Source #

(/=~) :: UnionM a -> UnionM a -> SymBool Source #

(Mergeable a, EvaluateSym a) => EvaluateSym (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

evaluateSym :: Bool -> Model -> UnionM a -> UnionM a Source #

ExtractSymbolics a => ExtractSymbolics (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

(Function f, Mergeable f, Mergeable a, Ret f ~ a) => Function (UnionM f) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Associated Types

type Arg (UnionM f) Source #

type Ret (UnionM f) Source #

Methods

(#) :: UnionM f -> Arg (UnionM f) -> Ret (UnionM f) Source #

Mergeable a => Mergeable (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

SOrd a => SOrd (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Mergeable a => SimpleMergeable (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

mrgIte :: SymBool -> UnionM a -> UnionM a -> UnionM a Source #

(Mergeable a, SubstituteSym a) => SubstituteSym (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

substituteSym :: TypedSymbol b -> Sym b -> UnionM a -> UnionM a Source #

Hashable a => Hashable (UnionM a) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

hashWithSalt :: Int -> UnionM a -> Int #

hash :: UnionM a -> Int #

(GenSym a a, Mergeable a) => GenSym (UnionM a) a Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

fresh :: MonadFresh m => UnionM a -> m (UnionM a) Source #

ToCon a b => ToCon (UnionM a) b Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toCon :: UnionM a -> Maybe b Source #

UnionWithExcept (UnionM (Either e v)) UnionM e v Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

(ToCon a b, Mergeable b) => ToCon (UnionM a) (UnionM b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toCon :: UnionM a -> Maybe (UnionM b) Source #

(ToSym a b, Mergeable b) => ToSym (UnionM a) (UnionM b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: UnionM a -> UnionM b Source #

(IsConcrete k, Mergeable t) => Mergeable (HashMap k (UnionM (Maybe t))) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

(IsConcrete k, Mergeable t) => SimpleMergeable (HashMap k (UnionM (Maybe t))) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

mrgIte :: SymBool -> HashMap k (UnionM (Maybe t)) -> HashMap k (UnionM (Maybe t)) -> HashMap k (UnionM (Maybe t)) Source #

type Arg (UnionM f) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

type Arg (UnionM f) = Arg f
type Ret (UnionM f) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

type Ret (UnionM f) = UnionM (Ret f)

underlyingUnion :: UnionM a -> Union a Source #

Extract the underlying Union. May be unmerged.

isMerged :: UnionM a -> Bool Source #

Check if a UnionM is already merged.