Line data    Source code

       1             : // Author(s): Jan Friso Groote
       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 mcrl2/data/detail/function_update.h
      10             : /// \brief This files contains the implementation of the function "is_not_a_function_update"
      11             : ///        which was declared as"defined_by_code" in the file build/code_generation/data_types/function_update.spec. 
      12             : 
      13             : #ifndef MCRL2_DATA_DETAIL_FUNCTION_UPDATE_H
      14             : #define MCRL2_DATA_DETAIL_FUNCTION_UPDATE_H
      15             : 
      16             : #include "mcrl2/data/find.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : namespace data
      21             : {
      22             : 
      23             : // Prototype. 
      24             : inline function_symbol function_update(const sort_expression& s, const sort_expression& t);
      25             : inline function_symbol function_update_stable(const sort_expression& s, const sort_expression& t);
      26             : 
      27             : 
      28         164 : inline data_expression is_not_a_function_update_manual_implementation(const data_expression& f)
      29             : {
      30         164 :   function_sort sort=atermpp::down_cast<function_sort>(f.sort());
      31         164 :   assert(sort.domain().front().size()==1);
      32             : 
      33         164 :   std::set<function_symbol> function_symbol_set = find_function_symbols(f);
      34         404 :   if (function_symbol_set.count(function_update_stable(sort.domain().front(), sort.codomain()))==0 &&
      35         240 :       function_symbol_set.count(function_update(sort.domain().front(), sort.codomain()))==0)
      36             :   {
      37          76 :     std::set<variable> variable_set = find_free_variables(f);
      38          76 :     if (variable_set.size()==0)
      39             :     {
      40          68 :       return sort_bool::true_();
      41             :     }
      42          76 :   }
      43          96 :   return sort_bool::false_();
      44         164 : }
      45             : 
      46         156 : inline data_expression if_always_else_manual_implementation(const data_expression& b, const data_expression& e1, const data_expression& e2)
      47             : {
      48         156 :   if (b==sort_bool::true_())
      49             :   {
      50          54 :     return e1;
      51             :   }
      52         102 :   return e2;
      53             : }
      54             : 
      55             : } // namespace data
      56             : } // namespace mcrl2
      57             : 
      58             : #endif // MCRL2_DATA_DETAIL_FUNCTION_UPDATE_H