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/lps/replace_constants_by_variables.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_LPS_REPLACE_CONSTANTS_BY_VARIABLES_H 13 : #define MCRL2_LPS_REPLACE_CONSTANTS_BY_VARIABLES_H 14 : 15 : #include "mcrl2/data/replace_constants_by_variables.h" 16 : #include "mcrl2/lps/builder.h" 17 : 18 : namespace mcrl2 { 19 : 20 : namespace lps { 21 : 22 : namespace detail { 23 : 24 : struct replace_constants_by_variables_builder: public data::detail::replace_constants_by_variables_builder<lps::data_expression_builder> 25 : { 26 : typedef data::detail::replace_constants_by_variables_builder<lps::data_expression_builder> super; 27 : using super::apply; 28 : using super::update; 29 : 30 0 : replace_constants_by_variables_builder(const data::rewriter& r, data::mutable_indexed_substitution<>& sigma) 31 0 : : super(r, sigma) 32 0 : {} 33 : }; 34 : 35 : } // namespace detail 36 : 37 : /// \brief Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma 38 : /// with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter 39 : /// multiple times. 40 : template <typename T> 41 0 : void replace_constants_by_variables(T& x, 42 : const data::rewriter& r, 43 : data::mutable_indexed_substitution<>& sigma, 44 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr 45 : ) 46 : { 47 0 : detail::replace_constants_by_variables_builder f(r, sigma); 48 0 : f.update(x); 49 0 : } 50 : 51 : /// \brief Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma 52 : /// with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter 53 : /// multiple times. 54 : template <typename T> 55 : T replace_constants_by_variables(const T& x, 56 : const data::rewriter& r, 57 : data::mutable_indexed_substitution<>& sigma, 58 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr 59 : ) 60 : { 61 : T result; 62 : detail::replace_constants_by_variables_builder f(r, sigma); 63 : f.apply(result, x); 64 : return result; 65 : } 66 : 67 : } // namespace lps 68 : 69 : } // namespace mcrl2 70 : 71 : #endif // MCRL2_LPS_REPLACE_CONSTANTS_BY_VARIABLES_H