mCRL2
Loading...
Searching...
No Matches
constelm.h
Go to the documentation of this file.
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//
9
10#ifndef MCRL2_PBES_CONSTELM_H
11#define MCRL2_PBES_CONSTELM_H
12
15#include "mcrl2/pbes/print.h"
16#include "mcrl2/pbes/replace.h"
18
19namespace mcrl2
20{
21
22namespace pbes_system
23{
24
25namespace detail
26{
27
28inline
29void make_constelm_substitution(const std::map<data::variable, data::data_expression>& m, data::rewriter::substitution_type& result)
30{
31 for (const auto& i : m)
32 {
33 result[i.first] = i.second;
34 }
35}
36
38{
39protected:
42
43public:
46 , m_var(var)
47 {}
48
49 bool is_forall() const
50 {
51 return m_is_forall;
52 }
53
54 const data::variable& variable() const
55 {
56 return m_var;
57 }
58
59 bool operator==(const quantified_variable& other) const
60 {
61 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 bool operator<(const quantified_variable& other) const
70 {
71 return m_is_forall < other.m_is_forall || (m_is_forall == other.m_is_forall && m_var < other.m_var);
72 }
73
75 {
77 }
78
79 std::string to_string() const
80 {
81 std::ostringstream out;
82 out << (is_forall() ? "forall " : "exists ") << variable() << ". ";
83 return out.str();
84 }
85};
86
88struct QPVI
89{
90 std::list<quantified_variable> Q;
92
93 bool operator<(const QPVI& other) const
94 {
95 return std::tie(Q, X_e) < std::tie(other.Q, other.X_e);
96 }
97};
98
100{
103 std::set<data::data_expression> conditions;
107 std::set<data::variable> conjunctive_context_FV;
111 std::set<data::variable> disjunctive_context_FV;
112};
113
115{
116 typedef std::multimap<QPVI, edge_details> edge_map;
117
120 std::set<data::variable> FV;
122
123 edge_traverser_stack_elem(const data::data_expression& cond_pos, const data::data_expression& cond_neg, std::set<data::variable>&& free_vars)
124 : Cpos(cond_pos), Cneg(cond_neg)
125 {
126 std::swap(FV, free_vars);
127 }
128};
129
130struct edge_condition_traverser: public pbes_expression_traverser<edge_condition_traverser>
131{
133 using super::enter;
134 using super::leave;
135 using super::apply;
136
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 void push(const stack_elem& x)
145 {
146 condition_fv_stack.push_back(x);
147 }
148
150 {
151 return condition_fv_stack.back();
152 }
153
154 const stack_elem& top() const
155 {
156 return condition_fv_stack.back();
157 }
158
160 {
162 condition_fv_stack.pop_back();
163 return result;
164 }
165
166 // N.B. As a side effect ec1 and ec2 are changed!!!
167 void merge_conditions(stack_elem& ec1, bool negate1,
168 stack_elem& ec2, bool negate2,
169 stack_elem& ec, bool is_conjunctive
170 )
171 {
172 for (auto& i: ec1.edges)
173 {
174 auto& [Q_X_e, details] = i;
175 details.conditions.insert(negate2 ? ec2.Cneg : ec2.Cpos);
176 (is_conjunctive ? details.conjunctive_context_FV : details.disjunctive_context_FV)
177 .insert(ec2.FV.begin(), ec2.FV.end());
178 ec.edges.insert(i);
179 }
180 for (auto& i: ec2.edges)
181 {
182 auto& [Q_X_e, details] = i;
183 details.conditions.insert(negate1 ? ec1.Cneg : ec1.Cpos);
184 (is_conjunctive ? details.conjunctive_context_FV : details.disjunctive_context_FV)
185 .insert(ec1.FV.begin(), ec1.FV.end());
186 ec.edges.insert(i);
187 }
188 }
189
190 // enter functions related to maintaining the quantfier scope
191 void enter(const not_&)
192 {
193 quantified_context.clear();
194 }
195
196 void enter(const and_&)
197 {
198 quantified_context.clear();
199 }
200
201 void enter(const or_&)
202 {
203 quantified_context.clear();
204 }
205
206 void enter(const imp&)
207 {
208 quantified_context.clear();
209 }
210
211 void enter(const forall& x)
212 {
213 quantified_context.push_back(x);
214 }
215
216 void enter(const exists& x)
217 {
218 quantified_context.push_back(x);
219 }
220
221 // leave functions, mostly used to build conditions and gather free variables
223 {
224 data::data_expression cond_not;
225 data::optimized_not(cond_not, x);
226
227 push(stack_elem(x, cond_not, data::find_free_variables(x)));
228 }
229
230 void leave(const not_&)
231 {
232 std::swap(top().Cpos, top().Cneg);
233 }
234
235 void leave(const and_&)
236 {
237 stack_elem ec_right = pop();
238 stack_elem ec_left = pop();
239 data::data_expression cond_and;
240 data::data_expression cond_or;
241 data::optimized_and(cond_and, ec_left.Cpos, ec_right.Cpos);
242 data::optimized_or(cond_or, ec_left.Cneg, ec_right.Cneg);
243
244 stack_elem ec(cond_and, cond_or,
245 utilities::detail::set_union(ec_left.FV, ec_right.FV));
246 merge_conditions(ec_left, false, ec_right, false, ec, true);
247 push(ec);
248 }
249
250 void leave(const or_&)
251 {
252 stack_elem ec_right = pop();
253 stack_elem ec_left = pop();
254 data::data_expression cond_and;
255 data::data_expression cond_or;
256
257 data::optimized_and(cond_and, ec_left.Cneg, ec_right.Cneg);
258 data::optimized_or(cond_or, ec_left.Cpos, ec_right.Cpos);
259
260 stack_elem ec(cond_or, cond_and,
261 utilities::detail::set_union(ec_left.FV, ec_right.FV));
262 merge_conditions(ec_left, true, ec_right, true, ec, false);
263 push(ec);
264 }
265
266 void leave(const imp&)
267 {
268 stack_elem ec_right = pop();
269 stack_elem ec_left = pop();
270 data::data_expression cond_or;
271 data::data_expression cond_and;
272
273 data::optimized_or(cond_or, ec_left.Cneg, ec_right.Cpos);
274 data::optimized_and(cond_and, ec_left.Cpos, ec_right.Cneg);
275
276 stack_elem ec(cond_or, cond_and,
277 utilities::detail::set_union(ec_left.FV, ec_right.FV));;
278 merge_conditions(ec_left, false, ec_right, true, ec, false);
279 push(ec);
280 }
281
282 void leave(const forall& x)
283 {
284 // build conditions and free variable sets
285 stack_elem ec = pop();
286 for (auto& [X_e, details]: ec.edges)
287 {
288 auto& [cond_set, conj_FV, disj_FV] = details;
289
290 // Update the conditions
291 std::set<data::data_expression> new_conditions;
292 for(const data::data_expression& e: cond_set)
293 {
295 data::optimized_exists(t, x.variables(), e, true);
296 new_conditions.insert(t);
297 }
298 cond_set = std::move(new_conditions);
301
302 cond_set.insert(forall);
303
304 // Update FV
305 conj_FV = ec.FV;
306 }
307 data::optimized_forall(ec.Cpos, x.variables(), ec.Cpos, true);
308 data::optimized_exists(ec.Cneg, x.variables(), ec.Cneg, true);
309 std::set<data::variable> bound_vars{x.variables().begin(), x.variables().end()};
310 ec.FV = utilities::detail::set_difference(ec.FV, bound_vars);
311 push(ec);
312
313 // maintain quantifier scope
314 if(!quantified_context.empty() && quantified_context.back() == x)
315 {
316 quantified_context.pop_back();
317 }
318 }
319
320 void leave(const exists& x)
321 {
322 // build conditions and free variable sets
323 stack_elem ec = pop();
324 for (auto& [X_e, details]: ec.edges)
325 {
326 auto& [cond_set, conj_FV, disj_FV] = details;
327
328 // Update the conditions
329 std::set<data::data_expression> new_conditions;
330 for(const data::data_expression& e: cond_set)
331 {
333 data::optimized_exists(t, x.variables(), e, true);
334 new_conditions.insert(t);
335 }
336 cond_set = std::move(new_conditions);
337
340 cond_set.insert(forall);
341
342 // Update FV
343 disj_FV = ec.FV;
344 }
345 data::optimized_exists(ec.Cpos, x.variables(), ec.Cpos, true);
346 data::optimized_forall(ec.Cneg, x.variables(), ec.Cneg, true);
347 std::set<data::variable> bound_vars{x.variables().begin(), x.variables().end()};
348 ec.FV = utilities::detail::set_difference(ec.FV, bound_vars);
349 push(ec);
350
351 // maintain quantifier scope
352 if(!quantified_context.empty() && quantified_context.back() == x)
353 {
354 quantified_context.pop_back();
355 }
356 }
357
359 {
360 // Build list of qvars from quantifier scope
361 qvar_list qvars;
362 for(const pbes_expression& expr: quantified_context)
363 {
364 assert(is_forall(expr) || is_exists(expr));
365 data::variable_list vars(is_forall(expr) ? atermpp::down_cast<forall>(expr).variables() : atermpp::down_cast<exists>(expr).variables());
366 for(const data::variable& v: vars)
367 {
368 qvars.emplace_back(is_forall(expr), v);
369 }
370 }
371 QPVI Q_X_e{qvars, x};
372
373 // Store the QPVI and the condition true
375 ec.edges.insert(std::make_pair(Q_X_e,
376 edge_details{std::set<data::data_expression>{data::sort_bool::true_()},
377 std::set<data::variable>{}, std::set<data::variable>{}}));
378 push(ec);
379 }
380
381 const edge_map& result() const
382 {
383 assert(condition_fv_stack.size() == 1);
384 return top().edges;
385 }
386};
387
388} // namespace detail
390
391
393template <typename DataRewriter, typename PbesRewriter>
395{
396 protected:
398 typedef std::map<data::variable, data::data_expression> constraint_map;
399 typedef std::list<detail::quantified_variable> qvar_list;
400
402 const DataRewriter& m_data_rewriter;
403
405 const PbesRewriter& m_pbes_rewriter;
406
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.
417 {
418 protected:
421
424
427
428 const std::set<data::variable> m_conj_context;
429 const std::set<data::variable> m_disj_context;
430
431 public:
433 edge() = default;
434
440 const propositional_variable& src,
441 const qvar_list& qvars,
443 const std::set<data::variable>& conj_context,
444 const std::set<data::variable>& disj_context,
446 )
447 : data::data_expression(c)
448 , m_source(src)
449 , m_qvars(qvars)
450 , m_target(tgt)
451 , m_conj_context(conj_context)
452 , m_disj_context(disj_context)
453 {}
454
457 std::string to_string() const
458 {
459 std::ostringstream out;
460 out << "(" << m_source.name() << ", " << m_target.name() << ") label = ";
462 {
463 out << qv.to_string();
464 }
465 out << m_target << " condition = " << condition();
466 return out.str();
467 }
468
471 {
472 return m_source;
473 }
474
476 {
477 return m_qvars;
478 }
479
482 {
483 return m_target;
484 }
485
488 {
489 return *this;
490 }
491
495 {
496 qvar_list result;
497 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 if (( it->is_forall() && m_disj_context.find(it->variable()) == m_disj_context.end()) ||
502 (!it->is_forall() && m_conj_context.find(it->variable()) == m_conj_context.end()))
503 {
504 result.push_front(*it);
505 }
506 else
507 {
508 break;
509 }
510 }
511 return result;
512 }
513 };
514
516 class vertex
517 {
518 protected:
521
524
526 // present in this map, it means that it represents NaC ("not a constant").
528
530 bool m_visited = false;
531
535 bool is_constant(const data::variable& v) const
536 {
537 auto i = m_constraints.find(v);
538 return i != m_constraints.end();
539 }
540
543 {
544 std::set<data::variable> free_vars = data::find_free_variables(e);
545 return std::all_of(free_vars.begin(), free_vars.end(), [&](const data::variable& v)
546 {
547 return std::find_if(qvars.begin(), qvars.end(), [&](const detail::quantified_variable& qvar){ return qvar.variable() == v; }) != qvars.end();
548 });
549 }
550
554 void fix_constraints(std::vector<data::data_expression> deleted_constraints)
555 {
556 while (!deleted_constraints.empty())
557 {
558 std::set<data::variable> vars_deleted;
559 for (const data::data_expression& fi: deleted_constraints)
560 {
561 data::find_free_variables(fi, std::inserter(vars_deleted, vars_deleted.end()));
562 }
563 deleted_constraints.clear();
564
565 auto del_i = std::find_if(m_qvars.rbegin(), m_qvars.rend(), [&](const detail::quantified_variable& qv)
566 {
567 return vars_deleted.find(qv.variable()) != vars_deleted.end();
568 });
569 // Remove quantified variables up to and including del_i
570 m_qvars.erase(m_qvars.begin(), del_i.base());
571
572 for (const data::variable& par: m_variable.parameters())
573 {
574 auto k = m_constraints.find(par);
575 if(k == m_constraints.end())
576 {
577 continue;
578 }
579 if(!bound_in_quantifiers(m_qvars, k->second))
580 {
581 deleted_constraints.push_back(k->second);
582 m_constraints.erase(k);
583 }
584 }
585 }
586 }
587
588 public:
590 vertex() = default;
591
595 : m_variable(x)
596 {}
597
600 {
601 return m_variable;
602 }
603
605 {
606 return m_qvars;
607 }
608
612 {
613 return m_constraints;
614 }
615
618 std::vector<std::size_t> constant_parameter_indices() const
619 {
620 std::vector<std::size_t> result;
621 std::size_t index = 0;
622 for (const data::variable& parameter: m_variable.parameters())
623 {
624 if (is_constant(parameter))
625 {
626 result.push_back(index);
627 }
628 index++;
629 }
630 return result;
631 }
632
635 std::string to_string() const
636 {
637 std::ostringstream out;
638 out << m_variable << " assertions = ";
639 for(const detail::quantified_variable& v: quantified_variables())
640 {
641 out << v.to_string();
642 }
643 for (const auto& constraint: m_constraints)
644 {
645 out << "{" << constraint.first << " := " << constraint.second << "} ";
646 }
647 return out.str();
648 }
649
652 bool update(const qvar_list& qvars, const data::data_expression_list& e, const constraint_map& e_constraints, const DataRewriter& datar)
653 {
654 bool changed = false;
655
656 data::variable_list params = m_variable.parameters();
659
660 if (!m_visited)
661 {
662 m_visited = true;
663 changed = true;
664
665 m_qvars = qvars;
666 // Partition expressions in e based on whether their free variables
667 // are bound in m_qvars.
668 std::vector<data::data_expression> deleted_constraints;
669 auto par = params.begin();
670 for (auto i = e.begin(); i != e.end(); ++i, ++par)
671 {
672 data::data_expression e1 = datar(*i, sigma);
673 if (bound_in_quantifiers(m_qvars, e1))
674 {
675 m_constraints[*par] = e1;
676 }
677 else
678 {
679 deleted_constraints.push_back(e1);
680 }
681 }
682 fix_constraints(deleted_constraints);
683 }
684 else
685 {
686 // Find longest common suffix of qvars
687 auto mismatch_it = std::mismatch(m_qvars.rbegin(), m_qvars.rend(), qvars.rbegin(), qvars.rend()).first;
688 changed |= mismatch_it != m_qvars.rend();
689 // Remove the outer quantifiers, up to and including mismatch_it
690 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 std::vector<data::data_expression> deleted_constraints;
695 auto i = e.begin();
696 for (auto par = params.begin(); i != e.end(); ++i, ++par)
697 {
698 auto k = m_constraints.find(*par);
699 if(k == m_constraints.end())
700 {
701 continue;
702 }
703 const data::data_expression& fi = k->second;
704 data::data_expression ei = datar(*i, sigma);
705 if (fi != ei || !bound_in_quantifiers(m_qvars, fi))
706 {
707 changed = true;
708 deleted_constraints.push_back(fi);
709 deleted_constraints.push_back(ei);
710 m_constraints.erase(k);
711 }
712 }
713 fix_constraints(deleted_constraints);
714 }
715 return changed;
716 }
717 };
718
720 typedef std::map<core::identifier_string, vertex> vertex_map;
721
723 typedef std::map<core::identifier_string, std::vector<edge> > edge_map;
724
728
732
734 std::map<core::identifier_string, std::vector<std::size_t> > m_redundant_parameters;
735
737 std::string print_vertices() const
738 {
739 std::ostringstream out;
740 for (const auto& v: m_vertices)
741 {
742 out << v.second.to_string() << std::endl;
743 }
744 return out.str();
745 }
746
748 std::string print_edges()
749 {
750 std::ostringstream out;
751 for (const auto& source: m_edges)
752 {
753 for (const auto& e: source.second)
754 {
755 out << e.to_string() << std::endl;
756 }
757 }
758 return out.str();
759 }
760
761 std::string print_todo_list(const std::deque<propositional_variable>& todo)
762 {
763 std::ostringstream out;
764 out << "\n<todo list> [";
765 for (auto i = todo.begin(); i != todo.end(); ++i)
766 {
767 if (i != todo.begin())
768 {
769 out << ", ";
770 }
771 out << core::pp(i->name());
772 }
773 out << "]" << std::endl;
774 return out.str();
775 }
776
777 std::string print_edge_update(const edge& e, const vertex& u, const vertex& v)
778 {
779 std::ostringstream out;
780 out << "\n<updating edge> " << e.to_string() << std::endl;
781 out << " <source vertex > " << u.to_string() << std::endl;
782 out << " <target vertex before> " << v.to_string() << std::endl;
783 return out.str();
784 }
785
786 std::string print_condition(const edge& e, const vertex& u, const pbes_expression& value)
787 {
788 std::ostringstream out;
791 out << " <condition > " << e.condition() << sigma << " to " << value << std::endl;
792 return out.str();
793 }
794
795 std::string print_evaluation_failure(const edge& e, const vertex& u)
796 {
797 std::ostringstream out;
800 out << "\nCould not evaluate condition " << e.condition() << sigma << " to true or false";
801 return out.str();
802 }
803
804 template <typename E>
805 std::list<E> concat(const std::list<E> a, const std::list<E> b)
806 {
807 std::list<E> result(a);
808 result.insert(result.end(), b.begin(), b.end());
809 return result;
810 }
811
812 public:
813
817 pbes_constelm_algorithm(const DataRewriter& datar, const PbesRewriter& pbesr)
818 : m_data_rewriter(datar), m_pbes_rewriter(pbesr)
819 {}
820
823 std::map<propositional_variable, std::vector<data::variable> > redundant_parameters() const
824 {
825 std::map<propositional_variable, std::vector<data::variable> > result;
826 for (const std::pair<const core::identifier_string, std::vector<std::size_t>>& red_pair: m_redundant_parameters)
827 {
828 const vertex& v = m_vertices.find(red_pair.first)->second;
829 std::vector<data::variable>& variables = result[v.variable()];
830 for (const std::size_t par: red_pair.second)
831 {
833 std::advance(k, par);
834 variables.push_back(*k);
835 }
836 }
837 return result;
838 }
839
844 void run(pbes& p, bool compute_conditions = false, bool check_quantifiers = true)
845 {
846 m_vertices.clear();
847 m_edges.clear();
848 m_redundant_parameters.clear();
849
850 // compute the vertices and edges of the dependency graph
851 for (pbes_equation& eqn: p.equations())
852 {
853 core::identifier_string name = eqn.variable().name();
854 m_vertices[name] = vertex(eqn.variable());
855
856 // use an edge_condition_traverser to compute the edges
858 f.apply(eqn.formula());
859
860 std::vector<edge>& edges = m_edges[name];
861 for (const auto& [Q_X_e, details]: f.result())
862 {
863 const auto& [Q, X_e] = Q_X_e;
864 const auto& [conditions, conj_FV, disj_FV] = details;
865
866 // check options for quantifiers and conditions.
867 qvar_list quantifier_list = check_quantifiers ? Q : qvar_list();
868 data::data_expression condition = compute_conditions
869 ? data::lazy::join_and(conditions.begin(), conditions.end())
871
872 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
878 std::deque<propositional_variable> todo;
879 const data::data_expression_list& e_init = init.parameters();
880 vertex& u_init = m_vertices[init.name()];
881 u_init.update(qvar_list(), e_init, constraint_map(), m_data_rewriter);
882 todo.push_back(u_init.variable());
883
884 mCRL2log(log::debug) << "\n--- initial vertices ---\n" << print_vertices();
885 mCRL2log(log::debug) << "\n--- edges ---\n" << print_edges();
886
887 // propagate constraints over the edges until the todo list is empty
888 while (!todo.empty())
889 {
890 mCRL2log(log::debug) << print_todo_list(todo);
891 propositional_variable var = todo.front();
892
893 // remove all occurrences of var from todo
894 todo.erase(std::remove(todo.begin(), todo.end(), var), todo.end());
895
896 const vertex& u = m_vertices[var.name()];
897 const std::vector<edge>& u_edges = m_edges[var.name()];
898
899 for (const edge& e: u_edges)
900 {
901 vertex& v = m_vertices[e.target().name()];
902 mCRL2log(log::debug) << print_edge_update(e, u, v);
903
906 pbes_expression needs_update = m_pbes_rewriter(e.condition(), sigma);
907 mCRL2log(log::debug) << print_condition(e, u, needs_update);
908
909 if (!is_false(needs_update) && !is_true(needs_update))
910 {
911 mCRL2log(log::debug) << print_evaluation_failure(e, u);
912 }
913 if (!is_false(needs_update))
914 {
915 bool changed = v.update(
916 concat(e.quantifier_inside_approximation(u.quantified_variables()), e.quantified_variables()),
917 e.target().parameters(),
918 u.constraints(),
919 m_data_rewriter);
920 if (changed)
921 {
922 todo.push_back(v.variable());
923 }
924 }
925 mCRL2log(log::debug) << " <target vertex after > " << v.to_string() << "\n";
926 }
927 }
928
929 mCRL2log(log::debug) << "\n--- final vertices ---\n" << print_vertices();
930
931 // compute the redundant parameters and the redundant equations
932 for (const pbes_equation& eqn: p.equations())
933 {
934 core::identifier_string name = eqn.variable().name();
935 const vertex& v = m_vertices[name];
936 if (!v.constraints().empty())
937 {
938 std::vector<std::size_t> r = v.constant_parameter_indices();
939 if (!r.empty())
940 {
941 m_redundant_parameters[name] = r;
942 }
943 }
944 }
945
946 // Apply the constraints to the equations.
947 for (pbes_equation& eqn: p.equations())
948 {
949 core::identifier_string name = eqn.variable().name();
950 const vertex& v = m_vertices[name];
951
952 if (!v.constraints().empty())
953 {
957 for (auto i = v.quantified_variables().crbegin(); i != v.quantified_variables().crend(); ++i)
958 {
959 body = i->make_expr(body);
960 }
961 eqn = pbes_equation(
962 eqn.symbol(),
963 eqn.variable(),
964 body
965 );
966 }
967 }
968
969 // remove the redundant parameters
970 pbes_system::algorithms::remove_parameters(p, m_redundant_parameters);
971
972 // print the parameters and equation that are removed
973 if (mCRL2logEnabled(log::verbose))
974 {
975 mCRL2log(log::verbose) << "\nremoved the following constant parameters:" << std::endl;
976 for (const std::pair<const propositional_variable, std::vector<data::variable>>& i: redundant_parameters())
977 {
978 for (const data::variable& var: i.second)
979 {
980 mCRL2log(log::verbose) << " (" << mcrl2::core::pp(i.first.name()) << ", " << data::pp(var) << ")" << std::endl;
981 }
982 }
983 }
984 }
985};
986
993inline
994void 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 data::rewriter datar(p.data(), rewrite_strategy);
1004
1005 // pbes rewriter
1006 switch (rewriter_type)
1007 {
1008 case simplify:
1009 {
1010 typedef simplify_data_rewriter<data::rewriter> pbes_rewriter;
1011 pbes_rewriter pbesr(datar);
1013 algorithm.run(p, compute_conditions, check_quantifiers);
1014 if (remove_redundant_equations)
1015 {
1016 std::vector<propositional_variable> V = algorithms::remove_unreachable_variables(p);
1017 mCRL2log(log::verbose) << algorithms::print_removed_equations(V);
1018 }
1019 break;
1020 }
1021 case quantifier_all:
1022 case quantifier_finite:
1023 {
1024 bool enumerate_infinite_sorts = (rewriter_type == quantifier_all);
1025 enumerate_quantifiers_rewriter pbesr(datar, p.data(), enumerate_infinite_sorts);
1027 algorithm.run(p, compute_conditions, check_quantifiers);
1028 if (remove_redundant_equations)
1029 {
1030 std::vector<propositional_variable> V = algorithms::remove_unreachable_variables(p);
1031 mCRL2log(log::verbose) << algorithms::print_removed_equations(V);
1032 }
1033 break;
1034 }
1035 default:
1036 { }
1037 }
1038}
1039
1040} // namespace pbes_system
1041
1042} // namespace mcrl2
1043
1044#endif // MCRL2_PBES_CONSTELM_H
Term containing a string.
Iterator for term_list.
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const Term & front() const
Returns the first element of the list.
Definition aterm_list.h:239
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
data_expression()
\brief Default constructor X3.
Rewriter that operates on data expressions.
Definition rewriter.h:81
basic_rewriter< data_expression >::substitution_type substitution_type
Definition rewriter.h:114
\brief A data variable
Definition variable.h:28
\brief The and operator for pbes expressions
const data::variable & variable() const
Definition constelm.h:54
pbes_expression make_expr(const pbes_expression &expr) const
Definition constelm.h:74
bool operator<(const quantified_variable &other) const
Definition constelm.h:69
quantified_variable(bool is_forall, const data::variable &var)
Definition constelm.h:44
bool operator==(const quantified_variable &other) const
Definition constelm.h:59
bool operator!=(const quantified_variable &other) const
Definition constelm.h:64
\brief The existential quantification operator for pbes expressions
const data::variable_list & variables() const
\brief The universal quantification operator for pbes expressions
const data::variable_list & variables() const
\brief The implication operator for pbes expressions
\brief The not operator for pbes expressions
\brief The or operator for pbes expressions
Represents an edge of the dependency graph. The assignments are stored implicitly using the 'right' p...
Definition constelm.h:417
edge(const propositional_variable &src, const qvar_list &qvars, const propositional_variable_instantiation &tgt, const std::set< data::variable > &conj_context, const std::set< data::variable > &disj_context, data::data_expression c=data::sort_bool::true_())
Constructor.
Definition constelm.h:439
const propositional_variable_instantiation & target() const
The propositional variable instantiation that determines the target of the edge.
Definition constelm.h:481
qvar_list quantifier_inside_approximation(const qvar_list &Q) const
Try to guess which quantifiers of Q can end up directly before target, when the quantifier inside rew...
Definition constelm.h:494
const propositional_variable_instantiation m_target
The propositional variable instantiation that determines the target of the edge.
Definition constelm.h:426
const qvar_list & quantified_variables() const
Definition constelm.h:475
const qvar_list m_qvars
The quantifiers in whose direct context the target PVI occurs.
Definition constelm.h:423
const propositional_variable m_source
The propositional variable at the source of the edge.
Definition constelm.h:420
const std::set< data::variable > m_disj_context
Definition constelm.h:429
const data::data_expression & condition() const
The condition of the edge.
Definition constelm.h:487
const std::set< data::variable > m_conj_context
Definition constelm.h:428
const propositional_variable & source() const
The propositional variable at the source of the edge.
Definition constelm.h:470
std::string to_string() const
Returns a string representation of the edge.
Definition constelm.h:457
Represents a vertex of the dependency graph.
Definition constelm.h:517
void fix_constraints(std::vector< data::data_expression > deleted_constraints)
Weaken the constraints so they satisfy.
Definition constelm.h:554
qvar_list m_qvars
The list of quantified variables that occur in the constraints.
Definition constelm.h:523
std::string to_string() const
Returns a string representation of the vertex.
Definition constelm.h:635
bool update(const qvar_list &qvars, const data::data_expression_list &e, const constraint_map &e_constraints, const DataRewriter &datar)
Assign new values to the parameters of this vertex, and update the constraints accordingly....
Definition constelm.h:652
constraint_map m_constraints
Maps data variables to data expressions. If a parameter is not.
Definition constelm.h:527
bool m_visited
Indicates whether this vertex has been visited at least once.
Definition constelm.h:530
const constraint_map & constraints() const
Maps data variables to data expressions. If the right hand side is a data variable,...
Definition constelm.h:611
bool is_constant(const data::variable &v) const
Returns true if the parameter v has been assigned a constant expression.
Definition constelm.h:535
propositional_variable m_variable
The propositional variable that corresponds to the vertex.
Definition constelm.h:520
std::vector< std::size_t > constant_parameter_indices() const
Returns the indices of the constant parameters of this vertex.
Definition constelm.h:618
const propositional_variable & variable() const
The propositional variable that corresponds to the vertex.
Definition constelm.h:599
bool bound_in_quantifiers(const qvar_list &qvars, const data::data_expression &e)
Returns true iff all free variables in e are bound in qvars.
Definition constelm.h:542
vertex(propositional_variable x)
Constructor.
Definition constelm.h:594
Algorithm class for the constelm algorithm.
Definition constelm.h:395
const PbesRewriter & m_pbes_rewriter
Compares data expressions for equality.
Definition constelm.h:405
std::string print_todo_list(const std::deque< propositional_variable > &todo)
Definition constelm.h:761
vertex_map m_vertices
The vertices of the dependency graph. They are stored in a map, to support searching for a vertex.
Definition constelm.h:727
std::string print_edge_update(const edge &e, const vertex &u, const vertex &v)
Definition constelm.h:777
std::map< propositional_variable, std::vector< data::variable > > redundant_parameters() const
Returns the parameters that have been removed by the constelm algorithm.
Definition constelm.h:823
std::string print_edges()
Logs the edges of the dependency graph.
Definition constelm.h:748
pbes_constelm_algorithm(const DataRewriter &datar, const PbesRewriter &pbesr)
Constructor.
Definition constelm.h:817
std::map< core::identifier_string, std::vector< edge > > edge_map
The storage type for edges.
Definition constelm.h:723
std::map< core::identifier_string, std::vector< std::size_t > > m_redundant_parameters
The redundant parameters.
Definition constelm.h:734
std::list< E > concat(const std::list< E > a, const std::list< E > b)
Definition constelm.h:805
std::string print_evaluation_failure(const edge &e, const vertex &u)
Definition constelm.h:795
std::map< core::identifier_string, vertex > vertex_map
The storage type for vertices.
Definition constelm.h:720
std::list< detail::quantified_variable > qvar_list
Definition constelm.h:399
std::map< data::variable, data::data_expression > constraint_map
A map with constraints on the vertices of the graph.
Definition constelm.h:398
const DataRewriter & m_data_rewriter
Compares data expressions for equality.
Definition constelm.h:402
void run(pbes &p, bool compute_conditions=false, bool check_quantifiers=true)
Runs the constelm algorithm.
Definition constelm.h:844
edge_map m_edges
The edges of the dependency graph. They are stored in a map, to easily access all out-edges correspon...
Definition constelm.h:731
std::string print_condition(const edge &e, const vertex &u, const pbes_expression &value)
Definition constelm.h:786
std::string print_vertices() const
Logs the vertices of the dependency graph.
Definition constelm.h:737
parameterized boolean equation system
Definition pbes.h:58
const data::data_specification & data() const
Returns the data specification.
Definition pbes.h:150
const propositional_variable_instantiation & initial_state() const
Returns the initial state.
Definition pbes.h:192
const std::vector< pbes_equation > & equations() const
Returns the equations.
Definition pbes.h:164
\brief A propositional variable instantiation
const data::data_expression_list & parameters() const
\brief A propositional variable declaration
const data::variable_list & parameters() const
const core::identifier_string & name() const
MCRL2_EXPORT bool init(rewriter_interface *i, RewriterCompilingJitty *this_rewriter)
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
std::string pp(const identifier_string &x)
Definition core.cpp:26
data_expression join_and(ForwardTraversalIterator first, ForwardTraversalIterator last)
Returns and applied to the sequence of data expressions [first, last)
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
void optimized_exists(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make an existential quantification.
void optimized_or(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
rewrite_strategy
The strategy of the rewriter.
std::string pp(const abstraction &x)
Definition data.cpp:39
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
void optimized_not(Term &result, const Term &arg)
Make a negation.
void optimized_and(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
void optimized_forall(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make a universal quantification.
@ verbose
Definition logger.h:35
void remove_parameters(pbes &x, const std::set< data::variable > &to_be_removed)
Removes parameters from propositional variable instantiations in a pbes expression.
void make_constelm_substitution(const std::map< data::variable, data::data_expression > &m, data::rewriter::substitution_type &result)
Definition constelm.h:29
bool is_conjunctive(const pbes_expression &phi)
Definition srf_pbes.h:523
pbes_rewriter_type
An enumerated type for the available pbes rewriters.
bool is_exists(const atermpp::aterm &x)
bool is_constant(const pbes_expression &x)
bool is_forall(const atermpp::aterm &x)
bool is_false(const pbes_expression &t)
Test for the value false.
void replace_free_variables(T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
Definition replace.h:182
bool is_true(const pbes_expression &t)
Test for the value true.
std::set< T > set_union(const std::set< T > &x, const std::set< T > &y)
Returns the union of two sets.
std::set< T > set_difference(const std::set< T > &x, const std::set< T > &y)
Returns the difference of two sets.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
void swap(atermpp::unprotected_aterm_core &t1, atermpp::unprotected_aterm_core &t2) noexcept
Swaps two aterms.
Definition aterm.h:462
add your file description here.
add your file description here.
add your file description here.
add your file description here.
add your file description here.
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:323
A quantified predicate variable instantiation.
Definition constelm.h:89
std::list< quantified_variable > Q
Definition constelm.h:90
propositional_variable_instantiation X_e
Definition constelm.h:91
bool operator<(const QPVI &other) const
Definition constelm.h:93
pbes_expression_traverser< edge_condition_traverser > super
Definition constelm.h:132
void leave(const propositional_variable_instantiation &x)
Definition constelm.h:358
std::list< detail::quantified_variable > qvar_list
Definition constelm.h:139
void merge_conditions(stack_elem &ec1, bool negate1, stack_elem &ec2, bool negate2, stack_elem &ec, bool is_conjunctive)
Definition constelm.h:167
std::list< pbes_expression > quantified_context
Definition constelm.h:142
void leave(const data::data_expression &x)
Definition constelm.h:222
std::set< data::variable > disjunctive_context_FV
The set of free variables that occur on the other side of the conjunctions this PVI occurs in....
Definition constelm.h:111
std::set< data::variable > conjunctive_context_FV
The set of free variables that occur on the other side of the conjunctions this PVI occurs in....
Definition constelm.h:107
std::set< data::data_expression > conditions
Contains expressions that characterise when an edge is enabled. The conjunction of these expressions ...
Definition constelm.h:103
std::multimap< QPVI, edge_details > edge_map
Definition constelm.h:116
edge_traverser_stack_elem(const data::data_expression &cond_pos, const data::data_expression &cond_neg, std::set< data::variable > &&free_vars)
Definition constelm.h:123
A rewriter that simplifies boolean expressions in a term, and rewrites data expressions.