Line data Source code
1 : // Author(s): Ruud Koolen, 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 : /// \file solver.cpp
10 :
11 : #include "mcrl2/data/list.h"
12 : #include "mcrl2/smt/translate_specification.h"
13 : #include "mcrl2/smt/solver.h"
14 : #include "mcrl2/smt/unfold_pattern_matching.h"
15 :
16 : namespace mcrl2
17 : {
18 : namespace smt
19 : {
20 :
21 0 : answer smt_solver::execute_and_check(const std::string& s, const std::chrono::microseconds& timeout) const
22 : {
23 0 : z3.write(s);
24 0 : std::string result = timeout == std::chrono::microseconds::zero() ? z3.read() : z3.read(timeout);
25 0 : if(result.compare(0, 3, "sat") == 0)
26 : {
27 0 : return answer::SAT;
28 : }
29 0 : else if(result.compare(0, 5, "unsat") == 0)
30 : {
31 0 : return answer::UNSAT;
32 : }
33 0 : else if(result.compare(0, 7, "unknown") == 0)
34 : {
35 0 : return answer::UNKNOWN;
36 : }
37 : else
38 : {
39 0 : mCRL2log(log::error) << "Error when checking satisfiability of \n" << s << std::endl;
40 0 : throw mcrl2::runtime_error("Got unexpected response from SMT-solver:\n" + result);
41 : }
42 0 : }
43 :
44 0 : smt_solver::smt_solver(const data::data_specification& dataspec)
45 0 : : m_native(initialise_native_translation(dataspec))
46 0 : , z3("Z3")
47 : {
48 0 : std::ostringstream out;
49 0 : translate_data_specification(dataspec, out, m_cache, m_native);
50 0 : z3.write(out.str());
51 0 : }
52 :
53 0 : answer smt_solver::solve(const data::variable_list& vars, const data::data_expression& expr, const std::chrono::microseconds& timeout)
54 : {
55 0 : z3.write("(push)\n");
56 0 : std::ostringstream out;
57 0 : translate_variable_declaration(vars, out, m_cache, m_native);
58 0 : translate_assertion(expr, out, m_cache, m_native);
59 0 : out << "(check-sat)\n";
60 0 : answer result = execute_and_check(out.str(), timeout);
61 0 : z3.write("(pop)\n");
62 0 : return result;
63 0 : }
64 :
65 :
66 : namespace detail {
67 :
68 : struct fixed_string_translation: public native_translation_t
69 : {
70 : std::string translation;
71 :
72 : fixed_string_translation(const std::string& s)
73 : : translation(s)
74 : {}
75 :
76 : void operator()(const data::data_expression& /*e*/,
77 : const std::function<void(std::string)>& output_func,
78 : const std::function<void(data::data_expression)>& /*translate_func*/) const
79 : {
80 : output_func(translation);
81 : }
82 : };
83 :
84 0 : static const native_translation_t pp_translation = [](const data::data_expression& e,
85 : const std::function<void(std::string)>& output_func,
86 : const std::function<void(data::data_expression)>& /*translate_func*/)
87 : {
88 0 : output_func(data::pp(e));
89 0 : };
90 0 : static const native_translation_t pp_real_translation = [](const data::data_expression& e,
91 : const std::function<void(std::string)>& output_func,
92 : const std::function<void(data::data_expression)>& /*translate_func*/)
93 : {
94 0 : assert(data::sort_real::is_creal_application(e));
95 0 : const data::application& a = atermpp::down_cast<data::application>(e);
96 0 : output_func("(/ " + data::pp(a[0]) + ".0 " + data::pp(a[1]) + ".0)");
97 0 : };
98 0 : static const native_translation_t reconstruct_divmod = [](const data::data_expression& e,
99 : const std::function<void(std::string)>& output_func,
100 : const std::function<void(data::data_expression)>& translate_func)
101 : {
102 0 : assert(data::sort_nat::is_first_application(e) || data::sort_nat::is_last_application(e));
103 0 : const data::application& a = atermpp::down_cast<data::application>(e);
104 0 : if(data::sort_nat::is_divmod_application(a[0]))
105 : {
106 0 : const data::application& a2 = atermpp::down_cast<data::application>(a[0]);
107 0 : output_func("(" + std::string(data::sort_nat::is_first_application(a2) ? "div" : "mod") + " ");
108 0 : translate_func(a2[0]);
109 0 : output_func(" ");
110 0 : translate_func(a2[1]);
111 0 : output_func(")");
112 : }
113 : else
114 : {
115 0 : throw translation_error("Cannot perform native translation of " + pp(e));
116 : }
117 0 : };
118 :
119 : } // namespace detail
120 :
121 0 : native_translations initialise_native_translation(const data::data_specification& dataspec)
122 : {
123 : using namespace detail;
124 : using namespace data;
125 0 : native_translations nt;
126 :
127 0 : nt.sorts[sort_bool::bool_()] = "Bool";
128 0 : nt.sorts[sort_pos::pos()] = "Int";
129 0 : nt.sorts[sort_nat::nat()] = "Int";
130 0 : nt.sorts[sort_int::int_()] = "Int";
131 0 : nt.sorts[sort_real::real_()] = "Real";
132 :
133 0 : std::vector<sort_expression> number_sorts({ sort_pos::pos(), sort_nat::nat(), sort_int::int_(), sort_real::real_() });
134 0 : std::set<sort_expression> sorts = dataspec.sorts();
135 : // Add native definitions for the left-hand side of every alias
136 0 : for(const auto& alias: dataspec.sort_alias_map())
137 : {
138 0 : sorts.insert(alias.first);
139 : }
140 0 : for(const sort_expression& sort: sorts)
141 : {
142 0 : if(is_basic_sort(sort) || is_container_sort(sort))
143 : {
144 0 : nt.set_native_definition(equal_to(sort), "=");
145 0 : nt.set_native_definition(not_equal_to(sort), "distinct");
146 0 : nt.set_native_definition(if_(sort), "ite");
147 :
148 0 : if(std::find(number_sorts.begin(), number_sorts.end(), sort) != number_sorts.end())
149 : {
150 0 : nt.set_native_definition(less(sort));
151 0 : nt.set_native_definition(less_equal(sort));
152 0 : nt.set_native_definition(greater(sort));
153 0 : nt.set_native_definition(greater_equal(sort));
154 0 : nt.set_alternative_name(sort_real::exp(sort, sort == sort_real::real_() ? sort_int::int_() : sort_nat::nat()), "^");
155 0 : nt.set_alternative_name(sort_real::minus(sort, sort), "-");
156 0 : nt.set_alternative_name(sort_real::negate(sort), "-");
157 : }
158 0 : else if(sort == basic_sort("@NatPair"))
159 : {
160 : // NatPair is not used and its equations upset Z3
161 0 : nt.set_native_definition(less(sort));
162 0 : nt.set_native_definition(less_equal(sort));
163 0 : nt.set_native_definition(greater(sort));
164 0 : nt.set_native_definition(greater_equal(sort));
165 : }
166 : else
167 : {
168 : // Functions <, <=, >, >= are already defined on Int/Real and cannot be overloaded
169 0 : nt.set_alternative_name(less(sort), "@less");
170 0 : nt.set_alternative_name(less_equal(sort), "@less_equal");
171 0 : nt.set_alternative_name(greater(sort), "@greater");
172 0 : nt.set_alternative_name(greater_equal(sort), "@greater_equal");
173 : }
174 :
175 0 : std::string printed_sort_name = nt.sorts.find(sort) != nt.sorts.end() ? nt.sorts.find(sort)->second : translate_identifier(pp(sort));
176 0 : std::string list_sort_name = "(List " + printed_sort_name + ")";
177 0 : nt.set_alternative_name(sort_list::count(sort), "@list_count");
178 0 : nt.set_alternative_name(sort_list::snoc(sort), "@snoc");
179 0 : nt.set_native_definition(sort_list::empty(sort), "nil");
180 0 : nt.set_ambiguous(sort_list::empty(sort));
181 0 : nt.set_native_definition(sort_list::cons_(sort), "insert");
182 0 : nt.set_native_definition(sort_list::head(sort));
183 0 : nt.set_native_definition(sort_list::tail(sort));
184 0 : nt.sorts[sort_list::list(sort)] = list_sort_name;
185 0 : }
186 : }
187 :
188 : std::vector<function_symbol_vector> fs_numbers(
189 : {
190 : sort_pos::pos_generate_functions_code(),
191 : sort_nat::nat_generate_functions_code(),
192 : sort_int::int_generate_functions_code(),
193 : sort_real::real_generate_functions_code()
194 : }
195 0 : );
196 0 : for(const auto& fsv: fs_numbers)
197 : {
198 0 : for(const auto& fs: fsv)
199 : {
200 0 : nt.set_native_definition(fs);
201 : }
202 : }
203 :
204 0 : auto one = [](const sort_expression& s)
205 : {
206 0 : return s == sort_int::int_() ? sort_int::int_(1) : sort_real::real_(1);
207 : };
208 0 : for(const sort_expression& s: { sort_int::int_(), sort_real::real_() })
209 : {
210 0 : variable v1("v1", s);
211 0 : variable v2("v2", s);
212 0 : variable_list l1({v1});
213 0 : variable_list l2({v1,v2});
214 0 : nt.mappings[sort_real::minimum(s,s)] = data_equation(l2, sort_real::minimum(v1, v2), if_(less(v1,v2), v1, v2));
215 0 : nt.mappings[sort_real::maximum(s,s)] = data_equation(l2, sort_real::maximum(v1, v2), if_(less(v1,v2), v2, v1));
216 0 : nt.mappings[sort_real::succ(s)] = data_equation(l1, sort_real::succ(v1), sort_real::plus(v1, one(s)));
217 0 : nt.mappings[sort_real::pred(s)] = data_equation(l1, sort_real::pred(v1), sort_real::minus(v1, one(s)));
218 0 : nt.set_ambiguous(sort_real::minimum(s,s));
219 0 : nt.set_ambiguous(sort_real::maximum(s,s));
220 0 : nt.set_ambiguous(sort_real::succ(s));
221 0 : nt.set_ambiguous(sort_real::pred(s));
222 0 : }
223 0 : nt.expressions[sort_nat::first()] = reconstruct_divmod;
224 0 : nt.expressions[sort_nat::last()] = reconstruct_divmod;
225 :
226 : // TODO come up with equations for these
227 : // nt.mappings[sort_real::floor(s)]
228 : // nt.mappings[sort_real::ceil(s)]
229 : // nt.mappings[sort_real::round(s)]
230 :
231 0 : nt.set_native_definition(sort_bool::not_(), "not");
232 0 : nt.set_native_definition(sort_bool::and_(), "and");
233 0 : nt.set_native_definition(sort_bool::or_(), "or");
234 0 : nt.set_native_definition(sort_bool::implies());
235 :
236 0 : nt.set_native_definition(sort_pos::c1(), pp(sort_pos::c1()));
237 0 : nt.set_native_definition(sort_nat::c0(), pp(sort_nat::c0()));
238 0 : nt.expressions[sort_pos::cdub()] = pp_translation;
239 0 : nt.set_native_definition(sort_nat::cnat(), "@id");
240 0 : nt.set_native_definition(sort_int::cneg(), "-");
241 0 : nt.set_native_definition(sort_int::cint(), "@id");
242 0 : nt.expressions[sort_real::creal()] = pp_real_translation;
243 0 : nt.set_native_definition(sort_real::creal());
244 :
245 0 : nt.special_recogniser[data::sort_bool::true_()] = "@id";
246 0 : nt.special_recogniser[data::sort_bool::false_()] = "not";
247 0 : nt.special_recogniser[data::sort_pos::c1()] = "= 1";
248 0 : nt.special_recogniser[data::sort_pos::cdub()] = ">= 2";
249 0 : nt.special_recogniser[data::sort_nat::c0()] = "= 0";
250 0 : nt.special_recogniser[data::sort_nat::cnat()] = ">= 1";
251 0 : nt.special_recogniser[data::sort_int::cneg()] = "< 0";
252 0 : nt.special_recogniser[data::sort_int::cint()] = ">= 0";
253 :
254 0 : nt.set_native_definition(sort_nat::pos2nat(), "@id");
255 0 : nt.set_native_definition(sort_nat::nat2pos(), "@id");
256 0 : nt.set_native_definition(sort_int::pos2int(), "@id");
257 0 : nt.set_native_definition(sort_int::int2pos(), "@id");
258 0 : nt.set_native_definition(sort_int::nat2int(), "@id");
259 0 : nt.set_native_definition(sort_int::int2nat(), "@id");
260 0 : nt.set_native_definition(sort_real::pos2real(), "to_real");
261 0 : nt.set_native_definition(sort_real::real2pos(), "to_int");
262 0 : nt.set_native_definition(sort_real::nat2real(), "to_real");
263 0 : nt.set_native_definition(sort_real::real2nat(), "to_int");
264 0 : nt.set_native_definition(sort_real::int2real(), "to_real");
265 0 : nt.set_native_definition(sort_real::real2int(), "to_int");
266 :
267 0 : function_symbol id_bool("@id", function_sort({sort_bool::bool_()}, sort_bool::bool_()));
268 0 : function_symbol id_int("@id", function_sort({sort_int::int_()}, sort_int::int_()));
269 0 : function_symbol id_real("@id", function_sort({sort_real::real_()}, sort_real::real_()));
270 0 : variable vb("b", sort_bool::bool_());
271 0 : variable vi("i", sort_int::int_());
272 0 : variable vr("r", sort_real::real_());
273 0 : nt.mappings[id_bool] = data_equation(variable_list({vb}), id_bool(vb), vb);
274 0 : nt.mappings[id_int] = data_equation(variable_list({vi}), id_int(vi), vi);
275 0 : nt.mappings[id_real] = data_equation(variable_list({vr}), id_real(vr), vr);
276 : // necessary for translating the equations above
277 0 : nt.set_native_definition(equal_to(sort_bool::bool_()), "=");
278 0 : nt.set_native_definition(equal_to(sort_int::int_()), "=");
279 0 : nt.set_native_definition(equal_to(sort_real::real_()), "=");
280 :
281 0 : unfold_pattern_matching(dataspec, nt);
282 :
283 0 : return nt;
284 0 : }
285 :
286 :
287 : } // namespace smt
288 : } // namespace mcrl2
|
