mCRL2
Loading...
Searching...
No Matches
standard_utility.h
Go to the documentation of this file.
1// Author(s): Jeroen van der Wulp
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_STANDARD_UTILITY_H
13#define MCRL2_DATA_STANDARD_UTILITY_H
14
15#include <queue>
16
17#include "mcrl2/data/real.h"
19
20namespace mcrl2
21{
22
23namespace data
24{
25
26namespace sort_bool
27{
30inline data_expression bool_(bool b)
31{
32 return (b) ? sort_bool::true_() : sort_bool::false_();
33}
34
38{
41}
42} // namespace sort_bool
43
46inline
47bool
49{
53}
54
62namespace lazy
63{
68{
69 if (p == sort_bool::true_())
70 {
71 return sort_bool::false_();
72 }
73 else if (p == sort_bool::false_())
74 {
75 return sort_bool::true_();
76 }
77
78 return sort_bool::not_(p);
79}
80
86{
87 if ((p == sort_bool::true_()) || (q == sort_bool::true_()))
88 {
89 return sort_bool::true_();
90 }
91 else if ((p == q) || (p == sort_bool::false_()))
92 {
93 return q;
94 }
95 else if (q == sort_bool::false_())
96 {
97 return p;
98 }
99
100 return sort_bool::or_(p, q);
101}
102
108{
109 if ((p == sort_bool::false_()) || (q == sort_bool::false_()))
110 {
111 return sort_bool::false_();
112 }
113 else if ((p == q) || (p == sort_bool::true_()))
114 {
115 return q;
116 }
117 else if (q == sort_bool::true_())
118 {
119 return p;
120 }
121
122 return sort_bool::and_(p, q);
123}
124
130{
131 if ((p == sort_bool::false_()) || (q == sort_bool::true_()) || (p == q))
132 {
133 return sort_bool::true_();
134 }
135 else if (p == sort_bool::true_())
136 {
137 return q;
138 }
139 else if (q == sort_bool::false_())
140 {
141 return sort_bool::not_(p);
142 }
143
144 return sort_bool::implies(p, q);
145}
146
152{
153 if (p == q)
154 {
155 return sort_bool::true_();
156 }
157
158 return data::equal_to(p, q);
159}
160
166{
167 if (p == q)
168 {
169 return sort_bool::false_();
170 }
171
172 return data::not_equal_to(p, q);
173}
174
177inline data_expression if_(const data_expression& cond, const data_expression& then, const data_expression& else_)
178{
179 if (cond == sort_bool::true_() || then == else_)
180 {
181 return then;
182 }
183 else if (cond == sort_bool::false_())
184 {
185 return else_;
186 }
187
188 return data::if_(cond, then, else_);
189}
190
195template < typename ForwardTraversalIterator >
196inline data_expression join_or(ForwardTraversalIterator first, ForwardTraversalIterator last)
197{
198 return utilities::detail::join(first, last, lazy::or_, static_cast< data_expression const& >(sort_bool::false_()));
199}
200
205template < typename ForwardTraversalIterator >
206inline data_expression join_and(ForwardTraversalIterator first, ForwardTraversalIterator last)
207{
208 return utilities::detail::join(first, last, lazy::and_, static_cast< data_expression const& >(sort_bool::true_()));
209}
210} // namespace lazy
211
212
214inline std::list<data_expression> split_disjunction(const data_expression& condition)
215{
216 std::list<data_expression> clauses;
217
218 std::queue<data_expression> todo;
219 todo.push(condition);
220
221 while (!todo.empty())
222 {
223 const data::data_expression& expr = todo.front();
224 todo.pop();
225
227 {
228 const auto& appl = static_cast<application>(expr);
229 todo.push(appl[0]);
230 todo.push(appl[1]);
231 }
232 else
233 {
234 clauses.push_front(expr);
235 }
236 }
237
238 return clauses;
239}
240
242inline std::list<data_expression> split_conjunction(const data_expression& condition)
243{
244 std::list<data_expression> clauses;
245
246 std::queue<data_expression> todo;
247 todo.push(condition);
248
249 while (!todo.empty())
250 {
251 const data_expression& expr = todo.front();
252 todo.pop();
253
255 {
256 const auto& appl = static_cast<application>(expr);
257 todo.push(appl[0]);
258 todo.push(appl[1]);
259 }
260 else
261 {
262 clauses.push_front(expr);
263 }
264 }
265
266 return clauses;
267}
268
269} // namespace data
270
271} // namespace mcrl2
272
273#endif
274
An application of a data expression to a number of arguments.
\brief A sort expression
data_expression implies(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p implies q.
data_expression join_and(ForwardTraversalIterator first, ForwardTraversalIterator last)
Returns and applied to the sequence of data expressions [first, last)
data_expression not_(data_expression const &p)
Returns an expression equivalent to not p.
data_expression equal_to(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p == q.
data_expression not_equal_to(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p == q.
data_expression and_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p or q.
data_expression or_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p and q.
data_expression join_or(ForwardTraversalIterator first, ForwardTraversalIterator last)
Returns or applied to the sequence of data expressions [first, last)
data_expression if_(const data_expression &cond, const data_expression &then, const data_expression &else_)
Returns an expression equivalent to if(cond,then,else_)
bool is_false_function_symbol(const atermpp::aterm &e)
Recogniser for function false.
Definition bool.h:119
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
Definition bool.h:345
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:54
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
const function_symbol & implies()
Constructor for function symbol =>.
Definition bool.h:363
bool is_boolean_constant(data_expression const &b)
Determines whether b is a Boolean constant.
const function_symbol & and_()
Constructor for function symbol &&.
Definition bool.h:235
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:281
const function_symbol & or_()
Constructor for function symbol ||.
Definition bool.h:299
bool is_true_function_symbol(const atermpp::aterm &e)
Recogniser for function true.
Definition bool.h:87
const function_symbol & not_()
Constructor for function symbol !.
Definition bool.h:173
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
bool is_int(const sort_expression &e)
Recogniser for sort expression Int.
Definition int1.h:57
bool is_nat(const sort_expression &e)
Recogniser for sort expression Nat.
Definition nat1.h:56
bool is_pos(const sort_expression &e)
Recogniser for sort expression Pos.
Definition pos1.h:55
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:58
bool is_structured_sort(const atermpp::aterm &x)
Returns true if the term t is a structured sort.
function_symbol not_equal_to(const sort_expression &s)
Constructor for function symbol !=.
Definition standard.h:163
bool is_system_defined(const sort_expression &s)
Returns true iff the expression represents a standard sort.
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
std::list< data_expression > split_disjunction(const data_expression &condition)
Split a disjunctive expression into a set of clauses.
std::list< data_expression > split_conjunction(const data_expression &condition)
Split a disjunctive expression into a set of clauses.
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:200
T join(FwdIt first, FwdIt last, BinaryOperation op, T empty_sequence_result)
Given a sequence [t1, t2, ..., tn] of elements of type T, returns op(t1, op(t2, .....
Definition join.h:55
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
The standard sort real_.
Generic join and split functions.