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/detail/stategraph_simplify_rewriter.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_STATEGRAPH_SIMPLIFY_REWRITER_H
13 : #define MCRL2_PBES_DETAIL_STATEGRAPH_SIMPLIFY_REWRITER_H
14 :
15 : #include "mcrl2/data/consistency.h"
16 : #include "mcrl2/data/rewriters/simplify_rewriter.h"
17 : #include "mcrl2/pbes/detail/stategraph_split.h"
18 : #include "mcrl2/pbes/rewriters/simplify_quantifiers_rewriter.h"
19 :
20 : namespace mcrl2 {
21 :
22 : namespace pbes_system {
23 :
24 : namespace detail {
25 :
26 : inline
27 0 : pbes_expression stategraph_not(const pbes_expression& x)
28 : {
29 0 : if (is_data(x))
30 : {
31 0 : auto const& x1 = atermpp::down_cast<data::data_expression>(x);
32 0 : if (data::is_not(x1))
33 : {
34 0 : return data::unary_operand1(x1);
35 : }
36 0 : else if (data::is_not_equal_to(x1))
37 : {
38 0 : auto const& left = data::binary_left1(x1);
39 0 : auto const& right = data::binary_right1(x1);
40 0 : return data::equal_to(left, right);
41 : }
42 0 : else if (data::is_equal_to(x1))
43 : {
44 0 : auto const& left = data::binary_left1(x1);
45 0 : auto const& right = data::binary_right1(x1);
46 0 : return data::not_equal_to(left, right);
47 : }
48 : else
49 : {
50 0 : return data::not_(x1);
51 : }
52 : }
53 0 : return not_(x);
54 : }
55 :
56 : inline
57 0 : pbes_expression smart_and(const pbes_expression& x, const pbes_expression& y)
58 : {
59 0 : if (is_data(x) && is_data(y))
60 : {
61 0 : return data::and_(atermpp::down_cast<data::data_expression>(x), atermpp::down_cast<data::data_expression>(y));
62 : }
63 0 : return and_(x, y);
64 : }
65 :
66 : inline
67 0 : pbes_expression smart_or(const pbes_expression& x, const pbes_expression& y)
68 : {
69 0 : if (is_data(x) && is_data(y))
70 : {
71 0 : return data::or_(atermpp::down_cast<data::data_expression>(x), atermpp::down_cast<data::data_expression>(y));
72 : }
73 0 : return or_(x, y);
74 : }
75 :
76 : template <typename Derived, typename DataRewriter, typename SubstitutionFunction>
77 : struct stategraph_simplify_builder: public simplify_quantifiers_data_rewriter_builder<Derived, DataRewriter, SubstitutionFunction>
78 : {
79 : typedef simplify_quantifiers_data_rewriter_builder<Derived, DataRewriter, SubstitutionFunction> super;
80 : using super::apply;
81 :
82 : /// \brief Constructor.
83 : /// \param rewr A data rewriter
84 108 : stategraph_simplify_builder(const DataRewriter& R, SubstitutionFunction& sigma)
85 108 : : super(R, sigma)
86 108 : { }
87 :
88 0 : Derived& derived()
89 : {
90 0 : return static_cast<Derived&>(*this);
91 : }
92 :
93 : // returns the argument of a not expression (pbes or data)
94 0 : const pbes_expression& not_arg(const pbes_expression& x)
95 : {
96 0 : if (is_data(x))
97 : {
98 0 : return atermpp::down_cast<pbes_expression>(*data::application(x).begin());
99 : }
100 : else
101 : {
102 0 : return atermpp::down_cast<not_>(x).operand();
103 : }
104 : }
105 :
106 0 : pbes_expression stategraph_join_or(const std::vector<pbes_expression>& terms) const
107 : {
108 0 : const pbes_expression& F = false_();
109 0 : return utilities::detail::join(terms.begin(), terms.end(), smart_or, F);
110 : }
111 :
112 0 : pbes_expression stategraph_join_and(const std::vector<pbes_expression>& terms) const
113 : {
114 0 : const pbes_expression& T = true_();
115 0 : return utilities::detail::join(terms.begin(), terms.end(), smart_and, T);
116 : }
117 :
118 : // apply de Morgan rules
119 110 : pbes_expression post_process(const pbes_expression& x)
120 : {
121 110 : pbes_expression result = x;
122 :
123 110 : if (is_universal_not(x))
124 : {
125 0 : const pbes_expression& arg = not_arg(x);
126 :
127 : // replace !(x1 \/ ... \/ xn) by !x1 /\ ... /\ !xn
128 0 : if (is_universal_or(arg))
129 : {
130 0 : std::vector<pbes_expression> terms;
131 0 : detail::stategraph_split_or(arg, terms);
132 0 : for (pbes_expression& term: terms)
133 : {
134 0 : term = stategraph_not(term);
135 : }
136 0 : result = stategraph_join_and(terms);
137 0 : }
138 : // replace !(x1 /\ ... /\ xn) by !x1 \/ ... \/ !xn
139 0 : else if (is_universal_and(arg))
140 : {
141 0 : std::vector<pbes_expression> terms;
142 0 : detail::stategraph_split_and(arg, terms);
143 0 : for (pbes_expression& term: terms)
144 : {
145 0 : term = stategraph_not(term);
146 : }
147 0 : result = stategraph_join_or(terms);
148 0 : }
149 : else
150 : {
151 0 : result = stategraph_not(arg);
152 : }
153 : }
154 110 : mCRL2log(log::trace) << " simplify-postprocess " << x << " -> " << result << std::endl;
155 110 : return result;
156 0 : }
157 :
158 : template <class T>
159 109 : void apply(T& result, const data::data_expression& x)
160 : {
161 109 : super::apply(result, data::simplify(x));
162 109 : result = post_process(result);
163 109 : }
164 :
165 : template <class T>
166 0 : void apply(T& result, const not_& x)
167 : {
168 0 : super::apply(result, x);
169 0 : result = post_process(result);
170 0 : }
171 :
172 : template <class T>
173 1 : void apply(T& result, const and_& x)
174 : {
175 :
176 1 : super::apply(result, x);
177 1 : result = post_process(result);
178 1 : }
179 :
180 : template <class T>
181 0 : void apply(T& result, const or_& x)
182 : {
183 0 : super::apply(result, x);
184 0 : result = post_process(result);
185 0 : }
186 :
187 : template <class T>
188 0 : void apply(T& result, const imp& x)
189 : {
190 0 : derived().apply(result, or_(not_(x.left()), x.right()));
191 0 : }
192 :
193 : template <class T>
194 0 : void apply(T& result, const forall& x)
195 : {
196 0 : super::apply(result, x);
197 0 : result = post_process(result);
198 0 : }
199 :
200 : template <class T>
201 0 : void apply(T& result, const exists& x)
202 : {
203 0 : super::apply(result, x);
204 0 : result = post_process(result);
205 0 : }
206 :
207 : template <class T>
208 0 : void apply(T& result, const propositional_variable_instantiation& x)
209 : {
210 0 : super::apply(result, x);
211 0 : result = post_process(result);
212 0 : }
213 : };
214 :
215 : /// \brief A rewriter that simplifies expressions that simplifies quantifiers.
216 : template <typename DataRewriter>
217 : class stategraph_simplify_rewriter
218 : {
219 : protected:
220 : /// \brief The data rewriter
221 : const DataRewriter& m_rewriter;
222 :
223 : public:
224 : /// \brief The term type
225 : typedef pbes_expression term_type;
226 :
227 : /// \brief The variable type
228 : typedef data::variable variable_type;
229 :
230 : /// \brief Constructor
231 : /// \param rewriter A data rewriter
232 108 : stategraph_simplify_rewriter(const DataRewriter& rewriter)
233 108 : : m_rewriter(rewriter)
234 108 : {}
235 :
236 : /// \brief Rewrites a pbes expression.
237 : /// \param x A term
238 : /// \return The rewrite result.
239 108 : pbes_expression operator()(const pbes_expression& x) const
240 : {
241 : data::no_substitution sigma;
242 108 : pbes_expression result;
243 108 : detail::make_apply_rewriter_builder<stategraph_simplify_builder>(m_rewriter, sigma).apply(result, x);
244 216 : return result;
245 0 : }
246 :
247 : /// \brief Rewrites a pbes expression.
248 : /// \param x A term
249 : /// \param sigma A substitution function
250 : /// \return The rewrite result.
251 : template <typename SubstitutionFunction>
252 : pbes_expression operator()(const pbes_expression& x, SubstitutionFunction& sigma) const
253 : {
254 : pbes_expression result;
255 : detail::make_apply_rewriter_builder<stategraph_simplify_builder>(m_rewriter, sigma).apply(result, x);
256 : return result;
257 : }
258 : };
259 :
260 : } // namespace detail
261 :
262 : } // namespace pbes_system
263 :
264 : } // namespace mcrl2
265 :
266 : #endif // MCRL2_PBES_DETAIL_STATEGRAPH_SIMPLIFY_REWRITER_H
|
