| 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 | Safe-Inferred |
| Language | Haskell2010 |
Grisette.Internal.SymPrim.Prim.Model
Contents
Description
Synopsis
- newtype SymbolSet knd = SymbolSet {
- unSymbolSet :: HashSet (SomeTypedSymbol knd)
- type ConstantSymbolSet = SymbolSet 'ConstantKind
- type AnySymbolSet = SymbolSet 'AnyKind
- newtype Model = Model {}
- 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 Source #
Set of symbols.
Check SymbolSetOps for operations, and
SymbolSetRep for manual constructions.
Constructors
| SymbolSet | |
Fields
| |
Instances
type ConstantSymbolSet = SymbolSet 'ConstantKind Source #
Set of constant symbols. Excluding unintepreted functions.
type AnySymbolSet = SymbolSet 'AnyKind Source #
Set of any symbols.
Constructors
| Model | |
Fields | |
Instances
data ModelValuePair t Source #
A type used for building a model by hand.
>>>buildModel ("x" ::= (1 :: Integer), "y" ::= True) :: ModelModel {x -> 1 :: Integer, y -> true :: Bool}
Constructors
| (TypedAnySymbol t) ::= t |
Instances
| Show t => Show (ModelValuePair t) Source # | |
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 # | |
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.