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