Line data Source code
1 : // Author(s): Wieger Wesselink
2 : //
3 : // Distributed under the Boost Software License, Version 1.0.
4 : // (See accompanying file LICENSE_1_0.txt or copy at
5 : // http://www.boost.org/LICENSE_1_0.txt)
6 : //
7 : /// \file mcrl2/pbes/constelm.h
8 : /// \brief The constelm algorithm.
9 :
10 : #ifndef MCRL2_PBES_CONSTELM_H
11 : #define MCRL2_PBES_CONSTELM_H
12 :
13 : #include "mcrl2/pbes/algorithms.h"
14 : #include "mcrl2/pbes/pbes_rewriter_type.h"
15 : #include "mcrl2/pbes/print.h"
16 : #include "mcrl2/pbes/replace.h"
17 : #include "mcrl2/pbes/rewriters/enumerate_quantifiers_rewriter.h"
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace pbes_system
23 : {
24 :
25 : namespace detail
26 : {
27 :
28 : inline
29 145 : void make_constelm_substitution(const std::map<data::variable, data::data_expression>& m, data::rewriter::substitution_type& result)
30 : {
31 287 : for (const auto& i : m)
32 : {
33 142 : result[i.first] = i.second;
34 : }
35 145 : }
36 :
37 : class quantified_variable
38 : {
39 : protected:
40 : bool m_is_forall;
41 : data::variable m_var;
42 :
43 : public:
44 1 : quantified_variable(bool is_forall, const data::variable& var)
45 1 : : m_is_forall(is_forall)
46 1 : , m_var(var)
47 1 : {}
48 :
49 0 : bool is_forall() const
50 : {
51 0 : return m_is_forall;
52 : }
53 :
54 0 : const data::variable& variable() const
55 : {
56 0 : return m_var;
57 : }
58 :
59 0 : bool operator==(const quantified_variable& other) const
60 : {
61 0 : return m_is_forall == other.m_is_forall && m_var == other.m_var;
62 : }
63 :
64 : bool operator!=(const quantified_variable& other) const
65 : {
66 : return !(*this == other);
67 : }
68 :
69 0 : bool operator<(const quantified_variable& other) const
70 : {
71 0 : return m_is_forall < other.m_is_forall || (m_is_forall == other.m_is_forall && m_var < other.m_var);
72 : }
73 :
74 0 : pbes_expression make_expr(const pbes_expression& expr) const
75 : {
76 0 : return m_is_forall ? pbes_expression(forall(data::variable_list({m_var}), expr)) : pbes_expression(exists(data::variable_list({m_var}), expr));
77 : }
78 :
79 0 : std::string to_string() const
80 : {
81 0 : std::ostringstream out;
82 0 : out << (is_forall() ? "forall " : "exists ") << variable() << ". ";
83 0 : return out.str();
84 0 : }
85 : };
86 :
87 : /// \brief A quantified predicate variable instantiation
88 : struct QPVI
89 : {
90 : std::list<quantified_variable> Q;
91 : propositional_variable_instantiation X_e;
92 :
93 42 : bool operator<(const QPVI& other) const
94 : {
95 42 : return std::tie(Q, X_e) < std::tie(other.Q, other.X_e);
96 : }
97 : };
98 :
99 : struct edge_details
100 : {
101 : /// \brief Contains expressions that characterise when an edge is enabled.
102 : /// The conjunction of these expressions is a guard for some PVI.
103 : std::set<data::data_expression> conditions;
104 : /// \brief The set of free variables that occur on the other side of the conjunctions this
105 : /// PVI occurs in. Can be used to determine whether the quantifier inside rewriter
106 : /// can manage to push an existential quantifier all the way to this PVI.
107 : std::set<data::variable> conjunctive_context_FV;
108 : /// \brief The set of free variables that occur on the other side of the conjunctions this
109 : /// PVI occurs in. Can be used to determine whether the quantifier inside rewriter
110 : /// can manage to push a universal quantifier all the way to this PVI.
111 : std::set<data::variable> disjunctive_context_FV;
112 : };
113 :
114 : struct edge_traverser_stack_elem
115 : {
116 : typedef std::multimap<QPVI, edge_details> edge_map;
117 :
118 : data::data_expression Cpos;
119 : data::data_expression Cneg;
120 : std::set<data::variable> FV;
121 : edge_map edges;
122 :
123 87 : edge_traverser_stack_elem(const data::data_expression& cond_pos, const data::data_expression& cond_neg, std::set<data::variable>&& free_vars)
124 87 : : Cpos(cond_pos), Cneg(cond_neg)
125 : {
126 87 : std::swap(FV, free_vars);
127 87 : }
128 : };
129 :
130 : struct edge_condition_traverser: public pbes_expression_traverser<edge_condition_traverser>
131 : {
132 : typedef pbes_expression_traverser<edge_condition_traverser> super;
133 : using super::enter;
134 : using super::leave;
135 : using super::apply;
136 :
137 : typedef edge_traverser_stack_elem stack_elem;
138 : typedef stack_elem::edge_map edge_map;
139 : typedef std::list<detail::quantified_variable> qvar_list;
140 :
141 : std::vector<stack_elem> condition_fv_stack;
142 : std::list<pbes_expression> quantified_context;
143 :
144 93 : void push(const stack_elem& x)
145 : {
146 93 : condition_fv_stack.push_back(x);
147 93 : }
148 :
149 64 : stack_elem& top()
150 : {
151 64 : return condition_fv_stack.back();
152 : }
153 :
154 29 : const stack_elem& top() const
155 : {
156 29 : return condition_fv_stack.back();
157 : }
158 :
159 64 : stack_elem pop()
160 : {
161 64 : stack_elem result = top();
162 64 : condition_fv_stack.pop_back();
163 64 : return result;
164 : }
165 :
166 : // N.B. As a side effect ec1 and ec2 are changed!!!
167 29 : void merge_conditions(stack_elem& ec1, bool negate1,
168 : stack_elem& ec2, bool negate2,
169 : stack_elem& ec, bool is_conjunctive
170 : )
171 : {
172 39 : for (auto& i: ec1.edges)
173 : {
174 10 : auto& [Q_X_e, details] = i;
175 10 : details.conditions.insert(negate2 ? ec2.Cneg : ec2.Cpos);
176 : (is_conjunctive ? details.conjunctive_context_FV : details.disjunctive_context_FV)
177 10 : .insert(ec2.FV.begin(), ec2.FV.end());
178 10 : ec.edges.insert(i);
179 : }
180 66 : for (auto& i: ec2.edges)
181 : {
182 37 : auto& [Q_X_e, details] = i;
183 37 : details.conditions.insert(negate1 ? ec1.Cneg : ec1.Cpos);
184 : (is_conjunctive ? details.conjunctive_context_FV : details.disjunctive_context_FV)
185 37 : .insert(ec1.FV.begin(), ec1.FV.end());
186 37 : ec.edges.insert(i);
187 : }
188 29 : }
189 :
190 : // enter functions related to maintaining the quantfier scope
191 0 : void enter(const not_&)
192 : {
193 0 : quantified_context.clear();
194 0 : }
195 :
196 14 : void enter(const and_&)
197 : {
198 14 : quantified_context.clear();
199 14 : }
200 :
201 15 : void enter(const or_&)
202 : {
203 15 : quantified_context.clear();
204 15 : }
205 :
206 0 : void enter(const imp&)
207 : {
208 0 : quantified_context.clear();
209 0 : }
210 :
211 4 : void enter(const forall& x)
212 : {
213 4 : quantified_context.push_back(x);
214 4 : }
215 :
216 2 : void enter(const exists& x)
217 : {
218 2 : quantified_context.push_back(x);
219 2 : }
220 :
221 : // leave functions, mostly used to build conditions and gather free variables
222 19 : void leave(const data::data_expression& x)
223 : {
224 19 : data::data_expression cond_not;
225 19 : data::optimized_not(cond_not, x);
226 :
227 19 : push(stack_elem(x, cond_not, data::find_free_variables(x)));
228 19 : }
229 :
230 0 : void leave(const not_&)
231 : {
232 0 : std::swap(top().Cpos, top().Cneg);
233 0 : }
234 :
235 14 : void leave(const and_&)
236 : {
237 14 : stack_elem ec_right = pop();
238 14 : stack_elem ec_left = pop();
239 14 : data::data_expression cond_and;
240 14 : data::data_expression cond_or;
241 14 : data::optimized_and(cond_and, ec_left.Cpos, ec_right.Cpos);
242 14 : data::optimized_or(cond_or, ec_left.Cneg, ec_right.Cneg);
243 :
244 : stack_elem ec(cond_and, cond_or,
245 14 : utilities::detail::set_union(ec_left.FV, ec_right.FV));
246 14 : merge_conditions(ec_left, false, ec_right, false, ec, true);
247 14 : push(ec);
248 14 : }
249 :
250 15 : void leave(const or_&)
251 : {
252 15 : stack_elem ec_right = pop();
253 15 : stack_elem ec_left = pop();
254 15 : data::data_expression cond_and;
255 15 : data::data_expression cond_or;
256 :
257 15 : data::optimized_and(cond_and, ec_left.Cneg, ec_right.Cneg);
258 15 : data::optimized_or(cond_or, ec_left.Cpos, ec_right.Cpos);
259 :
260 : stack_elem ec(cond_or, cond_and,
261 15 : utilities::detail::set_union(ec_left.FV, ec_right.FV));
262 15 : merge_conditions(ec_left, true, ec_right, true, ec, false);
263 15 : push(ec);
264 15 : }
265 :
266 0 : void leave(const imp&)
267 : {
268 0 : stack_elem ec_right = pop();
269 0 : stack_elem ec_left = pop();
270 0 : data::data_expression cond_or;
271 0 : data::data_expression cond_and;
272 :
273 0 : data::optimized_or(cond_or, ec_left.Cneg, ec_right.Cpos);
274 0 : data::optimized_and(cond_and, ec_left.Cpos, ec_right.Cneg);
275 :
276 : stack_elem ec(cond_or, cond_and,
277 0 : utilities::detail::set_union(ec_left.FV, ec_right.FV));;
278 0 : merge_conditions(ec_left, false, ec_right, true, ec, false);
279 0 : push(ec);
280 0 : }
281 :
282 4 : void leave(const forall& x)
283 : {
284 : // build conditions and free variable sets
285 4 : stack_elem ec = pop();
286 8 : for (auto& [X_e, details]: ec.edges)
287 : {
288 4 : auto& [cond_set, conj_FV, disj_FV] = details;
289 :
290 : // Update the conditions
291 4 : std::set<data::data_expression> new_conditions;
292 11 : for(const data::data_expression& e: cond_set)
293 : {
294 7 : data::data_expression t;
295 7 : data::optimized_exists(t, x.variables(), e, true);
296 7 : new_conditions.insert(t);
297 7 : }
298 4 : cond_set = std::move(new_conditions);
299 4 : data::data_expression forall;
300 4 : data::optimized_forall(forall, x.variables(), ec.Cpos, true);
301 :
302 4 : cond_set.insert(forall);
303 :
304 : // Update FV
305 4 : conj_FV = ec.FV;
306 4 : }
307 4 : data::optimized_forall(ec.Cpos, x.variables(), ec.Cpos, true);
308 4 : data::optimized_exists(ec.Cneg, x.variables(), ec.Cneg, true);
309 4 : std::set<data::variable> bound_vars{x.variables().begin(), x.variables().end()};
310 4 : ec.FV = utilities::detail::set_difference(ec.FV, bound_vars);
311 4 : push(ec);
312 :
313 : // maintain quantifier scope
314 4 : if(!quantified_context.empty() && quantified_context.back() == x)
315 : {
316 1 : quantified_context.pop_back();
317 : }
318 4 : }
319 :
320 2 : void leave(const exists& x)
321 : {
322 : // build conditions and free variable sets
323 2 : stack_elem ec = pop();
324 4 : for (auto& [X_e, details]: ec.edges)
325 : {
326 2 : auto& [cond_set, conj_FV, disj_FV] = details;
327 :
328 : // Update the conditions
329 2 : std::set<data::data_expression> new_conditions;
330 6 : for(const data::data_expression& e: cond_set)
331 : {
332 4 : data::data_expression t;
333 4 : data::optimized_exists(t, x.variables(), e, true);
334 4 : new_conditions.insert(t);
335 4 : }
336 2 : cond_set = std::move(new_conditions);
337 :
338 2 : data::data_expression forall;
339 2 : data::optimized_forall(forall, x.variables(), ec.Cneg, true);
340 2 : cond_set.insert(forall);
341 :
342 : // Update FV
343 2 : disj_FV = ec.FV;
344 2 : }
345 2 : data::optimized_exists(ec.Cpos, x.variables(), ec.Cpos, true);
346 2 : data::optimized_forall(ec.Cneg, x.variables(), ec.Cneg, true);
347 2 : std::set<data::variable> bound_vars{x.variables().begin(), x.variables().end()};
348 2 : ec.FV = utilities::detail::set_difference(ec.FV, bound_vars);
349 2 : push(ec);
350 :
351 : // maintain quantifier scope
352 2 : if(!quantified_context.empty() && quantified_context.back() == x)
353 : {
354 0 : quantified_context.pop_back();
355 : }
356 2 : }
357 :
358 39 : void leave(const propositional_variable_instantiation& x)
359 : {
360 : // Build list of qvars from quantifier scope
361 39 : qvar_list qvars;
362 40 : for(const pbes_expression& expr: quantified_context)
363 : {
364 1 : assert(is_forall(expr) || is_exists(expr));
365 1 : data::variable_list vars(is_forall(expr) ? atermpp::down_cast<forall>(expr).variables() : atermpp::down_cast<exists>(expr).variables());
366 2 : for(const data::variable& v: vars)
367 : {
368 1 : qvars.emplace_back(is_forall(expr), v);
369 : }
370 1 : }
371 39 : QPVI Q_X_e{qvars, x};
372 :
373 : // Store the QPVI and the condition true
374 39 : stack_elem ec(data::sort_bool::true_(), data::sort_bool::true_(), data::find_free_variables(x.parameters()));
375 39 : ec.edges.insert(std::make_pair(Q_X_e,
376 117 : edge_details{std::set<data::data_expression>{data::sort_bool::true_()},
377 : std::set<data::variable>{}, std::set<data::variable>{}}));
378 39 : push(ec);
379 39 : }
380 :
381 29 : const edge_map& result() const
382 : {
383 29 : assert(condition_fv_stack.size() == 1);
384 29 : return top().edges;
385 : }
386 : };
387 :
388 : } // namespace detail
389 : /// \endcond
390 :
391 :
392 : /// \brief Algorithm class for the constelm algorithm
393 : template <typename DataRewriter, typename PbesRewriter>
394 : class pbes_constelm_algorithm
395 : {
396 : protected:
397 : /// \brief A map with constraints on the vertices of the graph
398 : typedef std::map<data::variable, data::data_expression> constraint_map;
399 : typedef std::list<detail::quantified_variable> qvar_list;
400 :
401 : /// \brief Compares data expressions for equality.
402 : const DataRewriter& m_data_rewriter;
403 :
404 : /// \brief Compares data expressions for equality.
405 : const PbesRewriter& m_pbes_rewriter;
406 :
407 : /// \brief Represents an edge of the dependency graph. The assignments are stored
408 : /// implicitly using the 'right' parameter. The condition determines under
409 : /// what circumstances the influence of the edge is propagated to its target
410 : /// vertex.
411 : //
412 : // N.B. The attribute condition "pbes_expression condition;" needs to be protected.
413 : // This is achieved by deriving from pbes_expression. This is very ugly, but AFAIK
414 : // this is the least destructive solution to garbage collection problems.
415 : // Note that source and target are protected elsewhere.
416 : class edge: public data::data_expression
417 : {
418 : protected:
419 : /// \brief The propositional variable at the source of the edge
420 : const propositional_variable m_source;
421 :
422 : /// \brief The quantifiers in whose direct context the target PVI occurs
423 : const qvar_list m_qvars;
424 :
425 : /// \brief The propositional variable instantiation that determines the target of the edge
426 : const propositional_variable_instantiation m_target;
427 :
428 : const std::set<data::variable> m_conj_context;
429 : const std::set<data::variable> m_disj_context;
430 :
431 : public:
432 : /// \brief Constructor
433 : edge() = default;
434 :
435 : /// \brief Constructor
436 : /// \param src A propositional variable declaration
437 : /// \param tgt A propositional variable
438 : /// \param c A term
439 39 : edge(
440 : const propositional_variable& src,
441 : const qvar_list& qvars,
442 : const propositional_variable_instantiation& tgt,
443 : const std::set<data::variable>& conj_context,
444 : const std::set<data::variable>& disj_context,
445 : data::data_expression c = data::sort_bool::true_()
446 : )
447 : : data::data_expression(c)
448 39 : , m_source(src)
449 39 : , m_qvars(qvars)
450 39 : , m_target(tgt)
451 39 : , m_conj_context(conj_context)
452 78 : , m_disj_context(disj_context)
453 39 : {}
454 :
455 : /// \brief Returns a string representation of the edge.
456 : /// \return A string representation of the edge.
457 0 : std::string to_string() const
458 : {
459 0 : std::ostringstream out;
460 0 : out << "(" << m_source.name() << ", " << m_target.name() << ") label = ";
461 0 : for(const detail::quantified_variable& qv: m_qvars)
462 : {
463 0 : out << qv.to_string();
464 : }
465 0 : out << m_target << " condition = " << condition();
466 0 : return out.str();
467 0 : }
468 :
469 : /// \brief The propositional variable at the source of the edge
470 : const propositional_variable& source() const
471 : {
472 : return m_source;
473 : }
474 :
475 55 : const qvar_list& quantified_variables() const
476 : {
477 55 : return m_qvars;
478 : }
479 :
480 : /// \brief The propositional variable instantiation that determines the target of the edge
481 114 : const propositional_variable_instantiation& target() const
482 : {
483 114 : return m_target;
484 : }
485 :
486 : /// \brief The condition of the edge
487 59 : const data::data_expression& condition() const
488 : {
489 59 : return *this;
490 : }
491 :
492 : /// \brief Try to guess which quantifiers of Q can end up directly
493 : /// before target, when the quantifier inside rewriter is applied.
494 55 : qvar_list quantifier_inside_approximation(const qvar_list& Q) const
495 : {
496 55 : qvar_list result;
497 55 : for (auto it = Q.crbegin(); it != Q.crend(); ++it)
498 : {
499 : // Variable of a universal quantifier cannot occur in the disjunctive context
500 : // Variable of an existential quantifier cannot occur in the conjunctive context
501 0 : if (( it->is_forall() && m_disj_context.find(it->variable()) == m_disj_context.end()) ||
502 0 : (!it->is_forall() && m_conj_context.find(it->variable()) == m_conj_context.end()))
503 : {
504 0 : result.push_front(*it);
505 : }
506 : else
507 : {
508 0 : break;
509 : }
510 : }
511 55 : return result;
512 0 : }
513 : };
514 :
515 : /// \brief Represents a vertex of the dependency graph.
516 : class vertex
517 : {
518 : protected:
519 : /// \brief The propositional variable that corresponds to the vertex
520 : propositional_variable m_variable;
521 :
522 : /// \brief The list of quantified variables that occur in the constraints
523 : qvar_list m_qvars;
524 :
525 : /// \brief Maps data variables to data expressions. If a parameter is not
526 : // present in this map, it means that it represents NaC ("not a constant").
527 : constraint_map m_constraints;
528 :
529 : /// \brief Indicates whether this vertex has been visited at least once.
530 : bool m_visited = false;
531 :
532 : /// \brief Returns true if the parameter v has been assigned a constant expression.
533 : /// \param v A parameter of this->variable()
534 : /// \return True if the data parameter v has been assigned a constant expression.
535 26 : bool is_constant(const data::variable& v) const
536 : {
537 26 : auto i = m_constraints.find(v);
538 26 : return i != m_constraints.end();
539 : }
540 :
541 : /// \brief Returns true iff all free variables in e are bound in qvars
542 71 : bool bound_in_quantifiers(const qvar_list& qvars, const data::data_expression& e)
543 : {
544 71 : std::set<data::variable> free_vars = data::find_free_variables(e);
545 71 : return std::all_of(free_vars.begin(), free_vars.end(), [&](const data::variable& v)
546 : {
547 0 : return std::find_if(qvars.begin(), qvars.end(), [&](const detail::quantified_variable& qvar){ return qvar.variable() == v; }) != qvars.end();
548 142 : });
549 71 : }
550 :
551 : /// \brief Weaken the constraints so they satisfy
552 : /// - vars(m_constraints[d]) subset vars(m_qvars); and
553 : /// - vars(deleted_constraints) intersection vars(m_qvars) = {}
554 73 : void fix_constraints(std::vector<data::data_expression> deleted_constraints)
555 : {
556 103 : while (!deleted_constraints.empty())
557 : {
558 15 : std::set<data::variable> vars_deleted;
559 55 : for (const data::data_expression& fi: deleted_constraints)
560 : {
561 40 : data::find_free_variables(fi, std::inserter(vars_deleted, vars_deleted.end()));
562 : }
563 15 : deleted_constraints.clear();
564 :
565 15 : auto del_i = std::find_if(m_qvars.rbegin(), m_qvars.rend(), [&](const detail::quantified_variable& qv)
566 : {
567 0 : return vars_deleted.find(qv.variable()) != vars_deleted.end();
568 : });
569 : // Remove quantified variables up to and including del_i
570 15 : m_qvars.erase(m_qvars.begin(), del_i.base());
571 :
572 58 : for (const data::variable& par: m_variable.parameters())
573 : {
574 28 : auto k = m_constraints.find(par);
575 28 : if(k == m_constraints.end())
576 : {
577 20 : continue;
578 : }
579 8 : if(!bound_in_quantifiers(m_qvars, k->second))
580 : {
581 0 : deleted_constraints.push_back(k->second);
582 0 : m_constraints.erase(k);
583 : }
584 : }
585 : }
586 73 : }
587 :
588 : public:
589 : /// \brief Constructor
590 29 : vertex() = default;
591 :
592 : /// \brief Constructor
593 : /// \param x A propositional variable declaration
594 29 : vertex(propositional_variable x)
595 29 : : m_variable(x)
596 29 : {}
597 :
598 : /// \brief The propositional variable that corresponds to the vertex
599 43 : const propositional_variable& variable() const
600 : {
601 43 : return m_variable;
602 : }
603 :
604 81 : const qvar_list& quantified_variables() const
605 : {
606 81 : return m_qvars;
607 : }
608 :
609 : /// \brief Maps data variables to data expressions. If the right hand side is a data
610 : /// variable, it means that it represents NaC ("not a constant").
611 185 : const constraint_map& constraints() const
612 : {
613 185 : return m_constraints;
614 : }
615 :
616 : /// \brief Returns the indices of the constant parameters of this vertex.
617 : /// \return The indices of the constant parameters of this vertex.
618 13 : std::vector<std::size_t> constant_parameter_indices() const
619 : {
620 13 : std::vector<std::size_t> result;
621 13 : std::size_t index = 0;
622 52 : for (const data::variable& parameter: m_variable.parameters())
623 : {
624 26 : if (is_constant(parameter))
625 : {
626 19 : result.push_back(index);
627 : }
628 26 : index++;
629 : }
630 26 : return result;
631 0 : }
632 :
633 : /// \brief Returns a string representation of the vertex.
634 : /// \return A string representation of the vertex.
635 0 : std::string to_string() const
636 : {
637 0 : std::ostringstream out;
638 0 : out << m_variable << " assertions = ";
639 0 : for(const detail::quantified_variable& v: quantified_variables())
640 : {
641 0 : out << v.to_string();
642 : }
643 0 : for (const auto& constraint: m_constraints)
644 : {
645 0 : out << "{" << constraint.first << " := " << constraint.second << "} ";
646 : }
647 0 : return out.str();
648 0 : }
649 :
650 : /// \brief Assign new values to the parameters of this vertex, and update the constraints accordingly.
651 : /// The new values have a number of constraints.
652 73 : bool update(const qvar_list& qvars, const data::data_expression_list& e, const constraint_map& e_constraints, const DataRewriter& datar)
653 : {
654 73 : bool changed = false;
655 :
656 73 : data::variable_list params = m_variable.parameters();
657 73 : data::rewriter::substitution_type sigma;
658 73 : detail::make_constelm_substitution(e_constraints, sigma);
659 :
660 73 : if (!m_visited)
661 : {
662 28 : m_visited = true;
663 28 : changed = true;
664 :
665 28 : m_qvars = qvars;
666 : // Partition expressions in e based on whether their free variables
667 : // are bound in m_qvars.
668 28 : std::vector<data::data_expression> deleted_constraints;
669 28 : auto par = params.begin();
670 67 : for (auto i = e.begin(); i != e.end(); ++i, ++par)
671 : {
672 39 : data::data_expression e1 = datar(*i, sigma);
673 39 : if (bound_in_quantifiers(m_qvars, e1))
674 : {
675 39 : m_constraints[*par] = e1;
676 : }
677 : else
678 : {
679 0 : deleted_constraints.push_back(e1);
680 : }
681 : }
682 28 : fix_constraints(deleted_constraints);
683 28 : }
684 : else
685 : {
686 : // Find longest common suffix of qvars
687 45 : auto mismatch_it = std::mismatch(m_qvars.rbegin(), m_qvars.rend(), qvars.rbegin(), qvars.rend()).first;
688 45 : changed |= mismatch_it != m_qvars.rend();
689 : // Remove the outer quantifiers, up to and including mismatch_it
690 45 : m_qvars.erase(m_qvars.begin(), mismatch_it.base());
691 :
692 : // Find constraints for which f[i] = e[i] and for which all free
693 : // variables are bound in m_qvars (which may have changed).
694 45 : std::vector<data::data_expression> deleted_constraints;
695 45 : auto i = e.begin();
696 159 : for (auto par = params.begin(); i != e.end(); ++i, ++par)
697 : {
698 70 : auto k = m_constraints.find(*par);
699 70 : if(k == m_constraints.end())
700 : {
701 26 : continue;
702 : }
703 44 : const data::data_expression& fi = k->second;
704 44 : data::data_expression ei = datar(*i, sigma);
705 44 : if (fi != ei || !bound_in_quantifiers(m_qvars, fi))
706 : {
707 20 : changed = true;
708 20 : deleted_constraints.push_back(fi);
709 20 : deleted_constraints.push_back(ei);
710 20 : m_constraints.erase(k);
711 : }
712 : }
713 45 : fix_constraints(deleted_constraints);
714 45 : }
715 73 : return changed;
716 73 : }
717 : };
718 :
719 : /// \brief The storage type for vertices
720 : typedef std::map<core::identifier_string, vertex> vertex_map;
721 :
722 : /// \brief The storage type for edges
723 : typedef std::map<core::identifier_string, std::vector<edge> > edge_map;
724 :
725 : /// \brief The vertices of the dependency graph. They are stored in a map, to
726 : /// support searching for a vertex.
727 : vertex_map m_vertices;
728 :
729 : /// \brief The edges of the dependency graph. They are stored in a map, to
730 : /// easily access all out-edges corresponding to a particular vertex.
731 : edge_map m_edges;
732 :
733 : /// \brief The redundant parameters.
734 : std::map<core::identifier_string, std::vector<std::size_t> > m_redundant_parameters;
735 :
736 : /// \brief Logs the vertices of the dependency graph.
737 0 : std::string print_vertices() const
738 : {
739 0 : std::ostringstream out;
740 0 : for (const auto& v: m_vertices)
741 : {
742 0 : out << v.second.to_string() << std::endl;
743 : }
744 0 : return out.str();
745 0 : }
746 :
747 : /// \brief Logs the edges of the dependency graph.
748 0 : std::string print_edges()
749 : {
750 0 : std::ostringstream out;
751 0 : for (const auto& source: m_edges)
752 : {
753 0 : for (const auto& e: source.second)
754 : {
755 0 : out << e.to_string() << std::endl;
756 : }
757 : }
758 0 : return out.str();
759 0 : }
760 :
761 0 : std::string print_todo_list(const std::deque<propositional_variable>& todo)
762 : {
763 0 : std::ostringstream out;
764 0 : out << "\n<todo list> [";
765 0 : for (auto i = todo.begin(); i != todo.end(); ++i)
766 : {
767 0 : if (i != todo.begin())
768 : {
769 0 : out << ", ";
770 : }
771 0 : out << core::pp(i->name());
772 : }
773 0 : out << "]" << std::endl;
774 0 : return out.str();
775 0 : }
776 :
777 0 : std::string print_edge_update(const edge& e, const vertex& u, const vertex& v)
778 : {
779 0 : std::ostringstream out;
780 0 : out << "\n<updating edge> " << e.to_string() << std::endl;
781 0 : out << " <source vertex > " << u.to_string() << std::endl;
782 0 : out << " <target vertex before> " << v.to_string() << std::endl;
783 0 : return out.str();
784 0 : }
785 :
786 0 : std::string print_condition(const edge& e, const vertex& u, const pbes_expression& value)
787 : {
788 0 : std::ostringstream out;
789 0 : data::rewriter::substitution_type sigma;
790 0 : detail::make_constelm_substitution(u.constraints(), sigma);
791 0 : out << " <condition > " << e.condition() << sigma << " to " << value << std::endl;
792 0 : return out.str();
793 0 : }
794 :
795 0 : std::string print_evaluation_failure(const edge& e, const vertex& u)
796 : {
797 0 : std::ostringstream out;
798 0 : data::rewriter::substitution_type sigma;
799 0 : detail::make_constelm_substitution(u.constraints(), sigma);
800 0 : out << "\nCould not evaluate condition " << e.condition() << sigma << " to true or false";
801 0 : return out.str();
802 0 : }
803 :
804 : template <typename E>
805 55 : std::list<E> concat(const std::list<E> a, const std::list<E> b)
806 : {
807 55 : std::list<E> result(a);
808 55 : result.insert(result.end(), b.begin(), b.end());
809 55 : return result;
810 0 : }
811 :
812 : public:
813 :
814 : /// \brief Constructor.
815 : /// \param datar A data rewriter
816 : /// \param pbesr A PBES rewriter
817 18 : pbes_constelm_algorithm(const DataRewriter& datar, const PbesRewriter& pbesr)
818 18 : : m_data_rewriter(datar), m_pbes_rewriter(pbesr)
819 18 : {}
820 :
821 : /// \brief Returns the parameters that have been removed by the constelm algorithm
822 : /// \return The removed parameters
823 0 : std::map<propositional_variable, std::vector<data::variable> > redundant_parameters() const
824 : {
825 0 : std::map<propositional_variable, std::vector<data::variable> > result;
826 0 : for (const std::pair<const core::identifier_string, std::vector<std::size_t>>& red_pair: m_redundant_parameters)
827 : {
828 0 : const vertex& v = m_vertices.find(red_pair.first)->second;
829 0 : std::vector<data::variable>& variables = result[v.variable()];
830 0 : for (const std::size_t par: red_pair.second)
831 : {
832 0 : typename data::variable_list::iterator k = v.variable().parameters().begin();
833 0 : std::advance(k, par);
834 0 : variables.push_back(*k);
835 : }
836 : }
837 0 : return result;
838 0 : }
839 :
840 : /// \brief Runs the constelm algorithm
841 : /// \param p A pbes
842 : /// \param compute_conditions If true, propagation conditions are computed. Note
843 : /// that the currently implementation has exponential behavior.
844 18 : void run(pbes& p, bool compute_conditions = false, bool check_quantifiers = true)
845 : {
846 18 : m_vertices.clear();
847 18 : m_edges.clear();
848 18 : m_redundant_parameters.clear();
849 :
850 : // compute the vertices and edges of the dependency graph
851 47 : for (pbes_equation& eqn: p.equations())
852 : {
853 29 : core::identifier_string name = eqn.variable().name();
854 29 : m_vertices[name] = vertex(eqn.variable());
855 :
856 : // use an edge_condition_traverser to compute the edges
857 29 : detail::edge_condition_traverser f;
858 29 : f.apply(eqn.formula());
859 :
860 29 : std::vector<edge>& edges = m_edges[name];
861 68 : for (const auto& [Q_X_e, details]: f.result())
862 : {
863 39 : const auto& [Q, X_e] = Q_X_e;
864 39 : const auto& [conditions, conj_FV, disj_FV] = details;
865 :
866 : // check options for quantifiers and conditions.
867 39 : qvar_list quantifier_list = check_quantifiers ? Q : qvar_list();
868 39 : data::data_expression condition = compute_conditions
869 : ? data::lazy::join_and(conditions.begin(), conditions.end())
870 28 : : data::data_expression(data::sort_bool::true_());
871 :
872 39 : edges.emplace_back(eqn.variable(), quantifier_list, X_e, conj_FV, disj_FV, condition);
873 : }
874 : }
875 :
876 : // initialize the todo list of vertices that need to be processed
877 18 : propositional_variable_instantiation init = p.initial_state();
878 18 : std::deque<propositional_variable> todo;
879 18 : const data::data_expression_list& e_init = init.parameters();
880 18 : vertex& u_init = m_vertices[init.name()];
881 18 : u_init.update(qvar_list(), e_init, constraint_map(), m_data_rewriter);
882 18 : todo.push_back(u_init.variable());
883 :
884 18 : mCRL2log(log::debug) << "\n--- initial vertices ---\n" << print_vertices();
885 18 : mCRL2log(log::debug) << "\n--- edges ---\n" << print_edges();
886 :
887 : // propagate constraints over the edges until the todo list is empty
888 100 : while (!todo.empty())
889 : {
890 41 : mCRL2log(log::debug) << print_todo_list(todo);
891 41 : propositional_variable var = todo.front();
892 :
893 : // remove all occurrences of var from todo
894 41 : todo.erase(std::remove(todo.begin(), todo.end(), var), todo.end());
895 :
896 41 : const vertex& u = m_vertices[var.name()];
897 41 : const std::vector<edge>& u_edges = m_edges[var.name()];
898 :
899 100 : for (const edge& e: u_edges)
900 : {
901 59 : vertex& v = m_vertices[e.target().name()];
902 59 : mCRL2log(log::debug) << print_edge_update(e, u, v);
903 :
904 59 : data::rewriter::substitution_type sigma;
905 59 : detail::make_constelm_substitution(u.constraints(), sigma);
906 59 : pbes_expression needs_update = m_pbes_rewriter(e.condition(), sigma);
907 59 : mCRL2log(log::debug) << print_condition(e, u, needs_update);
908 :
909 59 : if (!is_false(needs_update) && !is_true(needs_update))
910 : {
911 4 : mCRL2log(log::debug) << print_evaluation_failure(e, u);
912 : }
913 59 : if (!is_false(needs_update))
914 : {
915 165 : bool changed = v.update(
916 55 : concat(e.quantifier_inside_approximation(u.quantified_variables()), e.quantified_variables()),
917 55 : e.target().parameters(),
918 : u.constraints(),
919 : m_data_rewriter);
920 55 : if (changed)
921 : {
922 25 : todo.push_back(v.variable());
923 : }
924 : }
925 59 : mCRL2log(log::debug) << " <target vertex after > " << v.to_string() << "\n";
926 : }
927 : }
928 :
929 18 : mCRL2log(log::debug) << "\n--- final vertices ---\n" << print_vertices();
930 :
931 : // compute the redundant parameters and the redundant equations
932 47 : for (const pbes_equation& eqn: p.equations())
933 : {
934 29 : core::identifier_string name = eqn.variable().name();
935 29 : const vertex& v = m_vertices[name];
936 29 : if (!v.constraints().empty())
937 : {
938 13 : std::vector<std::size_t> r = v.constant_parameter_indices();
939 13 : if (!r.empty())
940 : {
941 13 : m_redundant_parameters[name] = r;
942 : }
943 13 : }
944 : }
945 :
946 : // Apply the constraints to the equations.
947 47 : for (pbes_equation& eqn: p.equations())
948 : {
949 29 : core::identifier_string name = eqn.variable().name();
950 29 : const vertex& v = m_vertices[name];
951 :
952 29 : if (!v.constraints().empty())
953 : {
954 13 : data::rewriter::substitution_type sigma;
955 13 : detail::make_constelm_substitution(v.constraints(), sigma);
956 13 : pbes_expression body = pbes_system::replace_free_variables(eqn.formula(), sigma);
957 13 : for (auto i = v.quantified_variables().crbegin(); i != v.quantified_variables().crend(); ++i)
958 : {
959 0 : body = i->make_expr(body);
960 : }
961 13 : eqn = pbes_equation(
962 13 : eqn.symbol(),
963 13 : eqn.variable(),
964 : body
965 : );
966 13 : }
967 : }
968 :
969 : // remove the redundant parameters
970 18 : pbes_system::algorithms::remove_parameters(p, m_redundant_parameters);
971 :
972 : // print the parameters and equation that are removed
973 18 : if (mCRL2logEnabled(log::verbose))
974 : {
975 0 : mCRL2log(log::verbose) << "\nremoved the following constant parameters:" << std::endl;
976 0 : for (const std::pair<const propositional_variable, std::vector<data::variable>>& i: redundant_parameters())
977 : {
978 0 : for (const data::variable& var: i.second)
979 : {
980 0 : mCRL2log(log::verbose) << " (" << mcrl2::core::pp(i.first.name()) << ", " << data::pp(var) << ")" << std::endl;
981 : }
982 : }
983 : }
984 18 : }
985 : };
986 :
987 : /// \brief Apply the constelm algorithm
988 : /// \param p A PBES to which the algorithm is applied
989 : /// \param rewrite_strategy A data rewrite strategy
990 : /// \param rewriter_type A PBES rewriter type
991 : /// \param compute_conditions If true, conditions for the edges of the dependency graph are used N.B. Very inefficient!
992 : /// \param remove_redundant_equations If true, unreachable equations will be removed.
993 : inline
994 0 : void constelm(pbes& p,
995 : data::rewrite_strategy rewrite_strategy,
996 : pbes_rewriter_type rewriter_type,
997 : bool compute_conditions = false,
998 : bool remove_redundant_equations = true,
999 : bool check_quantifiers = true
1000 : )
1001 : {
1002 : // data rewriter
1003 0 : data::rewriter datar(p.data(), rewrite_strategy);
1004 :
1005 : // pbes rewriter
1006 0 : switch (rewriter_type)
1007 : {
1008 0 : case simplify:
1009 : {
1010 : typedef simplify_data_rewriter<data::rewriter> pbes_rewriter;
1011 0 : pbes_rewriter pbesr(datar);
1012 0 : pbes_constelm_algorithm<data::rewriter, pbes_rewriter> algorithm(datar, pbesr);
1013 0 : algorithm.run(p, compute_conditions, check_quantifiers);
1014 0 : if (remove_redundant_equations)
1015 : {
1016 0 : std::vector<propositional_variable> V = algorithms::remove_unreachable_variables(p);
1017 0 : mCRL2log(log::verbose) << algorithms::print_removed_equations(V);
1018 0 : }
1019 0 : break;
1020 0 : }
1021 0 : case quantifier_all:
1022 : case quantifier_finite:
1023 : {
1024 0 : bool enumerate_infinite_sorts = (rewriter_type == quantifier_all);
1025 0 : enumerate_quantifiers_rewriter pbesr(datar, p.data(), enumerate_infinite_sorts);
1026 0 : pbes_constelm_algorithm<data::rewriter, enumerate_quantifiers_rewriter> algorithm(datar, pbesr);
1027 0 : algorithm.run(p, compute_conditions, check_quantifiers);
1028 0 : if (remove_redundant_equations)
1029 : {
1030 0 : std::vector<propositional_variable> V = algorithms::remove_unreachable_variables(p);
1031 0 : mCRL2log(log::verbose) << algorithms::print_removed_equations(V);
1032 0 : }
1033 0 : break;
1034 0 : }
1035 0 : default:
1036 : { }
1037 : }
1038 0 : }
1039 :
1040 : } // namespace pbes_system
1041 :
1042 : } // namespace mcrl2
1043 :
1044 : #endif // MCRL2_PBES_CONSTELM_H
|