mCRL2
Loading...
Searching...
No Matches
map_substitution.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_DATA_SUBSTITUTIONS_MAP_SUBSTITUTION_H
13#define MCRL2_DATA_SUBSTITUTIONS_MAP_SUBSTITUTION_H
14
17
18namespace mcrl2 {
19
20namespace data {
21
24template <typename AssociativeContainer>
26{
27 typedef typename AssociativeContainer::key_type variable_type;
28 typedef typename AssociativeContainer::mapped_type expression_type;
31
32 const AssociativeContainer& m_map;
33
34 map_substitution(const AssociativeContainer& m)
35 : m_map(m)
36 { }
37
39 {
40 typename AssociativeContainer::const_iterator i = m_map.find(v);
41 if (i == m_map.end())
42 {
43 return v;
44 }
45 else
46 {
47 return i->second;
48 }
49 // N.B. This does not work!
50 // return i == m_map.end() ? v : i->second;
51 }
52
53 std::string to_string() const
54 {
55 std::ostringstream out;
56 out << "[";
57 for (typename AssociativeContainer::const_iterator i = m_map.begin(); i != m_map.end(); ++i)
58 {
59 out << (i == m_map.begin() ? "" : "; ") << i->first << ":" << i->first.sort() << " := " << i->second;
60 }
61 out << "]";
62 return out.str();
63 }
64};
65
67template <typename AssociativeContainer>
68map_substitution<AssociativeContainer>
69make_map_substitution(const AssociativeContainer& m)
70{
72}
73
74template <typename AssociativeContainer>
76{
77 std::set<data::variable> result;
78 for (const auto& [key, value]: sigma.m_map)
79 {
80 data::find_free_variables(value, std::inserter(result, result.end()));
81 }
82 return result;
83}
84
85template <typename AssociativeContainer>
87{
88 for (auto i = sigma.m_map.begin(); i != sigma.m_map.end(); ++i)
89 {
90 if (!is_simple_substitution(i->first, i->second))
91 {
92 return false;
93 }
94 }
95 return true;
96}
97
98} // namespace data
99
100} // namespace mcrl2
101
102#endif // MCRL2_DATA_SUBSTITUTIONS_MAP_SUBSTITUTION_H
add your file description here.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
std::set< data::variable > substitution_variables(const Substitution &)
Returns the variables appearing in the right hand sides of the substitution.
Definition replace.h:161
map_substitution< AssociativeContainer > make_map_substitution(const AssociativeContainer &m)
Utility function for creating a map_substitution.
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
bool is_simple_substitution(const Substitution &)
Returns true if the substitution sigma satisfies the property that FV(sigma(x)) is included in {x} fo...
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Generic substitution function. The substitution is stored as a mapping of variables to expressions.
const expression_type operator()(const variable_type &v) const
const AssociativeContainer & m_map
map_substitution(const AssociativeContainer &m)
AssociativeContainer::mapped_type expression_type
AssociativeContainer::key_type variable_type
add your file description here.