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