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	Safe-Inferred
Language	Haskell2010

Grisette.IR.SymPrim.Data.Prim.Model

Contents

Orphan instances

Description

Synopsis

newtype SymbolSet = SymbolSet {
- unSymbolSet :: HashSet SomeTypedSymbol
}
newtype Model = Model {
- unModel :: HashMap SomeTypedSymbol ModelValue
}
data ModelValuePair t = (TypedSymbol t) ::= t
equation :: TypedSymbol a -> Model -> Maybe (Term Bool)
evaluateTerm :: forall a. SupportedPrim a => Bool -> Model -> Term a -> Term a

Documentation

newtype SymbolSet Source #

Symbolic constant set.

Constructors

SymbolSet
Fields unSymbolSet :: HashSet SomeTypedSymbol

Instances

Instances details

Monoid SymbolSet Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods mempty :: SymbolSet # mappend :: SymbolSet -> SymbolSet -> SymbolSet # mconcat :: [SymbolSet] -> SymbolSet #
Semigroup SymbolSet Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods (<>) :: SymbolSet -> SymbolSet -> SymbolSet # sconcat :: NonEmpty SymbolSet -> SymbolSet # stimes :: Integral b => b -> SymbolSet -> SymbolSet #
Generic SymbolSet Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Associated Types type Rep SymbolSet :: Type -> Type # Methods from :: SymbolSet -> Rep SymbolSet x # to :: Rep SymbolSet x -> SymbolSet #
Show SymbolSet Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods showsPrec :: Int -> SymbolSet -> ShowS # show :: SymbolSet -> String # showList :: [SymbolSet] -> ShowS #
Eq SymbolSet Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods (==) :: SymbolSet -> SymbolSet -> Bool # (/=) :: SymbolSet -> SymbolSet -> Bool #
ExtractSymbolics SymbolSet Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods extractSymbolics :: SymbolSet -> SymbolSet Source #
Hashable SymbolSet Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods hashWithSalt :: Int -> SymbolSet -> Int # hash :: SymbolSet -> Int #
SymbolSetOps SymbolSet TypedSymbol Source #
Instance details 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 #
ModelOps Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods emptyModel :: Model Source # isEmptyModel :: Model -> Bool Source # modelContains :: TypedSymbol a -> Model -> Bool Source # valueOf :: TypedSymbol t -> Model -> Maybe t Source # insertValue :: TypedSymbol t -> t -> Model -> Model Source # exceptFor :: SymbolSet -> Model -> Model Source # exceptFor' :: TypedSymbol t -> Model -> Model Source # restrictTo :: SymbolSet -> Model -> Model Source # extendTo :: SymbolSet -> Model -> Model Source # exact :: SymbolSet -> Model -> Model Source #
SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildSymbolSet :: TypedSymbol t -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b) -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c) -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d) -> SymbolSet Source #
SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e) -> SymbolSet Source #
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 Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f) -> SymbolSet Source #
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 Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g) -> SymbolSet Source #
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 Methods buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d, TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h) -> SymbolSet Source #
type Rep SymbolSet Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model type Rep SymbolSet = D1 ('MetaData "SymbolSet" "Grisette.IR.SymPrim.Data.Prim.Model" "grisette-0.2.0.0-CYZZ7WjRTnw1wxrPITB8ce" 'True) (C1 ('MetaCons "SymbolSet" 'PrefixI 'True) (S1 ('MetaSel ('Just "unSymbolSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet SomeTypedSymbol))))

newtype Model Source #

Model returned by the solver.

Constructors

Model
Fields unModel :: HashMap SomeTypedSymbol ModelValue

Instances

Instances details

Monoid Model Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods mempty :: Model # mappend :: Model -> Model -> Model # mconcat :: [Model] -> Model #
Semigroup Model Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods (<>) :: Model -> Model -> Model # sconcat :: NonEmpty Model -> Model # stimes :: Integral b => b -> Model -> Model #
Generic Model Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Associated Types type Rep Model :: Type -> Type # Methods from :: Model -> Rep Model x # to :: Rep Model x -> Model #
Show Model Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods showsPrec :: Int -> Model -> ShowS # show :: Model -> String # showList :: [Model] -> ShowS #
Eq Model Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods (==) :: Model -> Model -> Bool # (/=) :: Model -> Model -> Bool #
Hashable Model Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods hashWithSalt :: Int -> Model -> Int # hash :: Model -> Int #
ModelOps Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods emptyModel :: Model Source # isEmptyModel :: Model -> Bool Source # modelContains :: TypedSymbol a -> Model -> Bool Source # valueOf :: TypedSymbol t -> Model -> Maybe t Source # insertValue :: TypedSymbol t -> t -> Model -> Model Source # exceptFor :: SymbolSet -> Model -> Model Source # exceptFor' :: TypedSymbol t -> Model -> Model Source # restrictTo :: SymbolSet -> Model -> Model Source # extendTo :: SymbolSet -> Model -> Model Source # exact :: SymbolSet -> Model -> Model Source #
ModelRep (ModelValuePair t) Model Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: ModelValuePair t -> Model Source #
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 #
type Rep Model Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model type Rep Model = D1 ('MetaData "Model" "Grisette.IR.SymPrim.Data.Prim.Model" "grisette-0.2.0.0-CYZZ7WjRTnw1wxrPITB8ce" 'True) (C1 ('MetaCons "Model" 'PrefixI 'True) (S1 ('MetaSel ('Just "unModel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap SomeTypedSymbol 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

(TypedSymbol t) ::= t

Instances

Instances details

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

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

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

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 #