Safe Haskell | None |
---|---|
Language | Haskell98 |
This module contains the types defining an SMTLIB2 interface.
- type Raw = Text
- data TheorySymbol = Thy {}
- data Sem
- data SmtSort
- sortSmtSort :: Bool -> SEnv DataDecl -> Sort -> SmtSort
- isIntSmtSort :: SEnv DataDecl -> Sort -> Bool
- data SymEnv = SymEnv {}
- symEnv :: SEnv Sort -> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv
- symEnvSort :: Symbol -> SymEnv -> Maybe Sort
- symEnvTheory :: Symbol -> SymEnv -> Maybe TheorySymbol
- insertSymEnv :: Symbol -> Sort -> SymEnv -> SymEnv
- symbolAtName :: PPrint a => Symbol -> SymEnv -> a -> Sort -> Symbol
- symbolAtSmtName :: PPrint a => Symbol -> SymEnv -> a -> FuncSort -> Symbol
Serialized Representation
Theory Symbol
Sem
describes the SMT semantics for a given symbol
Theory Sorts
A Refinement of Sort
that describes SMTLIB Sorts
sortSmtSort :: Bool -> SEnv DataDecl -> Sort -> SmtSort Source #
The poly
parameter is True when we are *declaring* sorts,
and so we need to leave type variables be; it is False when
we are declaring variables etc., and there, we serialize them
using Int
(though really, there SHOULD BE NO floating tyVars...
'smtSort True msg t' serializes a sort t
using type variables,
'smtSort False msg t' serializes a sort t
using Int
instead of tyvars.
Symbol Environments
SymEnv | |
|
symEnvTheory :: Symbol -> SymEnv -> Maybe TheorySymbol Source #