grisette-0.2.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.Core.Data.Class.ModelOps

Description

 
Synopsis

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

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) :: 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.IR.SymPrim.Data.Prim.Model

SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol Source # 
Instance details

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

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c) SymbolSet TypedSymbol Source # 
Instance details

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

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) SymbolSet TypedSymbol Source # 
Instance details

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

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) SymbolSet TypedSymbol Source # 
Instance details

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

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) SymbolSet TypedSymbol Source # 
Instance details

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

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) SymbolSet TypedSymbol Source # 
Instance details

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

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

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}

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.

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

ModelRep (ModelSymPair ct st) Model Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: ModelSymPair ct st -> Model Source #

(ModelRep a Model, ModelRep b Model) => ModelRep (a, b) Model Source # 
Instance details

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

Methods

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