LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/rewriters - simplify_rewriter.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 40 40 100.0 %
Date: 2019-06-26 00:32:26 Functions: 49 73 67.1 %
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/pbes/rewriters/simplify_rewriter.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_REWRITERS_SIMPLIFY_REWRITER_H
      13             : #define MCRL2_PBES_REWRITERS_SIMPLIFY_REWRITER_H
      14             : 
      15             : #include "mcrl2/data/optimized_boolean_operators.h"
      16             : #include "mcrl2/pbes/rewriters/data_rewriter.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : namespace detail {
      23             : 
      24             : template <template <class> class Builder, class Derived>
      25        6601 : struct add_simplify: public Builder<Derived>
      26             : {
      27             :   typedef Builder<Derived> super;
      28             :   using super::apply;
      29             : 
      30          47 :   pbes_expression apply(const not_& x)
      31             :   {
      32          47 :     return data::optimized_not(apply(x.operand()));
      33             :   }
      34             : 
      35       27685 :   pbes_expression apply(const and_& x)
      36             :   {
      37       55370 :     auto left = apply(x.left());
      38       27685 :     if (is_false(left))
      39             :     {
      40        3280 :       return false_();
      41             :     }
      42       48810 :     auto right = apply(x.right());
      43       24405 :     return data::optimized_and(left, right);
      44             :   }
      45             : 
      46       27223 :   pbes_expression apply(const or_& x)
      47             :   {
      48       54446 :     auto left = apply(x.left());
      49       27223 :     if (is_true(left))
      50             :     {
      51       17312 :       return true_();
      52             :     }
      53       19822 :     auto right = apply(x.right());
      54        9911 :     return data::optimized_or(left, right);
      55             :   }
      56             : 
      57          14 :   pbes_expression apply(const imp& x)
      58             :   {
      59          28 :     auto left = apply(x.left());
      60          14 :     if (is_false(left))
      61             :     {
      62           5 :       return true_();
      63             :     }
      64          18 :     auto right = apply(x.right());
      65           9 :     return data::optimized_imp(left, right);
      66             :   }
      67             : 
      68          34 :   pbes_expression apply(const forall& x)
      69             :   {
      70          68 :     auto body = apply(x.body());
      71          68 :     return data::optimized_forall(x.variables(), body, true);
      72             :   }
      73             : 
      74          30 :   pbes_expression apply(const exists& x)
      75             :   {
      76          60 :     auto body = apply(x.body());
      77          60 :     return data::optimized_exists(x.variables(), body, true);
      78             :   }
      79             : };
      80             : 
      81             : template <typename Derived>
      82        6601 : struct simplify_builder: public add_simplify<pbes_system::pbes_expression_builder, Derived>
      83             : { };
      84             : 
      85             : template <typename Derived, typename DataRewriter, typename SubstitutionFunction>
      86             : struct simplify_data_rewriter_builder : public add_data_rewriter < pbes_system::detail::simplify_builder, Derived, DataRewriter, SubstitutionFunction >
      87             : {
      88             :   typedef add_data_rewriter < pbes_system::detail::simplify_builder, Derived, DataRewriter, SubstitutionFunction > super;
      89        5974 :   simplify_data_rewriter_builder(const DataRewriter& R, SubstitutionFunction& sigma)
      90        5974 :     : super(R, sigma)
      91        5974 :   {}
      92             : };
      93             : 
      94             : } // namespace detail
      95             : 
      96             : /// \brief A rewriter that simplifies boolean expressions in a term.
      97             : struct simplify_rewriter
      98             : {
      99             :   typedef pbes_expression term_type;
     100             :   typedef data::variable variable_type;
     101             : 
     102           2 :   pbes_expression operator()(const pbes_expression& x) const
     103             :   {
     104           2 :     return core::make_apply_builder<detail::simplify_builder>().apply(x);
     105             :   }
     106             : };
     107             : 
     108             : /// \brief A rewriter that simplifies boolean expressions in a term, and rewrites data expressions.
     109             : template <typename DataRewriter>
     110             : struct simplify_data_rewriter
     111             : {
     112             :   typedef pbes_expression term_type;
     113             :   typedef data::variable variable_type;
     114             : 
     115             :   const DataRewriter& R;
     116             : 
     117         224 :   explicit simplify_data_rewriter(const DataRewriter& R_)
     118         224 :     : R(R_)
     119         224 :   {}
     120             : 
     121         116 :   pbes_expression operator()(const pbes_expression& x) const
     122             :   {
     123             :     data::no_substitution sigma;
     124         116 :     return detail::make_apply_rewriter_builder<pbes_system::detail::simplify_data_rewriter_builder>(R, sigma).apply(x);
     125             :   }
     126             : 
     127             :   template <typename SubstitutionFunction>
     128          90 :   pbes_expression operator()(const pbes_expression& x, SubstitutionFunction& sigma) const
     129             :   {
     130          90 :     return detail::make_apply_rewriter_builder<pbes_system::detail::simplify_data_rewriter_builder>(R, sigma).apply(x);
     131             :   }
     132             : };
     133             : 
     134             : } // namespace pbes_system
     135             : 
     136             : } // namespace mcrl2
     137             : 
     138             : #endif // MCRL2_PBES_REWRITERS_SIMPLIFY_REWRITER_H

Generated by: LCOV version 1.12