mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
update pretty printer for recursive function filtering
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7f62fa2b66
commit
1028c80851
|
@ -27,9 +27,8 @@ void ast_pp_util::collect(expr* e) {
|
|||
}
|
||||
|
||||
void ast_pp_util::collect(unsigned n, expr* const* es) {
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
for (unsigned i = 0; i < n; ++i)
|
||||
coll.visit(es[i]);
|
||||
}
|
||||
}
|
||||
|
||||
void ast_pp_util::collect(expr_ref_vector const& es) {
|
||||
|
@ -38,31 +37,31 @@ void ast_pp_util::collect(expr_ref_vector const& es) {
|
|||
|
||||
void ast_pp_util::display_decls(std::ostream& out) {
|
||||
ast_smt_pp pp(m);
|
||||
bool first = m_num_decls == 0;
|
||||
coll.order_deps(m_num_sorts);
|
||||
coll.order_deps(m_sorts);
|
||||
unsigned n = coll.get_num_sorts();
|
||||
ast_mark seen;
|
||||
for (unsigned i = m_num_sorts; i < n; ++i)
|
||||
for (unsigned i = m_sorts; i < n; ++i)
|
||||
pp.display_sort_decl(out, coll.get_sorts()[i], seen);
|
||||
m_num_sorts = n;
|
||||
m_sorts = n;
|
||||
|
||||
n = coll.get_num_decls();
|
||||
for (unsigned i = m_num_decls; i < n; ++i) {
|
||||
for (unsigned i = m_decls; i < n; ++i) {
|
||||
func_decl* f = coll.get_func_decls()[i];
|
||||
if (f->get_family_id() == null_family_id && !m_removed.contains(f)) {
|
||||
if (f->get_family_id() == null_family_id && !m_removed.contains(f))
|
||||
ast_smt2_pp(out, f, m_env) << "\n";
|
||||
}
|
||||
}
|
||||
m_num_decls = n;
|
||||
if (first) {
|
||||
vector<std::pair<func_decl*, expr*>> recfuns;
|
||||
recfun::util u(m);
|
||||
func_decl_ref_vector funs = u.get_rec_funs();
|
||||
if (funs.empty()) return;
|
||||
for (func_decl * f : funs) {
|
||||
recfuns.push_back(std::make_pair(f, u.get_def(f).get_rhs()));
|
||||
}
|
||||
m_decls = n;
|
||||
|
||||
n = coll.get_rec_decls().size();
|
||||
vector<std::pair<func_decl*, expr*>> recfuns;
|
||||
recfun::util u(m);
|
||||
for (unsigned i = m_rec_decls; i < n; ++i) {
|
||||
func_decl* f = coll.get_rec_decls()[i];
|
||||
recfuns.push_back(std::make_pair(f, u.get_def(f).get_rhs()));
|
||||
}
|
||||
if (!recfuns.empty())
|
||||
ast_smt2_pp_recdefs(out, recfuns, m_env);
|
||||
}
|
||||
m_rec_decls = n;
|
||||
}
|
||||
|
||||
void ast_pp_util::remove_decl(func_decl* f) {
|
||||
|
@ -116,14 +115,14 @@ void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls
|
|||
|
||||
void ast_pp_util::push() {
|
||||
coll.push();
|
||||
m_num_sorts_trail.push_back(m_num_sorts);
|
||||
m_num_decls_trail.push_back(m_num_decls);
|
||||
m_rec_decls.push();
|
||||
m_decls.push();
|
||||
m_sorts.push();
|
||||
}
|
||||
|
||||
void ast_pp_util::pop(unsigned n) {
|
||||
coll.pop(n);
|
||||
m_num_sorts = m_num_sorts_trail[m_num_sorts_trail.size() - n];
|
||||
m_num_decls = m_num_decls_trail[m_num_decls_trail.size() - n];
|
||||
m_num_sorts_trail.shrink(m_num_sorts_trail.size() - n);
|
||||
m_num_decls_trail.shrink(m_num_decls_trail.size() - n);
|
||||
m_rec_decls.pop(n);
|
||||
m_decls.pop(n);
|
||||
m_sorts.pop(n);
|
||||
}
|
||||
|
|
|
@ -21,22 +21,24 @@ Revision History:
|
|||
#include "ast/decl_collector.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "util/obj_hashtable.h"
|
||||
#include "util/stacked_value.h"
|
||||
|
||||
class ast_pp_util {
|
||||
ast_manager& m;
|
||||
obj_hashtable<func_decl> m_removed;
|
||||
smt2_pp_environment_dbg m_env;
|
||||
unsigned m_num_sorts, m_num_decls;
|
||||
unsigned_vector m_num_sorts_trail, m_num_decls_trail;
|
||||
stacked_value<unsigned> m_rec_decls;
|
||||
stacked_value<unsigned> m_decls;
|
||||
stacked_value<unsigned> m_sorts;
|
||||
|
||||
public:
|
||||
|
||||
decl_collector coll;
|
||||
|
||||
ast_pp_util(ast_manager& m): m(m), m_env(m), m_num_sorts(0), m_num_decls(0), coll(m) {}
|
||||
|
||||
void reset() { coll.reset(); m_removed.reset(); m_num_sorts = 0; m_num_decls = 0; }
|
||||
ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m), m_rec_decls(0), m_decls(0), m_sorts(0) {}
|
||||
|
||||
void reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u); }
|
||||
|
||||
|
||||
void collect(expr* e);
|
||||
|
||||
|
|
|
@ -19,6 +19,7 @@ Revision History:
|
|||
--*/
|
||||
#include "ast/decl_collector.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/recfun_decl_plugin.h"
|
||||
|
||||
void decl_collector::visit_sort(sort * n) {
|
||||
SASSERT(!m_visited.is_marked(n));
|
||||
|
@ -49,8 +50,12 @@ bool decl_collector::is_bool(sort * s) {
|
|||
void decl_collector::visit_func(func_decl * n) {
|
||||
if (!m_visited.is_marked(n)) {
|
||||
family_id fid = n->get_family_id();
|
||||
if (fid == null_family_id) {
|
||||
if (fid == null_family_id)
|
||||
m_decls.push_back(n);
|
||||
else if (fid == m_rec_fid) {
|
||||
m_rec_decls.push_back(n);
|
||||
recfun::util u(m());
|
||||
m_todo.push_back(u.get_def(n).get_rhs());
|
||||
}
|
||||
m_visited.mark(n, true);
|
||||
m_trail.push_back(n);
|
||||
|
@ -63,6 +68,8 @@ decl_collector::decl_collector(ast_manager & m):
|
|||
m_dt_util(m) {
|
||||
m_basic_fid = m_manager.get_basic_family_id();
|
||||
m_dt_fid = m_dt_util.get_family_id();
|
||||
recfun::util rec_util(m);
|
||||
m_rec_fid = rec_util.get_family_id();
|
||||
}
|
||||
|
||||
void decl_collector::visit(ast* n) {
|
||||
|
@ -143,9 +150,8 @@ void decl_collector::collect_deps(sort* s, sort_set& set) {
|
|||
set.insert(s);
|
||||
if (s->is_sort_of(m_dt_util.get_family_id(), DATATYPE_SORT)) {
|
||||
unsigned num_sorts = m_dt_util.get_datatype_num_parameter_sorts(s);
|
||||
for (unsigned i = 0; i < num_sorts; ++i) {
|
||||
for (unsigned i = 0; i < num_sorts; ++i)
|
||||
set.insert(m_dt_util.get_datatype_parameter_sort(s, i));
|
||||
}
|
||||
unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(s);
|
||||
for (unsigned i = 0; i < num_cnstr; i++) {
|
||||
func_decl * cnstr = m_dt_util.get_datatype_constructors(s)->get(i);
|
||||
|
@ -157,29 +163,27 @@ void decl_collector::collect_deps(sort* s, sort_set& set) {
|
|||
|
||||
for (unsigned i = s->get_num_parameters(); i-- > 0; ) {
|
||||
parameter const& p = s->get_parameter(i);
|
||||
if (p.is_ast() && is_sort(p.get_ast())) {
|
||||
if (p.is_ast() && is_sort(p.get_ast()))
|
||||
set.insert(to_sort(p.get_ast()));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void decl_collector::push() {
|
||||
m_trail_lim.push_back(m_trail.size());
|
||||
m_sorts_lim.push_back(m_sorts.size());
|
||||
m_decls_lim.push_back(m_decls.size());
|
||||
m_sorts.push_scope();
|
||||
m_decls.push_scope();
|
||||
m_rec_decls.push_scope();
|
||||
}
|
||||
|
||||
void decl_collector::pop(unsigned n) {
|
||||
SASSERT(n > 0);
|
||||
unsigned sz = m_trail_lim[m_trail_lim.size() - n];
|
||||
for (unsigned i = m_trail.size(); i-- > sz; ) {
|
||||
for (unsigned i = m_trail.size(); i-- > sz; )
|
||||
m_visited.mark(m_trail.get(i), false);
|
||||
}
|
||||
m_trail.shrink(sz);
|
||||
m_sorts.shrink(m_sorts_lim[m_sorts_lim.size() - n]);
|
||||
m_decls.shrink(m_decls_lim[m_decls_lim.size() - n]);
|
||||
m_trail_lim.shrink(m_trail_lim.size() - n);
|
||||
m_sorts_lim.shrink(m_sorts_lim.size() - n);
|
||||
m_decls_lim.shrink(m_decls_lim.size() - n);
|
||||
m_sorts.pop_scope(n);
|
||||
m_decls.pop_scope(n);
|
||||
m_rec_decls.pop_scope(n);
|
||||
}
|
||||
|
||||
|
|
|
@ -20,21 +20,22 @@ Revision History:
|
|||
#pragma once
|
||||
|
||||
#include "util/top_sort.h"
|
||||
#include "util/lim_vector.h"
|
||||
#include "ast/ast.h"
|
||||
#include "ast/datatype_decl_plugin.h"
|
||||
|
||||
class decl_collector {
|
||||
ast_manager & m_manager;
|
||||
ptr_vector<sort> m_sorts;
|
||||
ptr_vector<func_decl> m_decls;
|
||||
lim_svector<sort*> m_sorts;
|
||||
lim_svector<func_decl*> m_decls;
|
||||
lim_svector<func_decl*> m_rec_decls;
|
||||
ast_mark m_visited;
|
||||
ast_ref_vector m_trail;
|
||||
unsigned_vector m_trail_lim;
|
||||
unsigned_vector m_sorts_lim;
|
||||
unsigned_vector m_decls_lim;
|
||||
family_id m_basic_fid;
|
||||
family_id m_dt_fid;
|
||||
datatype_util m_dt_util;
|
||||
family_id m_rec_fid;
|
||||
ptr_vector<ast> m_todo;
|
||||
|
||||
void visit_sort(sort* n);
|
||||
|
@ -64,7 +65,8 @@ public:
|
|||
unsigned get_num_sorts() const { return m_sorts.size(); }
|
||||
unsigned get_num_decls() const { return m_decls.size(); }
|
||||
|
||||
ptr_vector<sort> const& get_sorts() const { return m_sorts; }
|
||||
ptr_vector<func_decl> const& get_func_decls() const { return m_decls; }
|
||||
lim_svector<sort*> const& get_sorts() const { return m_sorts; }
|
||||
lim_svector<func_decl*> const& get_func_decls() const { return m_decls; }
|
||||
lim_svector<func_decl*> const& get_rec_decls() const { return m_rec_decls; }
|
||||
};
|
||||
|
||||
|
|
|
@ -20,23 +20,24 @@ Revision History:
|
|||
|
||||
#pragma once
|
||||
// add to value the stack semantics
|
||||
#include <stack>
|
||||
#include "util/vector.h"
|
||||
template <typename T> class stacked_value {
|
||||
T m_value;
|
||||
std::stack<T> m_stack;
|
||||
vector<T> m_stack;
|
||||
public:
|
||||
|
||||
|
||||
void push() {
|
||||
m_stack.push(m_value);
|
||||
m_stack.push_back(m_value);
|
||||
}
|
||||
|
||||
void clear() {
|
||||
m_stack.clear();
|
||||
void clear(T const& m) {
|
||||
pop(m_stack.size());
|
||||
m_value = m;
|
||||
}
|
||||
|
||||
unsigned stack_size() const {
|
||||
return static_cast<unsigned>(m_stack.size());
|
||||
return m_stack.size();
|
||||
}
|
||||
|
||||
void pop() {
|
||||
|
@ -46,8 +47,8 @@ public:
|
|||
while (k-- > 0) {
|
||||
if (m_stack.empty())
|
||||
return;
|
||||
m_value = m_stack.top();
|
||||
m_stack.pop();
|
||||
m_value = m_stack.back();
|
||||
m_stack.pop_back();
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue