mCRL2
Loading...
Searching...
No Matches
equality_one_point_substitution.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink, Thomas Neele
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//
10
11
12#ifndef MCRL2_DATA_EQUALITY_ONE_POINT_SUBSTITUTION_H
13#define MCRL2_DATA_EQUALITY_ONE_POINT_SUBSTITUTION_H
14
15
16#include "mcrl2/data/replace.h"
18
19namespace mcrl2::data
20{
21namespace detail
22{
23
25{
26 std::map<data::variable, std::vector<data::data_expression> > equalities;
28 std::set<data::variable> sigma_lhs_variables;
30
31 // applies the substitution sigma to all right hand sides of equalities
33 {
34 for (auto& [_, exprs]: equalities)
35 {
36 for (data::data_expression& e: exprs)
37 {
39 }
40 }
41 }
42
43 // finds all assignments to a constant, and adds them to sigma
44 // returns true if any assignment was found
46 {
47 std::vector<data::variable> to_be_removed;
48 for (const auto& [lhs, exprs]: equalities)
49 {
50 for (const data::data_expression& e: exprs)
51 {
52 if (data::is_constant(e))
53 {
54 sigma[lhs] = e;
55 sigma_lhs_variables.insert(lhs);
56 to_be_removed.push_back(lhs);
57 }
58 }
59 }
60
61 // remove entries for the assignments
62 for (const data::variable& v: to_be_removed)
63 {
64 equalities.erase(v);
65 }
66
67 // apply sigma to the right hand sides
69
70 return !to_be_removed.empty();
71 }
72
73 // finds an arbitrary assignment and adds it to sigma
74 // returns true if any assignment was found
76 {
77 std::set<data::variable> to_be_removed;
78 for (const auto& [lhs,exprs]: equalities)
79 {
80 for (const data::data_expression& e: exprs)
81 {
82 if (e != lhs)
83 {
84 sigma[lhs] = e;
85 sigma_lhs_variables.insert(lhs);
86 std::set<data::variable> FV = data::find_free_variables(e);
87 for (const data::variable& v: FV)
88 {
90 }
91 to_be_removed.insert(lhs);
92 to_be_removed.insert(FV.begin(), FV.end());
93 break;
94 }
95 }
96 if (!to_be_removed.empty())
97 {
98 break;
99 }
100 }
101
102 // remove entries for the assignments
103 for (const data::variable& v: to_be_removed)
104 {
105 equalities.erase(v);
106 }
107
108 // apply sigma to the right hand sides
109 apply_sigma();
110
111 return !to_be_removed.empty();
112 }
113
114 void build_equality_map(const std::map<data::variable, std::set<data::data_expression> >& equalities_, bool check_vars, const data::variable_list& vars = data::variable_list())
115 {
117 for (const auto& [lhs,exprs]: equalities_)
118 {
119 if (check_vars && !contains(vars, lhs))
120 {
121 continue;
122 }
123 std::vector<data::data_expression> E;
124 for (const data::data_expression& e: exprs)
125 {
126 if (!contains(data::find_free_variables(e), lhs))
127 {
128 E.push_back(e);
129 }
130 }
131 if (!E.empty())
132 {
133 equalities[lhs] = E;
134 }
135 }
136 }
137
138 one_point_rule_substitution_algorithm(const std::map<data::variable, std::set<data::data_expression> >& equalities_)
139 {
140 build_equality_map(equalities_, false);
141 }
142
143 one_point_rule_substitution_algorithm(const std::map<data::variable, std::set<data::data_expression> >& equalities_, const data::variable_list& quantifier_variables)
144 {
145 build_equality_map(equalities_, true, quantifier_variables);
146 }
147
148 data::mutable_map_substitution<> run(bool find_all_assignments = true)
149 {
151 while (find_all_assignments)
152 {
153 if (!find_assignment())
154 {
155 break;
156 }
157 }
158 return sigma;
159 }
160
161 // creates a substitution from a set of (in-)equalities for a given list of quantifier variables
162 // returns the substitution, and the subset of quantifier variables that are not used in the substitution
163 std::pair<data::mutable_map_substitution<>, std::vector<data::variable> > run(const data::variable_list& quantifier_variables, bool find_all_assignments = true)
164 {
166
167 run(find_all_assignments);
168
169 std::vector<data::variable> remaining_variables;
170 for (const data::variable& v: quantifier_variables)
171 {
172 if (!contains(sigma_lhs_variables, v))
173 {
174 remaining_variables.push_back(v);
175 }
176 }
177
178 return std::make_pair(sigma, remaining_variables);
179 }
180};
181
182} // namespace detail
183
184
189inline
190std::pair<data::mutable_map_substitution<>, std::vector<data::variable> > make_one_point_rule_substitution(
191 const std::map<data::variable, std::set<data::data_expression> >& equalities,
192 const data::variable_list& quantifier_variables,
193 bool find_all_assignments = true)
194{
195 detail::one_point_rule_substitution_algorithm algorithm(equalities, quantifier_variables);
196 return algorithm.run(quantifier_variables, find_all_assignments);
197}
198
202inline
204 const std::map<data::variable, std::set<data::data_expression> >& equalities,
205 bool find_all_assignments = true)
206{
208 return algorithm.run(find_all_assignments);
209}
210
211} // namespace mcrl2::data
212
213#endif // MCRL2_DATA_EQUALITY_ONE_POINT_SUBSTITUTION_H
Generic substitution function. The substitution is stored as a mapping of variables to expressions....
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 data variable
Definition variable.h:28
add your file description here.
add your file description here.
static void check_vars(const data_expression &expr, const std::set< variable > &vars, std::set< variable > &used_vars)
Definition rewrite.cpp:541
Namespace for all data library functionality.
Definition abstraction.h:22
std::pair< data::mutable_map_substitution<>, std::vector< data::variable > > make_one_point_rule_substitution(const std::map< data::variable, std::set< data::data_expression > > &equalities, const data::variable_list &quantifier_variables, bool find_all_assignments=true)
creates a substitution from a set of (in-)equalities for a given list of quantifier variables
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
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)
bool is_constant(const data_expression &x)
bool contains(const atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable > &c, const typename atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable >::key_type &v, const std::size_t thread_index=0)
Definition indexed_set.h:86
one_point_rule_substitution_algorithm(const std::map< data::variable, std::set< data::data_expression > > &equalities_, const data::variable_list &quantifier_variables)
std::pair< data::mutable_map_substitution<>, std::vector< data::variable > > run(const data::variable_list &quantifier_variables, bool find_all_assignments=true)
one_point_rule_substitution_algorithm(const std::map< data::variable, std::set< data::data_expression > > &equalities_)
data::mutable_map_substitution run(bool find_all_assignments=true)
std::map< data::variable, std::vector< data::data_expression > > equalities
void build_equality_map(const std::map< data::variable, std::set< data::data_expression > > &equalities_, bool check_vars, const data::variable_list &vars=data::variable_list())