LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/rewriters - data2pbes_rewriter.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 31 38 81.6 %
Date: 2019-06-20 00:49:45 Functions: 11 12 91.7 %
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/detail/data2pbes_rewriter.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_REWRITERS_DATA2PBES_REWRITER_H
      13             : #define MCRL2_PBES_REWRITERS_DATA2PBES_REWRITER_H
      14             : 
      15             : #include "mcrl2/data/consistency.h"
      16             : #include "mcrl2/pbes/builder.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : namespace detail {
      23             : 
      24             : // transforms outer level data operators to their pbes equivalents, for the following operators:
      25             : // x && y
      26             : // x || y
      27             : // x => y
      28             : // exists d:D. x
      29             : // forall d:D. x
      30             : template <typename Derived>
      31             : struct data2pbes_builder: public pbes_expression_builder<Derived>
      32             : {
      33             :   typedef pbes_expression_builder<Derived> super;
      34             :   using super::apply;
      35             : 
      36           7 :   bool is_not(const data::data_expression& x) const
      37             :   {
      38           7 :     return data::is_not(x);
      39             :   }
      40             : 
      41           7 :   bool is_and(const data::data_expression& x) const
      42             :   {
      43           7 :     return data::is_and(x);
      44             :   }
      45             : 
      46           5 :   bool is_or(const data::data_expression& x) const
      47             :   {
      48           5 :     return data::is_or(x);
      49             :   }
      50             : 
      51           5 :   bool is_imp(const data::data_expression& x) const
      52             :   {
      53           5 :     return data::is_imp(x);
      54             :   }
      55             : 
      56           5 :   bool is_forall(const data::data_expression& x) const
      57             :   {
      58           5 :     return data::is_forall(x);
      59             :   }
      60             : 
      61           4 :   bool is_exists(const data::data_expression& x) const
      62             :   {
      63           4 :     return data::is_exists(x);
      64             :   }
      65             : 
      66           0 :   data::data_expression operand(const data::data_expression& x) const
      67             :   {
      68           0 :     return data::unary_operand(atermpp::down_cast<data::application>(x));
      69             :   }
      70             : 
      71           2 :   data::data_expression left(const data::data_expression& x) const
      72             :   {
      73           2 :     return data::binary_left(atermpp::down_cast<data::application>(x));
      74             :   }
      75             : 
      76           2 :   data::data_expression right(const data::data_expression& x) const
      77             :   {
      78           2 :     return data::binary_right(atermpp::down_cast<data::application>(x));
      79             :   }
      80             : 
      81             :   // transforms outer level data operators to their pbes equivalents, for the following operators:
      82             :   // !x
      83             :   // x && y
      84             :   // x || y
      85             :   // x => y
      86             :   // exists d:D. x
      87             :   // forall d:D. x
      88           7 :   pbes_expression data2pbes(const data::data_expression& x) const
      89             :   {
      90           7 :     if (is_not(x))
      91             :     {
      92           0 :       return not_(data2pbes(operand(x)));
      93             :     }
      94           7 :     else if (is_and(x))
      95             :     {
      96           2 :       return and_(data2pbes(left(x)), data2pbes(right(x)));
      97             :     }
      98           5 :     else if (is_or(x))
      99             :     {
     100           0 :       return or_(data2pbes(left(x)), data2pbes(right(x)));
     101             :     }
     102           5 :     else if (is_imp(x))
     103             :     {
     104           0 :       return imp(data2pbes(left(x)), data2pbes(right(x)));
     105             :     }
     106           5 :     else if (is_forall(x))
     107             :     {
     108           2 :       data::forall y(x);
     109           1 :       return forall(y.variables(), data2pbes(y.body()));
     110             :     }
     111           4 :     else if (is_exists(x))
     112             :     {
     113           0 :       data::exists y(x);
     114           0 :       return exists(y.variables(), data2pbes(y.body()));
     115             :     }
     116           4 :     return x;
     117             :   }
     118             : 
     119           2 :   pbes_expression apply(const data::data_expression& x)
     120             :   {
     121           2 :     return data2pbes(x);
     122             :   }
     123             : };
     124             : 
     125             : template <typename T>
     126           2 : T data2pbes(const T& x,
     127             :             typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
     128             :            )
     129             : {
     130           2 :   return core::make_apply_builder<data2pbes_builder>().apply(x);
     131             : }
     132             : 
     133             : template <typename T>
     134             : void data2pbes(T& x,
     135             :                typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
     136             :               )
     137             : {
     138             :   core::make_apply_builder<data2pbes_builder>().update(x);
     139             : }
     140             : 
     141             : } // namespace detail
     142             : 
     143             : /// \brief A rewriter that applies one point rule quantifier elimination to a PBES.
     144             : class data2pbes_rewriter
     145             : {
     146             :   public:
     147             :     /// \brief The term type
     148             :     typedef pbes_expression term_type;
     149             : 
     150             :     /// \brief The variable type
     151             :     typedef data::variable variable_type;
     152             : 
     153             :     /// \brief Rewrites a pbes expression.
     154             :     /// \param x A term
     155             :     /// \return The rewrite result.
     156             :     pbes_expression operator()(const pbes_expression& x) const
     157             :     {
     158             :       return detail::data2pbes(x);
     159             :     }
     160             : };
     161             : 
     162             : } // namespace pbes_system
     163             : 
     164             : } // namespace mcrl2
     165             : 
     166             : #endif // MCRL2_PBES_REWRITERS_DATA2PBES_REWRITER_H

Generated by: LCOV version 1.12