mCRL2
Loading...
Searching...
No Matches
simplify_rewriter.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_PBES_REWRITERS_SIMPLIFY_REWRITER_H
13#define MCRL2_PBES_REWRITERS_SIMPLIFY_REWRITER_H
14
16
17namespace mcrl2 {
18
19namespace pbes_system {
20
21namespace detail {
22
23template <template <class> class Builder, class Derived>
24struct add_simplify: public Builder<Derived>
25{
26 typedef Builder<Derived> super;
27 using super::apply;
28
29 template <class T>
30 void apply(T& result, const not_& x)
31 {
32 assert(&result!=&x); // Result is used as temporary store and cannot match x.
33 apply(result, x.operand());
34 if (is_false(result))
35 {
36 result = true_();
37 return;
38 }
39 if (is_true(result))
40 {
41 result = false_();
42 return;
43 }
44 if (is_not(result))
45 {
46 result = atermpp::down_cast<not_>(result).operand();
47 return;
48 }
49 make_not_(result, result);
50 }
51
52 template <class T>
53 void apply(T& result, const and_& x)
54 {
55 assert(&result!=&x); // Result is used as temporary store and cannot match x.
56 apply(result, x.left());
57 if (is_false(result))
58 {
59 result = false_();
60 return;
61 }
62 if (is_true(result))
63 {
64 apply(result, x.right());
65 return;
66 }
67 pbes_expression right;
68 apply(right, x.right());
69 if (is_false(right))
70 {
71 result = false_();
72 return;
73 }
74 if (is_true(right) || result==right)
75 {
76 return;
77 }
78 make_and_(result,result, right);
79 }
80
81 template <class T>
82 void apply(T& result, const or_& x)
83 {
84 assert(&result!=&x); // Result is used as temporary store and cannot match x.
85 apply(result, x.left());
86 if (is_true(result))
87 {
88 result = true_();
89 return;
90 }
91 if (is_false(result))
92 {
93 apply(result, x.right());
94 return;
95 }
96 pbes_expression right;
97 apply(right, x.right());
98 if (is_true(right))
99 {
100 result = true_();
101 return;
102 }
103 if (is_false(right) || result==right)
104 {
105 return;
106 }
107 make_or_(result,result, right);
108 }
109
110 template <class T>
111 void apply(T& result, const imp& x)
112 {
113 assert(&result!=&x); // Result is used as temporary store and cannot match x.
114 if (is_false(x.left())) // This test is cheap.
115 {
116 result = true_();
117 return;
118 }
119 apply(result, x.right());
120 if (is_true(result))
121 {
122 result = true_();
123 return;
124 }
125 if (is_false(result))
126 {
127 apply(result, x.left());
128 if (is_not(result))
129 {
130 result = atermpp::down_cast<not_>(result).operand();
131 return;
132 }
133 if (is_true(result))
134 {
135 result = false_();
136 return;
137 }
138 if (is_false(result))
139 {
140 result = true_();
141 return;
142 }
143 make_not_(result, result);
144 return;
145 }
146 pbes_expression left;
147 apply(left, x.left());
148 if (is_true(left))
149 {
150 return;
151 }
152 if (is_false(left) || result==left)
153 {
154 result = true_();
155 return;
156 }
157 make_imp(result, left, result);
158 }
159
160 template <class T>
161 void apply(T& result, const forall& x)
162 {
163 apply(result, x.body());
164 data::optimized_forall(result, x.variables(), result, true);
165 }
166
167 template <class T>
168 void apply(T& result, const exists& x)
169 {
170 apply(result, x.body());
171 data::optimized_exists(result, x.variables(), result, true);
172 }
173};
174
175template <typename Derived>
176struct simplify_builder: public add_simplify<pbes_system::pbes_expression_builder, Derived>
177{ };
178
179template <typename Derived, typename DataRewriter, typename SubstitutionFunction>
180struct 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 simplify_data_rewriter_builder(const DataRewriter& R, SubstitutionFunction& sigma)
184 : super(R, sigma)
185 {}
186};
187
188} // namespace detail
189
192{
195
197 {
198 pbes_expression result;
199 core::make_apply_builder<detail::simplify_builder>().apply(result, x);
200 return result;
201 }
202
203 void operator()(pbes_expression& result, const pbes_expression& x) const
204 {
205 core::make_apply_builder<detail::simplify_builder>().apply(result, x);
206 }
207};
208
210template <typename DataRewriter>
212{
215
216 const DataRewriter& R;
217
218 explicit simplify_data_rewriter(const DataRewriter& R_)
219 : R(R_)
220 {}
221
223 {
225 pbes_expression result;
226 detail::make_apply_rewriter_builder<pbes_system::detail::simplify_data_rewriter_builder>(R, sigma).apply(result,x);
227 return result;
228 }
229
230 template <typename SubstitutionFunction>
231 pbes_expression operator()(const pbes_expression& x, SubstitutionFunction& sigma) const
232 {
233 pbes_expression result;
234 detail::make_apply_rewriter_builder<pbes_system::detail::simplify_data_rewriter_builder>(R, sigma).apply(result, x);
235 return result;
236 }
237
238 template <typename SubstitutionFunction>
239 void operator()(pbes_expression& result, const pbes_expression& x, SubstitutionFunction& sigma) const
240 {
241 detail::make_apply_rewriter_builder<pbes_system::detail::simplify_data_rewriter_builder>(R, sigma).apply(result, x);
242 }
243};
244
245} // namespace pbes_system
246
247} // namespace mcrl2
248
249#endif // MCRL2_PBES_REWRITERS_SIMPLIFY_REWRITER_H
\brief A data variable
Definition variable.h:28
\brief The and operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
\brief The existential quantification operator for pbes expressions
const data::variable_list & variables() const
const pbes_expression & body() const
\brief The universal quantification operator for pbes expressions
const pbes_expression & body() const
const data::variable_list & variables() const
\brief The implication operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
\brief The not operator for pbes expressions
const pbes_expression & operand() const
\brief The or operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
void optimized_exists(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make an existential quantification.
void optimized_forall(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make a universal quantification.
const pbes_expression & true_()
void make_or_(atermpp::aterm_appl &t, const ARGUMENTS &... args)
bool is_not(const atermpp::aterm_appl &x)
void make_imp(atermpp::aterm_appl &t, const ARGUMENTS &... args)
bool is_false(const pbes_expression &t)
Test for the value false.
void make_and_(atermpp::aterm_appl &t, const ARGUMENTS &... args)
void make_not_(atermpp::aterm_appl &t, const ARGUMENTS &... args)
bool is_true(const pbes_expression &t)
Test for the value true.
const pbes_expression & false_()
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
add your file description here.
An empty struct that is used to denote the absence of a substitution. Used for rewriters.
void apply(T &result, const forall &x)
void apply(T &result, const exists &x)
void apply(T &result, const or_ &x)
void apply(T &result, const not_ &x)
void apply(T &result, const and_ &x)
simplify_data_rewriter_builder(const DataRewriter &R, SubstitutionFunction &sigma)
add_data_rewriter< pbes_system::detail::simplify_builder, Derived, DataRewriter, SubstitutionFunction > super
A rewriter that simplifies boolean expressions in a term, and rewrites data expressions.
pbes_expression operator()(const pbes_expression &x) const
pbes_expression operator()(const pbes_expression &x, SubstitutionFunction &sigma) const
void operator()(pbes_expression &result, const pbes_expression &x, SubstitutionFunction &sigma) const
A rewriter that simplifies boolean expressions in a term.
void operator()(pbes_expression &result, const pbes_expression &x) const
pbes_expression operator()(const pbes_expression &x) const