12#ifndef MCRL2_PROCESS_REPLACE_CAPTURE_AVOIDING_H
13#define MCRL2_PROCESS_REPLACE_CAPTURE_AVOIDING_H
25template<
template<
class>
class Builder,
class Derived,
class Substitution>
29 typedef data::detail::add_capture_avoiding_replacement <Builder, Derived, Substitution>
super;
38 for (
auto i = a.
begin(); i != a.
end(); ++i)
55 static_cast<Derived&
>(*this).enter(x);
57 std::vector <data::assignment> v;
68 v.emplace_back(variable, e);
75 v.emplace_back(k->lhs(), rhs);
79 static_cast<Derived&
>(*this).leave(x);
112template <
typename T,
typename Substitution>
116 typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* =
nullptr
120 data::detail::apply_replace_capture_avoiding_variables_builder<process::data_expression_builder, process::detail::add_capture_avoiding_replacement>(sigma1).update(x);
127template <
typename T,
typename Substitution>
131 typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* =
nullptr
136 data::detail::apply_replace_capture_avoiding_variables_builder<process::data_expression_builder, process::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x);
143template <
typename T,
typename Substitution>
146 typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* =
nullptr
161template <
typename T,
typename Substitution>
164 typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* =
nullptr
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
void add_identifiers(const std::set< core::identifier_string > &ids)
Add a set of identifiers to the context.
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
void add_identifier(const core::identifier_string &s) override
Adds the identifier s to the context.
\brief A process expression
const data::variable_list & variables() const
\brief A process assignment
const data::assignment_list & assignments() const
const process_identifier & identifier() const
\brief The distribution operator
const data::variable_list & variables() const
const data::data_expression & distribution() const
const process_expression & operand() const
const process_expression & operand() const
const data::variable_list & variables() const
add your file description here.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
void find_identifiers(const T &x, OutputIterator o)
void replace_variables_capture_avoiding(T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
void make_stochastic_operator(atermpp::aterm &t, const ARGUMENTS &... args)
void make_process_instance_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
void make_sum(atermpp::aterm &t, const ARGUMENTS &... args)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
add your file description here.
add your file description here.
void apply(atermpp::term_list< T > &result, const assignment_list &x)
capture_avoiding_substitution_updater< Substitution > & sigma
data::detail::add_capture_avoiding_replacement< Builder, Derived, Substitution > super
capture_avoiding_substitution_updater< Substitution > & sigma
void apply(T &result, const process::process_instance_assignment &x)
void apply(T &result, const sum &x)
void apply(T &result, const stochastic_operator &x)
add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater< Substitution > &sigma)
data::assignment_list::const_iterator find_variable(const data::assignment_list &a, const data::variable &v) const