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/one_point_rule_preprocessor.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_ONE_POINT_RULE_PREPROCESSOR_H
      13             : #define MCRL2_DATA_DETAIL_ONE_POINT_RULE_PREPROCESSOR_H
      14             : 
      15             : #include "mcrl2/data/join.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace data {
      20             : 
      21             : namespace detail {
      22             : 
      23             : struct
      24             : one_point_rule_preprocessor
      25             : {
      26          27 :   data::data_expression operator()(const data::data_expression& x) const
      27             :   {
      28          27 :     if (data::sort_bool::is_not_application(x)) // x == !y
      29             :     {
      30          25 :       const data::data_expression& y = unary_operand1(x);
      31          25 :       if (data::sort_bool::is_not_application(y))
      32             :       {
      33           3 :         return (*this)(unary_operand1(y));
      34             :       }
      35          22 :       else if (data::sort_bool::is_and_application(y))
      36             :       {
      37           3 :         std::set<data::data_expression> args = data::split_and(y);
      38           3 :         std::vector<data::data_expression> result;
      39          10 :         for (const data::data_expression& arg: args)
      40             :         {
      41           7 :           result.push_back((*this)(data::sort_bool::not_(arg)));
      42             :         }
      43           3 :         return data::join_or(result.begin(), result.end());
      44           3 :       }
      45          19 :       else if (data::sort_bool::is_or_application(y))
      46             :       {
      47           3 :         std::set<data::data_expression> args = data::split_or(y);
      48           3 :         std::vector<data::data_expression> result;
      49          10 :         for (const data::data_expression& arg: args)
      50             :         {
      51           7 :           result.push_back((*this)(data::sort_bool::not_(arg)));
      52             :         }
      53           3 :         return data::join_and(result.begin(), result.end());
      54           3 :       }
      55          16 :       else if (data::is_equal_to_application(y))
      56             :       {
      57           3 :         return data::not_equal_to(binary_left(atermpp::down_cast<application>(y)), binary_right(atermpp::down_cast<application>(y)));
      58             :       }
      59          13 :       else if (data::is_not_equal_to_application(y))
      60             :       {
      61           5 :         return data::equal_to(binary_left(atermpp::down_cast<application>(y)), binary_right(atermpp::down_cast<application>(y)));
      62             :       }
      63             :     }
      64          10 :     return x;
      65             :   }
      66             : };
      67             : 
      68             : } // namespace detail
      69             : 
      70             : } // namespace data
      71             : 
      72             : } // namespace mcrl2
      73             : 
      74             : #endif // MCRL2_DATA_DETAIL_ONE_POINT_RULE_PREPROCESSOR_H