[−][src]Crate smt2
Re-exports
pub use location::*; |
pub use error::Error; |
pub use error::Result; |
pub use syntax::lexer; |
pub use syntax::lexer::Lexer; |
pub use typing::Typed; |
pub use typing::TypeChecker; |
pub use typing::TypeRef; |
pub use typing::GroundTypeRef; |
pub use client::Client; |
Modules
client | |
error | |
location | |
response | |
syntax | |
typing |
Structs
Binding | Variable binding. |
ConstructorDeclaration | |
Context | Evaluation context. Maps each variable to its sort. |
DataTypeDeclaration | Data type declaration. |
GroundSort | A ground sort is a sort fully applied (arity 0). |
MatchCase | |
SelectorDeclaration | Selector declaration. |
SortDeclaration | Sort declaration. |
Sorted | |
SortedVar | Sorted variable. |
UnresolvedConstructorDeclaration | |
UnresolvedDataTypeDeclaration | Data type declaration. |
UnresolvedSelectorDeclaration | Selector declaration, where sorts are unresolved references. |
Enums
AbstractGroundSort | A ground sort with sort parameter variables, used in a datatype declaration. Parameters are identified with their index. |
Command | SMT2-lib command. |
Pattern | |
Term | A term. |
TypeCheckError | Functions type check errors. |
Traits
Compiler | |
Environment | SMT2-lib solver environment. |
Function | SMT2-lib function. |
Server | |
SortedWith |
Functions
Type Definitions
ExecResult |
Trait aliases
Sort |