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: 35 46 76.1 %
Date: 2024-03-08 02:52:28 Functions: 11 13 84.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/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           1 :       data::forall y(x);
     109           1 :       return forall(y.variables(), data2pbes(y.body()));
     110           1 :     }
     111           4 :     else if (is_exists(x))
     112             :     {
     113           0 :       data::exists y(x);
     114           0 :       return exists(y.variables(), data2pbes(y.body()));
     115           0 :     }
     116           4 :     return x;
     117             :   }
     118             : 
     119             :   template <class T>
     120           2 :   void apply(T& result, const data::data_expression& x)
     121             :   {
     122           2 :     result = data2pbes(x);
     123           2 :   }
     124             : };
     125             : 
     126             : template <typename T>
     127           2 : T data2pbes(const T& x,
     128             :             typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
     129             :            )
     130             : {
     131           2 :   T result;
     132           2 :   core::make_apply_builder<data2pbes_builder>().apply(result, x);
     133           2 :   return result;
     134           0 : }
     135             : 
     136             : template <typename T>
     137             : void data2pbes(T& x,
     138             :                typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
     139             :               )
     140             : {
     141             :   core::make_apply_builder<data2pbes_builder>().update(x);
     142             : }
     143             : 
     144             : } // namespace detail
     145             : 
     146             : /// \brief A rewriter that applies one point rule quantifier elimination to a PBES.
     147             : class data2pbes_rewriter
     148             : {
     149             :   public:
     150             :     /// \brief The term type
     151             :     typedef pbes_expression term_type;
     152             : 
     153             :     /// \brief The variable type
     154             :     typedef data::variable variable_type;
     155             : 
     156             :     /// \brief Rewrites a pbes expression.
     157             :     /// \param x A term
     158             :     /// \return The rewrite result.
     159           0 :     pbes_expression operator()(const pbes_expression& x) const
     160             :     {
     161           0 :       return detail::data2pbes(x);
     162             :     }
     163             : };
     164             : 
     165             : } // namespace pbes_system
     166             : 
     167             : } // namespace mcrl2
     168             : 
     169             : #endif // MCRL2_PBES_REWRITERS_DATA2PBES_REWRITER_H

Generated by: LCOV version 1.14