Line data Source code
1 : // Author(s): 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 : //
9 : /// \file mcrl2/pbes/quantifier_propagate.h
10 :
11 : #ifndef MCRL2_PBES_QUANTIFIER_PROPAGATE_H
12 : #define MCRL2_PBES_QUANTIFIER_PROPAGATE_H
13 :
14 : #include "mcrl2/data/rewriter.h"
15 : #include "mcrl2/pbes/replace.h"
16 :
17 : #include <queue>
18 :
19 : namespace mcrl2 {
20 :
21 : namespace pbes_system {
22 :
23 : namespace detail {
24 :
25 : pbes_expression quantifier_propagate(const pbes_expression& x);
26 :
27 : inline
28 2 : pbes_expression make_exists_(std::set<data::variable> vars, const pbes_expression& expr)
29 : {
30 4 : return vars.empty() ? expr : exists(data::variable_list(vars.begin(), vars.end()), expr);
31 : }
32 :
33 : inline
34 4 : pbes_expression make_forall_(std::set<data::variable> vars, const pbes_expression& expr)
35 : {
36 8 : return vars.empty() ? expr : forall(data::variable_list(vars.begin(), vars.end()), expr);
37 : }
38 :
39 : inline
40 10 : pbes_expression make_quantifier(bool is_forall, const data::variable_list& vars, const pbes_expression& body)
41 : {
42 20 : return is_forall ? pbes_expression(forall(vars, body)) : pbes_expression(exists(vars, body));
43 : }
44 :
45 : class quantifier
46 : {
47 : protected:
48 : bool m_is_forall;
49 : std::set<data::variable> m_vars;
50 :
51 6 : pbes_expression make_expr(const std::set<data::variable>& vars, const pbes_expression& expr) const
52 : {
53 6 : return m_is_forall ? make_forall_(vars, expr) : make_exists_(vars, expr);
54 : }
55 :
56 : public:
57 4 : quantifier(bool is_forall, const data::variable_list& vars)
58 4 : : m_is_forall(is_forall)
59 4 : , m_vars(vars.begin(), vars.end())
60 4 : {}
61 :
62 0 : void add_variables(const data::variable_list& vars)
63 : {
64 0 : m_vars.insert(vars.begin(), vars.end());
65 0 : }
66 :
67 1 : bool is_forall() const
68 : {
69 1 : return m_is_forall;
70 : }
71 :
72 15 : const std::set<data::variable>& variables() const
73 : {
74 15 : return m_vars;
75 : }
76 :
77 : bool operator==(const quantifier& other) const
78 : {
79 : return m_is_forall == other.m_is_forall && m_vars == other.m_vars;
80 : }
81 :
82 : bool operator<(const quantifier& other) const
83 : {
84 : return m_is_forall < other.m_is_forall || (m_is_forall == other.m_is_forall && m_vars < other.m_vars);
85 : }
86 :
87 3 : pbes_expression make_expr_include_only(const std::set<data::variable>& include, const pbes_expression& expr) const
88 : {
89 6 : return make_expr(utilities::detail::set_intersection(m_vars, include), expr);
90 : }
91 :
92 3 : pbes_expression make_expr_exclude(const std::set<data::variable>& exclude, const pbes_expression& expr) const
93 : {
94 6 : return make_expr(utilities::detail::set_difference(m_vars, exclude), expr);
95 : }
96 :
97 : std::string to_string() const
98 : {
99 : std::ostringstream out;
100 : out << (is_forall() ? "forall " : "exists ") << core::detail::print_list(variables()) << ". ";
101 : return out.str();
102 : }
103 : };
104 :
105 : struct quantifier_propagate_builder: public pbes_expression_builder<quantifier_propagate_builder>
106 : {
107 : public:
108 : typedef pbes_expression_builder<quantifier_propagate_builder> super;
109 : typedef std::map<core::identifier_string, pbes_equation> equation_map_t;
110 : using super::apply;
111 : using super::enter;
112 :
113 : private:
114 : std::list<std::pair<core::identifier_string, pbes_equation>>& m_new_equations;
115 : const equation_map_t& m_eqn_map;
116 : data::set_identifier_generator& id_gen;
117 :
118 : std::list<pbes_expression> quantified_context;
119 :
120 7 : std::list<quantifier> make_quantifier_list(const std::list<pbes_expression>& ctx) const
121 : {
122 : // Create list of quantified variables around X_e
123 7 : std::list<quantifier> result;
124 11 : for(const pbes_expression& pe: ctx)
125 : {
126 4 : assert(is_forall(pe) || is_exists(pe));
127 :
128 4 : data::variable_list vars(is_forall(pe) ? atermpp::down_cast<forall>(pe).variables() : atermpp::down_cast<exists>(pe).variables());
129 :
130 4 : if(result.empty() || result.back().is_forall() != is_forall(pe))
131 : {
132 4 : result.emplace_back(is_forall(pe), vars);
133 : }
134 : else
135 : {
136 0 : result.back().add_variables(vars);
137 : }
138 4 : }
139 7 : return result;
140 0 : }
141 :
142 10 : pbes_equation find_equation(const propositional_variable_instantiation& X_e)
143 : {
144 10 : return m_eqn_map.at(X_e.name());
145 : }
146 :
147 : public:
148 8 : quantifier_propagate_builder(std::list<std::pair<core::identifier_string, pbes_equation>>& new_eqns,
149 : data::set_identifier_generator& ig,
150 : const equation_map_t& eq_idx)
151 8 : : m_new_equations(new_eqns)
152 8 : , m_eqn_map(eq_idx)
153 8 : , id_gen(ig)
154 8 : {}
155 :
156 7 : pbes_expression apply_quantifier(bool is_forall, const data::variable_list& vars, const pbes_expression& body)
157 : {
158 7 : pbes_expression x = make_quantifier(is_forall, vars, body);
159 7 : quantified_context.push_back(x);
160 :
161 7 : pbes_expression result;
162 7 : apply(result, body);
163 :
164 7 : if(quantified_context.empty())
165 : {
166 : // The body contained some other operator and the stack was cleared
167 : // Reconstruct the quantifier
168 3 : return make_quantifier(is_forall, vars, result);
169 : }
170 : else
171 : {
172 : // The body contained a QPVI
173 4 : quantified_context.pop_back();
174 4 : if(result == body)
175 : {
176 : // The body didn't change, we just return ourselves as well
177 1 : return x;
178 : }
179 : else
180 : {
181 : // The body changed, it reconstructed the QPVI, we should not
182 : // add anything
183 3 : return result;
184 : }
185 : }
186 7 : }
187 :
188 : template <class T>
189 6 : void apply(T& result, const forall& x)
190 : {
191 6 : result = apply_quantifier(true, x.variables(), x.body());
192 6 : }
193 :
194 : template <class T>
195 1 : void apply(T& result, const exists& x)
196 : {
197 1 : result = apply_quantifier(false, x.variables(), x.body());
198 1 : }
199 :
200 0 : void enter(const and_& /*x*/)
201 : {
202 0 : quantified_context.clear();
203 0 : }
204 :
205 6 : void enter(const or_& /*x*/)
206 : {
207 6 : quantified_context.clear();
208 6 : }
209 :
210 0 : void enter(const imp& /*x*/)
211 : {
212 0 : quantified_context.clear();
213 0 : }
214 :
215 0 : void enter(const not_& /*x*/)
216 : {
217 0 : quantified_context.clear();
218 0 : }
219 :
220 : template <class T>
221 7 : void apply(T& result, const propositional_variable_instantiation& X_e)
222 : {
223 : using utilities::detail::contains;
224 : using utilities::detail::set_difference;
225 : using utilities::detail::set_includes;
226 : using utilities::detail::set_intersection;
227 :
228 7 : std::list<quantifier> qvars = make_quantifier_list(quantified_context);
229 7 : if(qvars.empty())
230 : {
231 4 : result = X_e;
232 4 : return;
233 : }
234 :
235 3 : const std::vector<data::variable> parameters(find_equation(X_e).variable().parameters().begin(), find_equation(X_e).variable().parameters().end());
236 3 : const std::vector<data::data_expression> updates(X_e.parameters().begin(), X_e.parameters().end());
237 :
238 3 : std::list<std::size_t> independent_pars;
239 3 : std::set<data::variable> quantified_variables;
240 7 : for(const quantifier& qv: qvars)
241 : {
242 4 : quantified_variables.insert(qv.variables().begin(), qv.variables().end());
243 : }
244 :
245 : // Start building a list of parameters that are constant and can be pushed through X_e
246 3 : std::set<data::variable> seen;
247 3 : std::size_t i = 0;
248 9 : for(const data::data_expression& up: updates)
249 : {
250 6 : std::set<data::variable> fv = find_free_variables(up);
251 6 : if(set_includes(quantified_variables, fv))
252 : {
253 2 : independent_pars.push_back(i);
254 : }
255 : else
256 : {
257 4 : seen.insert(fv.begin(), fv.end());
258 : }
259 6 : i++;
260 : }
261 6 : std::queue<data::variable> todo(std::deque<data::variable>(seen.begin(), seen.end()));
262 :
263 : // Add all transitive dependencies, either because they occur together in one
264 : // of the updates, or because of their quantifier scopes
265 11 : while(!todo.empty())
266 : {
267 4 : data::variable elem = todo.front();
268 4 : todo.pop();
269 :
270 : // Check for each update if it contains elem. If so, elem also influences the
271 : // other free variables in that update expression an the parameter is not independent.
272 8 : for(std::list<std::size_t>::const_iterator ip = independent_pars.begin(); ip != independent_pars.end(); )
273 : {
274 2 : std::set<data::variable> fv = find_free_variables(updates[*ip]);
275 2 : if(contains(fv, elem))
276 : {
277 0 : for(const data::variable& var: set_difference(fv, seen))
278 : {
279 0 : todo.push(var);
280 0 : seen.insert(var);
281 : }
282 0 : ip = independent_pars.erase(ip);
283 : }
284 : else
285 : {
286 2 : ++ip;
287 : }
288 : }
289 :
290 : // Check if we need to add quantified variables that have a larger scope and
291 : // and are at least one quantifier alternation away from elem
292 4 : bool add_rest = false;
293 9 : for(auto qv = qvars.rbegin(); qv != qvars.rend(); ++qv)
294 : {
295 5 : const std::set<data::variable>& vars = qv->variables();
296 5 : if(add_rest)
297 : {
298 0 : for(const data::variable& var: set_difference(vars, seen))
299 : {
300 0 : seen.insert(var);
301 0 : todo.push(var);
302 : }
303 : }
304 5 : else if(contains(vars, elem))
305 : {
306 1 : add_rest = true;
307 : }
308 : }
309 : }
310 :
311 : // Check whether there is at least one independent parameter and we are
312 : // propagating at least one quantified variable.
313 5 : if(independent_pars.empty() ||
314 5 : set_difference(qvars.back().variables(), seen).empty())
315 : {
316 1 : result = X_e;
317 1 : return;
318 : }
319 :
320 : // Build a new equation based on the independent parameters found
321 2 : data::variable_list new_parameter_list;
322 2 : data::data_expression_list new_update_list;
323 2 : i = 0;
324 2 : auto ip = independent_pars.begin();
325 2 : data::rewriter::substitution_type sigma;
326 :
327 6 : for(const data::variable& par: parameters)
328 : {
329 4 : if(ip != independent_pars.end() && *ip == i)
330 : {
331 2 : sigma[par] = updates[i];
332 2 : ++ip;
333 : }
334 : else
335 : {
336 2 : new_parameter_list.push_front(par);
337 2 : new_update_list.push_front(updates[i]);
338 : }
339 4 : i++;
340 : }
341 2 : new_parameter_list = reverse(new_parameter_list);
342 2 : new_update_list = reverse(new_update_list);
343 :
344 : // Construct a new PVI and a new equation
345 2 : core::identifier_string new_name = id_gen(X_e.name());
346 2 : pbes_expression new_rhs_X = pbes_system::replace_free_variables(find_equation(X_e).formula(), sigma);
347 2 : propositional_variable_instantiation new_X_e(new_name, new_update_list);
348 2 : pbes_expression new_Q_X_e = new_X_e;
349 5 : for(auto qv = qvars.rbegin(); qv != qvars.rend(); ++qv)
350 : {
351 3 : new_Q_X_e = qv->make_expr_include_only(seen, new_Q_X_e);
352 3 : new_rhs_X = qv->make_expr_exclude(seen, new_rhs_X);
353 : }
354 4 : pbes_equation new_eqn(find_equation(X_e).symbol(), propositional_variable(new_name, new_parameter_list), new_rhs_X);
355 2 : m_new_equations.emplace_back(X_e.name(), new_eqn);
356 :
357 2 : result = new_Q_X_e;
358 13 : }
359 : };
360 :
361 : inline
362 8 : void quantifier_propagate(
363 : std::list<std::pair<core::identifier_string, pbes_equation>>& new_equations,
364 : data::set_identifier_generator& id_gen,
365 : const quantifier_propagate_builder::equation_map_t eqn_map,
366 : pbes_expression& x)
367 : {
368 8 : quantifier_propagate_builder f(new_equations, id_gen, eqn_map);
369 8 : f.update(x);
370 8 : }
371 :
372 : } // namespace detail
373 :
374 : inline
375 4 : void quantifier_propagate(pbes& p)
376 : {
377 4 : std::list<std::pair<core::identifier_string, pbes_equation>> new_equations;
378 4 : detail::quantifier_propagate_builder::equation_map_t m_eqn_map;
379 4 : data::set_identifier_generator id_gen;
380 12 : for(const pbes_equation& eq: p.equations())
381 : {
382 8 : id_gen.add_identifier(eq.variable().name());
383 8 : m_eqn_map[eq.variable().name()] = eq;
384 : }
385 :
386 12 : for(pbes_equation& eqn: p.equations())
387 : {
388 8 : detail::quantifier_propagate(new_equations, id_gen, m_eqn_map, eqn.formula());
389 : }
390 :
391 : // Insert new equations
392 6 : for(const auto& [target, eqn]: new_equations)
393 : {
394 : // Find the original location, so ranks are preserved
395 4 : p.equations().insert(
396 4 : std::find_if(p.equations().begin(), p.equations().end(),
397 4 : [t = target](const pbes_equation& eq){ return eq.variable().name() == t; }),
398 : eqn
399 : );
400 : }
401 4 : }
402 :
403 : inline
404 4 : pbes quantifier_propagate(const pbes& p)
405 : {
406 4 : pbes result{p};
407 4 : quantifier_propagate(result);
408 4 : return result;
409 0 : }
410 :
411 : } // namespace pbes_system
412 :
413 : } // namespace mcrl2
414 :
415 : #endif // MCRL2_PBES_QUANTIFIER_PROPAGATE_H
|
