1 /*++
2 Copyright (c) 2013 Microsoft Corporation
3
4 Module Name:
5
6 ast_counter.cpp
7
8 Abstract:
9
10 Routines for counting features of terms, such as free variables.
11
12 Author:
13
14 Nikolaj Bjorner (nbjorner) 2013-03-18.
15
16 Revision History:
17
18 --*/
19
20 #include "ast/rewriter/ast_counter.h"
21
update(unsigned el,int delta)22 void counter::update(unsigned el, int delta) {
23 int & counter = get(el);
24 counter += delta;
25 }
26
get(unsigned el)27 int & counter::get(unsigned el) {
28 return m_data.insert_if_not_there(el, 0);
29 }
30
count(unsigned sz,const unsigned * els,int delta)31 counter & counter::count(unsigned sz, const unsigned * els, int delta) {
32 for(unsigned i = 0; i < sz; i++) {
33 update(els[i], delta);
34 }
35 return *this;
36 }
37
get_positive_count() const38 unsigned counter::get_positive_count() const {
39 unsigned cnt = 0;
40 for (auto const& kv : *this)
41 if (kv.m_value > 0)
42 cnt++;
43 return cnt;
44 }
45
collect_positive(uint_set & acc) const46 void counter::collect_positive(uint_set & acc) const {
47 for (auto const& kv : *this)
48 if(kv.m_value > 0)
49 acc.insert(kv.m_key);
50 }
51
get_max_positive(unsigned & res) const52 bool counter::get_max_positive(unsigned & res) const {
53 bool found = false;
54 for (auto const& kv : *this) {
55 if (kv.m_value > 0 && (!found || kv.m_key > res) ) {
56 found = true;
57 res = kv.m_key;
58 }
59 }
60 return found;
61 }
62
get_max_positive() const63 unsigned counter::get_max_positive() const {
64 unsigned max_pos;
65 VERIFY(get_max_positive(max_pos));
66 return max_pos;
67 }
68
get_max_counter_value() const69 int counter::get_max_counter_value() const {
70 int res = 0;
71 for (auto const& kv : *this) {
72 if (kv.m_value > res)
73 res = kv.m_value;
74 }
75 return res;
76 }
77
count_vars(const app * pred,int coef)78 void var_counter::count_vars(const app * pred, int coef) {
79 unsigned n = pred->get_num_args();
80 for (unsigned i = 0; i < n; i++) {
81 m_fv(pred->get_arg(i));
82 for (unsigned j = 0; j < m_fv.size(); ++j) {
83 if (m_fv[j]) {
84 update(j, coef);
85 }
86 }
87 }
88 m_fv.reset();
89 }
90
91
get_max_var(bool & has_var)92 unsigned var_counter::get_max_var(bool& has_var) {
93 has_var = false;
94 unsigned max_var = 0;
95 ptr_vector<quantifier> qs;
96 while (!m_todo.empty()) {
97 expr* e = m_todo.back();
98 m_todo.pop_back();
99 if (m_visited.is_marked(e)) {
100 continue;
101 }
102 m_visited.mark(e, true);
103 switch(e->get_kind()) {
104 case AST_QUANTIFIER: {
105 qs.push_back(to_quantifier(e));
106 break;
107 }
108 case AST_VAR: {
109 if (to_var(e)->get_idx() >= max_var) {
110 has_var = true;
111 max_var = to_var(e)->get_idx();
112 }
113 break;
114 }
115 case AST_APP: {
116 app* a = to_app(e);
117 for (unsigned i = 0; i < a->get_num_args(); ++i) {
118 m_todo.push_back(a->get_arg(i));
119 }
120 break;
121 }
122 default:
123 UNREACHABLE();
124 break;
125 }
126 }
127 m_visited.reset();
128
129 while (!qs.empty()) {
130 var_counter aux_counter;
131 quantifier* q = qs.back();
132 qs.pop_back();
133 aux_counter.m_todo.push_back(q->get_expr());
134 bool has_var1 = false;
135 unsigned max_v = aux_counter.get_max_var(has_var1);
136 if (max_v >= max_var + q->get_num_decls()) {
137 max_var = max_v - q->get_num_decls();
138 has_var = has_var || has_var1;
139 }
140 }
141
142 return max_var;
143 }
144
145
get_max_var(expr * e)146 unsigned var_counter::get_max_var(expr* e) {
147 bool has_var = false;
148 m_todo.push_back(e);
149 return get_max_var(has_var);
150 }
151
get_next_var(expr * e)152 unsigned var_counter::get_next_var(expr* e) {
153 bool has_var = false;
154 m_todo.push_back(e);
155 unsigned mv = get_max_var(has_var);
156 if (has_var) mv++;
157 return mv;
158 }
159
160