| 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.Core.Data.Class.ModelOps
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 :: * -> *) where
- buildSymbolSet :: rep -> symbolSet
- class SymbolSetOps symbolSet typedSymbol => ModelOps model symbolSet typedSymbol | model -> symbolSet typedSymbol where
- emptyModel :: model
- isEmptyModel :: model -> Bool
- valueOf :: typedSymbol t -> model -> Maybe t
- insertValue :: typedSymbol t -> t -> model -> model
- exceptFor :: symbolSet -> model -> model
- restrictTo :: symbolSet -> model -> model
- extendTo :: symbolSet -> model -> model
- exact :: symbolSet -> model -> model
- class ModelOps model symbolSet typedSymbol => ModelRep rep model symbolSet (typedSymbol :: * -> *) 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 :: SymbolSetSymbolSet {}>>>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 acSetSymbolSet {a :: Bool}>>>unionSet abSet acSetSymbolSet {a :: Bool, b :: Bool, c :: Bool}>>>differenceSet abSet acSetSymbolSet {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
| SymbolSetOps SymbolSet TypedSymbol Source # | |
Defined in Grisette.IR.SymPrim.Data.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 :: * -> *) 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) :: SymbolSetSymbolSet {a :: Bool, b :: Bool}
Instances
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 :: ModelModel {}>>>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 abModelModel {b -> False :: Bool}>>>restrictTo acSet abModelModel {a -> True :: Bool}>>>extendTo acSet abModelModel {a -> True :: Bool, b -> False :: Bool, c -> False :: Bool}>>>exact acSet abModelModel {a -> True :: Bool, c -> False :: Bool}
Minimal complete definition
emptyModel, isEmptyModel, valueOf, insertValue, exceptFor, restrictTo, extendTo
Methods
emptyModel :: model Source #
Construct an empty model
isEmptyModel :: model -> Bool Source #
Check if the model is empty
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
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
| ModelOps Model SymbolSet TypedSymbol Source # | |
Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods emptyModel :: Model Source # isEmptyModel :: Model -> Bool Source # valueOf :: TypedSymbol t -> Model -> Maybe t Source # insertValue :: TypedSymbol t -> t -> Model -> Model Source # exceptFor :: SymbolSet -> Model -> Model Source # restrictTo :: SymbolSet -> Model -> Model Source # | |
class ModelOps model symbolSet typedSymbol => ModelRep rep model symbolSet (typedSymbol :: * -> *) 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) :: ModelModel {a -> True :: Bool, b -> False :: Bool}