LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/rewriters - simplify_rewriter.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 38 44 86.4 %
Date: 2020-02-28 00:44:21 Functions: 10 10 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/rewriters/simplify_rewriter.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_REWRITERS_SIMPLIFY_REWRITER_H
      13             : #define MCRL2_DATA_REWRITERS_SIMPLIFY_REWRITER_H
      14             : 
      15             : #include "mcrl2/data/builder.h"
      16             : #include "mcrl2/data/expression_traits.h"
      17             : #include "mcrl2/data/optimized_boolean_operators.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace data {
      22             : 
      23             : namespace detail {
      24             : 
      25             : template <typename Derived>
      26             : class simplify_rewrite_builder: public data_expression_builder<Derived>
      27             : {
      28             :   public:
      29             :     typedef data_expression_builder<Derived> super;
      30             : 
      31             :     using super::apply;
      32             : 
      33         667 :     Derived& derived()
      34             :     {
      35         667 :       return static_cast<Derived&>(*this);
      36             :     }
      37             : 
      38         326 :     bool is_not(const data_expression& x) const
      39             :     {
      40         326 :       return data::sort_bool::is_not_application(x);
      41             :     }
      42             : 
      43         323 :     bool is_and(const data_expression& x) const
      44             :     {
      45         323 :       return data::sort_bool::is_and_application(x);
      46             :     }
      47             : 
      48         318 :     bool is_or(const data_expression& x) const
      49             :     {
      50         318 :       return data::sort_bool::is_or_application(x);
      51             :     }
      52             : 
      53         318 :     bool is_imp(const data_expression& x) const
      54             :     {
      55         318 :       return data::sort_bool::is_implies_application(x);
      56             :     }
      57             : 
      58             :     bool is_forall(const data_expression& x) const
      59             :     {
      60             :       return data::is_forall(x);
      61             :     }
      62             : 
      63             :     bool is_exists(const data_expression& x) const
      64             :     {
      65             :       return data::is_exists(x);
      66             :     }
      67             : 
      68         326 :     data_expression apply(const application& x)
      69             :     {
      70         326 :       data_expression result;
      71         326 :       derived().enter(x);
      72         326 :       if (is_not(x)) // x = !y
      73             :       {
      74           6 :         data_expression y = derived().apply(*x.begin());
      75           3 :         result = data::optimized_not(y);
      76             :       }
      77         323 :       else if (is_and(x)) // x = y && z
      78             :       {
      79          10 :         data_expression y = derived().apply(binary_left(x));
      80          10 :         data_expression z = derived().apply(binary_right(x));
      81           5 :         result = data::optimized_and(y, z);
      82             :       }
      83         318 :       else if (is_or(x)) // x = y || z
      84             :       {
      85           0 :         data_expression y = derived().apply(binary_left(x));
      86           0 :         data_expression z = derived().apply(binary_right(x));
      87           0 :         result = data::optimized_or(y, z);
      88             :       }
      89         318 :       else if (is_imp(x)) // x = y => z
      90             :       {
      91           0 :         data_expression y = derived().apply(binary_left(x));
      92           0 :         data_expression z = derived().apply(binary_right(x));
      93           0 :         result = data::optimized_imp(y, z);
      94             :       }
      95             :       else
      96             :       {
      97         318 :         result = super::apply(x);
      98             :       }
      99         326 :       derived().leave(x);
     100         326 :       return result;
     101             :     }
     102             : 
     103           1 :     data_expression apply(const forall& x) // x = forall d. y
     104             :     {
     105           2 :       variable_list d = forall(x).variables();
     106           2 :       data_expression y = derived().apply(forall(x).body());
     107           2 :       return data::optimized_forall(d, y, true);
     108             :     }
     109             : 
     110           1 :     data_expression apply(const exists& x) // x = exists d. y
     111             :     {
     112           2 :       variable_list d = exists(x).variables();
     113           2 :       data_expression y = derived().apply(exists(x).body());
     114           2 :       return data::optimized_exists(d, y, true);
     115             :     }
     116             : };
     117             : 
     118             : } // namespace detail
     119             : 
     120             : struct simplify_rewriter
     121             : {
     122             :   using argument_type = data_expression;
     123             : 
     124         221 :   data_expression operator()(const data_expression& x) const
     125             :   {
     126         221 :     return core::make_apply_builder<detail::simplify_rewrite_builder>().apply(x);
     127             :   }
     128             : };
     129             : 
     130             : template <typename T>
     131             : void simplify(T& x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0)
     132             : {
     133             :   core::make_update_apply_builder<data::data_expression_builder>(simplify_rewriter()).update(x);
     134             : }
     135             : 
     136             : template <typename T>
     137         109 : T simplify(const T& x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr)
     138             : {
     139         109 :   T result = core::make_update_apply_builder<data::data_expression_builder>(simplify_rewriter()).apply(x);
     140         109 :   return result;
     141             : }
     142             : 
     143             : } // namespace data
     144             : 
     145             : } // namespace mcrl2
     146             : 
     147             : #endif // MCRL2_DATA_REWRITERS_SIMPLIFY_REWRITER_H
     148             : 

Generated by: LCOV version 1.13