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/data/optimized_boolean_operators.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_DATA_OPTIMIZED_BOOLEAN_OPERATORS_H
13 : #define MCRL2_DATA_OPTIMIZED_BOOLEAN_OPERATORS_H
14 :
15 : #include "mcrl2/core/term_traits.h"
16 : #include "mcrl2/data/detail/data_sequence_algorithm.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace data
22 : {
23 :
24 : namespace detail
25 : {
26 : /// \return The value <tt>!arg</tt>
27 : template <typename TermTraits>
28 : inline
29 568 : void optimized_not(typename TermTraits::term_type& result,
30 : const typename TermTraits::term_type& arg,
31 : TermTraits)
32 : {
33 : typedef TermTraits tr;
34 :
35 568 : if (tr::is_true(arg))
36 : {
37 42 : result=tr::false_();
38 : }
39 526 : else if (tr::is_false(arg))
40 : {
41 101 : result=tr::true_();
42 : }
43 425 : else if (tr::is_not(arg))
44 : {
45 152 : result=tr::not_arg(arg);
46 : }
47 : else
48 : {
49 273 : tr::make_not_(result, arg);
50 : }
51 568 : }
52 :
53 : /// \brief Make a conjunction and optimize it if possible.
54 : /// \param left A term
55 : /// \param right A term
56 : /// \return The value <tt>left && right</tt>
57 : template <typename TermTraits>
58 : inline
59 9838 : void 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 9838 : if (tr::is_true(left))
67 : {
68 1936 : result=right;
69 : }
70 7902 : else if (tr::is_false(left))
71 : {
72 2346 : result=tr::false_();
73 : }
74 5556 : else if (tr::is_true(right))
75 : {
76 746 : result=left;
77 : }
78 4810 : else if (tr::is_false(right))
79 : {
80 1818 : result=tr::false_();
81 : }
82 2992 : else if (left == right)
83 : {
84 18 : result=left;
85 : }
86 : else
87 : {
88 2974 : tr::make_and_(result, left, right);
89 : }
90 9838 : }
91 :
92 : /* template <typename TermTraits>
93 : inline
94 : typename 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 :
126 : /// \brief Make a disjunction
127 : /// \param left A term
128 : /// \param right A term
129 : /// \return The value <tt>left || right</tt>
130 : template <typename TermTraits>
131 : inline
132 4610 : void 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 4610 : if (tr::is_true(left))
139 : {
140 37 : result=tr::true_();
141 : }
142 4573 : else if (tr::is_false(left))
143 : {
144 637 : result=right;
145 : }
146 3936 : else if (tr::is_true(right))
147 : {
148 198 : result=tr::true_();
149 : }
150 3738 : else if (tr::is_false(right))
151 : {
152 2677 : result=left;
153 : }
154 1061 : else if (left == right)
155 : {
156 5 : result=left;
157 : }
158 : else
159 : {
160 1056 : tr::make_or_(result, left, right);
161 : }
162 4610 : }
163 :
164 : /// \brief Make an implication
165 : /// \param left A term
166 : /// \param right A term
167 : /// \return The value <tt>left => right</tt>
168 : template <typename TermTraits>
169 : inline
170 972 : void 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 972 : if (tr::is_true(left))
177 : {
178 95 : result=right;
179 : }
180 877 : else if (tr::is_false(left))
181 : {
182 288 : result=tr::true_();
183 : }
184 589 : else if (tr::is_true(right))
185 : {
186 0 : result=tr::true_();
187 : }
188 589 : else if (tr::is_false(right))
189 : {
190 54 : optimized_not(result,left, t);
191 : }
192 535 : else if (left == right)
193 : {
194 0 : result=tr::true_();
195 : }
196 : else
197 : {
198 535 : tr::make_imp(result, left, right);
199 : }
200 972 : }
201 :
202 : /// \brief Make a universal quantification
203 : /// \param v A sequence of variables
204 : /// \param arg A term
205 : ////// \param remove_variables If true, remove bound variables that do not occur in \a arg.
206 : /// \param empty_domain_allowed If true, and there are no variables in \a v, treat
207 : /// as empty domain, hence yielding <tt>true</tt>, otherwise <tt>arg</tt> arg
208 : /// is returned in this case.
209 : /// \return The universal quantification <tt>forall v.arg</tt>
210 : template <typename TermTraits>
211 : inline
212 2221 : void 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 2221 : if (v.empty())
221 : {
222 2044 : if (empty_domain_allowed)
223 : {
224 0 : result = tr::true_();
225 : }
226 : else
227 : {
228 2044 : result = arg;
229 : }
230 : }
231 177 : else if (tr::is_true(arg))
232 : {
233 19 : result = tr::true_();
234 : }
235 158 : else if (tr::is_false(arg))
236 : {
237 11 : result = tr::false_();
238 : }
239 : else
240 : {
241 147 : if (remove_variables)
242 : {
243 130 : data::variable_list variables = data::detail::set_intersection(v, free_variables(arg));
244 130 : if (variables.empty())
245 : {
246 21 : result = arg;
247 : }
248 : else
249 : {
250 109 : tr::make_forall(result, variables, arg);
251 : }
252 130 : }
253 : else
254 : {
255 17 : tr::make_forall(result, v, arg);
256 : }
257 : }
258 2221 : }
259 :
260 : /// \brief Make an existential quantification
261 : /// \param v A sequence of variables
262 : /// \param arg A term
263 : /// \param remove_variables If true, remove bound variables that do not occur in \a arg.
264 : /// \param empty_domain_allowed If true, and there are no variables in \a v, treat
265 : /// as empty domain, hence yielding <tt>false</tt>, otherwise <tt>arg</tt> arg
266 : /// is returned in this case.
267 : /// \return The existential quantification <tt>exists v.arg</tt>
268 : template <typename TermTraits>
269 : inline
270 868 : void 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 868 : if (v.empty())
280 : {
281 536 : if (empty_domain_allowed)
282 : {
283 0 : result = tr::false_();
284 : }
285 : else
286 : {
287 536 : result = arg;
288 : }
289 : }
290 332 : else if (tr::is_true(arg))
291 : {
292 21 : result = tr::true_();
293 : }
294 311 : else if (tr::is_false(arg))
295 : {
296 187 : result = tr::false_();
297 : }
298 : else
299 : {
300 124 : if (remove_variables)
301 : {
302 118 : data::variable_list variables = data::detail::set_intersection(v, free_variables(arg));
303 118 : if (variables.empty())
304 : {
305 10 : result = arg;
306 : }
307 : else
308 : {
309 108 : result = tr::exists(variables, arg);
310 : }
311 118 : }
312 : else
313 : {
314 6 : result = tr::exists(v, arg);
315 : }
316 : }
317 868 : }
318 :
319 : /// \brief Make a negation
320 : /// \param arg A term
321 : /// \param not_ The operation not
322 : /// \param true_ The value true
323 : /// \param is_true Function that tests for the value true
324 : /// \param false_ The value false
325 : /// \param is_false Function that tests for the value false
326 : /// \return The value <tt>!arg</tt>
327 : /* template <typename T1, typename T2, typename UnaryFunction, typename UnaryPredicate>
328 : inline
329 : T1 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 :
345 : /// \brief Make a conjunction
346 : /// \param left A term
347 : /// \param right A term
348 : /// \param and_ The operation and
349 : /// \param true_ The value true
350 : /// \param is_true Function that tests for the value true
351 : /// \param false_ The value false
352 : /// \param is_false Function that tests for the value false
353 : /// \return The value <tt>left && right</tt>
354 : /* template <typename T1, typename T2, typename UnaryPredicate, typename BinaryFunction>
355 : inline
356 : T1 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 :
385 : /// \brief Make a disjunction
386 : /// \param left A term
387 : /// \param right A term
388 : /// \param or_ The operation or
389 : /// \param true_ The value true
390 : /// \param is_true Function that tests for the value true
391 : /// \param false_ The value false
392 : /// \param is_false Function that tests for the value false
393 : /// \return The value <tt>left || right</tt>
394 : /* template <typename T1, typename T2, typename UnaryPredicate, typename BinaryFunction>
395 : inline
396 : T1 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 :
425 : /// \brief Make an implication
426 : /// \param left A term
427 : /// \param right A term
428 : /// \param imp The implication operator
429 : /// \param not_ The operation not
430 : /// \param true_ The value true
431 : /// \param is_true Function that tests for the value true
432 : /// \param false_ The value false
433 : /// \param is_false Function that tests for the value false
434 : /// \return The value <tt>left => right</tt>
435 : /* template <typename T1, typename T2, typename UnaryPredicate, typename UnaryFunction, typename BinaryFunction>
436 : inline
437 : T1 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 :
466 : /// \brief Make a universal quantification
467 : /// \param v A sequence of variables
468 : /// \param arg A term
469 : /// \param forall The universal quantification operator
470 : /// \param true_ The value true
471 : /// \param is_true Function that tests for the value true
472 : /// \param false_ The value false
473 : /// \param is_false Function that tests for the value false
474 : /// \return The universal quantification <tt>forall v.arg</tt>
475 : /* template <typename T1, typename T2, typename VariableSequence, typename UnaryPredicate, typename Forall>
476 : inline
477 : void 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 :
493 : /// \brief Make an existential quantification
494 : /// \param v A sequence of variables
495 : /// \param arg A term
496 : /// \param exists The existential quantification operator
497 : /// \param true_ The value true
498 : /// \param is_true Function that tests for the value true
499 : /// \param false_ The value false
500 : /// \param is_false Function that tests for the value false
501 : /// \return The existential quantification <tt>exists v.arg</tt>
502 : /* template <typename T1, typename T2, typename VariableSequence, typename UnaryPredicate, typename Exists>
503 : inline
504 : void 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 :
522 : /// \brief Make a negation
523 : /// \param arg A term
524 : /// \return The application of not to the argument.
525 : template <typename Term>
526 : inline
527 514 : void optimized_not(Term& result, const Term& arg)
528 : {
529 514 : detail::optimized_not(result, arg, core::term_traits<Term>());
530 514 : }
531 :
532 : /// \brief Make a conjunction, and optimize if possible.
533 : /// \param result Contains the optimized and.
534 : /// \param p A term
535 : /// \param q A term
536 : template <typename Term>
537 : inline
538 9838 : void optimized_and(Term& result, const Term& p, const Term& q)
539 : {
540 9838 : return detail::optimized_and(result, p, q, core::term_traits<Term>());
541 : }
542 :
543 : /// \brief Make a conjunction, and optimize if possible.
544 : /// \param p A term
545 : /// \param q A term
546 : /// \return The application of and to the arguments.
547 : /* template <typename Term>
548 : inline
549 : Term optimized_and(const Term& p, const Term& q)
550 : {
551 : return detail::optimized_and(p, q, core::term_traits<Term>());
552 : } */
553 :
554 : /// \brief Make a disjunction
555 : /// \param p A term
556 : /// \param q A term
557 : /// \return The application of or to the arguments.
558 : template <typename Term>
559 : inline
560 4610 : void optimized_or(Term& result, const Term& p, const Term& q)
561 : {
562 4610 : detail::optimized_or(result, p, q, core::term_traits<Term>());
563 4610 : }
564 :
565 : /// \brief Make an implication
566 : /// \param p A term
567 : /// \param q A term
568 : /// \return The application of implication to the arguments.
569 : template <typename Term>
570 : inline
571 972 : void optimized_imp(Term& result, const Term& p, const Term& q)
572 : {
573 972 : detail::optimized_imp(result, p, q, core::term_traits<Term>());
574 972 : }
575 :
576 : /// \brief Make a universal quantification
577 : /// \param l A sequence of variables
578 : /// \param p A term
579 : /// \param remove_variables If true, unused quantifier variables are removed
580 : /// \return The application of universal quantification to the arguments.
581 : template <typename Term, typename VariableSequence>
582 : inline
583 100 : void optimized_forall(Term& result, const VariableSequence& l, const Term& p, bool remove_variables = false)
584 : {
585 100 : bool empty_domain_allowed = true;
586 100 : detail::optimized_forall(result, l, p, remove_variables, empty_domain_allowed, core::term_traits<Term>());
587 100 : }
588 :
589 : /// \brief Make a universal quantification
590 : /// \param l A sequence of variables
591 : /// \param p A term
592 : /// \param remove_variables If true, unused quantifier variables are removed
593 : /// \return The application of universal quantification to the arguments.
594 : /// The optimization forall x:empty_set. phi = true is not applied.
595 : template <typename Term, typename VariableSequence>
596 : inline
597 2121 : void optimized_forall_no_empty_domain(Term& result, const VariableSequence& l, const Term& p, bool remove_variables = false)
598 : {
599 2121 : bool empty_domain_allowed = false;
600 2121 : detail::optimized_forall(result, l, p, remove_variables, empty_domain_allowed, core::term_traits<Term>());
601 2121 : }
602 :
603 : /// \brief Make an existential quantification
604 : /// \param l A sequence of variables
605 : /// \param p A term
606 : /// \param remove_variables If true, unused quantifier variables are removed
607 : /// \return The application of existential quantification to the arguments.
608 : template <typename Term, typename VariableSequence>
609 : inline
610 302 : void optimized_exists(Term& result, const VariableSequence& l, const Term& p, bool remove_variables = false)
611 : {
612 302 : bool empty_domain_allowed = true;
613 302 : detail::optimized_exists(result, l, p, remove_variables, empty_domain_allowed, core::term_traits<Term>());
614 302 : }
615 :
616 : /// \brief Make an existential quantification
617 : /// \param l A sequence of variables
618 : /// \param p A term
619 : /// \param remove_variables If true, unused quantifier variables are removed
620 : /// \return The application of existential quantification to the arguments.
621 : /// The optimization exists x:empty_set. phi = false is not applied.
622 : template <typename Term, typename VariableSequence>
623 : inline
624 566 : void optimized_exists_no_empty_domain(Term& result, const VariableSequence& l, const Term& p, bool remove_variables = false)
625 : {
626 566 : bool empty_domain_allowed = false;
627 566 : detail::optimized_exists(result, l, p, remove_variables, empty_domain_allowed, core::term_traits<Term>());
628 566 : }
629 :
630 : } // namespace data
631 :
632 : } // namespace mcrl2
633 :
634 : #endif // MCRL2_DATA_OPTIMIZED_BOOLEAN_OPERATORS_H
|
