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_NATIVE_TRANSLATION_H
      10             : #define MCRL2_SMT_NATIVE_TRANSLATION_H
      11             : 
      12             : #include "mcrl2/data/data_specification.h"
      13             : 
      14             : namespace mcrl2
      15             : {
      16             : namespace smt
      17             : {
      18             : 
      19             : typedef std::function<void(data::data_expression, std::function<void(std::string)>, std::function<void(data::data_expression)>)> native_translation_t;
      20             : struct native_translations
      21             : {
      22             :   // If f occurs in symbols, its translation should be symbols[f]
      23             :   std::map<data::function_symbol, std::string> symbols;
      24             :   // If f occurs in expressions, all applications f(a) should be translated by the function expressions[f]
      25             :   std::map<data::function_symbol, native_translation_t> expressions;
      26             :   // Function symbols for which the equations should not be defined
      27             :   std::set<data::function_symbol> do_not_define;
      28             :   // Pairs of mappings and equations that need to be translated as well
      29             :   std::map<data::function_symbol, data::data_equation> mappings;
      30             :   // Sorts that have a native definition in Z3
      31             :   std::map<data::sort_expression, std::string> sorts;
      32             :   // Function symbols that are overloaded
      33             :   std::set<data::function_symbol> ambiguous_symbols;
      34             :   // Constructors that have a native recogniser
      35             :   std::map<data::function_symbol, std::string> special_recogniser;
      36             : 
      37           0 :   native_translations() = default;
      38             : 
      39             :   // native_translations(native_translation_map_t s,
      40             :   //                     native_translation_map_t e,
      41             :   //                     std::map<data::function_symbol, data::data_equation> m,
      42             :   //                     std::map<data::sort_expression, std::string> so
      43             :   //                    )
      44             :   // : symbols(std::move(s))
      45             :   // , expressions(std::move(e))
      46             :   // , mappings(std::move(m))
      47             :   // , sorts(std::move(so))
      48             :   // {}
      49             : 
      50           0 :   std::map<data::function_symbol, native_translation_t>::const_iterator find_native_translation(const data::application& a) const
      51             :   {
      52           0 :     if(data::is_function_symbol(a.head()))
      53             :     {
      54           0 :       auto& f = atermpp::down_cast<data::function_symbol>(a.head());
      55           0 :       return expressions.find(f);
      56             :     }
      57           0 :     return expressions.end();
      58             :   }
      59             : 
      60           0 :   bool has_native_definition(const data::function_symbol& f) const
      61             :   {
      62           0 :     return do_not_define.find(f) != do_not_define.end();
      63             :   }
      64             : 
      65             :   bool has_native_definition(const data::application& a) const
      66             :   {
      67             :     if(data::is_function_symbol(a.head()))
      68             :     {
      69             :       auto& f = atermpp::down_cast<data::function_symbol>(a.head());
      70             :       return has_native_definition(f);
      71             :     }
      72             :     return false;
      73             :   }
      74             : 
      75           0 :   bool has_native_definition(const data::data_equation& eq) const
      76             :   {
      77           0 :     const data::data_expression& lhs = eq.lhs();
      78           0 :     if(data::is_function_symbol(lhs))
      79             :     {
      80           0 :       return has_native_definition(atermpp::down_cast<data::function_symbol>(lhs));
      81             :     }
      82           0 :     else if(data::is_application(lhs) && data::is_function_symbol(atermpp::down_cast<data::application>(lhs).head()))
      83             :     {
      84           0 :       return has_native_definition(atermpp::down_cast<data::function_symbol>(atermpp::down_cast<data::application>(lhs).head()));
      85             :     }
      86             :     else
      87             :     {
      88           0 :       return false;
      89             :     }
      90             :   }
      91             : 
      92           0 :   bool is_ambiguous(const data::function_symbol& f) const
      93             :   {
      94           0 :     return ambiguous_symbols.find(f) != ambiguous_symbols.end();
      95             :   }
      96             : 
      97             :   /**
      98             :    * \brief Record that the mapping and equations for f should not be translated
      99             :    * \details This translation is either not desired because there is a native Z3
     100             :    * counterpart, or because the function symbol is only used internally.
     101             :    */
     102           0 :   void set_native_definition(const data::function_symbol& f)
     103             :   {
     104           0 :     do_not_define.insert(f);
     105           0 :   }
     106             : 
     107           0 :   void set_native_definition(const data::function_symbol& f, const data::data_equation& eq)
     108             :   {
     109           0 :     do_not_define.insert(f);
     110           0 :     mappings[f] = eq;
     111           0 :   }
     112             : 
     113           0 :   void set_native_definition(const data::function_symbol& f, const std::string& s)
     114             :   {
     115           0 :     symbols[f] = s;
     116           0 :     do_not_define.insert(f);
     117           0 :   }
     118             : 
     119           0 :   void set_alternative_name(const data::function_symbol& f, const std::string& s)
     120             :   {
     121           0 :     symbols[f] = s;
     122           0 :   }
     123             : 
     124           0 :   void set_ambiguous(const data::function_symbol& f)
     125             :   {
     126           0 :     ambiguous_symbols.insert(f);
     127           0 :   }
     128             : };
     129             : 
     130             : 
     131             : native_translations initialise_native_translation(const data::data_specification& dataspec);
     132             : 
     133             : } // namespace smt
     134             : } // namespace mcrl2
     135             : 
     136             : #endif