grisette-0.1.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellSafe-Inferred
LanguageHaskell2010

Grisette.IR.SymPrim.Data.Prim.Model

Description

 
Synopsis

Documentation

newtype SymbolSet Source #

Symbolic constant set.

Instances

Instances details
Monoid SymbolSet Source # 
Instance details

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

Semigroup SymbolSet Source # 
Instance details

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

Generic SymbolSet Source # 
Instance details

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

Associated Types

type Rep SymbolSet :: Type -> Type #

Show SymbolSet Source # 
Instance details

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

Eq SymbolSet Source # 
Instance details

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

ExtractSymbolics SymbolSet Source # 
Instance details

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

Hashable SymbolSet Source # 
Instance details

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

SymbolSetOps SymbolSet TypedSymbol Source # 
Instance details

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

ModelOps Model SymbolSet TypedSymbol Source # 
Instance details

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

SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelValuePair t) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b) SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair a, ModelSymPair b) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SymbolSetRep (TypedSymbol a, TypedSymbol b, TypedSymbol c) SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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

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

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

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

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

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

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

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

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.

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

ModelRep (ModelValuePair t) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair t) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair a, ModelSymPair b) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

ModelRep (ModelSymPair a, ModelSymPair b, ModelSymPair c, ModelSymPair d, ModelSymPair e) Model SymbolSet TypedSymbol Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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

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

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

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

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

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

ModelRep (ModelValuePair t) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelValuePair a, ModelValuePair b) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c) Model SymbolSet TypedSymbol Source # 
Instance details

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

ModelRep (ModelValuePair a, ModelValuePair b, ModelValuePair c, ModelValuePair d) Model SymbolSet TypedSymbol Source # 
Instance details

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

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

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

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

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

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