Grisette.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" :: TypedSymbol Bool
>>> let bBool = "b" :: TypedSymbol Bool
>>> let cBool = "c" :: TypedSymbol Bool
>>> let aInteger = "a" :: TypedSymbol Integer
>>> emptySet :: SymbolSet
SymbolSet {}
>>> containsSymbol aBool (buildSymbolSet aBool :: SymbolSet)
True
>>> containsSymbol bBool (buildSymbolSet aBool :: SymbolSet)
False
>>> insertSymbol aBool (buildSymbolSet aBool :: SymbolSet)
SymbolSet {a :: Bool}
>>> insertSymbol aInteger (buildSymbolSet aBool :: SymbolSet)
SymbolSet {a :: Bool, a :: Integer}
>>> let abSet = buildSymbolSet (aBool, bBool) :: SymbolSet
>>> let acSet = buildSymbolSet (aBool, cBool) :: SymbolSet
>>> 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 TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

emptySet :: SymbolSet

isEmptySet :: SymbolSet -> Bool

containsSymbol :: TypedSymbol a -> SymbolSet -> Bool

insertSymbol :: TypedSymbol a -> SymbolSet -> SymbolSet

intersectionSet :: SymbolSet -> SymbolSet -> SymbolSet

unionSet :: SymbolSet -> SymbolSet -> SymbolSet

differenceSet :: SymbolSet -> SymbolSet -> SymbolSet

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

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

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

Methods

buildSymbolSet :: rep -> symbolSet

Build a symbolic constant set

Instances

SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildSymbolSet :: TypedSymbol t -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

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" :: TypedSymbol Bool
>>> let bBool = "b" :: TypedSymbol Bool
>>> let cBool = "c" :: TypedSymbol Bool
>>> let aInteger = "a" :: TypedSymbol 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) :: SymbolSet
>>> 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 SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

emptyModel :: Model

isEmptyModel :: Model -> Bool

modelContains :: TypedSymbol a -> Model -> Bool

valueOf :: TypedSymbol t -> Model -> Maybe t

insertValue :: TypedSymbol t -> t -> Model -> Model

exceptFor :: SymbolSet -> Model -> Model

exceptFor' :: TypedSymbol t -> Model -> Model

restrictTo :: SymbolSet -> Model -> Model

extendTo :: SymbolSet -> Model -> Model

exact :: SymbolSet -> 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" :: TypedSymbol Bool
>>> let bBool = "b" :: TypedSymbol Bool
>>> buildModel (aBool ::= True, bBool ::= False) :: Model
Model {a -> True :: Bool, b -> False :: Bool}

Instances

ModelRep (ModelValuePair t) Model

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: ModelValuePair t -> Model

ModelRep (ModelSymPair ct st) Model

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: ModelSymPair ct st -> Model

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (a, b) -> Model

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

Defined in Grisette.IR.SymPrim.Data.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.IR.SymPrim.Data.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.IR.SymPrim.Data.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.IR.SymPrim.Data.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.IR.SymPrim.Data.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.IR.SymPrim.Data.Prim.Model

Methods

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