LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail - test_rewriters.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 52 57 91.2 %
Date: 2020-04-01 00:44:46 Functions: 22 22 100.0 %
Legend: Lines: hit not hit

          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/test_rewriters.h
      10             : /// \brief Functions for testing a rewriter
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_TEST_REWRITERS_H
      13             : #define MCRL2_DATA_DETAIL_TEST_REWRITERS_H
      14             : 
      15             : #include "mcrl2/data/builder.h"
      16             : #include "mcrl2/data/detail/print_utility.h"
      17             : #include "mcrl2/data/join.h"
      18             : #include "mcrl2/data/optimized_boolean_operators.h"
      19             : #include "mcrl2/data/parse.h"
      20             : #include "mcrl2/utilities/detail/test_operation.h"
      21             : 
      22             : namespace mcrl2 {
      23             : 
      24             : namespace data {
      25             : 
      26             : namespace detail {
      27             : 
      28             : // Normalizes conjunctions and disjunctions.
      29             : template <typename Derived>
      30             : struct normalize_and_or_builder: public data_expression_builder<Derived>
      31             : {
      32             :   typedef data_expression_builder<Derived> super;
      33             :   using super::enter;
      34             :   using super::leave;
      35             :   using super::update;
      36             :   using super::apply;
      37             : 
      38             :   /// \brief Splits a disjunction into a sequence of operands
      39             :   /// Given a data expression of the form p1 || p2 || .... || pn, this will yield a
      40             :   /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main
      41             :   /// function symbol.
      42             :   /// \param expr A data expression
      43             :   /// \return A sequence of operands
      44          10 :   std::multiset<data_expression> split_or(const data_expression& expr)
      45             :   {
      46          10 :     std::multiset<data_expression> result;
      47          10 :     utilities::detail::split(expr, std::insert_iterator<std::multiset<data_expression> >(result, result.begin()), sort_bool::is_or_application, data::binary_left1, data::binary_right1);
      48          10 :     return result;
      49             :   }
      50             : 
      51             :   /// \brief Splits a conjunction into a sequence of operands
      52             :   /// Given a data expression of the form p1 && p2 && .... && pn, this will yield a
      53             :   /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main
      54             :   /// function symbol.
      55             :   /// \param expr A data expression
      56             :   /// \return A sequence of operands
      57          12 :   std::multiset<data_expression> split_and(const data_expression& expr)
      58             :   {
      59          12 :     std::multiset<data_expression> result;
      60          12 :     utilities::detail::split(expr, std::insert_iterator<std::multiset<data_expression> >(result, result.begin()), sort_bool::is_and_application, data::binary_left1, data::binary_right1);
      61          12 :     return result;
      62             :   }
      63             : 
      64          66 :   data_expression apply(const application& x)
      65             :   {
      66         132 :     data_expression y = super::apply(x);
      67          66 :     if (sort_bool::is_and_application(y))
      68             :     {
      69          24 :       std::multiset<data_expression> s = split_and(y);
      70          12 :       return data::join_and(s.begin(), s.end());
      71             :     }
      72          54 :     else if (sort_bool::is_or_application(y))
      73             :     {
      74          20 :       std::multiset<data_expression> s = split_or(y);
      75          10 :       return data::join_or(s.begin(), s.end());
      76             :     }
      77          44 :     return y;
      78             :   }
      79             : };
      80             : 
      81             : template <typename T>
      82          28 : T normalize_and_or(const T& x,
      83             :                    typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
      84             :                   )
      85             : {
      86          28 :   return core::make_apply_builder<normalize_and_or_builder>().apply(x);
      87             : }
      88             : 
      89             : template <typename T>
      90             : void normalize_and_or(T& x,
      91             :                       typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
      92             :                      )
      93             : {
      94             :   core::make_apply_builder<normalize_and_or_builder>().update(x);
      95             : }
      96             : 
      97             : // Normalizes equalities.
      98             : template <typename Derived>
      99             : struct normalize_equality_builder: public data_expression_builder<Derived>
     100             : {
     101             :   typedef data_expression_builder<Derived> super;
     102             :   using super::enter;
     103             :   using super::leave;
     104             :   using super::apply;
     105             : 
     106          14 :   data_expression apply(const application& x)
     107             :   {
     108          28 :     data_expression y = super::apply(x);
     109          14 :     if (data::is_equal_to_application(y))
     110             :     {
     111           8 :       const data_expression& left = data::binary_left1(y);
     112           8 :       const data_expression& right = data::binary_right1(y);
     113           8 :       if (left < right)
     114             :       {
     115           4 :         return data::equal_to(left, right);
     116             :       }
     117             :       else
     118             :       {
     119           4 :         return data::equal_to(right, left);
     120             :       }
     121             :     }
     122           6 :     else if (data::is_not_equal_to_application(y))
     123             :     {
     124           0 :       const data_expression& left = data::binary_left1(y);
     125           0 :       const data_expression& right = data::binary_right1(y);
     126           0 :       if (left < right)
     127             :       {
     128           0 :         return data::not_equal_to(left, right);
     129             :       }
     130             :       else
     131             :       {
     132           0 :         return data::not_equal_to(right, left);
     133             :       }
     134             :     }
     135           6 :     return y;
     136             :   }
     137             : };
     138             : 
     139             : template <typename T>
     140           2 : T normalize_equality(const T& x,
     141             :                      typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
     142             :                     )
     143             : {
     144           2 :   return core::make_apply_builder<normalize_equality_builder>().apply(x);
     145             : }
     146             : 
     147             : template <typename T>
     148             : void normalize_equality(T& x,
     149             :                         typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
     150             :                        )
     151             : {
     152             :   core::make_apply_builder<normalize_equality_builder>().update(x);
     153             : }
     154             : 
     155             : // normalize operator
     156             : template <typename Function>
     157             : struct normalizer
     158             : {
     159             :   const Function& f;
     160             : 
     161          26 :   normalizer(const Function& f0)
     162          26 :     : f(f0)
     163          26 :   {}
     164             : 
     165          26 :   data_expression operator()(const data_expression& t) const
     166             :   {
     167          26 :     return detail::normalize_and_or(f(t));
     168             :   }
     169             : };
     170             : 
     171             : // utility function for creating a normalizer
     172             : template <typename Function>
     173          26 : normalizer<Function> N(const Function& f)
     174             : {
     175          26 :   return normalizer<Function>(f);
     176             : }
     177             : 
     178             : inline
     179          13 : std::string VARIABLE_SPECIFICATION()
     180             : {
     181             :   return
     182             :     "  b:  Bool;     \n"
     183             :     "  b1: Bool;     \n"
     184             :     "  b2: Bool;     \n"
     185             :     "  b3: Bool;     \n"
     186             :     "                \n"
     187             :     "  n:  Nat;      \n"
     188             :     "  n1: Nat;      \n"
     189             :     "  n2: Nat;      \n"
     190             :     "  n3: Nat;      \n"
     191             :     "                \n"
     192             :     "  p:  Pos;      \n"
     193             :     "  p1: Pos;      \n"
     194             :     "  p2: Pos;      \n"
     195          13 :     "  p3: Pos;      \n"
     196             :     ;
     197             : }
     198             : 
     199          13 : class parser
     200             : {
     201             :   protected:
     202             :     std::string m_var_decl;
     203             :     std::string m_data_spec;
     204             : 
     205             :   public:
     206             : 
     207          13 :     parser(const std::string& var_decl = VARIABLE_SPECIFICATION(), const std::string& data_spec = "")
     208          13 :       : m_var_decl(var_decl),
     209          13 :         m_data_spec(data_spec)
     210          13 :     {}
     211             : 
     212          26 :     data_expression operator()(const std::string& expr)
     213             :     {
     214          26 :       return parse_data_expression(expr, parse_variables(m_var_decl), parse_data_specification(m_data_spec));
     215             :     }
     216             : };
     217             : 
     218             : template <typename Rewriter1, typename Rewriter2>
     219          13 : void test_rewriters(Rewriter1 R1, Rewriter2 R2, std::string expr1, std::string expr2, const std::string& var_decl = VARIABLE_SPECIFICATION(), const std::string& data_spec = "")
     220             : {
     221          13 :   utilities::detail::test_operation(
     222             :     expr1,
     223             :     expr2,
     224             :     parser(var_decl, data_spec),
     225             :     std::equal_to<data_expression>(),
     226             :     R1,
     227             :     "R1",
     228             :     R2,
     229             :     "R2"
     230             :   );
     231          13 : }
     232             : 
     233             : inline
     234          13 : data_expression I(const data_expression& x)
     235             : {
     236          13 :   return x;
     237             : }
     238             : 
     239             : } // namespace detail
     240             : 
     241             : } // namespace data
     242             : 
     243             : } // namespace mcrl2
     244             : 
     245             : #endif // MCRL2_DATA_DETAIL_TEST_REWRITERS_H
     246             : 

Generated by: LCOV version 1.13