mCRL2
Loading...
Searching...
No Matches
if_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_DATA_REWRITERS_IF_REWRITER_H
13#define MCRL2_DATA_REWRITERS_IF_REWRITER_H
14
15#include "mcrl2/data/rewriter.h"
16#include "mcrl2/data/builder.h"
18#include "mcrl2/data/standard.h"
19
20namespace mcrl2 {
21
22namespace data {
23
24namespace detail {
25
26// Returns f(x0, ..., x_i-1, y, x_i+1, ..., xn)
27inline
28application replace_argument(const application& x, std::size_t i, const data_expression& y)
29{
30 std::size_t j = 0;
31 return application(x.head(), x.begin(), x.end(), [&](const data_expression& x_i) { return (j++ == i+1) ? y : x_i; });
32}
33
34inline
36{
37 for (std::size_t i = 0; i < x.size(); i++)
38 {
39 if (is_if_application(x[i]))
40 {
41 const auto& x_i = atermpp::down_cast<application>(x[i]);
42 const data_expression& b = x_i[0];
43 const data_expression& t1 = x_i[1];
44 const data_expression& t2 = x_i[2];
46 }
47 }
48 return x;
49}
50
51template <typename Derived>
53{
55
56 using super::apply;
57
58 bool is_simple(const data_expression& x) const
59 {
60 return !is_and(x) && !is_or(x) && !is_imp(x) && !is_not(x) && !is_true(x) && !is_false(x);
61 }
62
64 {
65 if (is_true(b))
66 {
67 return t1;
68 }
69 else if (is_false(b))
70 {
71 return t2;
72 }
73 else if (is_and(b))
74 {
75 const data_expression& b1 = binary_left1(b);
76 const data_expression& b2 = binary_right1(b);
77 return if_(b1, if_(b2, t1, t2), t2);
78 }
79 else if (is_or(b))
80 {
81 const data_expression& b1 = binary_left1(b);
82 const data_expression& b2 = binary_right1(b);
83 return if_(b1, t1, if_(b2, t1, t2));
84 }
85 else if (is_imp(b))
86 {
87 const data_expression& b1 = binary_left1(b);
88 const data_expression& b2 = binary_right1(b);
89 return if_(b1, if_(b2, t1, t2), t1);
90 }
91 else if (is_not(b))
92 {
93 const data_expression& b1 = unary_operand1(b);
94 return if_(b1, t2, t1);
95 }
96 else
97 {
98 assert(is_simple(b));
99 if (t1 == t2)
100 {
101 return t1;
102 }
103 else if (is_if_application(t1))
104 {
105 const application& t1_ = atermpp::down_cast<application>(t1);
106 const data_expression& c = t1_[0];
107 const data_expression& u1 = t1_[1];
108 const data_expression& u2 = t1_[2];
109 if (b == c)
110 {
111 return apply_if(b, u1, t2);
112 }
113 else if (b > c) // use the aterm pointer comparison
114 {
115 assert(is_simple(c));
116 return apply_if(c, apply_if(b, u1, t2), apply_if(b, u2, t2));
117 }
118 else
119 {
120 return if_(b, t1, t2);
121 }
122 }
123 else if (is_if_application(t2))
124 {
125 const application& t2_ = atermpp::down_cast<application>(t2);
126 const data_expression& c = t2_[0];
127 const data_expression& u1 = t2_[1];
128 const data_expression& u2 = t2_[2];
129 if (b == c)
130 {
131 return apply_if(b, t1, u2);
132 }
133 else if (b > c) // use the aterm pointer comparison
134 {
135 assert(is_simple(c));
136 return apply_if(c, apply_if(b, t1, u1), apply_if(b, t1, u2));
137 }
138 else
139 {
140 return if_(b, t1, t2);
141 }
142 }
143 else
144 {
145 return if_(b, t1, t2);
146 }
147 }
148 }
149
150 template <class T>
151 void apply(T& result, const application& x)
152 {
153 if (is_if_application(x))
154 {
156 super::apply(b, x[0]);
158 super::apply(t1, x[1]);
160 super::apply(t2, x[2]);
161 result = apply_if(b, t1, t2);
162 }
163 else
164 {
165 super::apply(result, x);
166 result = push_if_outside(atermpp::down_cast<application>(result));
167 }
168 }
169};
170
171struct if_rewrite_with_rewriter_builder: public if_rewrite_builder<if_rewrite_with_rewriter_builder>
172{
174 using super::apply;
175 using super::apply_if;
176
178
180 {}
181
182 template <class T>
183 void apply(T& result, const application& x)
184 {
185 if (is_if_application(x))
186 {
188 super::apply(b, x[0]);
190 super::apply(t1, x[1]);
192 super::apply(t2, x[2]);
193 result = apply_if(b, t1, t2);
194 }
195 else
196 {
197 super::apply(result, x);
198 result = push_if_outside(atermpp::down_cast<application>(result));
199 }
200 result = rewr(result);
201 }
202};
203
204} // namespace detail
205
207{
210
212 {
213 data_expression result;
214 core::make_apply_builder<detail::if_rewrite_builder>().apply(result, x);
215 return result;
216 }
217};
218
219template <typename T>
220void if_rewrite(T& x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0)
221{
222 core::make_update_apply_builder<data::data_expression_builder>(if_rewriter()).update(x);
223}
224
225template <typename T>
226T if_rewrite(const T& x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = 0)
227{
228 T result;
229 core::make_update_apply_builder<data::data_expression_builder>(if_rewriter()).apply(result, x);
230 return result;
231}
232
233} // namespace data
234
235} // namespace mcrl2
236
237#endif // MCRL2_DATA_REWRITERS_IF_REWRITER_H
An application of a data expression to a number of arguments.
const_iterator end() const
Returns an iterator pointing past the last argument of the application.
const_iterator begin() const
Returns an iterator pointing to the first argument of the application.
const data_expression & head() const
Get the function at the head of this expression.
std::size_t size() const
Rewriter that operates on data expressions.
Definition rewriter.h:81
This file contains some functions that are present in all libraries except the data library....
add your file description here.
The class rewriter.
bool is_or(const application &x)
Definition print.h:179
bool is_and(const application &x)
Definition print.h:173
application replace_argument(const application &x, std::size_t i, const data_expression &y)
Definition if_rewriter.h:28
data_expression push_if_outside(const application &x)
Definition if_rewriter.h:35
void if_rewrite(T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
bool is_if_application(const DataExpression &e)
Recogniser for application of if.
Definition standard.h:232
bool is_false(const data_expression &x)
Test if x is false.
Definition consistency.h:37
bool is_not(const data_expression &x)
Test if x is a negation.
Definition consistency.h:45
bool is_true(const data_expression &x)
Test if x is true.
Definition consistency.h:29
bool is_imp(const data_expression &x)
Test if x is an implication.
Definition consistency.h:69
const data_expression & unary_operand1(const data_expression &x)
const data_expression & binary_right1(const data_expression &x)
const data_expression & binary_left1(const data_expression &x)
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:200
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Standard functions that are available for all sorts.
void apply(T &result, const data::variable &x)
Definition builder.h:443
bool is_simple(const data_expression &x) const
Definition if_rewriter.h:58
data_expression_builder< Derived > super
Definition if_rewriter.h:54
data_expression apply_if(const data_expression &b, const data_expression &t1, const data_expression &t2)
Definition if_rewriter.h:63
void apply(T &result, const application &x)
if_rewrite_builder< if_rewrite_with_rewriter_builder > super
void apply(T &result, const application &x)
data_expression operator()(const data_expression &x) const