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: 66 77 85.7 %
Date: 2024-03-08 02:52:28 Functions: 21 21 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           0 :   }
      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           0 :   }
      63             : 
      64             :   template<class T>
      65          66 :   void apply(T& result, const application& x)
      66             :   {
      67          66 :     data_expression y;
      68          66 :     super::apply(y, x);
      69          66 :     if (sort_bool::is_and_application(y))
      70             :     {
      71          12 :       std::multiset<data_expression> s = split_and(y);
      72          12 :       result = data::join_and(s.begin(), s.end());
      73          12 :       return;
      74          12 :     }
      75          54 :     else if (sort_bool::is_or_application(y))
      76             :     {
      77          10 :       std::multiset<data_expression> s = split_or(y);
      78          10 :       result = data::join_or(s.begin(), s.end());
      79          10 :       return;
      80          10 :     }
      81          44 :     result = y;
      82          66 :   }
      83             : };
      84             : 
      85             : template <typename T>
      86          28 : T normalize_and_or(const T& x,
      87             :                    typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
      88             :                   )
      89             : {
      90          28 :   T result;
      91          28 :   core::make_apply_builder<normalize_and_or_builder>().apply(result, x);
      92          28 :   return result;
      93           0 : }
      94             : 
      95             : template <typename T>
      96             : void normalize_and_or(T& x,
      97             :                       typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
      98             :                      )
      99             : {
     100             :   core::make_apply_builder<normalize_and_or_builder>().update(x);
     101             : }
     102             : 
     103             : // Normalizes equalities.
     104             : template <typename Derived>
     105             : struct normalize_equality_builder: public data_expression_builder<Derived>
     106             : {
     107             :   typedef data_expression_builder<Derived> super;
     108             :   using super::enter;
     109             :   using super::leave;
     110             :   using super::apply;
     111             : 
     112             :   template<class T>
     113          14 :   void apply(T& result, const application& x)
     114             :   {
     115          14 :     data_expression y;
     116          14 :     super::apply(y, x);
     117          14 :     if (data::is_equal_to_application(y))
     118             :     {
     119           8 :       const data_expression& left = data::binary_left1(y);
     120           8 :       const data_expression& right = data::binary_right1(y);
     121           8 :       if (left < right)
     122             :       {
     123           4 :         result = data::equal_to(left, right);
     124           4 :         return;
     125             :       }
     126             :       else
     127             :       {
     128           4 :         result = data::equal_to(right, left);
     129           4 :         return;
     130             :       }
     131             :     }
     132           6 :     else if (data::is_not_equal_to_application(y))
     133             :     {
     134           0 :       const data_expression& left = data::binary_left1(y);
     135           0 :       const data_expression& right = data::binary_right1(y);
     136           0 :       if (left < right)
     137             :       {
     138           0 :         result = data::not_equal_to(left, right);
     139           0 :         return;
     140             :       }
     141             :       else
     142             :       {
     143           0 :         result = data::not_equal_to(right, left);
     144           0 :         return;
     145             :       }
     146             :     }
     147           6 :     result = y;
     148          14 :   }
     149             : };
     150             : 
     151             : template <typename T>
     152           2 : T normalize_equality(const T& x,
     153             :                      typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
     154             :                     )
     155             : {
     156           2 :   T result;
     157           2 :   core::make_apply_builder<normalize_equality_builder>().apply(result, x);
     158           2 :   return result;
     159           0 : }
     160             : 
     161             : template <typename T>
     162             : void normalize_equality(T& x,
     163             :                         typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
     164             :                        )
     165             : {
     166             :   core::make_apply_builder<normalize_equality_builder>().update(x);
     167             : }
     168             : 
     169             : // normalize operator
     170             : template <typename Function>
     171             : struct normalizer
     172             : {
     173             :   const Function& f;
     174             : 
     175          26 :   normalizer(const Function& f0)
     176          26 :     : f(f0)
     177          26 :   {}
     178             : 
     179          26 :   data_expression operator()(const data_expression& t) const
     180             :   {
     181          26 :     return detail::normalize_and_or(f(t));
     182             :   }
     183             : };
     184             : 
     185             : // utility function for creating a normalizer
     186             : template <typename Function>
     187          26 : normalizer<Function> N(const Function& f)
     188             : {
     189          26 :   return normalizer<Function>(f);
     190             : }
     191             : 
     192             : inline
     193          13 : std::string VARIABLE_SPECIFICATION()
     194             : {
     195             :   return
     196             :     "  b:  Bool;     \n"
     197             :     "  b1: Bool;     \n"
     198             :     "  b2: Bool;     \n"
     199             :     "  b3: Bool;     \n"
     200             :     "                \n"
     201             :     "  n:  Nat;      \n"
     202             :     "  n1: Nat;      \n"
     203             :     "  n2: Nat;      \n"
     204             :     "  n3: Nat;      \n"
     205             :     "                \n"
     206             :     "  p:  Pos;      \n"
     207             :     "  p1: Pos;      \n"
     208             :     "  p2: Pos;      \n"
     209          13 :     "  p3: Pos;      \n"
     210             :     ;
     211             : }
     212             : 
     213             : class parser
     214             : {
     215             :   protected:
     216             :     std::string m_var_decl;
     217             :     std::string m_data_spec;
     218             : 
     219             :   public:
     220             : 
     221          13 :     parser(const std::string& var_decl = VARIABLE_SPECIFICATION(), const std::string& data_spec = "")
     222          13 :       : m_var_decl(var_decl),
     223          13 :         m_data_spec(data_spec)
     224          13 :     {}
     225             : 
     226          26 :     data_expression operator()(const std::string& expr)
     227             :     {
     228          52 :       return parse_data_expression(expr, parse_variables(m_var_decl), parse_data_specification(m_data_spec));
     229             :     }
     230             : };
     231             : 
     232             : template <typename Rewriter1, typename Rewriter2>
     233          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 = "")
     234             : {
     235          39 :   utilities::detail::test_operation(
     236             :     expr1,
     237             :     expr2,
     238          26 :     parser(var_decl, data_spec),
     239             :     std::equal_to<data_expression>(),
     240             :     R1,
     241             :     "R1",
     242             :     R2,
     243             :     "R2"
     244             :   );
     245          13 : }
     246             : 
     247             : inline
     248          13 : data_expression I(const data_expression& x)
     249             : {
     250          13 :   return x;
     251             : }
     252             : 
     253             : } // namespace detail
     254             : 
     255             : } // namespace data
     256             : 
     257             : } // namespace mcrl2
     258             : 
     259             : #endif // MCRL2_DATA_DETAIL_TEST_REWRITERS_H
     260             : 

Generated by: LCOV version 1.14