LCOV - code coverage report
Current view: top level - smt/include/mcrl2/smt - translate_specification.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 126 0.0 %
Date: 2020-09-22 00:46:14 Functions: 0 11 0.0 %
Legend: Lines: hit not hit

          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             : }
      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             : }
     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             :   }
     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             : }
     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

Generated by: LCOV version 1.13