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 127 0.0 %
Date: 2020-02-19 00:44:21 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             : {
      97           0 :   std::map<data::sort_expression, std::set<data::sort_expression>> result;
      98           0 :   for(const data::sort_expression& s: dataspec.context_sorts())
      99             :   {
     100           0 :     if(data::is_function_sort(s))
     101             :     {
     102             :       // SMT-LIB2 does not support function sorts
     103           0 :       continue;
     104             :     }
     105           0 :     auto find_alias = dataspec.sort_alias_map().find(s);
     106           0 :     if(find_alias != dataspec.sort_alias_map().end() && find_alias->second != s)
     107             :     {
     108             :       // translate only the unique representation of a sort
     109           0 :       continue;
     110             :     }
     111             : 
     112           0 :     result[s] = find_dependencies(dataspec, s);
     113             :   }
     114           0 :   for(const data::basic_sort& s: dataspec.user_defined_sorts())
     115             :   {
     116           0 :     result[s] = find_dependencies(dataspec, s);
     117             :   }
     118           0 :   return result;
     119             : }
     120             : 
     121             : template <typename OutputStream>
     122             : inline
     123           0 : void translate_sort_definitions(const data::data_specification& dataspec,
     124             :                                OutputStream& out,
     125             :                                const native_translations& nt,
     126             :                                data::set_identifier_generator& id_gen,
     127             :                                std::map<data::structured_sort, std::string>& struct_name_map)
     128             : {
     129           0 :   auto sort_dependencies = find_sorts_and_dependencies(dataspec);
     130             :   // for(const auto& p: sort_dependencies)
     131             :   // {
     132             :   //   std::cout << p.first << " := " << core::detail::print_set(p.second) << std::endl;
     133             :   // }
     134           0 :   auto sorts = topological_sort(sort_dependencies);
     135           0 :   for(const data::sort_expression& s: sorts)
     136             :   {
     137           0 :     std::string name(pp(s));
     138           0 :     if(data::is_structured_sort(s))
     139             :     {
     140           0 :       name = pp(id_gen("@struct"));
     141           0 :       struct_name_map[atermpp::down_cast<data::structured_sort>(s)] = name;
     142             :     }
     143           0 :     translate_sort_definition(name, s, dataspec, out, nt, struct_name_map);
     144             :   }
     145           0 : }
     146             : 
     147             : 
     148             : 
     149             : template <typename OutputStream>
     150             : inline
     151           0 : void translate_alias(const data::alias& s,
     152             :                      OutputStream& out, const native_translations& nt,
     153             :                      const std::map<data::structured_sort, std::string>& struct_name_map)
     154             : {
     155           0 :   out << "(define-sort " << translate_identifier(s.name().name()) << " () ";
     156           0 :   translate_sort_expression(s.reference(), out, nt, struct_name_map);
     157           0 :   out << ")\n";
     158           0 : }
     159             : 
     160             : inline
     161           0 : bool is_higher_order(const data::function_symbol& f)
     162             : {
     163           0 :   const data::sort_expression& s = f.sort();
     164           0 :   if(data::is_function_sort(s))
     165             :   {
     166           0 :     const data::function_sort& fs = atermpp::down_cast<data::function_sort>(s);
     167           0 :     for(const data::sort_expression& arg: fs.domain())
     168             :     {
     169           0 :       if(data::is_function_sort(arg))
     170             :       {
     171           0 :         return true;
     172             :       }
     173             :     }
     174             :   }
     175           0 :   return false;
     176             : }
     177             : 
     178             : inline
     179             : bool is_higher_order(const data::application& a)
     180             : {
     181             :   if(data::is_function_symbol(a.head()))
     182             :   {
     183             :     auto& f = atermpp::down_cast<data::function_symbol>(a.head());
     184             :     return is_higher_order(f);
     185             :   }
     186             :   return true;
     187             : }
     188             : 
     189             : inline
     190           0 : bool is_higher_order(const data::data_equation& eq)
     191             : {
     192           0 :   const data::data_expression& lhs = eq.lhs();
     193           0 :   if(data::is_function_symbol(lhs))
     194             :   {
     195           0 :     return data::is_function_sort(lhs.sort());
     196             :   }
     197           0 :   else if(data::is_application(lhs) && data::is_function_symbol(atermpp::down_cast<data::application>(lhs).head()))
     198             :   {
     199           0 :     return is_higher_order(atermpp::down_cast<data::function_symbol>(atermpp::down_cast<data::application>(lhs).head()));
     200             :   }
     201             :   else
     202             :   {
     203           0 :     return true;
     204             :   }
     205             : }
     206             : 
     207             : template <typename OutputStream>
     208             : inline
     209           0 : void translate_mapping(const data::function_symbol& f, OutputStream& out, const native_translations& nt,
     210             :                        const std::map<data::structured_sort, std::string>& snm, bool check_native = true)
     211             : {
     212           0 :   if(is_higher_order(f) || (check_native && nt.has_native_definition(f)))
     213             :   {
     214           0 :     return;
     215             :   }
     216             : 
     217           0 :   out << "(declare-fun " << translate_symbol(f, nt) << " ";
     218           0 :   if(data::is_function_sort(f.sort()))
     219             :   {
     220           0 :     out << "(";
     221           0 :     data::function_sort fs(atermpp::down_cast<data::function_sort>(f.sort()));
     222           0 :     for(const data::sort_expression& s: fs.domain())
     223             :     {
     224           0 :       translate_sort_expression(s, out, nt, snm);
     225           0 :       out << " ";
     226             :     }
     227           0 :     out << ") ";
     228           0 :     translate_sort_expression(fs.codomain(), out, nt, snm);
     229             :   }
     230             :   else
     231             :   {
     232           0 :     out << "() ";
     233           0 :     translate_sort_expression(f.sort(), out, nt, snm);
     234             :   }
     235           0 :   out << ")\n";
     236             : }
     237             : 
     238             : template <typename OutputStream>
     239             : inline
     240           0 : void translate_native_mappings(OutputStream& out,
     241             :                                std::unordered_map<data::data_expression, std::string>& c,
     242             :                                const native_translations& nt,
     243             :                                const std::map<data::structured_sort, std::string>& snm)
     244             : {
     245           0 :   out << "(define-funs-rec (\n";
     246           0 :   for(const auto& f: nt.mappings)
     247             :   {
     248           0 :     const data::function_symbol& mapping = f.first;
     249           0 :     const data::data_equation& eqn = f.second;
     250           0 :     if(is_higher_order(mapping))
     251             :     {
     252           0 :       continue;
     253             :     }
     254             : 
     255           0 :     out << "(" << translate_symbol(mapping, nt) << " ";
     256           0 :     data::data_expression condition = declare_variables_binder(eqn.variables(), out, nt);
     257           0 :     out << " ";
     258           0 :     translate_sort_expression(mapping.sort().target_sort(), out, nt, snm);
     259           0 :     out << ")\n";
     260             :   }
     261           0 :   out << ")\n";
     262             : 
     263           0 :   out << "(\n";
     264           0 :   for(const auto& f: nt.mappings)
     265             :   {
     266           0 :     const data::function_symbol& mapping = f.first;
     267           0 :     const data::data_equation& eqn = f.second;
     268           0 :     if(is_higher_order(mapping))
     269             :     {
     270           0 :       continue;
     271             :     }
     272             : 
     273           0 :     translate_data_expression(eqn.rhs(), out, c, nt);
     274           0 :     out << "\n";
     275             :   }
     276           0 :   out << "))\n";
     277           0 : }
     278             : 
     279             : template <typename OutputStream>
     280             : inline
     281           0 : void translate_equation(const data::data_equation& eq,
     282             :                         OutputStream& out,
     283             :                         std::unordered_map<data::data_expression, std::string>& c,
     284             :                         const native_translations& nt)
     285             : {
     286           0 :   if(is_higher_order(eq) || nt.has_native_definition(eq))
     287             :   {
     288           0 :     return;
     289             :   }
     290             : 
     291           0 :   const data::variable_list& vars = eq.variables();
     292           0 :   data::data_expression body(data::lazy::implies(eq.condition(), data::equal_to(eq.lhs(), eq.rhs())));
     293           0 :   data::data_expression definition(vars.empty() ? body : data::forall(vars, body));
     294             : 
     295           0 :   translate_assertion(definition, out, c, nt);
     296             : }
     297             : 
     298             : } // namespace detail
     299             : 
     300             : template <typename OutputStream>
     301           0 : void translate_data_specification(const data::data_specification& dataspec,
     302             :                                   OutputStream& o,
     303             :                                   std::unordered_map<data::data_expression, std::string>& c,
     304             :                                   const native_translations& nt)
     305             : {
     306             :   // Generator for new names of projection functions and structs
     307           0 :   data::set_identifier_generator id_gen;
     308             :   // Inline struct definitions are anonymous, we keep track of a newly-generate name for each
     309           0 :   std::map<data::structured_sort, std::string> struct_name_map;
     310             : 
     311             :   // Translate sorts
     312           0 :   detail::translate_sort_definitions(dataspec, o, nt, id_gen, struct_name_map);
     313           0 :   for(const data::alias& s: dataspec.user_defined_aliases())
     314             :   {
     315           0 :     if(dataspec.sort_alias_map().find(s.reference())->second == s.name())
     316             :     {
     317             :       // Left-hand side is already the normalized form
     318           0 :       continue;
     319             :     }
     320           0 :     detail::translate_alias(s, o, nt, struct_name_map);
     321             :   }
     322             : 
     323             :   // Translate mappings
     324           0 :   for(const data::function_symbol& f: dataspec.mappings())
     325             :   {
     326           0 :     detail::translate_mapping(f, o, nt, struct_name_map);
     327             :   }
     328           0 :   detail::translate_native_mappings(o, c, nt, struct_name_map);
     329             : 
     330             :   // Translate remaining equations
     331           0 :   for(const data::data_equation& eq: dataspec.equations())
     332             :   {
     333           0 :     detail::translate_equation(eq, o, c, nt);
     334             :   }
     335           0 : }
     336             : 
     337             : } // namespace smt
     338             : } // namespace mcrl2
     339             : 
     340             : #endif

Generated by: LCOV version 1.13