mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 12:51:22 +00:00
Code Activity

Improved decl_collector for uninterpreted sorts in :print_benchmark output

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-03-31 12:04:46 +01:00
parent 041520f727
commit ef3d340c85
1 changed files with 21 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/ast/decl_collector.cpp
View file

@ -23,8 +23,21 @@ void decl_collector::visit_sort(sort * n) {
family_id fid = n->get_family_id(); family_id fid = n->get_family_id();
if (m().is_uninterp(n)) if (m().is_uninterp(n))
m_sorts.push_back(n); m_sorts.push_back(n);
if (fid == m_dt_fid) if (fid == m_dt_fid) {
m_sorts.push_back(n); m_sorts.push_back(n);
unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n);
for (unsigned i = 0; i < num_cnstr; i++) {
func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i);
m_decls.push_back(cnstr);
ptr_vector<func_decl> const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr);
unsigned num_cas = cnstr_acc.size();
for (unsigned j = 0; j < num_cas; j++) {
func_decl * accsr = cnstr_acc.get(j);
m_decls.push_back(accsr);
}
}
}
} }
bool decl_collector::is_bool(sort * s) { bool decl_collector::is_bool(sort * s) {
@ -38,14 +51,15 @@ void decl_collector::visit_func(func_decl * n) {
m_preds.push_back(n); m_preds.push_back(n);
else else
m_decls.push_back(n); m_decls.push_back(n);
} }
} }
decl_collector::decl_collector(ast_manager & m, bool preds): decl_collector::decl_collector(ast_manager & m, bool preds):
m_manager(m), m_manager(m),
m_sep_preds(preds) { m_sep_preds(preds),
m_dt_util(m) {
m_basic_fid = m_manager.get_basic_family_id(); m_basic_fid = m_manager.get_basic_family_id();
m_dt_fid = m_manager.mk_family_id("datatype"); m_dt_fid = m_dt_util.get_family_id();
} }
void decl_collector::visit(ast* n) { void decl_collector::visit(ast* n) {
@ -55,7 +69,7 @@ void decl_collector::visit(ast* n) {
n = todo.back(); n = todo.back();
todo.pop_back(); todo.pop_back();
if (!m_visited.is_marked(n)) { if (!m_visited.is_marked(n)) {
m_visited.mark(n, true); m_visited.mark(n, true);
switch(n->get_kind()) { switch(n->get_kind()) {
case AST_APP: { case AST_APP: {
app * a = to_app(n); app * a = to_app(n);
@ -64,7 +78,7 @@ void decl_collector::visit(ast* n) {
} }
todo.push_back(a->get_decl()); todo.push_back(a->get_decl());
break; break;
} }
case AST_QUANTIFIER: { case AST_QUANTIFIER: {
quantifier * q = to_quantifier(n); quantifier * q = to_quantifier(n);
unsigned num_decls = q->get_num_decls(); unsigned num_decls = q->get_num_decls();
@ -77,7 +91,7 @@ void decl_collector::visit(ast* n) {
} }
break; break;
} }
case AST_SORT: case AST_SORT:
visit_sort(to_sort(n)); visit_sort(to_sort(n));
break; break;
case AST_FUNC_DECL: { case AST_FUNC_DECL: {