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: 38 38 100.0 %
Date: 2020-01-19 00:33:35 Functions: 34 57 59.6 %
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/pbes/rewriters/data_rewriter.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace pbes_system {
      20             : 
      21             : namespace detail {
      22             : 
      23             : template <template <class> class Builder, class Derived>
      24             : struct add_simplify: public Builder<Derived>
      25             : {
      26             :   typedef Builder<Derived> super;
      27             :   using super::apply;
      28             : 
      29          10 :   pbes_expression apply(const not_& x)
      30             :   {
      31          10 :     return data::optimized_not(apply(x.operand()));
      32             :   }
      33             : 
      34       27641 :   pbes_expression apply(const and_& x)
      35             :   {
      36       55282 :     auto left = apply(x.left());
      37       27641 :     if (is_false(left))
      38             :     {
      39        3276 :       return false_();
      40             :     }
      41       48730 :     auto right = apply(x.right());
      42       24365 :     return data::optimized_and(left, right);
      43             :   }
      44             : 
      45       27217 :   pbes_expression apply(const or_& x)
      46             :   {
      47       54434 :     auto left = apply(x.left());
      48       27217 :     if (is_true(left))
      49             :     {
      50       17312 :       return true_();
      51             :     }
      52       19810 :     auto right = apply(x.right());
      53        9905 :     return data::optimized_or(left, right);
      54             :   }
      55             : 
      56          14 :   pbes_expression apply(const imp& x)
      57             :   {
      58          28 :     auto left = apply(x.left());
      59          14 :     if (is_false(left))
      60             :     {
      61           5 :       return true_();
      62             :     }
      63          18 :     auto right = apply(x.right());
      64           9 :     return data::optimized_imp(left, right);
      65             :   }
      66             : 
      67          24 :   pbes_expression apply(const forall& x)
      68             :   {
      69          48 :     auto body = apply(x.body());
      70          48 :     return data::optimized_forall(x.variables(), body, true);
      71             :   }
      72             : 
      73          20 :   pbes_expression apply(const exists& x)
      74             :   {
      75          40 :     auto body = apply(x.body());
      76          40 :     return data::optimized_exists(x.variables(), body, true);
      77             :   }
      78             : };
      79             : 
      80             : template <typename Derived>
      81             : struct simplify_builder: public add_simplify<pbes_system::pbes_expression_builder, Derived>
      82             : { };
      83             : 
      84             : template <typename Derived, typename DataRewriter, typename SubstitutionFunction>
      85             : struct simplify_data_rewriter_builder : public add_data_rewriter < pbes_system::detail::simplify_builder, Derived, DataRewriter, SubstitutionFunction >
      86             : {
      87             :   typedef add_data_rewriter < pbes_system::detail::simplify_builder, Derived, DataRewriter, SubstitutionFunction > super;
      88        5975 :   simplify_data_rewriter_builder(const DataRewriter& R, SubstitutionFunction& sigma)
      89        5975 :     : super(R, sigma)
      90        5975 :   {}
      91             : };
      92             : 
      93             : } // namespace detail
      94             : 
      95             : /// \brief A rewriter that simplifies boolean expressions in a term.
      96             : struct simplify_rewriter
      97             : {
      98             :   typedef pbes_expression term_type;
      99             :   typedef data::variable variable_type;
     100             : 
     101           2 :   pbes_expression operator()(const pbes_expression& x) const
     102             :   {
     103           2 :     return core::make_apply_builder<detail::simplify_builder>().apply(x);
     104             :   }
     105             : };
     106             : 
     107             : /// \brief A rewriter that simplifies boolean expressions in a term, and rewrites data expressions.
     108             : template <typename DataRewriter>
     109             : struct simplify_data_rewriter
     110             : {
     111             :   typedef pbes_expression term_type;
     112             :   typedef data::variable variable_type;
     113             : 
     114             :   const DataRewriter& R;
     115             : 
     116         225 :   explicit simplify_data_rewriter(const DataRewriter& R_)
     117         225 :     : R(R_)
     118         225 :   {}
     119             : 
     120         116 :   pbes_expression operator()(const pbes_expression& x) const
     121             :   {
     122             :     data::no_substitution sigma;
     123         116 :     return detail::make_apply_rewriter_builder<pbes_system::detail::simplify_data_rewriter_builder>(R, sigma).apply(x);
     124             :   }
     125             : 
     126             :   template <typename SubstitutionFunction>
     127          91 :   pbes_expression operator()(const pbes_expression& x, SubstitutionFunction& sigma) const
     128             :   {
     129          91 :     return detail::make_apply_rewriter_builder<pbes_system::detail::simplify_data_rewriter_builder>(R, sigma).apply(x);
     130             :   }
     131             : };
     132             : 
     133             : } // namespace pbes_system
     134             : 
     135             : } // namespace mcrl2
     136             : 
     137             : #endif // MCRL2_PBES_REWRITERS_SIMPLIFY_REWRITER_H

Generated by: LCOV version 1.13