mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

remove unused static features

Browse source 
remove static features that tax solving time on large instances.
This commit is contained in:
Nikolaj Bjorner 2022-06-16 15:39:40 -07:00
parent 477e9625ef
commit 08c44bc6f6
2 changed files with 3 additions and 63 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

53
src/ast/static_features.cpp
View file

@ -56,12 +56,6 @@ void static_features::reset() {
m_num_nested_formulas = 0;
m_num_bool_exprs = 0;
m_num_bool_constants = 0;
m_num_formula_trees = 0;
m_max_formula_depth = 0;
m_sum_formula_depth = 0;
m_num_or_and_trees = 0;
m_max_or_and_tree_depth = 0;
m_sum_or_and_tree_depth = 0;
m_num_ite_trees = 0;
m_max_ite_tree_depth = 0;
m_sum_ite_tree_depth = 0;
@ -461,10 +455,6 @@ void static_features::post_process(expr * e, bool form_ctx, bool or_and_ctx, boo
m.is_not(arg, arg);
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));
if (or_and_ctx_new)
or_and_depth = std::max(or_and_depth, get_or_and_depth(arg));
if (ite_ctx_new)
ite_depth = std::max(ite_depth, get_ite_depth(arg));
}
@ -473,27 +463,7 @@ void static_features::post_process(expr * e, bool form_ctx, bool or_and_ctx, boo
set_depth(e, depth);
if (depth > m_max_depth)
m_max_depth = depth;
if (form_ctx_new) {
form_depth++;
if (!form_ctx) {
m_num_formula_trees++;
m_sum_formula_depth += form_depth;
if (form_depth > m_max_formula_depth)
m_max_formula_depth = form_depth;
}
set_form_depth(e, form_depth);
}
if (or_and_ctx_new) {
or_and_depth++;
if (!or_and_ctx) {
m_num_or_and_trees++;
m_sum_or_and_tree_depth += or_and_depth;
if (or_and_depth > m_max_or_and_tree_depth)
m_max_or_and_tree_depth = or_and_depth;
}
set_or_and_depth(e, or_and_depth);
}
if (ite_ctx_new) {
ite_depth++;
if (!ite_ctx) {
@ -572,25 +542,11 @@ void static_features::process_root(expr * e) {
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));
}
depth++;
set_depth(e, depth);
if (depth > m_max_depth)
m_max_depth = depth;
form_depth++;
m_num_formula_trees++;
m_sum_formula_depth += form_depth;
if (form_depth > m_max_formula_depth)
m_max_formula_depth = form_depth;
set_form_depth(e, form_depth);
or_and_depth++;
m_num_or_and_trees++;
m_sum_or_and_tree_depth += or_and_depth;
if (or_and_depth > m_max_or_and_tree_depth)
m_max_or_and_tree_depth = or_and_depth;
set_or_and_depth(e, or_and_depth);
return;
}
if (!is_gate(e)) {
@ -647,12 +603,6 @@ void static_features::display_primitive(std::ostream & out) const {
out << "NUM_NESTED_FORMULAS " << m_num_nested_formulas << "\n";
out << "NUM_BOOL_EXPRS " << m_num_bool_exprs << "\n";
out << "NUM_BOOL_CONSTANTS " << m_num_bool_constants << "\n";
out << "NUM_FORMULA_TREES " << m_num_formula_trees << "\n";
out << "MAX_FORMULA_DEPTH " << m_max_formula_depth << "\n";
out << "SUM_FORMULA_DEPTH " << m_sum_formula_depth << "\n";
out << "NUM_OR_AND_TREES " << m_num_or_and_trees << "\n";
out << "MAX_OR_AND_TREE_DEPTH " << m_max_or_and_tree_depth << "\n";
out << "SUM_OR_AND_TREE_DEPTH " << m_sum_or_and_tree_depth << "\n";
out << "NUM_ITE_TREES " << m_num_ite_trees << "\n";
out << "MAX_ITE_TREE_DEPTH " << m_max_ite_tree_depth << "\n";
out << "SUM_ITE_TREE_DEPTH " << m_sum_ite_tree_depth << "\n";
@ -695,7 +645,6 @@ void static_features::display(std::ostream & out) const {
out << "BEGIN_STATIC_FEATURES" << "\n";
out << "CNF " << m_cnf << "\n";
out << "MAX_DEPTH " << m_max_depth << "\n";
out << "MAX_OR_AND_TREE_DEPTH " << m_max_or_and_tree_depth << "\n";
out << "MAX_ITE_TREE_DEPTH " << m_max_ite_tree_depth << "\n";
out << "HAS_INT " << m_has_int << "\n";
out << "HAS_REAL " << m_has_real << "\n";

13
src/ast/static_features.h
View file

@ -59,13 +59,7 @@ struct static_features {
unsigned m_sum_clause_size;
unsigned m_num_nested_formulas; //
unsigned m_num_bool_exprs; //
unsigned m_num_bool_constants; //
unsigned m_num_formula_trees;
unsigned m_max_formula_depth;
unsigned m_sum_formula_depth;
unsigned m_num_or_and_trees;
unsigned m_max_or_and_tree_depth;
unsigned m_sum_or_and_tree_depth;
unsigned m_num_bool_constants; //
unsigned m_num_ite_trees;
unsigned m_max_ite_tree_depth;
unsigned m_sum_ite_tree_depth;
@ -179,12 +173,9 @@ struct static_features {
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); }
unsigned get_or_and_depth(expr const * e) const { unsigned d = 0; m_expr2or_and_depth.find(e->get_id(), d); return d; }
void set_or_and_depth(expr const * e, unsigned d) { m_expr2or_and_depth.insert(e->get_id(), d); }
unsigned get_ite_depth(expr const * e) const { unsigned d = 0; m_expr2ite_depth.find(e->get_id(), d); return d; }
void set_ite_depth(expr const * e, unsigned d) { m_expr2ite_depth.insert(e->get_id(), d); }
unsigned get_form_depth(expr const * e) const { unsigned d = 0; m_expr2formula_depth.find(e->get_id(), d); return d; }
void set_form_depth(expr const * e, unsigned d) { m_expr2formula_depth.insert(e->get_id(), d); }
static_features(ast_manager & m);
void reset();
void flush_cache();