Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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/print_utility.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_PRINT_UTILITY_H
      13             : #define MCRL2_DATA_DETAIL_PRINT_UTILITY_H
      14             : 
      15             : #include "mcrl2/core/detail/print_utility.h"
      16             : #include "mcrl2/data/bag.h"
      17             : #include "mcrl2/data/function_update.h"
      18             : #include "mcrl2/data/lambda.h"
      19             : #include "mcrl2/data/list.h"
      20             : #include "mcrl2/data/standard_numbers_utility.h"
      21             : 
      22             : namespace mcrl2 {
      23             : 
      24             : namespace data {
      25             : 
      26             : namespace detail {
      27             : 
      28             : /// \pre BoolExpr is a boolean expression, SortExpr is of type Pos, Nat, Int or
      29             : //     Real.
      30             : /// \return if(BoolExpr, 1, 0) of sort SortExpr
      31             : inline
      32         220 : data::data_expression bool_to_numeric(data::data_expression const& e, data::sort_expression const& s)
      33             : {
      34             :   // TODO Maybe enforce that SortExpr is a PNIR sort
      35         220 :   return data::if_(e, data::function_symbol("1", s), data::function_symbol("0", s));
      36             : }
      37             : 
      38             : inline
      39         641 : data_expression reconstruct_pos_mult(const data_expression& x, std::vector<char>& result)
      40             : {
      41         641 :   data_expression reconstruction_result;
      42         641 :   if (data::sort_pos::is_c1_function_symbol(x))
      43             :   {
      44             :     //x is 1; return result
      45           1 :     reconstruction_result = data::function_symbol(data::detail::vector_number_to_string(result), data::sort_pos::pos());
      46             :   }
      47         640 :   else if (data::sort_pos::is_cdub_application(x))
      48             :   {
      49             :     //x is of the form cDub(b,p); return (result*2)*v(p) + result*v(b)
      50         322 :     data_expression bool_arg = sort_pos::left(x);
      51         322 :     data_expression pos_arg = sort_pos::right(x);
      52         322 :     std::vector<char> double_result = result;
      53         322 :     data::detail::decimal_number_multiply_by_two(double_result);
      54         322 :     pos_arg = reconstruct_pos_mult(pos_arg, double_result);
      55         322 :     if (data::sort_bool::is_false_function_symbol(bool_arg))
      56             :     {
      57             :       //result*v(b) = 0
      58          63 :       reconstruction_result = pos_arg;
      59             :     }
      60         259 :     else if (data::sort_bool::is_true_function_symbol(bool_arg))
      61             :     {
      62             :       //result*v(b) = result
      63          78 :       reconstruction_result = data::sort_real::plus(pos_arg,
      64         117 :                                                     data::function_symbol(data::detail::vector_number_to_string(result), data::sort_pos::pos()));
      65             :     }
      66         220 :     else if (data::detail::vector_number_to_string(result) == "1")
      67             :     {
      68             :       //result*v(b) = v(b)
      69         217 :       reconstruction_result = data::sort_real::plus(pos_arg, bool_to_numeric(bool_arg, data::sort_nat::nat()));
      70             :     }
      71             :     else
      72             :     {
      73             :       //result*v(b)
      74           6 :       reconstruction_result = data::sort_real::plus(pos_arg,
      75           6 :                                                     data::sort_real::times(data::function_symbol(data::detail::vector_number_to_string(result), data::sort_nat::nat()),
      76           9 :                                                     bool_to_numeric(bool_arg, data::sort_nat::nat())));
      77             :     }
      78         322 :   }
      79             :   else
      80             :   {
      81             :     //x is not a Pos constructor
      82         318 :     if (data::detail::vector_number_to_string(result) == "1")
      83             :     {
      84           0 :       reconstruction_result = x;
      85             :     }
      86             :     else
      87             :     {
      88         318 :       reconstruction_result = data::sort_real::times(data::function_symbol(data::detail::vector_number_to_string(result), data::sort_pos::pos()), x);
      89             :     }
      90             :   }
      91         641 :   return reconstruction_result;
      92           0 : }
      93             : 
      94             : } // namespace detail
      95             : 
      96             : } // namespace data
      97             : 
      98             : } // namespace mcrl2
      99             : 
     100             : #endif // MCRL2_DATA_DETAIL_PRINT_UTILITY_H