Copyright	(c) Sirui Lu 2021-2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	None
Language	Haskell2010

Grisette.Internal.SymPrim.Prim.Model

Contents

Orphan instances

Description

Synopsis

newtype SymbolSet (knd :: SymbolKind) = SymbolSet {
- unSymbolSet :: HashSet (SomeTypedSymbol knd)
}
type ConstantSymbolSet = SymbolSet 'ConstantKind
type AnySymbolSet = SymbolSet 'AnyKind
newtype Model = Model {
- unModel :: HashMap SomeTypedAnySymbol ModelValue
}
data ModelValuePair t = (TypedAnySymbol t) ::= t
equation :: TypedAnySymbol a -> Model -> Maybe (Term Bool)
evalTerm :: SupportedPrim a => Bool -> Model -> HashSet SomeTypedConstantSymbol -> Term a -> Term a

Documentation

newtype SymbolSet (knd :: SymbolKind) Source #

Set of symbols.

Check SymbolSetOps for operations, and SymbolSetRep for manual constructions.

Constructors

SymbolSet
Fields unSymbolSet :: HashSet (SomeTypedSymbol knd)

Instances

Instances details

ModelOps Model AnySymbolSet TypedAnySymbol Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptyModel :: Model Source #

isEmptyModel :: Model -> Bool Source #

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

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

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

exceptFor :: AnySymbolSet -> Model -> Model Source #

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

restrictTo :: AnySymbolSet -> Model -> Model Source #

extendTo :: AnySymbolSet -> Model -> Model Source #

exact :: AnySymbolSet -> Model -> Model Source #

IsSymbolKind knd => Binary (SymbolSet knd) Source #

Instance details

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

Instance details

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

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

put :: Putter (SymbolSet knd) #

get :: Get (SymbolSet knd) #

Monoid (SymbolSet knd) Source #

Instance details

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

Instance details

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

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Associated Types

type Rep (SymbolSet knd)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model type Rep (SymbolSet knd) = D1 ('MetaData "SymbolSet" "Grisette.Internal.SymPrim.Prim.Model" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "SymbolSet" 'PrefixI 'True) (S1 ('MetaSel ('Just "unSymbolSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (SomeTypedSymbol knd)))))

Methods

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

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

Show (SymbolSet knd) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

showsPrec :: Int -> SymbolSet knd -> ShowS #

show :: SymbolSet knd -> String #

showList :: [SymbolSet knd] -> ShowS #

Eq (SymbolSet knd) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

PPrint (SymbolSet knd) Source #

Instance details

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

Methods

pformat :: SymbolSet knd -> Doc ann Source #

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

pformatList :: [SymbolSet knd] -> Doc ann Source #

Hashable (SymbolSet knd) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

hashWithSalt :: Int -> SymbolSet knd -> Int #

hash :: SymbolSet knd -> Int #

SymbolSetOps (SymbolSet knd) (TypedSymbol knd) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptySet :: SymbolSet knd Source #

isEmptySet :: SymbolSet knd -> Bool Source #

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

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

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

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

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

SymbolSetRep (SomeTypedSymbol knd) (SymbolSet knd) (TypedSymbol knd) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: SomeTypedSymbol knd -> SymbolSet knd Source #

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

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: [SomeTypedSymbol knd] -> SymbolSet knd Source #

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

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

SymbolSetRep (TypedSymbol knd t) (SymbolSet knd) (TypedSymbol knd) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

buildSymbolSet :: TypedSymbol knd t -> SymbolSet knd Source #

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

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

Instance details

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

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

Instance details

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

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

Instance details

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

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

Instance details

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

type Rep (SymbolSet knd) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

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

type ConstantSymbolSet = SymbolSet 'ConstantKind Source #

Set of constant symbols. Excluding unintepreted functions.

type AnySymbolSet = SymbolSet 'AnyKind Source #

Set of any symbols.

newtype Model Source #

Model returned by the solver.

Check ModelOps for operations, and ModelRep for manual constructions.

Constructors

Model
Fields unModel :: HashMap SomeTypedAnySymbol ModelValue

Instances

Instances details

Binary Model Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

put :: Model -> Put #

get :: Get Model #

putList :: [Model] -> Put #

Serial Model Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

deserialize :: MonadGet m => m Model #

Serialize Model Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

put :: Putter Model #

get :: Get Model #

NFData Model Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

rnf :: Model -> () #

Monoid Model Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

mempty :: Model #

mappend :: Model -> Model -> Model #

mconcat :: [Model] -> Model #

Semigroup Model Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

sconcat :: NonEmpty Model -> Model #

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

Generic Model Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Associated Types

type Rep Model
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model type Rep Model = D1 ('MetaData "Model" "Grisette.Internal.SymPrim.Prim.Model" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "Model" 'PrefixI 'True) (S1 ('MetaSel ('Just "unModel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SomeTypedAnySymbol ModelValue))))

Methods

from :: Model -> Rep Model x #

to :: Rep Model x -> Model #

Show Model Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

showsPrec :: Int -> Model -> ShowS #

show :: Model -> String #

showList :: [Model] -> ShowS #

Eq Model Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

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

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

PPrint Model Source #

Instance details

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

Methods

pformat :: Model -> Doc ann Source #

pformatPrec :: Int -> Model -> Doc ann Source #

pformatList :: [Model] -> Doc ann Source #

Hashable Model Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

hashWithSalt :: Int -> Model -> Int #

hash :: Model -> Int #

Lift Model Source #

Instance details

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

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

Methods

emptyModel :: Model Source #

isEmptyModel :: Model -> Bool Source #

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

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

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

exceptFor :: AnySymbolSet -> Model -> Model Source #

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

restrictTo :: AnySymbolSet -> Model -> Model Source #

extendTo :: AnySymbolSet -> Model -> Model Source #

exact :: AnySymbolSet -> Model -> Model Source #

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 #

type Rep Model Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Model

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

data ModelValuePair t Source #

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

Instances details

Show t => Show (ModelValuePair t) Source #
Instance details 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 Source #
Instance details Defined in Grisette.Internal.SymPrim.Prim.Model Methods buildModel :: ModelValuePair t -> Model Source #

equation :: TypedAnySymbol a -> Model -> Maybe (Term Bool) Source #

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

Evaluate a term in the given model.

Orphan instances

(ModelRep a Model, ModelRep b Model) => ModelRep (a, b) Model Source #
Instance details Methods buildModel :: (a, b) -> Model Source #
(ModelRep a Model, ModelRep b Model, ModelRep c Model) => ModelRep (a, b, c) Model Source #
Instance details 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 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 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 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 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 Methods buildModel :: (a, b, c, d, e, f, g, h) -> Model Source #