Line data    Source code

       1             : // Author(s): Jeroen Keiren
       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/data/join.h
      10             : /// \brief Join and split functions for data expressions.
      11             : 
      12             : #ifndef MCRL2_DATA_JOIN_H
      13             : #define MCRL2_DATA_JOIN_H
      14             : 
      15             : #include "mcrl2/data/expression_traits.h"
      16             : #include "mcrl2/utilities/detail/join.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace data
      22             : {
      23             : 
      24             :   /// \brief Returns or applied to the sequence of data expressions [first, last)
      25             :   /// \param first Start of a sequence of data expressions
      26             :   /// \param last End of a sequence of of data expressions
      27             :   /// \return Or applied to the sequence of data expressions [first, last)
      28             :   template <typename FwdIt>
      29          13 :   data_expression join_or(FwdIt first, FwdIt last)
      30             :   {
      31             :     typedef core::term_traits<data::data_expression> tr;
      32          13 :     return utilities::detail::join(first, last, tr::or_, tr::false_());
      33             :   }
      34             : 
      35             :   /// \brief Returns and applied to the sequence of data expressions [first, last)
      36             :   /// \param first Start of a sequence of data expressions
      37             :   /// \param last End of a sequence of of data expressions
      38             :   /// \return And applied to the sequence of data expressions [first, last)
      39             :   template <typename FwdIt>
      40          15 :   data_expression join_and(FwdIt first, FwdIt last)
      41             :   {
      42             :     typedef core::term_traits<data::data_expression> tr;
      43          15 :     return utilities::detail::join(first, last, tr::and_, tr::true_());
      44             :   }
      45             : 
      46             :   /// \brief Splits a disjunction into a sequence of operands
      47             :   /// Given a data expression of the form p1 || p2 || .... || pn, this will yield a
      48             :   /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main
      49             :   /// function symbol.
      50             :   /// \param expr A data expression
      51             :   /// \return A sequence of operands
      52             :   inline
      53           3 :   std::set<data_expression> split_or(const data_expression& expr)
      54             :   {
      55             :     typedef core::term_traits<data::data_expression> tr;
      56           3 :     std::set<data_expression> result;
      57           3 :     utilities::detail::split(expr, std::insert_iterator<std::set<data_expression> >(result, result.begin()), tr::is_or, tr::left, tr::right);
      58           3 :     return result;
      59           0 :   }
      60             : 
      61             :   /// \brief Splits a conjunction into a sequence of operands
      62             :   /// Given a data expression of the form p1 && p2 && .... && pn, this will yield a
      63             :   /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main
      64             :   /// function symbol.
      65             :   /// \param expr A data expression
      66             :   /// \return A sequence of operands
      67             :   inline
      68          32 :   std::set<data_expression> split_and(const data_expression& expr)
      69             :   {
      70             :     typedef core::term_traits<data::data_expression> tr;
      71          32 :     std::set<data_expression> result;
      72          32 :     utilities::detail::split(expr, std::insert_iterator<std::set<data_expression> >(result, result.begin()), tr::is_and, tr::left, tr::right);
      73          32 :     return result;
      74           0 :   }
      75             : 
      76             : } // namespace data
      77             : 
      78             : } // namespace mcrl2
      79             : 
      80             : #endif // MCRL2_DATA_JOIN_H