Grisette.Internal.Core.Data.Class.ModelOps

Model and symbolic set operations

class Monoid symbolSet => SymbolSetOps symbolSet (typedSymbol :: Type -> Type) | symbolSet -> typedSymbol where

The operations on symbolic constant sets

Note that symbolic constants with different types are considered different.

>>> let aBool = "a" :: TypedAnySymbol Bool
>>> let bBool = "b" :: TypedAnySymbol Bool
>>> let cBool = "c" :: TypedAnySymbol Bool
>>> let aInteger = "a" :: TypedAnySymbol Integer
>>> emptySet :: AnySymbolSet
SymbolSet {}
>>> containsSymbol aBool (buildSymbolSet aBool :: AnySymbolSet)
True
>>> containsSymbol bBool (buildSymbolSet aBool :: AnySymbolSet)
False
>>> insertSymbol aBool (buildSymbolSet aBool :: AnySymbolSet)
SymbolSet {a :: Bool}
>>> insertSymbol aInteger (buildSymbolSet aBool :: AnySymbolSet)
SymbolSet {a :: Bool, a :: Integer}
>>> let abSet = buildSymbolSet (aBool, bBool) :: AnySymbolSet
>>> let acSet = buildSymbolSet (aBool, cBool) :: AnySymbolSet
>>> intersectionSet abSet acSet
SymbolSet {a :: Bool}
>>> unionSet abSet acSet
SymbolSet {a :: Bool, b :: Bool, c :: Bool}
>>> differenceSet abSet acSet
SymbolSet {b :: Bool}

Methods

emptySet :: symbolSet

Construct an empty set

isEmptySet :: symbolSet -> Bool

Check if the set is empty

containsSymbol :: forall a. typedSymbol a -> symbolSet -> Bool

Check if the set contains the given symbol

insertSymbol :: forall a. typedSymbol a -> symbolSet -> symbolSet

Insert a symbol into the set

intersectionSet :: symbolSet -> symbolSet -> symbolSet

Set intersection

unionSet :: symbolSet -> symbolSet -> symbolSet

Set union

differenceSet :: symbolSet -> symbolSet -> symbolSet

Set difference

Instances

SymbolSetOps (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptySet :: SymbolSet knd

isEmptySet :: SymbolSet knd -> Bool

containsSymbol :: TypedSymbol knd a -> SymbolSet knd -> Bool

insertSymbol :: TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd

intersectionSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd

unionSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd

differenceSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd

class SymbolSetOps symbolSet typedSymbol => SymbolSetRep rep symbolSet (typedSymbol :: Type -> Type) where

A type class for building a symbolic constant set manually from a symbolic constant set representation

>>> buildSymbolSet ("a" :: TypedAnySymbol Bool, "b" :: TypedAnySymbol Bool) :: AnySymbolSet
SymbolSet {a :: Bool, b :: Bool}

Methods

buildSymbolSet :: rep -> symbolSet

Build a symbolic constant set

Instances

SymbolSetRep (SomeTypedSymbol knd) (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: SomeTypedSymbol knd -> SymbolSet knd

SymbolSetRep [SomeTypedSymbol knd] (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: [SomeTypedSymbol knd] -> SymbolSet knd

SymbolSetRep [TypedSymbol knd t] (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: [TypedSymbol knd t] -> SymbolSet knd

SymbolSetRep (TypedSymbol knd t) (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: TypedSymbol knd t -> SymbolSet knd

SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b) (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b) -> SymbolSet knd

SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c) (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c) -> SymbolSet knd

SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d) (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d) -> SymbolSet knd

SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e) (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e) -> SymbolSet knd

SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f) (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f) -> SymbolSet knd

SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f, TypedSymbol knd g) (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f, TypedSymbol knd g) -> SymbolSet knd

SymbolSetRep (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f, TypedSymbol knd g, TypedSymbol knd h) (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c, TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f, TypedSymbol knd g, TypedSymbol knd h) -> SymbolSet knd

class SymbolSetOps symbolSet typedSymbol => ModelOps model symbolSet typedSymbol | model -> symbolSet typedSymbol where

The operations on Models.

Note that symbolic constants with different types are considered different.

>>> let aBool = "a" :: TypedAnySymbol Bool
>>> let bBool = "b" :: TypedAnySymbol Bool
>>> let cBool = "c" :: TypedAnySymbol Bool
>>> let aInteger = "a" :: TypedAnySymbol Integer
>>> emptyModel :: Model
Model {}
>>> valueOf aBool (buildModel (aBool ::= True) :: Model)
Just True
>>> valueOf bBool (buildModel (aBool ::= True) :: Model)
Nothing
>>> insertValue bBool False (buildModel (aBool ::= True) :: Model)
Model {a -> true :: Bool, b -> false :: Bool}
>>> let abModel = buildModel (aBool ::= True, bBool ::= False) :: Model
>>> let acSet = buildSymbolSet (aBool, cBool) :: AnySymbolSet
>>> exceptFor acSet abModel
Model {b -> false :: Bool}
>>> restrictTo acSet abModel
Model {a -> true :: Bool}
>>> extendTo acSet abModel
Model {a -> true :: Bool, b -> false :: Bool, c -> false :: Bool}
>>> exact acSet abModel
Model {a -> true :: Bool, c -> false :: Bool}

Minimal complete definition

emptyModel, isEmptyModel, modelContains, valueOf, insertValue, exceptFor, exceptFor', restrictTo, extendTo

Methods

emptyModel :: model

Construct an empty model

isEmptyModel :: model -> Bool

Check if the model is empty

modelContains :: typedSymbol a -> model -> Bool

Check if the model contains the given symbol

valueOf :: typedSymbol t -> model -> Maybe t

Extract the assigned value for a given symbolic constant

insertValue :: typedSymbol t -> t -> model -> model

Insert an assignment into the model

exceptFor :: symbolSet -> model -> model

Returns a model that removed all the assignments for the symbolic constants in the set

exceptFor' :: typedSymbol t -> model -> model

Returns a model that removed the assignments for the symbolic constants

restrictTo :: symbolSet -> model -> model

Returns a model that only keeps the assignments for the symbolic constants in the set

extendTo :: symbolSet -> model -> model

Returns a model that extends the assignments for the symbolic constants in the set by assigning default values to them

exact :: symbolSet -> model -> model

Returns a model that contains the assignments for exactly the symbolic constants in the set by removing assignments for the symbolic constants that are not in the set and add assignments for the missing symbolic constants by assigning default values to them.

Instances

ModelOps Model AnySymbolSet TypedAnySymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptyModel :: Model

isEmptyModel :: Model -> Bool

modelContains :: TypedAnySymbol a -> Model -> Bool

valueOf :: TypedAnySymbol t -> Model -> Maybe t

insertValue :: TypedAnySymbol t -> t -> Model -> Model

exceptFor :: AnySymbolSet -> Model -> Model

exceptFor' :: TypedAnySymbol t -> Model -> Model

restrictTo :: AnySymbolSet -> Model -> Model

extendTo :: AnySymbolSet -> Model -> Model

exact :: AnySymbolSet -> Model -> Model

class ModelRep rep model | rep -> model where

A type class for building a model manually from a model representation

Methods

buildModel :: rep -> model

Build a model

>>> let aBool = "a" :: TypedAnySymbol Bool
>>> let bBool = "b" :: TypedAnySymbol Bool
>>> buildModel (aBool ::= True, bBool ::= False) :: Model
Model {a -> true :: Bool, b -> false :: Bool}

Instances

ModelRep (ModelValuePair t) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: ModelValuePair t -> Model

ModelRep (ModelSymPair ct st) Model

Defined in Grisette.Internal.SymPrim.ModelRep

Methods

buildModel :: ModelSymPair ct st -> Model

(ModelRep a Model, ModelRep b Model) => ModelRep (a, b) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model) => ModelRep (a, b, c) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b, c) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model, ModelRep d Model) => ModelRep (a, b, c, d) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b, c, d) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model, ModelRep d Model, ModelRep e Model) => ModelRep (a, b, c, d, e) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b, c, d, e) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model, ModelRep d Model, ModelRep e Model, ModelRep f Model) => ModelRep (a, b, c, d, e, f) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b, c, d, e, f) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model, ModelRep d Model, ModelRep e Model, ModelRep f Model, ModelRep g Model) => ModelRep (a, b, c, d, e, f, g) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b, c, d, e, f, g) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model, ModelRep d Model, ModelRep e Model, ModelRep f Model, ModelRep g Model, ModelRep h Model) => ModelRep (a, b, c, d, e, f, g, h) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: (a, b, c, d, e, f, g, h) -> Model