mCRL2
Loading...
Searching...
No Matches
optimized_boolean_operators.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_OPTIMIZED_BOOLEAN_OPERATORS_H
13#define MCRL2_DATA_OPTIMIZED_BOOLEAN_OPERATORS_H
14
17
18namespace mcrl2
19{
20
21namespace data
22{
23
24namespace detail
25{
27template <typename TermTraits>
28inline
29void optimized_not(typename TermTraits::term_type& result,
30 const typename TermTraits::term_type& arg,
31 TermTraits)
32{
33 typedef TermTraits tr;
34
35 if (tr::is_true(arg))
36 {
37 result=tr::false_();
38 }
39 else if (tr::is_false(arg))
40 {
41 result=tr::true_();
42 }
43 else if (tr::is_not(arg))
44 {
45 result=tr::not_arg(arg);
46 }
47 else
48 {
49 tr::make_not_(result, arg);
50 }
51}
52
57template <typename TermTraits>
58inline
59void optimized_and(typename TermTraits::term_type& result,
60 const typename TermTraits::term_type& left,
61 const typename TermTraits::term_type& right,
62 TermTraits)
63{
64 typedef TermTraits tr;
65
66 if (tr::is_true(left))
67 {
68 result=right;
69 }
70 else if (tr::is_false(left))
71 {
72 result=tr::false_();
73 }
74 else if (tr::is_true(right))
75 {
76 result=left;
77 }
78 else if (tr::is_false(right))
79 {
80 result=tr::false_();
81 }
82 else if (left == right)
83 {
84 result=left;
85 }
86 else
87 {
88 tr::make_and_(result, left, right);
89 }
90}
91
92/* template <typename TermTraits>
93inline
94typename TermTraits::term_type optimized_and(const typename TermTraits::term_type& left, const typename TermTraits::term_type& right, TermTraits)
95{
96 typedef TermTraits tr;
97
98 if (tr::is_true(left))
99 {
100 return right;
101 }
102 else if (tr::is_false(left))
103 {
104 return tr::false_();
105 }
106 else if (tr::is_true(right))
107 {
108 return left;
109 }
110 else if (tr::is_false(right))
111 {
112 return tr::false_();
113 }
114 else if (left == right)
115 {
116 return left;
117 }
118 else
119 {
120 return tr::and_(left, right);
121 }
122} */
123
124
125
130template <typename TermTraits>
131inline
132void optimized_or(typename TermTraits::term_type& result,
133 const typename TermTraits::term_type& left,
134 const typename TermTraits::term_type& right, TermTraits)
135{
136 typedef TermTraits tr;
137
138 if (tr::is_true(left))
139 {
140 result=tr::true_();
141 }
142 else if (tr::is_false(left))
143 {
144 result=right;
145 }
146 else if (tr::is_true(right))
147 {
148 result=tr::true_();
149 }
150 else if (tr::is_false(right))
151 {
152 result=left;
153 }
154 else if (left == right)
155 {
156 result=left;
157 }
158 else
159 {
160 tr::make_or_(result, left, right);
161 }
162}
163
168template <typename TermTraits>
169inline
170void optimized_imp(typename TermTraits::term_type& result,
171 const typename TermTraits::term_type& left,
172 const typename TermTraits::term_type& right, TermTraits t)
173{
174 typedef TermTraits tr;
175
176 if (tr::is_true(left))
177 {
178 result=right;
179 }
180 else if (tr::is_false(left))
181 {
182 result=tr::true_();
183 }
184 else if (tr::is_true(right))
185 {
186 result=tr::true_();
187 }
188 else if (tr::is_false(right))
189 {
190 optimized_not(result,left, t);
191 }
192 else if (left == right)
193 {
194 result=tr::true_();
195 }
196 else
197 {
198 tr::make_imp(result, left, right);
199 }
200}
201
210template <typename TermTraits>
211inline
212void optimized_forall(typename TermTraits::term_type& result,
213 const typename TermTraits::variable_sequence_type& v,
214 const typename TermTraits::term_type& arg,
215 bool remove_variables,
216 bool empty_domain_allowed, TermTraits)
217{
218 typedef TermTraits tr;
219
220 if (v.empty())
221 {
222 if (empty_domain_allowed)
223 {
224 result = tr::true_();
225 }
226 else
227 {
228 result = arg;
229 }
230 }
231 else if (tr::is_true(arg))
232 {
233 result = tr::true_();
234 }
235 else if (tr::is_false(arg))
236 {
237 result = tr::false_();
238 }
239 else
240 {
241 if (remove_variables)
242 {
244 if (variables.empty())
245 {
246 result = arg;
247 }
248 else
249 {
250 tr::make_forall(result, variables, arg);
251 }
252 }
253 else
254 {
255 tr::make_forall(result, v, arg);
256 }
257 }
258}
259
268template <typename TermTraits>
269inline
270void optimized_exists(typename TermTraits::term_type& result,
271 const typename TermTraits::variable_sequence_type& v,
272 const typename TermTraits::term_type& arg,
273 bool remove_variables,
274 bool empty_domain_allowed,
275 TermTraits)
276{
277 typedef TermTraits tr;
278
279 if (v.empty())
280 {
281 if (empty_domain_allowed)
282 {
283 result = tr::false_();
284 }
285 else
286 {
287 result = arg;
288 }
289 }
290 else if (tr::is_true(arg))
291 {
292 result = tr::true_();
293 }
294 else if (tr::is_false(arg))
295 {
296 result = tr::false_();
297 }
298 else
299 {
300 if (remove_variables)
301 {
303 if (variables.empty())
304 {
305 result = arg;
306 }
307 else
308 {
309 result = tr::exists(variables, arg);
310 }
311 }
312 else
313 {
314 result = tr::exists(v, arg);
315 }
316 }
317}
318
327/* template <typename T1, typename T2, typename UnaryFunction, typename UnaryPredicate>
328inline
329T1 optimized_not(T1 arg, UnaryFunction not_, T2 true_, UnaryPredicate is_true, T2 false_, UnaryPredicate is_false)
330{
331 if (is_true(arg))
332 {
333 return false_;
334 }
335 else if (is_false(arg))
336 {
337 return true_;
338 }
339 else
340 {
341 return not_(arg);
342 }
343} */
344
354/* template <typename T1, typename T2, typename UnaryPredicate, typename BinaryFunction>
355inline
356T1 optimized_and(T1 left, T1 right, BinaryFunction and_, T2 true_, UnaryPredicate is_true, T2 false_, UnaryPredicate is_false)
357{
358 (void) true_; // Suppress a non used warning.
359 if (is_true(left))
360 {
361 return right;
362 }
363 else if (is_false(left))
364 {
365 return false_;
366 }
367 else if (is_true(right))
368 {
369 return left;
370 }
371 else if (is_false(right))
372 {
373 return false_;
374 }
375 else if (left == right)
376 {
377 return left;
378 }
379 else
380 {
381 return and_(left, right);
382 }
383} */
384
394/* template <typename T1, typename T2, typename UnaryPredicate, typename BinaryFunction>
395inline
396T1 optimized_or(T1 left, T1 right, BinaryFunction or_, T2 true_, UnaryPredicate is_true, T2 false_, UnaryPredicate is_false)
397{
398 (void) false_; // Suppress a non used variable warning.
399 if (is_true(left))
400 {
401 return true_;
402 }
403 else if (is_false(left))
404 {
405 return right;
406 }
407 else if (is_true(right))
408 {
409 return true_;
410 }
411 else if (is_false(right))
412 {
413 return left;
414 }
415 else if (left == right)
416 {
417 return left;
418 }
419 else
420 {
421 return or_(left, right);
422 }
423} */
424
435/* template <typename T1, typename T2, typename UnaryPredicate, typename UnaryFunction, typename BinaryFunction>
436inline
437T1 optimized_imp(T1 left, T1 right, BinaryFunction imp, UnaryFunction not_, T2 true_, UnaryPredicate is_true, T2 false_, UnaryPredicate is_false)
438{
439 (void)false_; // Suppress a non used variable warning.
440 if (is_true(left))
441 {
442 return right;
443 }
444 else if (is_false(left))
445 {
446 return true_;
447 }
448 else if (is_true(right))
449 {
450 return true_;
451 }
452 else if (is_false(right))
453 {
454 return not_(left);
455 }
456 else if (left == right)
457 {
458 return true_;
459 }
460 else
461 {
462 return imp(left, right);
463 }
464} */
465
475/* template <typename T1, typename T2, typename VariableSequence, typename UnaryPredicate, typename Forall>
476inline
477void optimized_forall(T1& result, VariableSequence v, T1 arg, Forall forall, T2 true_, UnaryPredicate is_true, T2 false_, UnaryPredicate is_false)
478{
479 if (is_true(arg))
480 {
481 result = true_;
482 }
483 else if (is_false(arg))
484 {
485 result = false_;
486 }
487 else
488 {
489 make_forall(result, v, arg);
490 }
491} */
492
502/* template <typename T1, typename T2, typename VariableSequence, typename UnaryPredicate, typename Exists>
503inline
504void optimized_exists(T1& result, VariableSequence v, T1 arg, Exists exists, T2 true_, UnaryPredicate is_true, T2 false_, UnaryPredicate is_false)
505{
506 if (is_true(arg))
507 {
508 result = true_;
509 }
510 else if (is_false(arg))
511 {
512 result = false_;
513 }
514 else
515 {
516 make_exists(result, v, arg);
517 }
518} */
519
520} // namespace detail
521
525template <typename Term>
526inline
527void optimized_not(Term& result, const Term& arg)
528{
530}
531
536template <typename Term>
537inline
538void optimized_and(Term& result, const Term& p, const Term& q)
539{
540 return detail::optimized_and(result, p, q, core::term_traits<Term>());
541}
542
547/* template <typename Term>
548inline
549Term optimized_and(const Term& p, const Term& q)
550{
551 return detail::optimized_and(p, q, core::term_traits<Term>());
552} */
553
558template <typename Term>
559inline
560void optimized_or(Term& result, const Term& p, const Term& q)
561{
563}
564
569template <typename Term>
570inline
571void optimized_imp(Term& result, const Term& p, const Term& q)
572{
574}
575
581template <typename Term, typename VariableSequence>
582inline
583void optimized_forall(Term& result, const VariableSequence& l, const Term& p, bool remove_variables = false)
584{
585 bool empty_domain_allowed = true;
586 detail::optimized_forall(result, l, p, remove_variables, empty_domain_allowed, core::term_traits<Term>());
587}
588
595template <typename Term, typename VariableSequence>
596inline
597void optimized_forall_no_empty_domain(Term& result, const VariableSequence& l, const Term& p, bool remove_variables = false)
598{
599 bool empty_domain_allowed = false;
600 detail::optimized_forall(result, l, p, remove_variables, empty_domain_allowed, core::term_traits<Term>());
601}
602
608template <typename Term, typename VariableSequence>
609inline
610void optimized_exists(Term& result, const VariableSequence& l, const Term& p, bool remove_variables = false)
611{
612 bool empty_domain_allowed = true;
613 detail::optimized_exists(result, l, p, remove_variables, empty_domain_allowed, core::term_traits<Term>());
614}
615
622template <typename Term, typename VariableSequence>
623inline
624void optimized_exists_no_empty_domain(Term& result, const VariableSequence& l, const Term& p, bool remove_variables = false)
625{
626 bool empty_domain_allowed = false;
627 detail::optimized_exists(result, l, p, remove_variables, empty_domain_allowed, core::term_traits<Term>());
628}
629
630} // namespace data
631
632} // namespace mcrl2
633
634#endif // MCRL2_DATA_OPTIMIZED_BOOLEAN_OPERATORS_H
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
add your file description here.
void optimized_forall(typename TermTraits::term_type &result, const typename TermTraits::variable_sequence_type &v, const typename TermTraits::term_type &arg, bool remove_variables, bool empty_domain_allowed, TermTraits)
Make a universal quantification.
void optimized_exists(typename TermTraits::term_type &result, const typename TermTraits::variable_sequence_type &v, const typename TermTraits::term_type &arg, bool remove_variables, bool empty_domain_allowed, TermTraits)
Make an existential quantification.
void optimized_or(typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)
Make a disjunction.
variable_list set_intersection(const variable_list &x, const variable_list &y)
Returns the intersection of two unordered sets, that are stored in ATerm lists.
void optimized_imp(typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits t)
Make an implication.
void optimized_not(typename TermTraits::term_type &result, const typename TermTraits::term_type &arg, TermTraits)
void optimized_and(typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)
Make a conjunction and optimize it if possible.
variable_list free_variables(const data_expression &x)
Definition data.cpp:195
void optimized_exists_no_empty_domain(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make an existential quantification.
void optimized_exists(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make an existential quantification.
void optimized_or(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
void optimized_imp(Term &result, const Term &p, const Term &q)
Make an implication.
void optimized_forall_no_empty_domain(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make a universal quantification.
void optimized_not(Term &result, const Term &arg)
Make a negation.
void optimized_and(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
void optimized_forall(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make a universal quantification.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Contains type information for terms.
Definition term_traits.h:24
Traits class for (boolean) terms.