Module smt2::syntax::ast

Structs

Attribute	::= | <attribute_value>
Binding	<var_binding> ::= ( )
ConstructorDeclaration	<constructor_dec> ::= ( <selector_dec>* )
DataTypeDeclaration	<datatype_dec> ::= ( <constructor_dec>+ ) | ( par ( + ) <constructor_dec>+ )
Ident	Identifiers.
Keyword
MatchCase
Pattern
SelectorDeclaration	<selector_dec> ::= ( )
Sort	::= | ( +)
SortDeclaration	<sort_dec> ::= ( )
SortedVar	<sorted_var> ::= ( )
Symbol	Symbol.

Enums

AttributeValue	<attribute_value> ::= <spec_const> | | <s_expr*>
Command	::= ( assert ) | ( check-sat ) | ( declare-const ) | ( declare-datatype <datatype_decl> ) | ( declare-datatypes ( <sort_dec>n+1 ) ( <datatype_dec>n+1 ) ) | ( exit ) | ( set-info ) | ( set-logic )
Index	Identifiers index.
SExpr	<s_expr> ::= <spec_const> | | | <s_expr*>
Term	::= <spec_const> | ( let ( <var_binding>+ ) ) | ( forall ( <sorted_var>+ ) ) | ( exists ( <sorted_var>+ ) )