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

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 # valueOf :: TypedSymbol t -> Model -> Maybe t Source # insertValue :: TypedSymbol t -> t -> Model -> Model Source # exceptFor :: SymbolSet -> 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 #
ModelRep (ModelValuePair t) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: ModelValuePair t -> Model Source #
ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: ModelSymPair t -> Model 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 #
ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b) -> Model 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 #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c) -> Model 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 #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) -> Model 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 #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) -> Model 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 #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) -> Model 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 #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g) -> Model 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 #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h) -> Model 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.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" '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

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 # valueOf :: TypedSymbol t -> Model -> Maybe t Source # insertValue :: TypedSymbol t -> t -> Model -> Model Source # exceptFor :: SymbolSet -> Model -> Model Source # restrictTo :: SymbolSet -> Model -> Model Source # extendTo :: SymbolSet -> Model -> Model Source # exact :: SymbolSet -> Model -> Model Source #
ModelRep (ModelValuePair t) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: ModelValuePair t -> Model Source #
ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: ModelSymPair t -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b) -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c) -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g) -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) -> Model Source #
ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.SymPrim Methods buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair 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.1.0.0-7JmpZvRpjzaDDLSSjCfe9O" '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 SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: ModelValuePair t -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b) -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c) -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) -> Model Source #
ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) Model SymbolSet TypedSymbol Source #
Instance details Defined in Grisette.IR.SymPrim.Data.Prim.Model Methods buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) -> Model Source #

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

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