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