-
Notifications
You must be signed in to change notification settings - Fork 1.6k
Expand file tree
/
Copy pathstatic_features.h
More file actions
197 lines (172 loc) · 9.03 KB
/
static_features.h
File metadata and controls
197 lines (172 loc) · 9.03 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
static_features.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-05-16.
Revision History:
--*/
#pragma once
#include "ast/ast.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/array_decl_plugin.h"
#include "ast/fpa_decl_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/special_relations_decl_plugin.h"
#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;
array_util m_arrayutil;
fpa_util m_fpautil;
seq_util m_sequtil;
family_id m_bfid;
family_id m_afid;
family_id m_lfid;
family_id m_arrfid;
family_id m_srfid;
ast_mark m_pre_processed, m_post_processed;
bool m_cnf;
unsigned m_num_exprs; //
unsigned m_num_roots; //
unsigned m_max_depth;
unsigned m_num_quantifiers; //
unsigned m_num_quantifiers_with_patterns; //
unsigned m_num_quantifiers_with_multi_patterns; //
unsigned m_num_clauses;
unsigned m_num_bin_clauses; //
unsigned m_num_units; //
unsigned m_sum_clause_size;
unsigned m_num_nested_formulas; //
unsigned m_num_bool_exprs; //
unsigned m_num_bool_constants; //
unsigned m_num_ite_trees;
unsigned m_max_ite_tree_depth;
unsigned m_sum_ite_tree_depth;
unsigned m_num_ands; //
unsigned m_num_ors; // num nested ors
unsigned m_num_iffs; //
unsigned m_num_ite_formulas; //
unsigned m_num_ite_terms; //
unsigned m_num_sharing;
unsigned m_num_interpreted_exprs; // doesn't include bool_exprs
unsigned m_num_uninterpreted_exprs; //
unsigned m_num_interpreted_constants; // doesn't include bool_consts
unsigned m_num_uninterpreted_constants; //
unsigned m_num_uninterpreted_functions; //
unsigned m_num_eqs; //
rational m_arith_k_sum; // sum of the numerals in arith atoms.
unsigned m_num_arith_terms;
unsigned m_num_arith_eqs; // equalities of the form t = k where k is a numeral
unsigned m_num_arith_ineqs;
unsigned m_num_diff_terms; // <= m_num_arith_terms
unsigned m_num_diff_eqs; // <= m_num_arith_eqs
unsigned m_num_diff_ineqs; // <= m_num_arith_ineqs
unsigned m_num_simple_eqs; // eqs of the form x = k
unsigned m_num_simple_ineqs; // ineqs of the form x <= k or x >= k
unsigned m_num_non_linear;
unsigned_vector m_num_apps; // mapping decl_id -> num_apps;
unsigned_vector m_num_theory_terms; // mapping family_id -> num_terms
unsigned_vector m_num_theory_atoms; // mapping family_id -> num_atoms
unsigned m_has_rational:1; //
unsigned m_has_int:1; //
unsigned m_has_real:1; //
unsigned m_has_bv:1; //
unsigned m_has_fpa:1; //
unsigned m_has_sr:1; // has special relations
unsigned m_has_str:1; // has String-typed terms
unsigned m_has_seq_non_str:1; // has non-String-typed Sequence terms
unsigned m_has_arrays:1; //
unsigned m_has_ext_arrays:1; // does this use extended array theory.
unsigned_vector m_num_theory_constants; // mapping family_id -> num_exprs
unsigned_vector m_num_theory_eqs; // mapping family_id -> num_eqs
unsigned m_num_aliens; //
unsigned_vector m_num_aliens_per_family; // mapping family_id -> num_alies exprs
unsigned_vector m_expr2depth; // expr-id -> depth
unsigned m_max_stack_depth; // maximal depth of stack we are willing to walk.
u_map<unsigned> m_expr2or_and_depth;
u_map<unsigned> m_expr2ite_depth;
u_map<unsigned> m_expr2formula_depth;
unsigned m_num_theories;
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_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; }
bool is_numeral(expr const * e) const { return m_autil.is_numeral(e); }
bool is_numeral(expr const * e, rational & r) const { return m_autil.is_numeral(e, r); }
bool is_minus_one(expr const * e) const { rational r; return m_autil.is_numeral(e, r) && r.is_minus_one(); }
bool is_diff_term(expr const * e, rational & r) const;
bool is_diff_atom(expr const * e) const;
bool is_gate(expr const * e) const;
void mark_theory(family_id fid) {
if (fid != null_family_id && !m.is_builtin_family_id(fid) && !m_theories.get(fid, false)) {
m_theories.setx(fid, true, false);
m_num_theories++;
}
}
void check_array(sort* s);
void acc_num(rational const & r) {
if (r.is_neg())
m_arith_k_sum -= r;
else
m_arith_k_sum += r;
}
void acc_num(expr const * e) {
rational r;
if (is_numeral(e, r)) {
acc_num(r);
}
}
bool arith_k_sum_is_small() const { return m_arith_k_sum < rational(INT_MAX / 8); }
void inc_num_apps(func_decl const * d) { unsigned id = d->get_small_id(); m_num_apps.reserve(id+1, 0); m_num_apps[id]++; }
void inc_theory_terms(family_id fid) { m_num_theory_terms.reserve(fid+1, 0); m_num_theory_terms[fid]++; }
void inc_theory_atoms(family_id fid) { m_num_theory_atoms.reserve(fid+1, 0); m_num_theory_atoms[fid]++; }
void inc_theory_constants(family_id fid) { m_num_theory_constants.reserve(fid+1, 0); m_num_theory_constants[fid]++; }
void inc_theory_eqs(family_id fid) { m_num_theory_eqs.reserve(fid+1, 0); m_num_theory_eqs[fid]++; }
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);
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); }
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); }
static_features(ast_manager & m);
void reset();
void flush_cache();
void collect(unsigned num_formulas, expr * const * formulas);
void collect(expr * f) { process_root(f); }
bool internal_family(symbol const & f_name) const;
void display_family_data(std::ostream & out, char const * prefix, unsigned_vector const & data) const;
void display_primitive(std::ostream & out) const;
void display(std::ostream & out) const;
void get_feature_vector(vector<double> & result);
bool has_uf() const;
unsigned num_theories() const;
unsigned num_non_uf_theories() const;
bool is_dense() const;
};