1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39

use crate::Located;
pub use crate::syntax::{
	Symbol,
	Term,
	SortedVar,
	Sort,
	SortDeclaration
};

/// (check-sat) command response.
/// <check_sat_response> ::= sat | unsat | unknown
pub type CheckSat = crate::response::CheckSat;

/// (get-model) command response.
/// <get_model_response> ::= ( <model_response>* )
pub struct Model {
	pub sorts: Vec<Located<SortDeclaration>>,
	pub definitions: Vec<Located<Definition>>
}

/// Model function definition.
/// <model_response> ::= ( define-fun <function_def> )
///					| ( define-fun-rec <function_def> )
///					| ( define-funs-rec ( <function_dec>n+1 ) ( <term>n+1 ) )
/// <function_def> ::= <symbol> ( <sorted_var>* ) <sort> <term>
pub struct Definition {
	pub rec: bool,
	pub declarations: Vec<Located<Declaration>>,
	pub bodies: Vec<Located<Term>>,
	pub comments: String
}

/// Function declaration.
/// <function_dec> ::= ( <symbol> ( <sorted_var>* ) <sort> )
pub struct Declaration {
	pub id: Located<Symbol>,
	pub args: Vec<Located<SortedVar>>,
	pub return_sort: Located<Sort>
}