1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 static_features.cpp
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 #include "ast/static_features.h"
20 #include "ast/ast_pp.h"
21 #include "ast/for_each_expr.h"
22
static_features(ast_manager & m)23 static_features::static_features(ast_manager & m):
24 m(m),
25 m_autil(m),
26 m_bvutil(m),
27 m_arrayutil(m),
28 m_fpautil(m),
29 m_sequtil(m),
30 m_bfid(m.get_basic_family_id()),
31 m_afid(m.mk_family_id("arith")),
32 m_lfid(m.mk_family_id("label")),
33 m_arrfid(m.mk_family_id("array")),
34 m_srfid(m.mk_family_id("specrels")),
35 m_label_sym("label"),
36 m_pattern_sym("pattern"),
37 m_expr_list_sym("expr-list") {
38 reset();
39 }
40
reset()41 void static_features::reset() {
42 m_already_visited .reset();
43 m_cnf = true;
44 m_num_exprs = 0;
45 m_num_roots = 0;
46 m_max_depth = 0;
47 m_num_quantifiers = 0;
48 m_num_quantifiers_with_patterns = 0;
49 m_num_quantifiers_with_multi_patterns = 0;
50 m_num_clauses = 0;
51 m_num_bin_clauses = 0;
52 m_num_units = 0;
53 m_sum_clause_size = 0;
54 m_num_nested_formulas = 0;
55 m_num_bool_exprs = 0;
56 m_num_bool_constants = 0;
57 m_num_formula_trees = 0;
58 m_max_formula_depth = 0;
59 m_sum_formula_depth = 0;
60 m_num_or_and_trees = 0;
61 m_max_or_and_tree_depth = 0;
62 m_sum_or_and_tree_depth = 0;
63 m_num_ite_trees = 0;
64 m_max_ite_tree_depth = 0;
65 m_sum_ite_tree_depth = 0;
66 m_num_ors = 0;
67 m_num_ands = 0;
68 m_num_iffs = 0;
69 m_num_ite_formulas = 0;
70 m_num_ite_terms = 0;
71 m_num_sharing = 0;
72 m_num_interpreted_exprs = 0;
73 m_num_uninterpreted_exprs = 0;
74 m_num_interpreted_constants = 0;
75 m_num_uninterpreted_constants = 0;
76 m_num_uninterpreted_functions = 0;
77 m_num_eqs = 0;
78 m_has_rational = false;
79 m_has_int = false;
80 m_has_real = false;
81 m_has_bv = false;
82 m_has_fpa = false;
83 m_has_sr = false;
84 m_has_str = false;
85 m_has_seq_non_str = false;
86 m_has_arrays = false;
87 m_has_ext_arrays = false;
88 m_arith_k_sum .reset();
89 m_num_arith_terms = 0;
90 m_num_arith_eqs = 0;
91 m_num_arith_ineqs = 0;
92 m_num_diff_terms = 0;
93 m_num_diff_eqs = 0;
94 m_num_diff_ineqs = 0;
95 m_num_simple_eqs = 0;
96 m_num_simple_ineqs = 0;
97 m_num_non_linear = 0;
98 m_num_apps .reset();
99 m_num_theory_terms .reset();
100 m_num_theory_atoms .reset();
101 m_num_theory_constants .reset();
102 m_num_theory_eqs .reset();
103 m_num_aliens = 0;
104 m_num_aliens_per_family .reset();
105 m_num_theories = 0;
106 m_theories .reset();
107 m_max_stack_depth = 30;
108 flush_cache();
109 }
110
flush_cache()111 void static_features::flush_cache() {
112 m_expr2depth.reset();
113 m_expr2or_and_depth.reset();
114 m_expr2ite_depth.reset();
115 m_expr2formula_depth.reset();
116 }
117
118
is_diff_term(expr const * e,rational & r) const119 bool static_features::is_diff_term(expr const * e, rational & r) const {
120 // lhs can be 'x' or '(+ k x)'
121 if (!is_arith_expr(e)) {
122 r.reset();
123 return true;
124 }
125 if (is_numeral(e, r))
126 return true;
127 expr* a1 = nullptr, *a2 = nullptr;
128 return m_autil.is_add(e, a1, a2) && is_numeral(a1, r) && !is_arith_expr(a2) && !m.is_ite(a2);
129 }
130
is_diff_atom(expr const * e) const131 bool static_features::is_diff_atom(expr const * e) const {
132 if (!is_bool(e))
133 return false;
134 if (!m.is_eq(e) && !is_arith_expr(e))
135 return false;
136 SASSERT(to_app(e)->get_num_args() == 2);
137 expr * lhs = to_app(e)->get_arg(0);
138 expr * rhs = to_app(e)->get_arg(1);
139 if (!is_arith_expr(lhs) && !is_arith_expr(rhs) && !m.is_ite(lhs) && !m.is_ite(rhs))
140 return true;
141 if (!is_numeral(rhs))
142 return false;
143 // lhs can be 'x' or '(+ x (* -1 y))' or '(+ (* -1 x) y)'
144 if (!is_arith_expr(lhs) && !m.is_ite(lhs))
145 return true;
146 expr* arg1, *arg2;
147 if (!m_autil.is_add(lhs, arg1, arg2))
148 return false;
149 expr* m1, *m2;
150 if (!is_arith_expr(arg1) && m_autil.is_mul(arg2, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2) && !m.is_ite(m2))
151 return true;
152 if (!is_arith_expr(arg2) && m_autil.is_mul(arg1, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2) && !m.is_ite(m2))
153 return true;
154 return false;
155
156 }
157
is_gate(expr const * e) const158 bool static_features::is_gate(expr const * e) const {
159 if (is_basic_expr(e)) {
160 switch (to_app(e)->get_decl_kind()) {
161 case OP_ITE: case OP_AND: case OP_OR: case OP_XOR: case OP_IMPLIES:
162 return true;
163 case OP_EQ:
164 return m.is_bool(e);
165 }
166 }
167 return false;
168 }
169
update_core(expr * e)170 void static_features::update_core(expr * e) {
171 m_num_exprs++;
172
173 // even if a benchmark does not contain any theory interpreted function decls, we still have to install
174 // the theory if the benchmark contains constants or function applications of an interpreted sort.
175 sort * s = e->get_sort();
176 if (!m.is_uninterp(s))
177 mark_theory(s->get_family_id());
178
179 bool _is_gate = is_gate(e);
180 bool _is_eq = m.is_eq(e);
181 if (_is_gate) {
182 m_cnf = false;
183 m_num_nested_formulas++;
184 switch (to_app(e)->get_decl_kind()) {
185 case OP_ITE:
186 if (is_bool(e))
187 m_num_ite_formulas++;
188 else {
189 m_num_ite_terms++;
190 // process then&else nodes
191 for (unsigned i = 1; i < 3; i++) {
192 expr * arg = to_app(e)->get_arg(i);
193 acc_num(arg);
194 // Must check whether arg is diff logic or not.
195 // Otherwise, problem can be incorrectly tagged as diff logic.
196 sort * arg_s = arg->get_sort();
197 family_id fid_arg = arg_s->get_family_id();
198 if (fid_arg == m_afid) {
199 m_num_arith_terms++;
200 rational k;
201 TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m) << "\n";);
202 if (is_diff_term(arg, k)) {
203 m_num_diff_terms++;
204 acc_num(k);
205 }
206 }
207 }
208 }
209 break;
210 case OP_AND:
211 m_num_ands++;
212 break;
213 case OP_OR:
214 m_num_ors++;
215 break;
216 case OP_EQ:
217 m_num_iffs++;
218 break;
219 }
220 }
221 if (is_bool(e)) {
222 m_num_bool_exprs++;
223 if (is_app(e) && to_app(e)->get_num_args() == 0)
224 m_num_bool_constants++;
225 }
226 if (is_quantifier(e)) {
227 m_num_quantifiers++;
228 unsigned num_patterns = to_quantifier(e)->get_num_patterns();
229 if (num_patterns > 0) {
230 m_num_quantifiers_with_patterns++;
231 for (unsigned i = 0; i < num_patterns; i++) {
232 expr * p = to_quantifier(e)->get_pattern(i);
233 if (is_app(p) && to_app(p)->get_num_args() > 1) {
234 m_num_quantifiers_with_multi_patterns++;
235 break;
236 }
237 }
238 }
239 }
240 bool _is_le_ge = m_autil.is_le(e) || m_autil.is_ge(e);
241 if (_is_le_ge) {
242 m_num_arith_ineqs++;
243 TRACE("diff_atom", tout << "diff_atom: " << is_diff_atom(e) << "\n" << mk_pp(e, m) << "\n";);
244 if (is_diff_atom(e))
245 m_num_diff_ineqs++;
246 if (!is_arith_expr(to_app(e)->get_arg(0)))
247 m_num_simple_ineqs++;
248 acc_num(to_app(e)->get_arg(1));
249 }
250 rational r;
251 if (is_numeral(e, r)) {
252 if (!r.is_int())
253 m_has_rational = true;
254 }
255 if (_is_eq) {
256 m_num_eqs++;
257 if (is_numeral(to_app(e)->get_arg(1))) {
258 acc_num(to_app(e)->get_arg(1));
259 m_num_arith_eqs++;
260 TRACE("diff_atom", tout << "diff_atom: " << is_diff_atom(e) << "\n" << mk_pp(e, m) << "\n";);
261 if (is_diff_atom(e))
262 m_num_diff_eqs++;
263 if (!is_arith_expr(to_app(e)->get_arg(0)))
264 m_num_simple_eqs++;
265 }
266 sort * s = to_app(e)->get_arg(0)->get_sort();
267 if (!m.is_uninterp(s)) {
268 family_id fid = s->get_family_id();
269 if (fid != null_family_id && fid != m_bfid)
270 inc_theory_eqs(fid);
271 }
272 }
273 if (!m_has_int && m_autil.is_int(e))
274 m_has_int = true;
275 if (!m_has_real && m_autil.is_real(e))
276 m_has_real = true;
277 if (!m_has_bv && m_bvutil.is_bv(e))
278 m_has_bv = true;
279 if (!m_has_fpa && (m_fpautil.is_float(e) || m_fpautil.is_rm(e)))
280 m_has_fpa = true;
281 if (is_app(e) && to_app(e)->get_family_id() == m_srfid)
282 m_has_sr = true;
283 if (!m_has_arrays && m_arrayutil.is_array(e))
284 check_array(e->get_sort());
285 if (!m_has_ext_arrays && m_arrayutil.is_array(e) &&
286 !m_arrayutil.is_select(e) && !m_arrayutil.is_store(e))
287 m_has_ext_arrays = true;
288 if (!m_has_str && m_sequtil.str.is_string_term(e))
289 m_has_str = true;
290 if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e))
291 m_has_seq_non_str = true;
292 if (is_app(e)) {
293 family_id fid = to_app(e)->get_family_id();
294 mark_theory(fid);
295 if (fid != null_family_id && fid != m_bfid) {
296 m_num_interpreted_exprs++;
297 if (is_bool(e))
298 inc_theory_atoms(fid);
299 else
300 inc_theory_terms(fid);
301 if (to_app(e)->get_num_args() == 0)
302 m_num_interpreted_constants++;
303 }
304 if (fid == m_afid) {
305 switch (to_app(e)->get_decl_kind()) {
306 case OP_MUL:
307 if (!is_numeral(to_app(e)->get_arg(0)) || to_app(e)->get_num_args() > 2) {
308 m_num_non_linear++;
309 }
310 break;
311 case OP_DIV:
312 case OP_IDIV:
313 case OP_REM:
314 case OP_MOD:
315 if (!is_numeral(to_app(e)->get_arg(1), r) || r.is_zero()) {
316 m_num_uninterpreted_functions++;
317 m_num_non_linear++;
318 }
319 break;
320 }
321 }
322 if (fid == null_family_id) {
323 m_num_uninterpreted_exprs++;
324 if (to_app(e)->get_num_args() == 0) {
325 m_num_uninterpreted_constants++;
326 sort * s = e->get_sort();
327 if (!m.is_uninterp(s)) {
328 family_id fid = s->get_family_id();
329 if (fid != null_family_id && fid != m_bfid)
330 inc_theory_constants(fid);
331 }
332 }
333 }
334 if (m_arrayutil.is_array(e)) {
335 TRACE("sf_array", tout << mk_ismt2_pp(e, m) << "\n";);
336 sort * ty = to_app(e)->get_decl()->get_range();
337 mark_theory(ty->get_family_id());
338 unsigned n = ty->get_num_parameters();
339 for (unsigned i = 0; i < n; i++) {
340 sort * ds = to_sort(ty->get_parameter(i).get_ast());
341 update_core(ds);
342 }
343 }
344 func_decl * d = to_app(e)->get_decl();
345 inc_num_apps(d);
346 if (d->get_arity() > 0 && !is_marked(d)) {
347 mark(d);
348 if (fid == null_family_id)
349 m_num_uninterpreted_functions++;
350 }
351 if (!_is_eq && !_is_gate) {
352 for (expr * arg : *to_app(e)) {
353 sort * arg_s = arg->get_sort();
354 if (!m.is_uninterp(arg_s)) {
355 family_id fid_arg = arg_s->get_family_id();
356 if (fid_arg != fid && fid_arg != null_family_id) {
357 m_num_aliens++;
358 inc_num_aliens(fid_arg);
359 if (fid_arg == m_afid) {
360 SASSERT(!_is_le_ge);
361 m_num_arith_terms++;
362 rational k;
363 TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m) << "\n";);
364 if (is_diff_term(arg, k)) {
365 m_num_diff_terms++;
366 acc_num(k);
367 }
368 }
369 }
370 }
371 }
372 }
373 }
374 }
375
check_array(sort * s)376 void static_features::check_array(sort* s) {
377 if (m_arrayutil.is_array(s)) {
378 m_has_arrays = true;
379 update_core(get_array_range(s));
380 for (unsigned i = get_array_arity(s); i-- > 0; )
381 update_core(get_array_domain(s, i));
382 }
383 }
384
385
update_core(sort * s)386 void static_features::update_core(sort * s) {
387 mark_theory(s->get_family_id());
388 if (!m_has_int && m_autil.is_int(s))
389 m_has_int = true;
390 if (!m_has_real && m_autil.is_real(s))
391 m_has_real = true;
392 if (!m_has_bv && m_bvutil.is_bv_sort(s))
393 m_has_bv = true;
394 if (!m_has_fpa && (m_fpautil.is_float(s) || m_fpautil.is_rm(s)))
395 m_has_fpa = true;
396 check_array(s);
397 }
398
process(expr * e,bool form_ctx,bool or_and_ctx,bool ite_ctx,unsigned stack_depth)399 void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth) {
400 TRACE("static_features", tout << "processing\n" << mk_pp(e, m) << "\n";);
401 if (is_var(e))
402 return;
403 if (is_marked(e)) {
404 m_num_sharing++;
405 return;
406 }
407
408 if (stack_depth > m_max_stack_depth) {
409 ptr_vector<expr> todo;
410 todo.push_back(e);
411 for (unsigned i = 0; i < todo.size(); ++i) {
412 e = todo[i];
413 if (is_marked(e))
414 continue;
415 if (is_basic_expr(e)) {
416 mark(e);
417 todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
418 }
419 else {
420 process(e, form_ctx, or_and_ctx, ite_ctx, stack_depth - 10);
421 }
422 }
423 return;
424 }
425
426 mark(e);
427
428 update_core(e);
429
430 if (is_quantifier(e)) {
431 expr * body = to_quantifier(e)->get_expr();
432 process(body, false, false, false, stack_depth+1);
433 set_depth(e, get_depth(body)+1);
434 return;
435 }
436
437 bool form_ctx_new = false;
438 bool or_and_ctx_new = false;
439 bool ite_ctx_new = false;
440
441 if (is_basic_expr(e)) {
442 switch (to_app(e)->get_decl_kind()) {
443 case OP_ITE:
444 form_ctx_new = m.is_bool(e);
445 ite_ctx_new = true;
446 break;
447 case OP_AND:
448 case OP_OR:
449 form_ctx_new = true;
450 or_and_ctx_new = true;
451 break;
452 case OP_EQ:
453 form_ctx_new = true;
454 break;
455 }
456 }
457
458 unsigned depth = 0;
459 unsigned form_depth = 0;
460 unsigned or_and_depth = 0;
461 unsigned ite_depth = 0;
462
463 for (expr* arg : *to_app(e)) {
464 m.is_not(arg, arg);
465 process(arg, form_ctx_new, or_and_ctx_new, ite_ctx_new, stack_depth+1);
466 depth = std::max(depth, get_depth(arg));
467 if (form_ctx_new)
468 form_depth = std::max(form_depth, get_form_depth(arg));
469 if (or_and_ctx_new)
470 or_and_depth = std::max(or_and_depth, get_or_and_depth(arg));
471 if (ite_ctx_new)
472 ite_depth = std::max(ite_depth, get_ite_depth(arg));
473 }
474
475 depth++;
476 set_depth(e, depth);
477 if (depth > m_max_depth)
478 m_max_depth = depth;
479
480 if (form_ctx_new) {
481 form_depth++;
482 if (!form_ctx) {
483 m_num_formula_trees++;
484 m_sum_formula_depth += form_depth;
485 if (form_depth > m_max_formula_depth)
486 m_max_formula_depth = form_depth;
487 }
488 set_form_depth(e, form_depth);
489 }
490 if (or_and_ctx_new) {
491 or_and_depth++;
492 if (!or_and_ctx) {
493 m_num_or_and_trees++;
494 m_sum_or_and_tree_depth += or_and_depth;
495 if (or_and_depth > m_max_or_and_tree_depth)
496 m_max_or_and_tree_depth = or_and_depth;
497 }
498 set_or_and_depth(e, or_and_depth);
499 }
500 if (ite_ctx_new) {
501 ite_depth++;
502 if (!ite_ctx) {
503 m_num_ite_trees++;
504 m_sum_ite_tree_depth += ite_depth;
505 if (ite_depth >= m_max_ite_tree_depth)
506 m_max_ite_tree_depth = ite_depth;
507 }
508 set_ite_depth(e, ite_depth);
509 }
510 }
511
process_root(expr * e)512 void static_features::process_root(expr * e) {
513 if (is_marked(e)) {
514 m_num_sharing++;
515 return;
516 }
517 m_num_roots++;
518 if (m.is_or(e)) {
519 mark(e);
520 m_num_clauses++;
521 m_num_bool_exprs++;
522 unsigned num_args = to_app(e)->get_num_args();
523 m_sum_clause_size += num_args;
524 if (num_args == 2)
525 m_num_bin_clauses++;
526 unsigned depth = 0;
527 unsigned form_depth = 0;
528 unsigned or_and_depth = 0;
529 for (unsigned i = 0; i < num_args; i++) {
530 expr * arg = to_app(e)->get_arg(i);
531 if (m.is_not(arg))
532 arg = to_app(arg)->get_arg(0);
533 process(arg, true, true, false, 0);
534 depth = std::max(depth, get_depth(arg));
535 form_depth = std::max(form_depth, get_form_depth(arg));
536 or_and_depth = std::max(or_and_depth, get_or_and_depth(arg));
537 }
538 depth++;
539 set_depth(e, depth);
540 if (depth > m_max_depth)
541 m_max_depth = depth;
542 form_depth++;
543 m_num_formula_trees++;
544 m_sum_formula_depth += form_depth;
545 if (form_depth > m_max_formula_depth)
546 m_max_formula_depth = form_depth;
547 set_form_depth(e, form_depth);
548 or_and_depth++;
549 m_num_or_and_trees++;
550 m_sum_or_and_tree_depth += or_and_depth;
551 if (or_and_depth > m_max_or_and_tree_depth)
552 m_max_or_and_tree_depth = or_and_depth;
553 set_or_and_depth(e, or_and_depth);
554 return;
555 }
556 if (!is_gate(e)) {
557 m_sum_clause_size++;
558 m_num_units++;
559 m_num_clauses++;
560 }
561 process(e, false, false, false, 0);
562 }
563
collect(unsigned num_formulas,expr * const * formulas)564 void static_features::collect(unsigned num_formulas, expr * const * formulas) {
565 for (unsigned i = 0; i < num_formulas; i++)
566 process_root(formulas[i]);
567 }
568
internal_family(symbol const & f_name) const569 bool static_features::internal_family(symbol const & f_name) const {
570 return f_name == m_label_sym || f_name == m_pattern_sym || f_name == m_expr_list_sym;
571 }
572
display_family_data(std::ostream & out,char const * prefix,unsigned_vector const & data) const573 void static_features::display_family_data(std::ostream & out, char const * prefix, unsigned_vector const & data) const {
574 for (unsigned fid = 0; fid < data.size(); fid++) {
575 symbol const & n = m.get_family_name(fid);
576 if (!internal_family(n))
577 out << prefix << "_" << n << " " << data[fid] << "\n";
578 }
579 }
580
has_uf() const581 bool static_features::has_uf() const {
582 return m_num_uninterpreted_functions > 0;
583 }
584
num_non_uf_theories() const585 unsigned static_features::num_non_uf_theories() const {
586 return m_num_theories;
587 }
588
num_theories() const589 unsigned static_features::num_theories() const {
590 return (num_non_uf_theories() + (has_uf() ? 1 : 0));
591 }
592
display_primitive(std::ostream & out) const593 void static_features::display_primitive(std::ostream & out) const {
594 out << "BEGIN_PRIMITIVE_STATIC_FEATURES" << "\n";
595 out << "CNF " << m_cnf << "\n";
596 out << "NUM_EXPRS " << m_num_exprs << "\n";
597 out << "NUM_ROOTS " << m_num_roots << "\n";
598 out << "MAX_DEPTH " << m_max_depth << "\n";
599 out << "NUM_QUANTIFIERS " << m_num_quantifiers << "\n";
600 out << "NUM_QUANTIFIERS_WITH_PATTERNS " << m_num_quantifiers_with_patterns << "\n";
601 out << "NUM_QUANTIFIERS_WITH_MULTI_PATTERNS " << m_num_quantifiers_with_multi_patterns << "\n";
602 out << "NUM_CLAUSES " << m_num_clauses << "\n";
603 out << "NUM_BIN_CLAUSES " << m_num_bin_clauses << "\n";
604 out << "NUM_UNITS " << m_num_units << "\n";
605 out << "SUM_CLAUSE_SIZE " << m_sum_clause_size << "\n";
606 out << "NUM_NESTED_FORMULAS " << m_num_nested_formulas << "\n";
607 out << "NUM_BOOL_EXPRS " << m_num_bool_exprs << "\n";
608 out << "NUM_BOOL_CONSTANTS " << m_num_bool_constants << "\n";
609 out << "NUM_FORMULA_TREES " << m_num_formula_trees << "\n";
610 out << "MAX_FORMULA_DEPTH " << m_max_formula_depth << "\n";
611 out << "SUM_FORMULA_DEPTH " << m_sum_formula_depth << "\n";
612 out << "NUM_OR_AND_TREES " << m_num_or_and_trees << "\n";
613 out << "MAX_OR_AND_TREE_DEPTH " << m_max_or_and_tree_depth << "\n";
614 out << "SUM_OR_AND_TREE_DEPTH " << m_sum_or_and_tree_depth << "\n";
615 out << "NUM_ITE_TREES " << m_num_ite_trees << "\n";
616 out << "MAX_ITE_TREE_DEPTH " << m_max_ite_tree_depth << "\n";
617 out << "SUM_ITE_TREE_DEPTH " << m_sum_ite_tree_depth << "\n";
618 out << "NUM_ORS " << m_num_ors << "\n";
619 out << "NUM_ANDS " << m_num_ands << "\n";
620 out << "NUM_IFFS " << m_num_iffs << "\n";
621 out << "NUM_ITE_FORMULAS " << m_num_ite_formulas << "\n";
622 out << "NUM_ITE_TERMS " << m_num_ite_terms << "\n";
623 out << "NUM_SHARING " << m_num_sharing << "\n";
624 out << "NUM_INTERPRETED_EXPRS " << m_num_interpreted_exprs << "\n";
625 out << "NUM_UNINTERPRETED_EXPRS " << m_num_uninterpreted_exprs << "\n";
626 out << "NUM_INTERPRETED_CONSTANTS " << m_num_interpreted_constants << "\n";
627 out << "NUM_UNINTERPRETED_CONSTANTS " << m_num_uninterpreted_constants << "\n";
628 out << "NUM_UNINTERPRETED_FUNCTIONS " << m_num_uninterpreted_functions << "\n";
629 out << "NUM_EQS " << m_num_eqs << "\n";
630 out << "HAS_RATIONAL " << m_has_rational << "\n";
631 out << "HAS_INT " << m_has_int << "\n";
632 out << "HAS_REAL " << m_has_real << "\n";
633 out << "ARITH_K_SUM " << m_arith_k_sum << "\n";
634 out << "NUM_ARITH_TERMS " << m_num_arith_terms << "\n";
635 out << "NUM_ARITH_EQS " << m_num_arith_eqs << "\n";
636 out << "NUM_ARITH_INEQS " << m_num_arith_ineqs << "\n";
637 out << "NUM_DIFF_TERMS " << m_num_diff_terms << "\n";
638 out << "NUM_DIFF_EQS " << m_num_diff_eqs << "\n";
639 out << "NUM_DIFF_INEQS " << m_num_diff_ineqs << "\n";
640 out << "NUM_SIMPLE_EQS " << m_num_simple_eqs << "\n";
641 out << "NUM_SIMPLE_INEQS " << m_num_simple_ineqs << "\n";
642 out << "NUM_NON_LINEAR " << m_num_non_linear << "\n";
643 out << "NUM_ALIENS " << m_num_aliens << "\n";
644 display_family_data(out, "NUM_TERMS", m_num_theory_terms);
645 display_family_data(out, "NUM_ATOMS", m_num_theory_atoms);
646 display_family_data(out, "NUM_CONSTANTS", m_num_theory_constants);
647 display_family_data(out, "NUM_EQS", m_num_theory_eqs);
648 display_family_data(out, "NUM_ALIENS", m_num_aliens_per_family);
649 out << "NUM_THEORIES " << num_theories() << "\n";
650 out << "END_PRIMITIVE_STATIC_FEATURES" << "\n";
651 }
652
display(std::ostream & out) const653 void static_features::display(std::ostream & out) const {
654 out << "BEGIN_STATIC_FEATURES" << "\n";
655 out << "CNF " << m_cnf << "\n";
656 out << "MAX_DEPTH " << m_max_depth << "\n";
657 out << "MAX_OR_AND_TREE_DEPTH " << m_max_or_and_tree_depth << "\n";
658 out << "MAX_ITE_TREE_DEPTH " << m_max_ite_tree_depth << "\n";
659 out << "HAS_INT " << m_has_int << "\n";
660 out << "HAS_REAL " << m_has_real << "\n";
661 out << "HAS_QUANTIFIERS " << (m_num_quantifiers > 0) << "\n";
662 out << "PERC_QUANTIFIERS_WITH_PATTERNS " << (m_num_quantifiers > 0 ? (double) m_num_quantifiers_with_patterns / (double) m_num_quantifiers : 0) << "\n";
663 out << "PERC_QUANTIFIERS_WITH_MULTI_PATTERNS " << (m_num_quantifiers > 0 ? (double) m_num_quantifiers_with_multi_patterns / (double) m_num_quantifiers : 0) << "\n";
664 out << "IS_NON_LINEAR " << (m_num_non_linear > 0) << "\n";
665 out << "THEORY_COMBINATION " << (num_theories() > 1) << "\n";
666 out << "AVG_CLAUSE_SIZE " << (m_num_clauses > 0 ? (double) m_sum_clause_size / (double) m_num_clauses : 0) << "\n";
667 out << "PERC_BOOL_CONSTANTS " << (m_num_uninterpreted_constants > 0 ? (double) m_num_bool_constants / (double) m_num_uninterpreted_constants : 0) << "\n";
668 out << "PERC_NESTED_FORMULAS " << (m_num_bool_exprs > 0 ? (double) m_num_nested_formulas / (double) m_num_bool_exprs : 0) << "\n";
669 out << "IS_DIFF " << (m_num_arith_eqs == m_num_diff_eqs && m_num_arith_ineqs == m_num_diff_ineqs && m_num_arith_terms == m_num_diff_terms) << "\n";
670 out << "INEQ_EQ_RATIO " << (m_num_arith_eqs > 0 ? (double) m_num_arith_ineqs / (double) m_num_arith_eqs : 0) << "\n";
671 out << "PERC_ARITH_EQS " << (m_num_eqs > 0 ? (double) m_num_arith_eqs / (double) m_num_eqs : 0) << "\n";
672 out << "PERC_DIFF_EQS " << (m_num_arith_eqs > 0 ? (double) m_num_diff_eqs / (double) m_num_arith_eqs : 0) << "\n";
673 out << "PERC_DIFF_INEQS " << (m_num_arith_ineqs > 0 ? (double) m_num_diff_ineqs / (double) m_num_arith_ineqs : 0) << "\n";
674 out << "PERC_SIMPLE_EQS " << (m_num_arith_eqs > 0 ? (double) m_num_simple_eqs / (double) m_num_arith_eqs : 0) << "\n";
675 out << "PERC_SIMPLE_INEQS " << (m_num_arith_ineqs > 0 ? (double) m_num_simple_ineqs / (double) m_num_arith_ineqs : 0) << "\n";
676 out << "PERC_ALIENS " << (m_num_exprs > 0 ? (double) m_num_aliens / (double) m_num_exprs : 0) << "\n";
677 out << "END_STATIC_FEATURES" << "\n";
678 }
679
get_feature_vector(vector<double> & result)680 void static_features::get_feature_vector(vector<double> & result) {
681 }
682