LCOV - code coverage report
Current view: top level - smt/source - solver.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 161 0.0 %
Date: 2020-10-20 00:45:57 Functions: 0 10 0.0 %
Legend: Lines: hit not hit

          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             : }
      43             : 
      44           0 : smt_solver::smt_solver(const data::data_specification& dataspec)
      45             : : 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             : }
      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           0 :                                                       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           0 :                                                            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           0 :                                                           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             :     }
     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           0 :   };
     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             :   }
     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             : }
     285             : 
     286             : 
     287             : } // namespace smt
     288           0 : } // namespace mcrl2

Generated by: LCOV version 1.13