Line data Source code
1 : // Author(s): Luc Engelen
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/detail/prover/manipulator.h
10 : /// \brief Interface to classes Manipulator.
11 :
12 : #ifndef MCRL2_DATA_DETAIL_PROVER_MANIPULATOR_H
13 : #define MCRL2_DATA_DETAIL_PROVER_MANIPULATOR_H
14 :
15 : #include "mcrl2/data/detail/prover/info.h"
16 :
17 : namespace mcrl2
18 : {
19 : namespace data
20 : {
21 : namespace detail
22 : {
23 :
24 : /// \brief Base class for classes that provide functionality to modify or create terms.
25 :
26 : class Manipulator
27 : {
28 : protected:
29 : /// \brief A class that provides information on the structure of expressions in one of the
30 : /// \brief internal formats of the rewriter.
31 : const Info& f_info;
32 :
33 : /// \brief A table used by the method Manipulator::orient.
34 : /// The method Manipulator::orient stores resulting terms in this
35 : /// table. If a term is encountered that has already been processed, it is
36 : /// not processed again, but retreived from this table.
37 : std::unordered_map < data_expression, data_expression> f_orient;
38 :
39 : /// \brief Replaces all occurences of \c a_guard in \c a_formula by \c true. Additionally, if the variable
40 : /// \brief on the righthand side of the guard is encountered in \c a_formula, it is replaced by the variable
41 : /// \brief on the lefthand side.
42 2138 : data_expression set_true_auxiliary(
43 : const data_expression& a_formula,
44 : const data_expression& a_guard,
45 : std::unordered_map < data_expression, data_expression >& f_set_true) const
46 : {
47 2138 : if (is_function_symbol(a_formula))
48 : {
49 1029 : return a_formula;
50 : }
51 :
52 1109 : if (is_abstraction(a_formula))
53 : {
54 0 : const abstraction& t=atermpp::down_cast<abstraction>(a_formula);
55 0 : return abstraction(t.binding_operator(), t.variables(), set_true_auxiliary(t.body(), a_guard, f_set_true));
56 : }
57 :
58 1109 : if (a_formula == a_guard)
59 : {
60 173 : return sort_bool::true_();
61 : }
62 :
63 936 : if (is_equal_to_application(a_guard))
64 : {
65 232 : const application& a = atermpp::down_cast<application>(a_guard);
66 232 : if (a[1]==a_formula)
67 : {
68 : // We can be sure that a[1] does not occur in a[0], due to the ordering on terms
69 : // Therefore, there are no never-ending substitutions occuring
70 17 : return a[0];
71 : }
72 : }
73 :
74 919 : if (is_variable(a_formula))
75 : {
76 209 : return a_formula;
77 : }
78 :
79 710 : std::unordered_map < data_expression, data_expression >::const_iterator i=f_set_true.find(a_formula);
80 710 : if (i!=f_set_true.end())
81 : {
82 50 : return i->second;
83 : }
84 :
85 660 : const application& t=atermpp::down_cast<application>(a_formula);
86 660 : data_expression v_result = application(t.head(),
87 660 : t.begin(),
88 660 : t.end(),
89 2653 : [&a_guard, &f_set_true, this](const data_expression& d){ return set_true_auxiliary(d, a_guard,f_set_true);});
90 :
91 660 : f_set_true[a_formula]=v_result;
92 :
93 660 : return v_result;
94 660 : }
95 :
96 : /// \brief Replaces all occurences of \c a_guard in \c a_formula by \c false.
97 2138 : data_expression set_false_auxiliary(
98 : const data_expression& a_formula,
99 : const data_expression& a_guard,
100 : std::unordered_map < data_expression, data_expression >& f_set_false) const
101 : {
102 2138 : if (is_function_symbol(a_formula))
103 : {
104 1029 : return a_formula;
105 : }
106 :
107 1109 : if (is_abstraction(a_formula))
108 : {
109 0 : const abstraction& t=atermpp::down_cast<abstraction>(a_formula);
110 0 : return abstraction(t.binding_operator(), t.variables(), set_false_auxiliary(t.body(), a_guard, f_set_false));
111 : }
112 :
113 1109 : if (a_formula == a_guard)
114 : {
115 173 : return sort_bool::false_();
116 : }
117 :
118 936 : if (is_variable(a_formula))
119 : {
120 226 : return a_formula;
121 : }
122 :
123 710 : std::unordered_map < data_expression, data_expression >::const_iterator i=f_set_false.find(a_formula);
124 710 : if (i!=f_set_false.end())
125 : {
126 50 : return i->second;
127 : }
128 :
129 660 : const application t(a_formula);
130 660 : data_expression v_result = application(t.head(),
131 660 : t.begin(),
132 660 : t.end(),
133 2653 : [&a_guard, &f_set_false, this](const data_expression& d){ return set_false_auxiliary(d, a_guard,f_set_false);});
134 660 : f_set_false[a_formula]=v_result;
135 660 : return v_result;
136 660 : }
137 :
138 : public:
139 : /// \brief Constructor initializing the rewriter and the field \c f_info.
140 18 : Manipulator(const Info& a_info):
141 18 : f_info(a_info)
142 18 : {}
143 :
144 : /// \brief Returns an expression in the internal format of the rewriter with the jitty strategy.
145 : /// \brief The main operator of this expression is an \c if \c then \c else function. Its guard is \c a_expr,
146 : /// \brief the true-branch is \c a_high and the false-branch is \c a_low. If \c a_high equals \c a_low, the
147 : /// \brief method returns \c a_high instead.
148 145 : static data_expression make_reduced_if_then_else(const data_expression& a_expr,
149 : const data_expression& a_high,
150 : const data_expression& a_low)
151 : {
152 290 : return a_high == a_low ? a_high : if_(a_expr, a_high, a_low);
153 : }
154 :
155 : /// \brief Orients the term \c a_term such that all equations of the form t1 == t2 are
156 : /// \brief replaced by t2 == t1 if t1 > t2.
157 1322 : data_expression orient(const data_expression& a_term)
158 : {
159 1322 : if (is_variable(a_term) || is_function_symbol(a_term) || is_where_clause(a_term))
160 : {
161 787 : return a_term;
162 : }
163 :
164 535 : if (is_abstraction(a_term))
165 : {
166 0 : const abstraction a(atermpp::down_cast<abstraction>(a_term));
167 0 : return abstraction(a.binding_operator(), a.variables(), orient(a.body()));
168 0 : }
169 :
170 535 : std::unordered_map < data_expression, data_expression> :: const_iterator it=f_orient.find(a_term);
171 535 : if (it!=f_orient.end()) // found
172 : {
173 204 : return it->second;
174 : }
175 :
176 331 : const application& a = atermpp::down_cast<application>(a_term);
177 1282 : application v_result(a.head(), a.begin(), a.end(), [this](const data_expression& d){return orient(d); });
178 :
179 331 : if (is_equal_to_application(v_result))
180 : {
181 76 : const data_expression& v_term1(v_result[0]);
182 76 : const data_expression& v_term2(v_result[1]);
183 76 : if (f_info.compare_term(v_term1, v_term2) == compare_result_bigger)
184 : {
185 43 : v_result = application(v_result.head(), v_term2, v_term1);
186 : }
187 : }
188 331 : f_orient[a_term]=v_result;
189 :
190 331 : return workaround::return_std_move(v_result);
191 331 : }
192 :
193 : /// \brief Initializes the table Manipulator::f_set_true and calls
194 : /// \brief f_set_true_auxiliary.
195 145 : data_expression set_true(
196 : const data_expression& a_formula,
197 : const data_expression& a_guard) const
198 : {
199 145 : std::unordered_map < data_expression, data_expression > f_set_true;
200 290 : return set_true_auxiliary(a_formula, a_guard, f_set_true);
201 145 : }
202 :
203 : /// \brief Initializes the table Manipulator::f_set_false and calls the method
204 : /// \brief AM_Jitty::f_set_false_auxiliary.
205 145 : data_expression set_false(
206 : const data_expression& a_formula,
207 : const data_expression& a_guard) const
208 : {
209 145 : std::unordered_map < data_expression, data_expression > f_set_false;
210 290 : return set_false_auxiliary(a_formula, a_guard,f_set_false);
211 145 : }
212 : };
213 :
214 : } // namespace detail
215 : } // namespace data
216 : } // namespace mcrl2
217 :
218 : #endif
|
