1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 static_features.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-05-16. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "ast/ast.h" 22 #include "ast/arith_decl_plugin.h" 23 #include "ast/bv_decl_plugin.h" 24 #include "ast/array_decl_plugin.h" 25 #include "ast/fpa_decl_plugin.h" 26 #include "ast/seq_decl_plugin.h" 27 #include "ast/special_relations_decl_plugin.h" 28 #include "util/map.h" 29 30 struct static_features { 31 ast_manager & m; 32 arith_util m_autil; 33 bv_util m_bvutil; 34 array_util m_arrayutil; 35 fpa_util m_fpautil; 36 seq_util m_sequtil; 37 family_id m_bfid; 38 family_id m_afid; 39 family_id m_lfid; 40 family_id m_arrfid; 41 family_id m_srfid; 42 ast_mark m_already_visited; 43 bool m_cnf; 44 unsigned m_num_exprs; // 45 unsigned m_num_roots; // 46 unsigned m_max_depth; 47 unsigned m_num_quantifiers; // 48 unsigned m_num_quantifiers_with_patterns; // 49 unsigned m_num_quantifiers_with_multi_patterns; // 50 unsigned m_num_clauses; 51 unsigned m_num_bin_clauses; // 52 unsigned m_num_units; // 53 unsigned m_sum_clause_size; 54 unsigned m_num_nested_formulas; // 55 unsigned m_num_bool_exprs; // 56 unsigned m_num_bool_constants; // 57 unsigned m_num_formula_trees; 58 unsigned m_max_formula_depth; 59 unsigned m_sum_formula_depth; 60 unsigned m_num_or_and_trees; 61 unsigned m_max_or_and_tree_depth; 62 unsigned m_sum_or_and_tree_depth; 63 unsigned m_num_ite_trees; 64 unsigned m_max_ite_tree_depth; 65 unsigned m_sum_ite_tree_depth; 66 unsigned m_num_ands; // 67 unsigned m_num_ors; // num nested ors 68 unsigned m_num_iffs; // 69 unsigned m_num_ite_formulas; // 70 unsigned m_num_ite_terms; // 71 unsigned m_num_sharing; 72 unsigned m_num_interpreted_exprs; // doesn't include bool_exprs 73 unsigned m_num_uninterpreted_exprs; // 74 unsigned m_num_interpreted_constants; // doesn't include bool_consts 75 unsigned m_num_uninterpreted_constants; // 76 unsigned m_num_uninterpreted_functions; // 77 unsigned m_num_eqs; // 78 bool m_has_rational; // 79 bool m_has_int; // 80 bool m_has_real; // 81 bool m_has_bv; // 82 bool m_has_fpa; // 83 bool m_has_sr; // has special relations 84 bool m_has_str; // has String-typed terms 85 bool m_has_seq_non_str; // has non-String-typed Sequence terms 86 bool m_has_arrays; // 87 bool m_has_ext_arrays; // does this use extended array theory. 88 rational m_arith_k_sum; // sum of the numerals in arith atoms. 89 unsigned m_num_arith_terms; 90 unsigned m_num_arith_eqs; // equalities of the form t = k where k is a numeral 91 unsigned m_num_arith_ineqs; 92 unsigned m_num_diff_terms; // <= m_num_arith_terms 93 unsigned m_num_diff_eqs; // <= m_num_arith_eqs 94 unsigned m_num_diff_ineqs; // <= m_num_arith_ineqs 95 unsigned m_num_simple_eqs; // eqs of the form x = k 96 unsigned m_num_simple_ineqs; // ineqs of the form x <= k or x >= k 97 unsigned m_num_non_linear; 98 unsigned_vector m_num_apps; // mapping decl_id -> num_apps; 99 unsigned_vector m_num_theory_terms; // mapping family_id -> num_terms 100 unsigned_vector m_num_theory_atoms; // mapping family_id -> num_atoms 101 unsigned_vector m_num_theory_constants; // mapping family_id -> num_exprs 102 unsigned_vector m_num_theory_eqs; // mapping family_id -> num_eqs 103 unsigned m_num_aliens; // 104 unsigned_vector m_num_aliens_per_family; // mapping family_id -> num_alies exprs 105 106 unsigned_vector m_expr2depth; // expr-id -> depth 107 unsigned m_max_stack_depth; // maximal depth of stack we are willing to walk. 108 109 u_map<unsigned> m_expr2or_and_depth; 110 u_map<unsigned> m_expr2ite_depth; 111 u_map<unsigned> m_expr2formula_depth; 112 113 unsigned m_num_theories; 114 bool_vector m_theories; // mapping family_id -> bool 115 116 symbol m_label_sym; 117 symbol m_pattern_sym; 118 symbol m_expr_list_sym; 119 is_markedstatic_features120 bool is_marked(ast * e) const { return m_already_visited.is_marked(e); } markstatic_features121 void mark(ast * e) { m_already_visited.mark(e, true); } is_boolstatic_features122 bool is_bool(expr const * e) const { return m.is_bool(e); } is_basic_exprstatic_features123 bool is_basic_expr(expr const * e) const { return is_app(e) && to_app(e)->get_family_id() == m_bfid; } is_arith_exprstatic_features124 bool is_arith_expr(expr const * e) const { return is_app(e) && to_app(e)->get_family_id() == m_afid; } is_numeralstatic_features125 bool is_numeral(expr const * e) const { return m_autil.is_numeral(e); } is_numeralstatic_features126 bool is_numeral(expr const * e, rational & r) const { return m_autil.is_numeral(e, r); } is_minus_onestatic_features127 bool is_minus_one(expr const * e) const { rational r; return m_autil.is_numeral(e, r) && r.is_minus_one(); } 128 bool is_diff_term(expr const * e, rational & r) const; 129 bool is_diff_atom(expr const * e) const; 130 bool is_gate(expr const * e) const; mark_theorystatic_features131 void mark_theory(family_id fid) { 132 if (fid != null_family_id && !m.is_builtin_family_id(fid) && !m_theories.get(fid, false)) { 133 m_theories.setx(fid, true, false); 134 m_num_theories++; 135 } 136 } 137 138 void check_array(sort* s); 139 acc_numstatic_features140 void acc_num(rational const & r) { 141 if (r.is_neg()) 142 m_arith_k_sum -= r; 143 else 144 m_arith_k_sum += r; 145 } 146 acc_numstatic_features147 void acc_num(expr const * e) { 148 rational r; 149 if (is_numeral(e, r)) { 150 acc_num(r); 151 } 152 } 153 arith_k_sum_is_smallstatic_features154 bool arith_k_sum_is_small() const { return m_arith_k_sum < rational(INT_MAX / 8); } 155 inc_num_appsstatic_features156 void inc_num_apps(func_decl const * d) { unsigned id = d->get_decl_id(); m_num_apps.reserve(id+1, 0); m_num_apps[id]++; } inc_theory_termsstatic_features157 void inc_theory_terms(family_id fid) { m_num_theory_terms.reserve(fid+1, 0); m_num_theory_terms[fid]++; } inc_theory_atomsstatic_features158 void inc_theory_atoms(family_id fid) { m_num_theory_atoms.reserve(fid+1, 0); m_num_theory_atoms[fid]++; } inc_theory_constantsstatic_features159 void inc_theory_constants(family_id fid) { m_num_theory_constants.reserve(fid+1, 0); m_num_theory_constants[fid]++; } inc_theory_eqsstatic_features160 void inc_theory_eqs(family_id fid) { m_num_theory_eqs.reserve(fid+1, 0); m_num_theory_eqs[fid]++; } inc_num_aliensstatic_features161 void inc_num_aliens(family_id fid) { m_num_aliens_per_family.reserve(fid+1, 0); m_num_aliens_per_family[fid]++; } 162 void update_core(expr * e); 163 void update_core(sort * s); 164 void process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth); 165 void process_root(expr * e); get_depthstatic_features166 unsigned get_depth(expr const * e) const { return m_expr2depth.get(e->get_id(), 1); } set_depthstatic_features167 void set_depth(expr const * e, unsigned d) { m_expr2depth.setx(e->get_id(), d, 1); } get_or_and_depthstatic_features168 unsigned get_or_and_depth(expr const * e) const { unsigned d = 0; m_expr2or_and_depth.find(e->get_id(), d); return d; } set_or_and_depthstatic_features169 void set_or_and_depth(expr const * e, unsigned d) { m_expr2or_and_depth.insert(e->get_id(), d); } get_ite_depthstatic_features170 unsigned get_ite_depth(expr const * e) const { unsigned d = 0; m_expr2ite_depth.find(e->get_id(), d); return d; } set_ite_depthstatic_features171 void set_ite_depth(expr const * e, unsigned d) { m_expr2ite_depth.insert(e->get_id(), d); } get_form_depthstatic_features172 unsigned get_form_depth(expr const * e) const { unsigned d = 0; m_expr2formula_depth.find(e->get_id(), d); return d; } set_form_depthstatic_features173 void set_form_depth(expr const * e, unsigned d) { m_expr2formula_depth.insert(e->get_id(), d); } 174 static_features(ast_manager & m); 175 void reset(); 176 void flush_cache(); 177 void collect(unsigned num_formulas, expr * const * formulas); collectstatic_features178 void collect(expr * f) { process_root(f); } 179 bool internal_family(symbol const & f_name) const; 180 void display_family_data(std::ostream & out, char const * prefix, unsigned_vector const & data) const; 181 void display_primitive(std::ostream & out) const; 182 void display(std::ostream & out) const; 183 void get_feature_vector(vector<double> & result); 184 bool has_uf() const; 185 unsigned num_theories() const; 186 unsigned num_non_uf_theories() const; 187 188 }; 189 190 191