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