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_EXPRESSION_H
10 : #define MCRL2_SMT_TRANSLATE_EXPRESSION_H
11 :
12 : #include "mcrl2/smt/translate_sort.h"
13 :
14 : namespace mcrl2
15 : {
16 : namespace smt
17 : {
18 :
19 : template <typename T, typename OutputStream>
20 : void translate_data_expression(const T& x, OutputStream& o, std::unordered_map<data::data_expression, std::string>& c, const native_translations& nt);
21 :
22 : namespace detail
23 : {
24 :
25 : inline
26 0 : std::string translate_symbol_disambiguate(const data::function_symbol& f, const native_translations& nt)
27 : {
28 0 : std::string f_pp(translate_symbol(f, nt));
29 0 : if(nt.is_ambiguous(f))
30 : {
31 0 : std::ostringstream o;
32 0 : translate_sort_expression(f.sort().target_sort(), o, nt);
33 0 : return "(as " + f_pp + " " + o.str() + ")";
34 0 : }
35 : else
36 : {
37 0 : return f_pp;
38 : }
39 0 : }
40 :
41 : /**
42 : * \brief Declare variables to be used in binder such as exists or forall and print the declaration to out
43 : * \return An expression that constrains the domains of Pos and Nat variables
44 : */
45 : template <typename OutputStream>
46 0 : data::data_expression declare_variables_binder(const data::variable_list& vars, OutputStream& out, const native_translations& nt)
47 : {
48 0 : data::data_expression result = data::sort_bool::true_();
49 0 : out << "(";
50 0 : for(const data::variable& var: vars)
51 : {
52 0 : out << "(" << translate_identifier(var.name()) << " ";
53 0 : translate_sort_expression(var.sort(), out, nt);
54 0 : out << ")";
55 0 : if(var.sort() == data::sort_pos::pos())
56 : {
57 0 : result = data::lazy::and_(result, greater_equal(var, data::sort_pos::c1()));
58 : }
59 0 : else if(var.sort() == data::sort_nat::nat())
60 : {
61 0 : result = data::lazy::and_(result, greater_equal(var, data::sort_nat::c0()));
62 : }
63 : }
64 0 : out << ")";
65 0 : return result;
66 0 : }
67 :
68 : template <template <class> class Traverser, class OutputStream>
69 : struct translate_data_expression_traverser: public Traverser<translate_data_expression_traverser<Traverser, OutputStream> >
70 : {
71 : typedef Traverser<translate_data_expression_traverser<Traverser, OutputStream> > super;
72 : using super::apply;
73 :
74 : stack_outstream<OutputStream> out;
75 : std::unordered_map<data::data_expression, std::string>& m_cache;
76 : const native_translations& m_native;
77 :
78 0 : translate_data_expression_traverser(OutputStream& out_, std::unordered_map<data::data_expression, std::string>& cache, const native_translations& nt)
79 0 : : out(out_)
80 0 : , m_cache(cache)
81 0 : , m_native(nt)
82 0 : {}
83 :
84 0 : void apply(const data::data_expression& d)
85 : {
86 0 : auto c = m_cache.find(d);
87 0 : if(c == m_cache.end())
88 : {
89 0 : out.push();
90 0 : super::apply(d);
91 0 : if(out.top_size() <= 400)
92 : {
93 0 : out.copy_top(m_cache[d]);
94 : }
95 0 : out.pop();
96 : }
97 : else
98 : {
99 0 : out << c->second;
100 : }
101 0 : }
102 :
103 0 : void apply(const data::application& v)
104 : {
105 0 : auto find_result = m_native.find_native_translation(v);
106 0 : if(find_result != m_native.expressions.end())
107 : {
108 0 : auto translate_func = [&](const data::data_expression& e) { return apply(e); };
109 0 : auto output_func = [&](const std::string& s) { out << s; };
110 0 : find_result->second(v, output_func, translate_func);
111 0 : out << " ";
112 : }
113 : else
114 : {
115 0 : out << "(";
116 0 : super::apply(v);
117 0 : out << ") ";
118 : }
119 0 : }
120 :
121 0 : void apply(const data::function_symbol& v)
122 : {
123 0 : out << translate_symbol_disambiguate(v, m_native) << " ";
124 0 : }
125 :
126 0 : void apply(const data::variable& v)
127 : {
128 0 : out << translate_identifier(v.name()) << " ";
129 0 : }
130 :
131 0 : void apply(const data::forall& v)
132 : {
133 0 : out << "(forall ";
134 0 : data::data_expression vars_conditions = declare_variables_binder(v.variables(), out, m_native);
135 0 : out << " ";
136 0 : apply(data::lazy::implies(vars_conditions, v.body()));
137 0 : out << ")";
138 0 : }
139 :
140 0 : void apply(const data::exists& v)
141 : {
142 0 : out << "(exists ";
143 0 : data::data_expression vars_conditions = declare_variables_binder(v.variables(), out, m_native);
144 0 : out << " ";
145 0 : apply(data::lazy::and_(vars_conditions, v.body()));
146 0 : out << ")";
147 0 : }
148 :
149 0 : void apply(const data::where_clause& v)
150 : {
151 0 : out << "(let (";
152 0 : for(const data::assignment_expression& a: v.declarations())
153 : {
154 0 : const data::assignment& as = atermpp::down_cast<data::assignment>(a);
155 0 : out << "(";
156 0 : apply(as.lhs());
157 0 : out << " ";
158 0 : apply(as.rhs());
159 0 : out << ")";
160 : }
161 0 : out << ") ";
162 0 : apply(v.body());
163 0 : out << ")";
164 0 : }
165 : };
166 :
167 : } // namespace detail
168 :
169 : template <typename T, typename OutputStream>
170 0 : void translate_data_expression(const T& x, OutputStream& o, std::unordered_map<data::data_expression, std::string>& c, const native_translations& nt)
171 : {
172 0 : detail::translate_data_expression_traverser<data::data_expression_traverser, OutputStream>(o, c, nt).apply(x);
173 0 : }
174 :
175 : template <typename T, typename OutputStream>
176 0 : void translate_assertion(const T& x, OutputStream& o, std::unordered_map<data::data_expression, std::string>& c, const native_translations& nt)
177 : {
178 0 : o << "(assert ";
179 0 : translate_data_expression(x, o, c, nt);
180 0 : o << ")\n";
181 0 : }
182 :
183 : template <typename Container, typename OutputStream>
184 0 : void translate_variable_declaration(const Container& vars, OutputStream& o, std::unordered_map<data::data_expression, std::string>& c, const native_translations& nt)
185 : {
186 0 : data::data_expression vars_conditions = data::sort_bool::true_();
187 0 : for(const data::variable& v: vars)
188 : {
189 0 : o << "(declare-fun " << translate_identifier(v.name()) << " (";
190 0 : data::sort_expression_list domain = data::is_function_sort(v.sort()) ?
191 0 : atermpp::down_cast<data::function_sort>(v.sort()).domain() : data::sort_expression_list();
192 0 : for(const data::sort_expression& s: domain)
193 : {
194 0 : translate_sort_expression(s, o, nt);
195 0 : o << " ";
196 0 : if(s == data::sort_pos::pos())
197 : {
198 0 : vars_conditions = data::lazy::and_(vars_conditions, greater_equal(v, data::sort_pos::c1()));
199 : }
200 0 : else if(s == data::sort_nat::nat())
201 : {
202 0 : vars_conditions = data::lazy::and_(vars_conditions, greater_equal(v, data::sort_nat::c0()));
203 : }
204 : }
205 0 : o << ") ";
206 0 : translate_sort_expression(v.sort().target_sort(), o, nt);
207 0 : o << ")\n";
208 : }
209 0 : translate_assertion(vars_conditions, o, c, nt);
210 0 : }
211 :
212 : } // namespace smt
213 : } // namespace mcrl2
214 :
215 : #endif
|
