Grisette.IR.SymPrim.Data.Prim.Model

Documentation

newtype SymbolSet

Symbolic constant set.

Constructors

SymbolSet

Fields

• unSymbolSet :: HashSet SomeTypedSymbol

Instances

Monoid SymbolSet

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

mempty :: SymbolSet

mappend :: SymbolSet -> SymbolSet -> SymbolSet

mconcat :: [SymbolSet] -> SymbolSet

Semigroup SymbolSet

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

sconcat :: NonEmpty SymbolSet -> SymbolSet

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

Generic SymbolSet

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

showsPrec :: Int -> SymbolSet -> ShowS

show :: SymbolSet -> String

showList :: [SymbolSet] -> ShowS

Eq SymbolSet

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

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

ExtractSymbolics SymbolSet

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

extractSymbolics :: SymbolSet -> SymbolSet

Hashable SymbolSet

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

hashWithSalt :: Int -> SymbolSet -> Int

hash :: SymbolSet -> Int

SymbolSetOps SymbolSet TypedSymbol

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

Methods

emptyModel :: Model

isEmptyModel :: Model -> Bool

valueOf :: TypedSymbol t -> Model -> Maybe t

insertValue :: TypedSymbol t -> t -> Model -> Model

exceptFor :: SymbolSet -> Model -> Model

restrictTo :: SymbolSet -> Model -> Model

extendTo :: SymbolSet -> Model -> Model

exact :: SymbolSet -> Model -> Model

SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildSymbolSet :: TypedSymbol t -> SymbolSet

ModelRep (ModelValuePair t) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: ModelValuePair t -> Model

ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: ModelSymPair t -> Model

SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (ModelValuePair a, ModelValuePair b) -> Model

ModelRep (ModelSymPair a, ModelSymPair b) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b) -> Model

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c) -> Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c) -> Model

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) -> Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) -> Model

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) -> Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) -> Model

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) Model SymbolSet TypedSymbol

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) Model SymbolSet TypedSymbol

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h) Model SymbolSet TypedSymbol

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

type Rep SymbolSet

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-6BNF0pL4m6OHMsp5yKPRPi" 'True) (C1 ('MetaCons "SymbolSet" 'PrefixI 'True) (S1 ('MetaSel ('Just "unSymbolSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet SomeTypedSymbol))))

newtype Model

Model returned by the solver.

Constructors

Model

Fields

• unModel :: HashMap SomeTypedSymbol ModelValue

Instances

Generic Model

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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

showsPrec :: Int -> Model -> ShowS

show :: Model -> String

showList :: [Model] -> ShowS

Eq Model

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

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

Hashable Model

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

hashWithSalt :: Int -> Model -> Int

hash :: Model -> Int

ModelOps Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

emptyModel :: Model

isEmptyModel :: Model -> Bool

valueOf :: TypedSymbol t -> Model -> Maybe t

insertValue :: TypedSymbol t -> t -> Model -> Model

exceptFor :: SymbolSet -> Model -> Model

restrictTo :: SymbolSet -> Model -> Model

extendTo :: SymbolSet -> Model -> Model

exact :: SymbolSet -> Model -> Model

ModelRep (ModelValuePair t) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: ModelValuePair t -> Model

ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: ModelSymPair t -> Model

ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (ModelValuePair a, ModelValuePair b) -> Model

ModelRep (ModelSymPair a, ModelSymPair b) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b) -> Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c) -> Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c) -> Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) -> Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) -> Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) -> Model

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

buildModel :: (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) -> Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) Model SymbolSet TypedSymbol

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) Model SymbolSet TypedSymbol

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e, ModelSymPair f, ModelSymPair g, ModelSymPair h) Model SymbolSet TypedSymbol

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

type Rep Model

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-6BNF0pL4m6OHMsp5yKPRPi" '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.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

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: ModelValuePair t -> Model

ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (ModelValuePair a, ModelValuePair b) -> Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c) -> Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) -> Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e) -> Model

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f) Model SymbolSet TypedSymbol

Defined in Grisette.IR.SymPrim.Data.Prim.Model

Methods

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g) Model SymbolSet TypedSymbol

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d, ModelValuePair e, ModelValuePair f, ModelValuePair g, ModelValuePair h) Model SymbolSet TypedSymbol

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

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

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