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.ModelOps

Contents

Model and symbolic set operations

Description

Synopsis

class Monoid symbolSet => SymbolSetOps symbolSet (typedSymbol :: Type -> Type) | symbolSet -> typedSymbol where
- emptySet :: symbolSet
- isEmptySet :: symbolSet -> Bool
- containsSymbol :: forall a. typedSymbol a -> symbolSet -> Bool
- insertSymbol :: forall a. typedSymbol a -> symbolSet -> symbolSet
- intersectionSet :: symbolSet -> symbolSet -> symbolSet
- unionSet :: symbolSet -> symbolSet -> symbolSet
- differenceSet :: symbolSet -> symbolSet -> symbolSet
class SymbolSetOps symbolSet typedSymbol => SymbolSetRep rep symbolSet (typedSymbol :: Type -> Type) where
- buildSymbolSet :: rep -> symbolSet
class SymbolSetOps symbolSet typedSymbol => ModelOps model symbolSet typedSymbol | model -> symbolSet typedSymbol where
- 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
- buildModel :: rep -> model

Model and symbolic set operations

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

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 Source #

Construct an empty set

isEmptySet :: symbolSet -> Bool Source #

Check if the set is empty

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

Check if the set contains the given symbol

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

Insert a symbol into the set

intersectionSet :: symbolSet -> symbolSet -> symbolSet Source #

Set intersection

unionSet :: symbolSet -> symbolSet -> symbolSet Source #

Set union

differenceSet :: symbolSet -> symbolSet -> symbolSet Source #

Set difference

Instances

Instances details

SymbolSetOps SymbolSet TypedSymbol Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptySet :: SymbolSet Source #

isEmptySet :: SymbolSet -> Bool Source #

containsSymbol :: TypedSymbol a -> SymbolSet -> Bool Source #

insertSymbol :: TypedSymbol a -> SymbolSet -> SymbolSet Source #

intersectionSet :: SymbolSet -> SymbolSet -> SymbolSet Source #

unionSet :: SymbolSet -> SymbolSet -> SymbolSet Source #

differenceSet :: SymbolSet -> SymbolSet -> SymbolSet Source #

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

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 Source #

Build a symbolic constant set

Instances

Instances details

SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: TypedSymbol t -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b) -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c) -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) -> SymbolSet Source #

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

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 Source #

Construct an empty model

isEmptyModel :: model -> Bool Source #

Check if the model is empty

modelContains :: typedSymbol a -> model -> Bool Source #

Check if the model contains the given symbol

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

Extract the assigned value for a given symbolic constant

insertValue :: typedSymbol t -> t -> model -> model Source #

Insert an assignment into the model

exceptFor :: symbolSet -> model -> model Source #

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

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

Returns a model that removed the assignments for the symbolic constants

restrictTo :: symbolSet -> model -> model Source #

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

extendTo :: symbolSet -> model -> model Source #

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

exact :: symbolSet -> model -> model Source #

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

Instances details

ModelOps Model SymbolSet TypedSymbol Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptyModel :: Model Source #

isEmptyModel :: Model -> Bool Source #

modelContains :: TypedSymbol a -> Model -> Bool Source #

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

insertValue :: TypedSymbol t -> t -> Model -> Model Source #

exceptFor :: SymbolSet -> Model -> Model Source #

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

restrictTo :: SymbolSet -> Model -> Model Source #

extendTo :: SymbolSet -> Model -> Model Source #

exact :: SymbolSet -> Model -> Model Source #

class ModelRep rep model | rep -> model where Source #

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

Methods

buildModel :: rep -> model Source #

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

Instances details

ModelRep (ModelValuePair t) Model Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildModel :: ModelValuePair t -> Model Source #
ModelRep (ModelSymPair ct st) Model Source #
Instance details Defined in Grisette.Internal.SymPrim.ModelRep Methods buildModel :: ModelSymPair ct st -> Model Source #
(ModelRep a Model, ModelRep b Model) => ModelRep (a, b) Model Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildModel :: (a, b) -> Model Source #
(ModelRep a Model, ModelRep b Model, ModelRep c Model) => ModelRep (a, b, c) Model Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildModel :: (a, b, c) -> Model Source #
(ModelRep a Model, ModelRep b Model, ModelRep c Model, ModelRep d Model) => ModelRep (a, b, c, d) Model Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildModel :: (a, b, c, d) -> Model Source #
(ModelRep a Model, ModelRep b Model, ModelRep c Model, ModelRep d Model, ModelRep e Model) => ModelRep (a, b, c, d, e) Model Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildModel :: (a, b, c, d, e) -> Model Source #
(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 Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildModel :: (a, b, c, d, e, f) -> Model Source #
(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 Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildModel :: (a, b, c, d, e, f, g) -> Model Source #
(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 Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildModel :: (a, b, c, d, e, f, g, h) -> Model Source #