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_rewriter.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_REWRITERS_SIMPLIFY_REWRITER_H
13 : #define MCRL2_PBES_REWRITERS_SIMPLIFY_REWRITER_H
14 :
15 : #include "mcrl2/pbes/rewriters/data_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: public Builder<Derived>
25 : {
26 : typedef Builder<Derived> super;
27 : using super::apply;
28 :
29 : template <class T>
30 10 : void apply(T& result, const not_& x)
31 : {
32 10 : assert(&result!=&x); // Result is used as temporary store and cannot match x.
33 10 : apply(result, x.operand());
34 10 : if (is_false(result))
35 : {
36 4 : result = true_();
37 4 : return;
38 : }
39 6 : if (is_true(result))
40 : {
41 3 : result = false_();
42 3 : return;
43 : }
44 3 : if (is_not(result))
45 : {
46 1 : result = atermpp::down_cast<not_>(result).operand();
47 1 : return;
48 : }
49 2 : make_not_(result, result);
50 : }
51 :
52 : template <class T>
53 27868 : void apply(T& result, const and_& x)
54 : {
55 27868 : assert(&result!=&x); // Result is used as temporary store and cannot match x.
56 27868 : apply(result, x.left());
57 27868 : if (is_false(result))
58 : {
59 3278 : result = false_();
60 23284 : return;
61 : }
62 24590 : if (is_true(result))
63 : {
64 12627 : apply(result, x.right());
65 12627 : return;
66 : }
67 11963 : pbes_expression right;
68 11963 : apply(right, x.right());
69 11963 : if (is_false(right))
70 : {
71 415 : result = false_();
72 415 : return;
73 : }
74 11548 : if (is_true(right) || result==right)
75 : {
76 6964 : return;
77 : }
78 4584 : make_and_(result,result, right);
79 11963 : }
80 :
81 : template <class T>
82 27652 : void apply(T& result, const or_& x)
83 : {
84 27652 : assert(&result!=&x); // Result is used as temporary store and cannot match x.
85 27652 : apply(result, x.left());
86 27652 : if (is_true(result))
87 : {
88 17311 : result = true_();
89 25651 : return;
90 : }
91 10341 : if (is_false(result))
92 : {
93 7269 : apply(result, x.right());
94 7269 : return;
95 : }
96 3072 : pbes_expression right;
97 3072 : apply(right, x.right());
98 3072 : if (is_true(right))
99 : {
100 353 : result = true_();
101 353 : return;
102 : }
103 2719 : if (is_false(right) || result==right)
104 : {
105 718 : return;
106 : }
107 2001 : make_or_(result,result, right);
108 3072 : }
109 :
110 : template <class T>
111 14 : void apply(T& result, const imp& x)
112 : {
113 14 : assert(&result!=&x); // Result is used as temporary store and cannot match x.
114 14 : if (is_false(x.left())) // This test is cheap.
115 : {
116 5 : result = true_();
117 13 : return;
118 : }
119 9 : apply(result, x.right());
120 9 : if (is_true(result))
121 : {
122 0 : result = true_();
123 0 : return;
124 : }
125 9 : if (is_false(result))
126 : {
127 0 : apply(result, x.left());
128 0 : if (is_not(result))
129 : {
130 0 : result = atermpp::down_cast<not_>(result).operand();
131 0 : return;
132 : }
133 0 : if (is_true(result))
134 : {
135 0 : result = false_();
136 0 : return;
137 : }
138 0 : if (is_false(result))
139 : {
140 0 : result = true_();
141 0 : return;
142 : }
143 0 : make_not_(result, result);
144 0 : return;
145 : }
146 9 : pbes_expression left;
147 9 : apply(left, x.left());
148 9 : if (is_true(left))
149 : {
150 6 : return;
151 : }
152 3 : if (is_false(left) || result==left)
153 : {
154 2 : result = true_();
155 2 : return;
156 : }
157 1 : make_imp(result, left, result);
158 9 : }
159 :
160 : template <class T>
161 32 : void apply(T& result, const forall& x)
162 : {
163 32 : apply(result, x.body());
164 32 : data::optimized_forall(result, x.variables(), result, true);
165 32 : }
166 :
167 : template <class T>
168 30 : void apply(T& result, const exists& x)
169 : {
170 30 : apply(result, x.body());
171 30 : data::optimized_exists(result, x.variables(), result, true);
172 30 : }
173 : };
174 :
175 : template <typename Derived>
176 : struct simplify_builder: public add_simplify<pbes_system::pbes_expression_builder, Derived>
177 : { };
178 :
179 : template <typename Derived, typename DataRewriter, typename SubstitutionFunction>
180 : struct simplify_data_rewriter_builder : public add_data_rewriter < pbes_system::detail::simplify_builder, Derived, DataRewriter, SubstitutionFunction >
181 : {
182 : typedef add_data_rewriter < pbes_system::detail::simplify_builder, Derived, DataRewriter, SubstitutionFunction > super;
183 6200 : simplify_data_rewriter_builder(const DataRewriter& R, SubstitutionFunction& sigma)
184 6200 : : super(R, sigma)
185 6200 : {}
186 : };
187 :
188 : } // namespace detail
189 :
190 : /// \brief A rewriter that simplifies boolean expressions in a term.
191 : struct simplify_rewriter
192 : {
193 : typedef pbes_expression term_type;
194 : typedef data::variable variable_type;
195 :
196 3 : pbes_expression operator()(const pbes_expression& x) const
197 : {
198 3 : pbes_expression result;
199 3 : core::make_apply_builder<detail::simplify_builder>().apply(result, x);
200 3 : return result;
201 0 : }
202 :
203 0 : void operator()(pbes_expression& result, const pbes_expression& x) const
204 : {
205 0 : core::make_apply_builder<detail::simplify_builder>().apply(result, x);
206 0 : }
207 : };
208 :
209 : /// \brief A rewriter that simplifies boolean expressions in a term, and rewrites data expressions.
210 : template <typename DataRewriter>
211 : struct simplify_data_rewriter
212 : {
213 : typedef pbes_expression term_type;
214 : typedef data::variable variable_type;
215 :
216 : const DataRewriter& R;
217 :
218 232 : explicit simplify_data_rewriter(const DataRewriter& R_)
219 232 : : R(R_)
220 232 : {}
221 :
222 214 : pbes_expression operator()(const pbes_expression& x) const
223 : {
224 : data::no_substitution sigma;
225 214 : pbes_expression result;
226 214 : detail::make_apply_rewriter_builder<pbes_system::detail::simplify_data_rewriter_builder>(R, sigma).apply(result,x);
227 428 : return result;
228 0 : }
229 :
230 : template <typename SubstitutionFunction>
231 84 : pbes_expression operator()(const pbes_expression& x, SubstitutionFunction& sigma) const
232 : {
233 84 : pbes_expression result;
234 84 : detail::make_apply_rewriter_builder<pbes_system::detail::simplify_data_rewriter_builder>(R, sigma).apply(result, x);
235 84 : return result;
236 0 : }
237 :
238 : template <typename SubstitutionFunction>
239 9 : void operator()(pbes_expression& result, const pbes_expression& x, SubstitutionFunction& sigma) const
240 : {
241 9 : detail::make_apply_rewriter_builder<pbes_system::detail::simplify_data_rewriter_builder>(R, sigma).apply(result, x);
242 9 : }
243 : };
244 :
245 : } // namespace pbes_system
246 :
247 : } // namespace mcrl2
248 :
249 : #endif // MCRL2_PBES_REWRITERS_SIMPLIFY_REWRITER_H
|
