mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

fix #4749

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-10-22 12:01:40 -07:00
parent c9900720f8
commit a083633ab4
3 changed files with 20 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast_pp_util.cpp
View file

@ -41,9 +41,9 @@ void ast_pp_util::display_decls(std::ostream& out) {
bool first = m_num_decls == 0; bool first = m_num_decls == 0;
coll.order_deps(m_num_sorts); coll.order_deps(m_num_sorts);
unsigned n = coll.get_num_sorts(); unsigned n = coll.get_num_sorts();
for (unsigned i = m_num_sorts; i < n; ++i) { ast_mark seen;
pp.display_ast_smt2(out, coll.get_sorts()[i], 0, 0, nullptr); for (unsigned i = m_num_sorts; i < n; ++i)
} pp.display_sort_decl(out, coll.get_sorts()[i], seen);
m_num_sorts = n; m_num_sorts = n;
n = coll.get_num_decls(); n = coll.get_num_decls();
for (unsigned i = m_num_decls; i < n; ++i) { for (unsigned i = m_num_decls; i < n; ++i) {

18
src/ast/ast_smt_pp.cpp
View file

@ -791,12 +791,18 @@ public:
ptr_vector<datatype::def> defs; ptr_vector<datatype::def> defs;
util.get_defs(s, defs); util.get_defs(s, defs);
unsigned j = 0;
for (datatype::def* d : defs) { for (datatype::def* d : defs) {
sort_ref sr = d->instantiate(ps); sort_ref sr = d->instantiate(ps);
if (mark.is_marked(sr)) return; // already processed if (mark.is_marked(sr))
continue;
mark.mark(sr, true); mark.mark(sr, true);
defs[j++] = d;
} }
defs.shrink(j);
if (defs.empty())
return;
m_out << "(declare-datatypes ("; m_out << "(declare-datatypes (";
bool first_def = true; bool first_def = true;
for (datatype::def* d : defs) { for (datatype::def* d : defs) {
@ -925,6 +931,14 @@ void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, u
} }
} }
void ast_smt_pp::display_sort_decl(std::ostream& out, sort* s, ast_mark& seen) {
ptr_vector<quantifier> ql;
smt_renaming rn;
smt_printer p(out, m_manager, ql, rn, m_logic, false, m_simplify_implies, 0, 0, nullptr);
p.pp_sort_decl(seen, s);
}
void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
ptr_vector<quantifier> ql; ptr_vector<quantifier> ql;

1
src/ast/ast_smt_pp.h
View file

@ -79,6 +79,7 @@ public:
void display_smt2(std::ostream& strm, expr* n); void display_smt2(std::ostream& strm, expr* n);
void display_expr_smt2(std::ostream& strm, expr* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = nullptr); void display_expr_smt2(std::ostream& strm, expr* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = nullptr);
void display_ast_smt2(std::ostream& strm, ast* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = nullptr); void display_ast_smt2(std::ostream& strm, ast* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = nullptr);
void display_sort_decl(std::ostream& out, sort* s, ast_mark& seen);
}; };