Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/pbes/rewriters/simplify_quantifiers_rewriter.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_REWRITERS_SIMPLIFY_QUANTIFIERS_REWRITER_H
13 : #define MCRL2_PBES_REWRITERS_SIMPLIFY_QUANTIFIERS_REWRITER_H
14 :
15 : #include "mcrl2/pbes/rewriters/simplify_rewriter.h"
16 :
17 : namespace mcrl2 {
18 :
19 : namespace pbes_system {
20 :
21 : namespace detail {
22 :
23 : template <template <class> class Builder, class Derived>
24 : struct add_simplify_quantifiers: public Builder<Derived>
25 : {
26 : typedef Builder<Derived> super;
27 : using super::apply;
28 :
29 : template <class T>
30 104 : void apply(T& result, const forall& x)
31 : {
32 104 : pbes_expression body;
33 104 : super::apply(body, x.body());
34 104 : const data::variable_list& variables = x.variables();
35 :
36 104 : if (variables.empty())
37 : {
38 0 : result = true_();
39 : }
40 104 : else if (is_not(body))
41 : {
42 0 : data::optimized_exists(result, variables, atermpp::down_cast<not_>(body).operand(), true);
43 0 : data::optimized_not(result, result);
44 : }
45 104 : if (is_and(body))
46 : {
47 9 : auto const& left = atermpp::down_cast<and_>(body).left();
48 9 : auto const& right = atermpp::down_cast<and_>(body).right();
49 9 : data::optimized_forall(result, variables, left, true);
50 9 : pbes_expression result_right;
51 9 : data::optimized_forall(result_right, variables, right, true);
52 9 : data::optimized_and(result, result, result_right);
53 9 : }
54 95 : else if (is_or(body))
55 : {
56 64 : auto const& left = atermpp::down_cast<or_>(body).left();
57 64 : auto const& right = atermpp::down_cast<or_>(body).right();
58 64 : data::variable_list lv = data::detail::set_intersection(variables, free_variables(left));
59 64 : data::variable_list rv = data::detail::set_intersection(variables, free_variables(right));
60 64 : if (lv.empty())
61 : {
62 55 : data::optimized_forall_no_empty_domain(result, rv, right, true);
63 55 : data::optimized_or(result, left, result);
64 : }
65 9 : else if (rv.empty())
66 : {
67 3 : data::optimized_forall_no_empty_domain(result, lv, left, true);
68 3 : data::optimized_or(result, result, right);
69 : }
70 : else
71 : {
72 6 : data::optimized_forall(result, variables, body, true);
73 : }
74 64 : }
75 : else
76 : {
77 31 : data::optimized_forall(result, variables, body, true);
78 : }
79 104 : }
80 :
81 : template <class T>
82 268 : void apply(T& result, const exists& x)
83 : {
84 268 : pbes_expression body;
85 268 : super::apply(body, x.body());
86 268 : const data::variable_list& variables = x.variables();
87 :
88 268 : if (variables.empty())
89 : {
90 0 : result = false_();
91 : }
92 268 : else if (is_not(body))
93 : {
94 0 : data::optimized_forall(result, variables, atermpp::down_cast<not_>(body).operand(), true);
95 0 : data::optimized_not(result, result);
96 : }
97 268 : if (is_or(body))
98 : {
99 9 : auto const& left = atermpp::down_cast<or_>(body).left();
100 9 : auto const& right = atermpp::down_cast<or_>(body).right();
101 9 : data::optimized_exists(result, variables, left, true);
102 9 : pbes_expression result_right;
103 9 : data::optimized_exists(result_right, variables, right, true);
104 9 : data::optimized_or(result, result, result_right);
105 9 : }
106 259 : else if (is_and(body))
107 : {
108 64 : auto const& left = atermpp::down_cast<and_>(body).left();
109 64 : auto const& right = atermpp::down_cast<and_>(body).right();
110 64 : data::variable_list lv = data::detail::set_intersection(variables, free_variables(left));
111 64 : data::variable_list rv = data::detail::set_intersection(variables, free_variables(right));
112 64 : if (lv.empty())
113 : {
114 20 : data::optimized_exists_no_empty_domain(result, rv, right, true);
115 20 : data::optimized_and(result, left, result);
116 : }
117 44 : else if (rv.empty())
118 : {
119 3 : data::optimized_exists_no_empty_domain(result, lv, left, true);
120 3 : data::optimized_and(result, right, result);
121 : }
122 : else
123 : {
124 41 : data::optimized_exists(result, variables, body, true);
125 : }
126 64 : }
127 : else
128 : {
129 195 : data::optimized_exists(result, variables, body, true);
130 : }
131 268 : }
132 : };
133 :
134 : template <typename Derived>
135 : struct simplify_quantifiers_builder: public add_simplify_quantifiers<pbes_system::detail::simplify_builder, Derived>
136 : { };
137 :
138 : template <typename Derived, typename DataRewriter, typename SubstitutionFunction>
139 : struct simplify_quantifiers_data_rewriter_builder: public add_data_rewriter<pbes_system::detail::simplify_quantifiers_builder, Derived, DataRewriter, SubstitutionFunction>
140 : {
141 : typedef add_data_rewriter<pbes_system::detail::simplify_quantifiers_builder, Derived, DataRewriter, SubstitutionFunction> super;
142 : using super::enter;
143 : using super::leave;
144 :
145 753 : simplify_quantifiers_data_rewriter_builder(const DataRewriter& R, SubstitutionFunction& sigma)
146 753 : : super(R, sigma)
147 753 : {}
148 : };
149 :
150 : } // namespace detail
151 :
152 : /// \brief A rewriter that simplifies boolean expressions and quantifiers.
153 : struct simplify_quantifiers_rewriter
154 : {
155 : typedef pbes_expression term_type;
156 : typedef data::variable variable_type;
157 :
158 0 : pbes_expression operator()(const pbes_expression& x) const
159 : {
160 0 : pbes_expression result;
161 0 : core::make_apply_builder<detail::simplify_quantifiers_builder>().apply(result, x);
162 0 : return result;
163 0 : }
164 : };
165 :
166 : /// \brief A rewriter that simplifies boolean expressions and quantifiers, and rewrites data expressions.
167 : template <typename DataRewriter>
168 : struct simplify_quantifiers_data_rewriter
169 : {
170 : typedef pbes_expression term_type;
171 : typedef data::variable variable_type;
172 :
173 : const DataRewriter& R;
174 :
175 146 : simplify_quantifiers_data_rewriter(const DataRewriter& R_)
176 146 : : R(R_)
177 146 : {}
178 :
179 645 : pbes_expression operator()(const pbes_expression& x) const
180 : {
181 : data::no_substitution sigma;
182 645 : pbes_expression result;
183 645 : detail::make_apply_rewriter_builder<detail::simplify_quantifiers_data_rewriter_builder>(R, sigma).apply(result, x);
184 1290 : return result;
185 0 : }
186 :
187 : template <typename SubstitutionFunction>
188 : pbes_expression operator()(const pbes_expression& x, SubstitutionFunction& sigma) const
189 : {
190 : pbes_expression result;
191 : detail::make_apply_rewriter_builder<detail::simplify_quantifiers_data_rewriter_builder>(R, sigma).apply(result, x);
192 : return result;
193 : }
194 : };
195 :
196 : } // namespace pbes_system
197 :
198 : } // namespace mcrl2
199 :
200 : #endif // MCRL2_PBES_REWRITERS_SIMPLIFY_QUANTIFIERS_REWRITER_H
|
