LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/detail - normalize_and_or.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 29 32 90.6 %
Date: 2024-03-08 02:52:28 Functions: 6 6 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/pbes/detail/normalize_and_or.h
      10             : /// \brief Function to normalize 'and' and 'or' sub expressions.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_NORMALIZE_AND_OR_H
      13             : #define MCRL2_PBES_DETAIL_NORMALIZE_AND_OR_H
      14             : 
      15             : #include "mcrl2/pbes/builder.h"
      16             : #include "mcrl2/pbes/join.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace pbes_system
      22             : {
      23             : 
      24             : namespace detail
      25             : {
      26             : 
      27             : // Simplifying PBES rewriter.
      28             : template <typename Derived>
      29             : struct normalize_and_or_builder: public pbes_expression_builder<Derived>
      30             : {
      31             :   typedef pbes_expression_builder<Derived> super;
      32             :   using super::enter;
      33             :   using super::leave;
      34             :   using super::update;
      35             :   using super::apply;
      36             : 
      37             :   /// \brief Splits a disjunction into a sequence of operands
      38             :   /// Given a pbes expression of the form p1 || p2 || .... || pn, this will yield a
      39             :   /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main
      40             :   /// function symbol.
      41             :   /// \param expr A PBES expression
      42             :   /// \return A sequence of operands
      43           6 :   std::multiset<pbes_expression> split_or(const pbes_expression& expr)
      44             :   {
      45             :     using namespace accessors;
      46           6 :     std::multiset<pbes_expression> result;
      47           6 :     utilities::detail::split(expr, std::insert_iterator<std::multiset<pbes_expression> >(result, result.begin()), is_or, left, right);
      48           6 :     return result;
      49           0 :   }
      50             : 
      51             :   /// \brief Splits a conjunction into a sequence of operands
      52             :   /// Given a pbes expression of the form p1 && p2 && .... && pn, this will yield a
      53             :   /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main
      54             :   /// function symbol.
      55             :   /// \param expr A PBES expression
      56             :   /// \return A sequence of operands
      57          24 :   std::multiset<pbes_expression> split_and(const pbes_expression& expr)
      58             :   {
      59             :     using namespace accessors;
      60          24 :     std::multiset<pbes_expression> result;
      61          24 :     utilities::detail::split(expr, std::insert_iterator<std::multiset<pbes_expression> >(result, result.begin()), is_and, left, right);
      62          24 :     return result;
      63           0 :   }
      64             : 
      65         186 :   pbes_expression normalize(const pbes_expression& x)
      66             :   {
      67         186 :     if (is_and(x))
      68             :     {
      69          24 :       std::multiset<pbes_expression> s = split_and(x);
      70          24 :       return join_and(s.begin(), s.end());
      71          24 :     }
      72         162 :     else if (is_or(x))
      73             :     {
      74           6 :       std::multiset<pbes_expression> s = split_or(x);
      75           6 :       return join_or(s.begin(), s.end());
      76           6 :     }
      77         156 :     return x;
      78             :   }
      79             : 
      80             :   // to prevent default operator() being called
      81             :   template <class T>
      82          72 :   void apply(T& result, const data::data_expression& x)
      83             :   {
      84          72 :     result = x;
      85          72 :   }
      86             : 
      87             :   template <class T>
      88         186 :   void apply(T& result, const pbes_expression& x)
      89             :   {
      90         186 :     super::apply(result, x);
      91         186 :     result = normalize(result);
      92         186 :   }
      93             : };
      94             : 
      95             : template <typename T>
      96         120 : T normalize_and_or(const T& x,
      97             :                    typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
      98             :                   )
      99             : {
     100         120 :   T result;
     101         120 :   core::make_apply_builder<normalize_and_or_builder>().apply(result, x);
     102         120 :   return result;
     103           0 : }
     104             : 
     105             : template <typename T>
     106             : void normalize_and_or(T& x,
     107             :                       typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
     108             :                      )
     109             : {
     110             :   core::make_apply_builder<normalize_and_or_builder>().update(x);
     111             : }
     112             : 
     113             : } // namespace detail
     114             : 
     115             : } // namespace pbes_system
     116             : 
     117             : } // namespace mcrl2
     118             : 
     119             : #endif // MCRL2_PBES_DETAIL_NORMALIZE_AND_OR_H

Generated by: LCOV version 1.14