Grisette.Internal.SymPrim.Prim.Model

Documentation

newtype SymbolSet

Set of symbols.

Check SymbolSetOps for operations, and SymbolSetRep for manual constructions.

Constructors

SymbolSet

Fields

• unSymbolSet :: HashSet SomeTypedSymbol

Instances

Monoid SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

mempty :: SymbolSet

mappend :: SymbolSet -> SymbolSet -> SymbolSet

mconcat :: [SymbolSet] -> SymbolSet

Semigroup SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

(<>) :: SymbolSet -> SymbolSet -> SymbolSet

sconcat :: NonEmpty SymbolSet -> SymbolSet

stimes :: Integral b => b -> SymbolSet -> SymbolSet

Generic SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

Associated Types

type Rep SymbolSet :: Type -> Type

Methods

from :: SymbolSet -> Rep SymbolSet x

to :: Rep SymbolSet x -> SymbolSet

Show SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

showsPrec :: Int -> SymbolSet -> ShowS

show :: SymbolSet -> String

showList :: [SymbolSet] -> ShowS

Eq SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

(==) :: SymbolSet -> SymbolSet -> Bool

(/=) :: SymbolSet -> SymbolSet -> Bool

Hashable SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

hashWithSalt :: Int -> SymbolSet -> Int

hash :: SymbolSet -> Int

SymbolSetOps SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.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

ModelOps Model SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.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

SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: TypedSymbol t -> SymbolSet

SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

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

Methods

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

type Rep SymbolSet

Defined in Grisette.Internal.SymPrim.Prim.Model

type Rep SymbolSet = D1 ('MetaData "SymbolSet" "Grisette.Internal.SymPrim.Prim.Model" "grisette-0.7.0.0-3DYM4wcz8TiF8sSQ1gvVO8" 'True) (C1 ('MetaCons "SymbolSet" 'PrefixI 'True) (S1 ('MetaSel ('Just "unSymbolSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet SomeTypedSymbol))))

newtype Model

Model returned by the solver.

Check ModelOps for operations, and ModelRep for manual constructions.

Constructors

Model

Fields

• unModel :: HashMap SomeTypedSymbol ModelValue

Instances

Monoid Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

mempty :: Model

mappend :: Model -> Model -> Model

mconcat :: [Model] -> Model

Semigroup Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

(<>) :: Model -> Model -> Model

sconcat :: NonEmpty Model -> Model

stimes :: Integral b => b -> Model -> Model

Generic Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Associated Types

type Rep Model :: Type -> Type

Methods

from :: Model -> Rep Model x

to :: Rep Model x -> Model

Show Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

showsPrec :: Int -> Model -> ShowS

show :: Model -> String

showList :: [Model] -> ShowS

Eq Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

(==) :: Model -> Model -> Bool

(/=) :: Model -> Model -> Bool

Hashable Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

hashWithSalt :: Int -> Model -> Int

hash :: Model -> Int

ModelOps Model SymbolSet TypedSymbol

Defined in Grisette.Internal.SymPrim.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

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

type Rep Model

Defined in Grisette.Internal.SymPrim.Prim.Model

type Rep Model = D1 ('MetaData "Model" "Grisette.Internal.SymPrim.Prim.Model" "grisette-0.7.0.0-3DYM4wcz8TiF8sSQ1gvVO8" 'True) (C1 ('MetaCons "Model" 'PrefixI 'True) (S1 ('MetaSel ('Just "unModel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SomeTypedSymbol ModelValue))))

data ModelValuePair t

A type used for building a model by hand.

>>> buildModel ("x" ::= (1 :: Integer), "y" ::= True) :: Model
Model {x -> 1 :: Integer, y -> True :: Bool}

Constructors

(TypedSymbol t) ::= t

Instances

Show t => Show (ModelValuePair t)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

showsPrec :: Int -> ModelValuePair t -> ShowS

show :: ModelValuePair t -> String

showList :: [ModelValuePair t] -> ShowS

ModelRep (ModelValuePair t) Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildModel :: ModelValuePair t -> Model

equation :: TypedSymbol a -> Model -> Maybe (Term Bool)

Given a typed symbol and a model, return the equation (symbol = value) encoded in the model.

evaluateTerm :: forall a. SupportedPrim a => Bool -> Model -> Term a -> Term a

Evaluate a term in the given model.

Orphan instances

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

Methods

buildModel :: (a, b) -> Model

(ModelRep a Model, ModelRep b Model, ModelRep c Model) => ModelRep (a, b, c) 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

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

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

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

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

Methods

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