Grisette.Internal.SymPrim.Prim.Model

Documentation

newtype SymbolSet knd

Set of symbols.

Check SymbolSetOps for operations, and SymbolSetRep for manual constructions.

Constructors

SymbolSet

Fields

• unSymbolSet :: HashSet (SomeTypedSymbol knd)

Instances

ModelOps Model AnySymbolSet TypedAnySymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptyModel :: Model

isEmptyModel :: Model -> Bool

modelContains :: TypedAnySymbol a -> Model -> Bool

valueOf :: TypedAnySymbol t -> Model -> Maybe t

insertValue :: TypedAnySymbol t -> t -> Model -> Model

exceptFor :: AnySymbolSet -> Model -> Model

exceptFor' :: TypedAnySymbol t -> Model -> Model

restrictTo :: AnySymbolSet -> Model -> Model

extendTo :: AnySymbolSet -> Model -> Model

exact :: AnySymbolSet -> Model -> Model

Monoid (SymbolSet knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

mempty :: SymbolSet knd

mappend :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd

mconcat :: [SymbolSet knd] -> SymbolSet knd

Semigroup (SymbolSet knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

sconcat :: NonEmpty (SymbolSet knd) -> SymbolSet knd

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

Generic (SymbolSet knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Associated Types

type Rep (SymbolSet knd) :: Type -> Type

Methods

from :: SymbolSet knd -> Rep (SymbolSet knd) x

to :: Rep (SymbolSet knd) x -> SymbolSet knd

Show (SymbolSet knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

showsPrec :: Int -> SymbolSet knd -> ShowS

show :: SymbolSet knd -> String

showList :: [SymbolSet knd] -> ShowS

IsSymbolKind knd => Binary (SymbolSet knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

put :: SymbolSet knd -> Put

get :: Get (SymbolSet knd)

putList :: [SymbolSet knd] -> Put

IsSymbolKind knd => Serial (SymbolSet knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

serialize :: MonadPut m => SymbolSet knd -> m ()

deserialize :: MonadGet m => m (SymbolSet knd)

IsSymbolKind knd => Serialize (SymbolSet knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

put :: Putter (SymbolSet knd)

get :: Get (SymbolSet knd)

Eq (SymbolSet knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

PPrint (SymbolSet knd)

Defined in Grisette.Internal.Core.Data.Class.PPrint

Methods

pformat :: SymbolSet knd -> Doc ann

pformatPrec :: Int -> SymbolSet knd -> Doc ann

pformatList :: [SymbolSet knd] -> Doc ann

Hashable (SymbolSet knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

hashWithSalt :: Int -> SymbolSet knd -> Int

hash :: SymbolSet knd -> Int

SymbolSetOps (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptySet :: SymbolSet knd

isEmptySet :: SymbolSet knd -> Bool

containsSymbol :: TypedSymbol knd a -> SymbolSet knd -> Bool

insertSymbol :: TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd

intersectionSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd

unionSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd

differenceSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd

SymbolSetRep (SomeTypedSymbol knd) (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: SomeTypedSymbol knd -> SymbolSet knd

SymbolSetRep [SomeTypedSymbol knd] (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: [SomeTypedSymbol knd] -> SymbolSet knd

SymbolSetRep [TypedSymbol knd t] (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: [TypedSymbol knd t] -> SymbolSet knd

SymbolSetRep (TypedSymbol knd t) (SymbolSet knd) (TypedSymbol knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: TypedSymbol knd t -> SymbolSet knd

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

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

type Rep (SymbolSet knd)

Defined in Grisette.Internal.SymPrim.Prim.Model

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

type ConstantSymbolSet = SymbolSet 'ConstantKind

Set of constant symbols. Excluding unintepreted functions.

type AnySymbolSet = SymbolSet 'AnyKind

Set of any symbols.

newtype Model

Model returned by the solver.

Check ModelOps for operations, and ModelRep for manual constructions.

Constructors

Model

Fields

• unModel :: HashMap SomeTypedAnySymbol 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

Binary Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

put :: Model -> Put

get :: Get Model

putList :: [Model] -> Put

Serial Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

serialize :: MonadPut m => Model -> m ()

deserialize :: MonadGet m => m Model

Serialize Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

put :: Putter Model

get :: Get Model

NFData Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

rnf :: Model -> ()

Eq Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

PPrint Model

Defined in Grisette.Internal.Core.Data.Class.PPrint

Methods

pformat :: Model -> Doc ann

pformatPrec :: Int -> Model -> Doc ann

pformatList :: [Model] -> Doc ann

Hashable Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

hashWithSalt :: Int -> Model -> Int

hash :: Model -> Int

Lift Model

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

lift :: Quote m => Model -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => Model -> Code m Model

ModelOps Model AnySymbolSet TypedAnySymbol

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptyModel :: Model

isEmptyModel :: Model -> Bool

modelContains :: TypedAnySymbol a -> Model -> Bool

valueOf :: TypedAnySymbol t -> Model -> Maybe t

insertValue :: TypedAnySymbol t -> t -> Model -> Model

exceptFor :: AnySymbolSet -> Model -> Model

exceptFor' :: TypedAnySymbol t -> Model -> Model

restrictTo :: AnySymbolSet -> Model -> Model

extendTo :: AnySymbolSet -> Model -> Model

exact :: AnySymbolSet -> 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.9.0.0-8b30m8DmEAJELhVBobm0Vc" 'True) (C1 ('MetaCons "Model" 'PrefixI 'True) (S1 ('MetaSel ('Just "unModel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SomeTypedAnySymbol 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

(TypedAnySymbol 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 :: TypedAnySymbol a -> Model -> Maybe (Term Bool)

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

evalTerm :: SupportedPrim a => Bool -> Model -> HashSet SomeTypedConstantSymbol -> 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