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/rewriters/if_rewriter.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PBES_REWRITERS_IF_REWRITER_H 13 : #define MCRL2_PBES_REWRITERS_IF_REWRITER_H 14 : 15 : #include "mcrl2/data/consistency.h" 16 : #include "mcrl2/data/rewriters/if_rewriter.h" 17 : #include "mcrl2/pbes/builder.h" 18 : 19 : namespace mcrl2 { 20 : 21 : namespace pbes_system { 22 : 23 : namespace detail { 24 : 25 : struct if_rewrite_builder: public pbes_system::data_expression_builder<if_rewrite_builder> 26 : { 27 : typedef pbes_system::data_expression_builder<if_rewrite_builder> super; 28 : using super::apply; 29 : using super::update; 30 : 31 : data::if_rewriter r; 32 : 33 : template <class T> 34 0 : void apply(T& result, const data::data_expression& x) 35 : { 36 0 : result = r(x); 37 0 : } 38 : }; 39 : 40 : } // namespace detail 41 : 42 : class if_rewriter 43 : { 44 : public: 45 : /// \brief The term type 46 : typedef pbes_expression term_type; 47 : 48 : /// \brief The variable type 49 : typedef data::variable variable_type; 50 : 51 : /// \brief Rewrites a pbes expression. 52 : /// \param x A term 53 : /// \return The rewrite result. 54 0 : pbes_expression operator()(const pbes_expression& x) const 55 : { 56 : detail::if_rewrite_builder f; 57 0 : pbes_expression result; 58 0 : f.apply(result, x); 59 0 : return result; 60 0 : } 61 : }; 62 : 63 : } // namespace pbes_system 64 : 65 : } // namespace mcrl2 66 : 67 : #endif // MCRL2_PBES_REWRITERS_IF_REWRITER_H