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/pbes/detail/term_traits_optimized.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_TERM_TRAITS_OPTIMIZED_H
13 : #define MCRL2_PBES_DETAIL_TERM_TRAITS_OPTIMIZED_H
14 :
15 : #include "mcrl2/pbes/pbes_expression.h"
16 :
17 : namespace mcrl2 {
18 :
19 : namespace core {
20 :
21 : /// \brief Contains type information for terms.
22 : template <typename T>
23 : struct term_traits_optimized
24 : {
25 : };
26 :
27 : /// \brief Contains type information for pbes expressions.
28 : template <>
29 : struct term_traits_optimized<pbes_system::pbes_expression>: public core::term_traits<pbes_system::pbes_expression>
30 : {
31 : typedef core::term_traits<pbes_system::pbes_expression> super;
32 :
33 : static inline
34 126 : term_type not_(const term_type& x)
35 : {
36 126 : term_type result;
37 126 : data::optimized_not(result, x);
38 126 : return result;
39 0 : }
40 :
41 : static inline
42 : void make_not_(term_type& result, const term_type& x)
43 : {
44 : data::optimized_not(result, x);
45 : }
46 :
47 : static inline
48 1577 : term_type and_(const term_type& x, const term_type& y)
49 : {
50 1577 : term_type result;
51 1577 : data::optimized_and(result, x, y);
52 1577 : return result;
53 0 : }
54 :
55 : static inline
56 : void make_and_(term_type& result, const term_type& x, const term_type& y)
57 : {
58 : data::optimized_and(result, x, y);
59 : }
60 :
61 : static inline
62 301 : term_type or_(const term_type& x, const term_type& y)
63 : {
64 301 : term_type result;
65 301 : data::optimized_or(result, x, y);
66 301 : return result;
67 0 : }
68 :
69 : static inline
70 : void make_or_(term_type& result, const term_type& x, const term_type& y)
71 : {
72 : data::optimized_or(result, x, y);
73 : }
74 :
75 : static inline
76 468 : term_type imp(const term_type& x, const term_type& y)
77 : {
78 468 : term_type result;
79 468 : data::optimized_imp(result, x, y);
80 468 : return result;
81 0 : }
82 :
83 : static inline
84 : void make_imp(term_type& result, const term_type& x, const term_type& y)
85 : {
86 : data::optimized_imp(result, x, y);
87 : }
88 :
89 : static inline
90 17 : void make_forall(term_type& result, const variable_sequence_type& d, const term_type& x)
91 : {
92 17 : data::optimized_forall_no_empty_domain(result, d, x);
93 17 : }
94 :
95 : static inline
96 7 : void make_exists(term_type& result, const variable_sequence_type& d, const term_type& x)
97 : {
98 7 : data::optimized_exists_no_empty_domain(result, d, x);
99 7 : }
100 :
101 : template <typename FwdIt>
102 : static inline
103 90 : term_type join_or(FwdIt first, FwdIt last)
104 : {
105 90 : return utilities::detail::join(first, last, or_, false_());
106 : }
107 :
108 : template <typename FwdIt>
109 : static inline
110 111 : term_type join_and(FwdIt first, FwdIt last)
111 : {
112 111 : return utilities::detail::join(first, last, and_, true_());
113 : }
114 : };
115 :
116 : } // namespace core
117 :
118 : } // namespace mcrl2
119 :
120 : #endif // MCRL2_PBES_DETAIL_TERM_TRAITS_OPTIMIZED_H
|