[−][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

compile
compile_binding
compile_constructor_declaration
compile_datatype_declaration
compile_function
compile_ident
compile_selector_declaration
compile_sort
compile_sort_declaration
compile_sort_ref
compile_sorted_var
compile_symbol
compile_term

Type Definitions

Trait aliases