1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 smt_decl_collector.cpp
7
8 Abstract:
9
10 Collect uninterpreted func_delcs and sorts.
11 This class was originally in ast_smt_pp.h
12
13 Author:
14
15 Leonardo (leonardo) 2011-10-04
16
17 Revision History:
18
19 --*/
20 #include "ast/decl_collector.h"
21 #include "ast/ast_pp.h"
22
visit_sort(sort * n)23 void decl_collector::visit_sort(sort * n) {
24 SASSERT(!m_visited.is_marked(n));
25 family_id fid = n->get_family_id();
26 if (m().is_uninterp(n))
27 m_sorts.push_back(n);
28 else if (fid == m_dt_fid) {
29 m_sorts.push_back(n);
30 for (func_decl * cnstr : *m_dt_util.get_datatype_constructors(n)) {
31 m_todo.push_back(cnstr);
32 ptr_vector<func_decl> const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr);
33 unsigned num_cas = cnstr_acc.size();
34 for (unsigned j = 0; j < num_cas; j++) {
35 m_todo.push_back(cnstr_acc.get(j));
36 }
37 }
38 }
39 for (unsigned i = n->get_num_parameters(); i-- > 0; ) {
40 parameter const& p = n->get_parameter(i);
41 if (p.is_ast()) m_todo.push_back(p.get_ast());
42 }
43 }
44
is_bool(sort * s)45 bool decl_collector::is_bool(sort * s) {
46 return m().is_bool(s);
47 }
48
visit_func(func_decl * n)49 void decl_collector::visit_func(func_decl * n) {
50 if (!m_visited.is_marked(n)) {
51 family_id fid = n->get_family_id();
52 if (fid == null_family_id) {
53 m_decls.push_back(n);
54 }
55 m_visited.mark(n, true);
56 m_trail.push_back(n);
57 }
58 }
59
decl_collector(ast_manager & m)60 decl_collector::decl_collector(ast_manager & m):
61 m_manager(m),
62 m_trail(m),
63 m_dt_util(m) {
64 m_basic_fid = m_manager.get_basic_family_id();
65 m_dt_fid = m_dt_util.get_family_id();
66 }
67
visit(ast * n)68 void decl_collector::visit(ast* n) {
69 if (m_visited.is_marked(n))
70 return;
71 datatype_util util(m());
72 m_todo.push_back(n);
73 while (!m_todo.empty()) {
74 n = m_todo.back();
75 m_todo.pop_back();
76 if (!m_visited.is_marked(n)) {
77 switch(n->get_kind()) {
78 case AST_APP: {
79 app * a = to_app(n);
80 for (expr* arg : *a) {
81 m_todo.push_back(arg);
82 }
83 m_todo.push_back(a->get_decl());
84 break;
85 }
86 case AST_QUANTIFIER: {
87 quantifier * q = to_quantifier(n);
88 unsigned num_decls = q->get_num_decls();
89 for (unsigned i = 0; i < num_decls; ++i) {
90 m_todo.push_back(q->get_decl_sort(i));
91 }
92 m_todo.push_back(q->get_expr());
93 for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
94 m_todo.push_back(q->get_pattern(i));
95 }
96 break;
97 }
98 case AST_SORT:
99 visit_sort(to_sort(n));
100 break;
101 case AST_FUNC_DECL: {
102 func_decl * d = to_func_decl(n);
103 for (sort* srt : *d) {
104 m_todo.push_back(srt);
105 }
106 m_todo.push_back(d->get_range());
107 visit_func(d);
108 break;
109 }
110 case AST_VAR:
111 break;
112 default:
113 UNREACHABLE();
114 }
115 m_visited.mark(n, true);
116 m_trail.push_back(n);
117 }
118 }
119 }
120
order_deps(unsigned n)121 void decl_collector::order_deps(unsigned n) {
122 top_sort<sort> st;
123 for (unsigned i = n; i < m_sorts.size(); ++i) {
124 sort* s = m_sorts.get(i);
125 st.insert(s, collect_deps(s));
126 }
127 st.topological_sort();
128 m_sorts.shrink(n);
129 for (sort* s : st.top_sorted()) {
130 m_sorts.push_back(s);
131 }
132 }
133
collect_deps(sort * s)134 decl_collector::sort_set* decl_collector::collect_deps(sort* s) {
135 sort_set* set = alloc(sort_set);
136 collect_deps(s, *set);
137 set->remove(s);
138 return set;
139 }
140
collect_deps(sort * s,sort_set & set)141 void decl_collector::collect_deps(sort* s, sort_set& set) {
142 if (set.contains(s)) return;
143 set.insert(s);
144 if (s->is_sort_of(m_dt_util.get_family_id(), DATATYPE_SORT)) {
145 unsigned num_sorts = m_dt_util.get_datatype_num_parameter_sorts(s);
146 for (unsigned i = 0; i < num_sorts; ++i) {
147 set.insert(m_dt_util.get_datatype_parameter_sort(s, i));
148 }
149 unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(s);
150 for (unsigned i = 0; i < num_cnstr; i++) {
151 func_decl * cnstr = m_dt_util.get_datatype_constructors(s)->get(i);
152 set.insert(cnstr->get_range());
153 for (unsigned j = 0; j < cnstr->get_arity(); ++j)
154 set.insert(cnstr->get_domain(j));
155 }
156 }
157
158 for (unsigned i = s->get_num_parameters(); i-- > 0; ) {
159 parameter const& p = s->get_parameter(i);
160 if (p.is_ast() && is_sort(p.get_ast())) {
161 set.insert(to_sort(p.get_ast()));
162 }
163 }
164 }
165
push()166 void decl_collector::push() {
167 m_trail_lim.push_back(m_trail.size());
168 m_sorts_lim.push_back(m_sorts.size());
169 m_decls_lim.push_back(m_decls.size());
170 }
171
pop(unsigned n)172 void decl_collector::pop(unsigned n) {
173 SASSERT(n > 0);
174 unsigned sz = m_trail_lim[m_trail_lim.size() - n];
175 for (unsigned i = m_trail.size(); i-- > sz; ) {
176 m_visited.mark(m_trail.get(i), false);
177 }
178 m_trail.shrink(sz);
179 m_sorts.shrink(m_sorts_lim[m_sorts_lim.size() - n]);
180 m_decls.shrink(m_decls_lim[m_decls_lim.size() - n]);
181 m_trail_lim.shrink(m_trail_lim.size() - n);
182 m_sorts_lim.shrink(m_sorts_lim.size() - n);
183 m_decls_lim.shrink(m_decls_lim.size() - n);
184 }
185
186