mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 03:15:50 +00:00
make static features avoid stack #5758
This commit is contained in:
Nikolaj Bjorner
parent
2c44454a17
commit
ef481073b2
2 changed files with 114 additions and 60 deletions
|
|
@ -18,6 +18,7 @@ Revision History:
|
|||
--*/
|
||||
#include "ast/static_features.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "ast/for_each_expr.h"
|
||||
|
||||
static_features::static_features(ast_manager & m):
|
||||
|
|
@ -39,7 +40,8 @@ static_features::static_features(ast_manager & m):
|
|||
}
|
||||
|
||||
void static_features::reset() {
|
||||
m_already_visited .reset();
|
||||
m_pre_processed .reset();
|
||||
m_post_processed.reset();
|
||||
m_cnf = true;
|
||||
m_num_exprs = 0;
|
||||
m_num_roots = 0;
|
||||
|
|
@ -343,8 +345,8 @@ void static_features::update_core(expr * e) {
|
|||
}
|
||||
func_decl * d = to_app(e)->get_decl();
|
||||
inc_num_apps(d);
|
||||
if (d->get_arity() > 0 && !is_marked(d)) {
|
||||
mark(d);
|
||||
if (d->get_arity() > 0 && !is_marked_pre(d)) {
|
||||
mark_pre(d);
|
||||
if (fid == null_family_id)
|
||||
m_num_uninterpreted_functions++;
|
||||
}
|
||||
|
|
@ -396,73 +398,68 @@ void static_features::update_core(sort * s) {
|
|||
check_array(s);
|
||||
}
|
||||
|
||||
void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth) {
|
||||
TRACE("static_features", tout << "processing\n" << mk_pp(e, m) << "\n";);
|
||||
if (is_var(e))
|
||||
return;
|
||||
if (is_marked(e)) {
|
||||
m_num_sharing++;
|
||||
return;
|
||||
}
|
||||
bool static_features::pre_process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx) {
|
||||
if (is_marked_post(e))
|
||||
return true;
|
||||
|
||||
if (stack_depth > m_max_stack_depth) {
|
||||
ptr_vector<expr> todo;
|
||||
todo.push_back(e);
|
||||
for (unsigned i = 0; i < todo.size(); ++i) {
|
||||
e = todo[i];
|
||||
if (is_marked(e))
|
||||
continue;
|
||||
if (is_basic_expr(e)) {
|
||||
mark(e);
|
||||
todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
|
||||
}
|
||||
else {
|
||||
process(e, form_ctx, or_and_ctx, ite_ctx, stack_depth - 10);
|
||||
}
|
||||
}
|
||||
return;
|
||||
if (is_var(e)) {
|
||||
mark_pre(e);
|
||||
mark_post(e);
|
||||
return true;
|
||||
}
|
||||
|
||||
mark(e);
|
||||
if (is_marked_pre(e)) {
|
||||
m_num_sharing++;
|
||||
return true;
|
||||
}
|
||||
|
||||
mark_pre(e);
|
||||
|
||||
update_core(e);
|
||||
|
||||
if (is_quantifier(e)) {
|
||||
expr * body = to_quantifier(e)->get_expr();
|
||||
process(body, false, false, false, stack_depth+1);
|
||||
if (is_marked_post(body))
|
||||
return true;
|
||||
add_process(body, false, false, false);
|
||||
return false;
|
||||
}
|
||||
|
||||
auto [form_ctx_new, or_and_ctx_new, ite_ctx_new] = new_ctx(e);
|
||||
|
||||
bool all_processed = true;
|
||||
for (expr* arg : *to_app(e)) {
|
||||
m.is_not(arg, arg);
|
||||
if (!is_marked_post(arg)) {
|
||||
add_process(arg, form_ctx_new, or_and_ctx_new, ite_ctx_new);
|
||||
all_processed = false;
|
||||
}
|
||||
}
|
||||
return all_processed;
|
||||
}
|
||||
|
||||
void static_features::post_process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx) {
|
||||
if (is_marked_post(e))
|
||||
return;
|
||||
|
||||
mark_post(e);
|
||||
|
||||
if (is_quantifier(e)) {
|
||||
expr * body = to_quantifier(e)->get_expr();
|
||||
set_depth(e, get_depth(body)+1);
|
||||
return;
|
||||
}
|
||||
|
||||
bool form_ctx_new = false;
|
||||
bool or_and_ctx_new = false;
|
||||
bool ite_ctx_new = false;
|
||||
|
||||
if (is_basic_expr(e)) {
|
||||
switch (to_app(e)->get_decl_kind()) {
|
||||
case OP_ITE:
|
||||
form_ctx_new = m.is_bool(e);
|
||||
ite_ctx_new = true;
|
||||
break;
|
||||
case OP_AND:
|
||||
case OP_OR:
|
||||
form_ctx_new = true;
|
||||
or_and_ctx_new = true;
|
||||
break;
|
||||
case OP_EQ:
|
||||
form_ctx_new = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
unsigned depth = 0;
|
||||
unsigned form_depth = 0;
|
||||
unsigned or_and_depth = 0;
|
||||
unsigned ite_depth = 0;
|
||||
|
||||
auto [form_ctx_new, or_and_ctx_new, ite_ctx_new] = new_ctx(e);
|
||||
|
||||
for (expr* arg : *to_app(e)) {
|
||||
m.is_not(arg, arg);
|
||||
process(arg, form_ctx_new, or_and_ctx_new, ite_ctx_new, stack_depth+1);
|
||||
SASSERT(is_marked_post(arg));
|
||||
depth = std::max(depth, get_depth(arg));
|
||||
if (form_ctx_new)
|
||||
form_depth = std::max(form_depth, get_form_depth(arg));
|
||||
|
|
@ -507,16 +504,57 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite
|
|||
}
|
||||
set_ite_depth(e, ite_depth);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
std::tuple<bool, bool, bool> static_features::new_ctx(expr* e) {
|
||||
bool form_ctx_new = false;
|
||||
bool or_and_ctx_new = false;
|
||||
bool ite_ctx_new = false;
|
||||
|
||||
if (is_basic_expr(e)) {
|
||||
switch (to_app(e)->get_decl_kind()) {
|
||||
case OP_ITE:
|
||||
form_ctx_new = m.is_bool(e);
|
||||
ite_ctx_new = true;
|
||||
break;
|
||||
case OP_AND:
|
||||
case OP_OR:
|
||||
form_ctx_new = true;
|
||||
or_and_ctx_new = true;
|
||||
break;
|
||||
case OP_EQ:
|
||||
form_ctx_new = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
return std::tuple(form_ctx_new, or_and_ctx_new, ite_ctx_new);
|
||||
}
|
||||
|
||||
void static_features::process_all() {
|
||||
while (!m_to_process.empty()) {
|
||||
auto const& [e, form, or_and, ite] = m_to_process.back();
|
||||
if (is_marked_post(e)) {
|
||||
m_to_process.pop_back();
|
||||
continue;
|
||||
}
|
||||
if (!pre_process(e, form, or_and, ite))
|
||||
continue;
|
||||
post_process(e, form, or_and, ite);
|
||||
m_to_process.pop_back();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void static_features::process_root(expr * e) {
|
||||
if (is_marked(e)) {
|
||||
if (is_marked_post(e)) {
|
||||
m_num_sharing++;
|
||||
return;
|
||||
}
|
||||
m_num_roots++;
|
||||
if (m.is_or(e)) {
|
||||
mark(e);
|
||||
mark_post(e);
|
||||
m_num_clauses++;
|
||||
m_num_bool_exprs++;
|
||||
unsigned num_args = to_app(e)->get_num_args();
|
||||
|
|
@ -530,7 +568,8 @@ void static_features::process_root(expr * e) {
|
|||
expr * arg = to_app(e)->get_arg(i);
|
||||
if (m.is_not(arg))
|
||||
arg = to_app(arg)->get_arg(0);
|
||||
process(arg, true, true, false, 0);
|
||||
add_process(arg, true, true, false);
|
||||
process_all();
|
||||
depth = std::max(depth, get_depth(arg));
|
||||
form_depth = std::max(form_depth, get_form_depth(arg));
|
||||
or_and_depth = std::max(or_and_depth, get_or_and_depth(arg));
|
||||
|
|
@ -558,7 +597,8 @@ void static_features::process_root(expr * e) {
|
|||
m_num_units++;
|
||||
m_num_clauses++;
|
||||
}
|
||||
process(e, false, false, false, 0);
|
||||
add_process(e, false, false, false);
|
||||
process_all();
|
||||
}
|
||||
|
||||
void static_features::collect(unsigned num_formulas, expr * const * formulas) {
|
||||
|
|
|
|||
|
|
@ -28,6 +28,12 @@ Revision History:
|
|||
#include "util/map.h"
|
||||
|
||||
struct static_features {
|
||||
struct to_process {
|
||||
expr* e;
|
||||
bool form_ctx;
|
||||
bool and_or_ctx;
|
||||
bool ite_ctx;
|
||||
};
|
||||
ast_manager & m;
|
||||
arith_util m_autil;
|
||||
bv_util m_bvutil;
|
||||
|
|
@ -39,7 +45,7 @@ struct static_features {
|
|||
family_id m_lfid;
|
||||
family_id m_arrfid;
|
||||
family_id m_srfid;
|
||||
ast_mark m_already_visited;
|
||||
ast_mark m_pre_processed, m_post_processed;
|
||||
bool m_cnf;
|
||||
unsigned m_num_exprs; //
|
||||
unsigned m_num_roots; //
|
||||
|
|
@ -111,14 +117,17 @@ struct static_features {
|
|||
u_map<unsigned> m_expr2formula_depth;
|
||||
|
||||
unsigned m_num_theories;
|
||||
bool_vector m_theories; // mapping family_id -> bool
|
||||
bool_vector m_theories; // mapping family_id -> bool
|
||||
|
||||
symbol m_label_sym;
|
||||
symbol m_pattern_sym;
|
||||
symbol m_expr_list_sym;
|
||||
svector<to_process> m_to_process;
|
||||
|
||||
bool is_marked(ast * e) const { return m_already_visited.is_marked(e); }
|
||||
void mark(ast * e) { m_already_visited.mark(e, true); }
|
||||
bool is_marked_pre(ast * e) const { return m_pre_processed.is_marked(e); }
|
||||
void mark_pre(ast * e) { m_pre_processed.mark(e, true); }
|
||||
bool is_marked_post(ast * e) const { return m_post_processed.is_marked(e); }
|
||||
void mark_post(ast * e) { m_post_processed.mark(e, true); }
|
||||
bool is_bool(expr const * e) const { return m.is_bool(e); }
|
||||
bool is_basic_expr(expr const * e) const { return is_app(e) && to_app(e)->get_family_id() == m_bfid; }
|
||||
bool is_arith_expr(expr const * e) const { return is_app(e) && to_app(e)->get_family_id() == m_afid; }
|
||||
|
|
@ -161,7 +170,12 @@ struct static_features {
|
|||
void inc_num_aliens(family_id fid) { m_num_aliens_per_family.reserve(fid+1, 0); m_num_aliens_per_family[fid]++; }
|
||||
void update_core(expr * e);
|
||||
void update_core(sort * s);
|
||||
void process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth);
|
||||
// void process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth);
|
||||
bool pre_process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx);
|
||||
void post_process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx);
|
||||
void add_process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx) { m_to_process.push_back({e, form_ctx, or_and_ctx, ite_ctx}); }
|
||||
void process_all();
|
||||
std::tuple<bool, bool, bool> new_ctx(expr* );
|
||||
void process_root(expr * e);
|
||||
unsigned get_depth(expr const * e) const { return m_expr2depth.get(e->get_id(), 1); }
|
||||
void set_depth(expr const * e, unsigned d) { m_expr2depth.setx(e->get_id(), d, 1); }
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue