Line data Source code
1 : // Author(s): Thomas Neele
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 :
9 : #ifndef MCRL2_SMT_TRANSLATE_SPECIFICATION_H
10 : #define MCRL2_SMT_TRANSLATE_SPECIFICATION_H
11 :
12 : #include "mcrl2/atermpp/aterm_io.h"
13 : #include "mcrl2/core/detail/print_utility.h"
14 : #include "mcrl2/data/find.h"
15 : #include "mcrl2/smt/translate_expression.h"
16 :
17 : namespace mcrl2
18 : {
19 : namespace smt
20 : {
21 : namespace detail
22 : {
23 :
24 : template <typename OutputStream>
25 : inline
26 0 : void translate_sort_definition(const std::string& sort_name,
27 : const data::sort_expression& s,
28 : const data::data_specification& dataspec,
29 : OutputStream& out,
30 : const native_translations& nt,
31 : std::map<data::structured_sort, std::string>& struct_name_map)
32 : {
33 0 : auto find_result = nt.sorts.find(s);
34 0 : if(find_result != nt.sorts.end())
35 : {
36 : // Do not output anything for natively defined sorts
37 0 : return;
38 : }
39 :
40 0 : out << "(declare-datatypes () ((" << translate_identifier(sort_name) << " ";
41 0 : for(const data::function_symbol& cons: dataspec.constructors(s))
42 : {
43 0 : out << "(" << translate_identifier(cons.name()) << " ";
44 0 : if(data::is_function_sort(cons.sort()))
45 : {
46 0 : const data::function_sort& cs = atermpp::down_cast<data::function_sort>(cons.sort());
47 0 : std::size_t index = 0;
48 0 : for(const data::sort_expression& arg: cs.domain())
49 : {
50 0 : out << "(" << make_projection_name(cons, index, nt) << " ";
51 0 : translate_sort_expression(arg, out, nt, struct_name_map);
52 0 : out << ") ";
53 0 : index++;
54 : }
55 : }
56 0 : out << ") ";
57 : }
58 0 : out << ")))\n";
59 : }
60 :
61 : template <typename OutputStream>
62 : inline
63 : void translate_sort_definition(const data::basic_sort& s,
64 : const data::data_specification& dataspec,
65 : OutputStream& out,
66 : const native_translations& nt,
67 : std::map<data::structured_sort, std::string>& struct_name_map)
68 : {
69 : translate_sort_definition(pp(s.name()), s, dataspec, out, nt, struct_name_map);
70 : }
71 :
72 : // Find the dependencies in the definition of a sort
73 : static inline
74 0 : std::set<data::sort_expression> find_dependencies(const data::data_specification& dataspec, const data::sort_expression& sort)
75 : {
76 0 : std::set<data::sort_expression> dependencies;
77 0 : for(const data::function_symbol& cons: dataspec.constructors(sort))
78 : {
79 0 : find_sort_expressions(cons, std::inserter(dependencies, dependencies.end()));
80 : }
81 :
82 0 : std::set<data::sort_expression> result;
83 0 : for(const data::sort_expression& s: dependencies)
84 : {
85 0 : if((data::is_basic_sort(s) || data::is_structured_sort(s)) && s != sort)
86 : {
87 0 : result.insert(s);
88 : }
89 : }
90 0 : return result;
91 0 : }
92 :
93 : // Find all sorts that need to be translated and the dependencies in their definitions
94 : inline
95 0 : std::map<data::sort_expression, std::set<data::sort_expression>> find_sorts_and_dependencies(const data::data_specification& dataspec,
96 : std::map<data::structured_sort, std::string>& struct_name_map)
97 : {
98 0 : std::map<data::sort_expression, std::set<data::sort_expression>> result;
99 0 : for(const data::sort_expression& s: dataspec.sorts())
100 : {
101 0 : if(data::is_function_sort(s))
102 : {
103 : // SMT-LIB2 does not support function sorts
104 : // Hope & pray that nothing breaks later...
105 0 : continue;
106 : }
107 0 : auto find_alias = dataspec.sort_alias_map().find(s);
108 0 : if(find_alias != dataspec.sort_alias_map().end() && find_alias->second != s)
109 : {
110 0 : if(data::is_structured_sort(s))
111 : {
112 0 : struct_name_map[atermpp::down_cast<data::structured_sort>(s)] = pp(find_alias->second);
113 : }
114 : // translate only the unique representation of a sort
115 0 : continue;
116 : }
117 :
118 0 : result[s] = find_dependencies(dataspec, s);
119 : }
120 0 : return result;
121 0 : }
122 :
123 : template <typename OutputStream>
124 : inline
125 0 : void translate_sort_definitions(const data::data_specification& dataspec,
126 : OutputStream& out,
127 : const native_translations& nt,
128 : data::set_identifier_generator& id_gen,
129 : std::map<data::structured_sort, std::string>& struct_name_map)
130 : {
131 0 : auto sort_dependencies = find_sorts_and_dependencies(dataspec, struct_name_map);
132 : // for(const auto& p: sort_dependencies)
133 : // {
134 : // std::cout << p.first << " := " << core::detail::print_set(p.second) << std::endl;
135 : // }
136 0 : auto sorts = topological_sort(sort_dependencies);
137 0 : for(const data::sort_expression& s: sorts)
138 : {
139 0 : std::string name(pp(s));
140 0 : if(data::is_structured_sort(s))
141 : {
142 : // The structured sort is anonymous. Can happen in a specification such as
143 : // sort StateList = List(struct s1 | s2);
144 0 : name = pp(id_gen("@struct"));
145 0 : struct_name_map[atermpp::down_cast<data::structured_sort>(s)] = name;
146 : }
147 0 : translate_sort_definition(name, s, dataspec, out, nt, struct_name_map);
148 : }
149 0 : }
150 :
151 :
152 :
153 : template <typename OutputStream>
154 : inline
155 0 : void translate_alias(const data::alias& s,
156 : OutputStream& out, const native_translations& nt,
157 : const std::map<data::structured_sort, std::string>& struct_name_map)
158 : {
159 0 : out << "(define-sort " << translate_identifier(s.name().name()) << " () ";
160 0 : translate_sort_expression(s.reference(), out, nt, struct_name_map);
161 0 : out << ")\n";
162 0 : }
163 :
164 : inline
165 0 : bool is_higher_order(const data::function_symbol& f)
166 : {
167 0 : const data::sort_expression& s = f.sort();
168 0 : if(data::is_function_sort(s))
169 : {
170 0 : const data::function_sort& fs = atermpp::down_cast<data::function_sort>(s);
171 0 : for(const data::sort_expression& arg: fs.domain())
172 : {
173 0 : if(data::is_function_sort(arg))
174 : {
175 0 : return true;
176 : }
177 : }
178 : }
179 0 : return false;
180 : }
181 :
182 : inline
183 : bool is_higher_order(const data::application& a)
184 : {
185 : if(data::is_function_symbol(a.head()))
186 : {
187 : auto& f = atermpp::down_cast<data::function_symbol>(a.head());
188 : return is_higher_order(f);
189 : }
190 : return true;
191 : }
192 :
193 : inline
194 0 : bool is_higher_order(const data::data_equation& eq)
195 : {
196 0 : const data::data_expression& lhs = eq.lhs();
197 0 : if(data::is_function_symbol(lhs))
198 : {
199 0 : return data::is_function_sort(lhs.sort());
200 : }
201 0 : else if(data::is_application(lhs) && data::is_function_symbol(atermpp::down_cast<data::application>(lhs).head()))
202 : {
203 0 : return is_higher_order(atermpp::down_cast<data::function_symbol>(atermpp::down_cast<data::application>(lhs).head()));
204 : }
205 : else
206 : {
207 0 : return true;
208 : }
209 : }
210 :
211 : template <typename OutputStream>
212 : inline
213 0 : void translate_mapping(const data::function_symbol& f, OutputStream& out, const native_translations& nt,
214 : const std::map<data::structured_sort, std::string>& snm, bool check_native = true)
215 : {
216 0 : if(is_higher_order(f) || (check_native && nt.has_native_definition(f)))
217 : {
218 0 : return;
219 : }
220 :
221 0 : out << "(declare-fun " << translate_symbol(f, nt) << " ";
222 0 : if(data::is_function_sort(f.sort()))
223 : {
224 0 : out << "(";
225 0 : data::function_sort fs(atermpp::down_cast<data::function_sort>(f.sort()));
226 0 : for(const data::sort_expression& s: fs.domain())
227 : {
228 0 : translate_sort_expression(s, out, nt, snm);
229 0 : out << " ";
230 : }
231 0 : out << ") ";
232 0 : translate_sort_expression(fs.codomain(), out, nt, snm);
233 0 : }
234 : else
235 : {
236 0 : out << "() ";
237 0 : translate_sort_expression(f.sort(), out, nt, snm);
238 : }
239 0 : out << ")\n";
240 : }
241 :
242 : template <typename OutputStream>
243 : inline
244 0 : void translate_native_mappings(OutputStream& out,
245 : std::unordered_map<data::data_expression, std::string>& c,
246 : const native_translations& nt,
247 : const std::map<data::structured_sort, std::string>& snm)
248 : {
249 0 : out << "(define-funs-rec (\n";
250 0 : for(const auto& f: nt.mappings)
251 : {
252 0 : const data::function_symbol& mapping = f.first;
253 0 : const data::data_equation& eqn = f.second;
254 0 : if(is_higher_order(mapping))
255 : {
256 0 : continue;
257 : }
258 :
259 0 : out << "(" << translate_symbol(mapping, nt) << " ";
260 0 : data::data_expression condition = declare_variables_binder(eqn.variables(), out, nt);
261 0 : out << " ";
262 0 : translate_sort_expression(mapping.sort().target_sort(), out, nt, snm);
263 0 : out << ")\n";
264 : }
265 0 : out << ")\n";
266 :
267 0 : out << "(\n";
268 0 : for(const auto& f: nt.mappings)
269 : {
270 0 : const data::function_symbol& mapping = f.first;
271 0 : const data::data_equation& eqn = f.second;
272 0 : if(is_higher_order(mapping))
273 : {
274 0 : continue;
275 : }
276 :
277 0 : translate_data_expression(eqn.rhs(), out, c, nt);
278 0 : out << "\n";
279 : }
280 0 : out << "))\n";
281 0 : }
282 :
283 : template <typename OutputStream>
284 : inline
285 0 : void translate_equation(const data::data_equation& eq,
286 : OutputStream& out,
287 : std::unordered_map<data::data_expression, std::string>& c,
288 : const native_translations& nt)
289 : {
290 0 : if(is_higher_order(eq) || nt.has_native_definition(eq))
291 : {
292 0 : return;
293 : }
294 :
295 0 : const data::variable_list& vars = eq.variables();
296 0 : data::data_expression body(data::lazy::implies(eq.condition(), data::equal_to(eq.lhs(), eq.rhs())));
297 0 : data::data_expression definition(vars.empty() ? body : data::forall(vars, body));
298 :
299 0 : translate_assertion(definition, out, c, nt);
300 0 : }
301 :
302 : } // namespace detail
303 :
304 : template <typename OutputStream>
305 0 : void translate_data_specification(const data::data_specification& dataspec,
306 : OutputStream& o,
307 : std::unordered_map<data::data_expression, std::string>& c,
308 : const native_translations& nt)
309 : {
310 : // Generator for new names of projection functions and structs
311 0 : data::set_identifier_generator id_gen;
312 : // Inline struct definitions are anonymous, we keep track of a newly-generate name for each
313 0 : std::map<data::structured_sort, std::string> struct_name_map;
314 :
315 : // Translate sorts
316 0 : detail::translate_sort_definitions(dataspec, o, nt, id_gen, struct_name_map);
317 0 : for(const auto& s: dataspec.sort_alias_map())
318 : {
319 0 : if(data::is_basic_sort(s.first))
320 : {
321 0 : detail::translate_alias(data::alias(atermpp::down_cast<data::basic_sort>(s.first), s.second), o, nt, struct_name_map);
322 : }
323 : }
324 :
325 : // Translate mappings
326 0 : for(const data::function_symbol& f: dataspec.mappings())
327 : {
328 0 : detail::translate_mapping(f, o, nt, struct_name_map);
329 : }
330 0 : detail::translate_native_mappings(o, c, nt, struct_name_map);
331 :
332 : // Translate remaining equations
333 0 : for(const data::data_equation& eq: dataspec.equations())
334 : {
335 0 : detail::translate_equation(eq, o, c, nt);
336 : }
337 0 : }
338 :
339 : } // namespace smt
340 : } // namespace mcrl2
341 :
342 : #endif
|
