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/stategraph_split.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_STATEGRAPH_SPLIT_H
      13             : #define MCRL2_PBES_DETAIL_STATEGRAPH_SPLIT_H
      14             : 
      15             : #include "mcrl2/pbes/pbes_expression.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace pbes_system {
      20             : 
      21             : namespace detail {
      22             : 
      23             : /// \brief The namespace for access functions that operate on both pbes and data expressions
      24             : namespace combined_access
      25             : {
      26             : 
      27             : /// \brief Test for a conjunction
      28             : /// \param t A PBES expression
      29             : /// \return True if it is a conjunction
      30         114 : inline bool is_and(const pbes_expression& t)
      31             : {
      32         114 :   return is_pbes_and(t) || data::sort_bool::is_and_application(t);
      33             : }
      34             : 
      35             : /// \brief Test for a disjunction
      36             : /// \param t A PBES expression
      37             : /// \return True if it is a disjunction
      38           0 : inline bool is_or(const pbes_expression& t)
      39             : {
      40           0 :   return is_pbes_or(t) || data::sort_bool::is_or_application(t);
      41             : }
      42             : 
      43             : /// \brief Returns the left hand side of an expression of type and, or or imp.
      44             : /// \param t A PBES expression or a data expression
      45             : /// \return The left hand side of an expression of type and, or or imp.
      46             : inline
      47           3 : pbes_expression left(const pbes_expression& t)
      48             : {
      49           3 :   return accessors::data_left(t);
      50             : }
      51             : 
      52             : /// \brief Returns the left hand side of an expression of type and, or or imp.
      53             : /// \param t A PBES expression or a data expression
      54             : /// \return The left hand side of an expression of type and, or or imp.
      55             : inline
      56           3 : pbes_expression right(const pbes_expression& t)
      57             : {
      58           3 :   return accessors::data_right(t);
      59             : }
      60             : 
      61             : } // namespace combined_access
      62             : 
      63             : inline
      64         108 : void stategraph_split_and(const pbes_expression& expr, std::vector<pbes_expression>& result)
      65             : {
      66             :   namespace a = combined_access;
      67         108 :   utilities::detail::split(expr, std::back_inserter(result), a::is_and, a::left, a::right);
      68         108 : }
      69             : 
      70             : inline
      71           0 : void stategraph_split_or(const pbes_expression& expr, std::vector<pbes_expression>& result)
      72             : {
      73             :   namespace a = combined_access;
      74           0 :   utilities::detail::split(expr, std::back_inserter(result), a::is_or, a::left, a::right);
      75           0 : }
      76             : 
      77             : } // namespace detail
      78             : 
      79             : } // namespace pbes_system
      80             : 
      81             : } // namespace mcrl2
      82             : 
      83             : #endif // MCRL2_PBES_DETAIL_STATEGRAPH_SPLIT_H