Line data Source code
1 : // Author(s): Jan Friso Groote
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 linear_inequalities_utilities.h
10 : /// \brief Contains utility functions for linear inequalities.
11 :
12 :
13 : #ifndef MCRL2_LPSREALELM_DETAIL_LINEAR_INEQUALITY_UTILITIES_H
14 : #define MCRL2_LPSREALELM_DETAIL_LINEAR_INEQUALITY_UTILITIES_H
15 :
16 :
17 : #include "mcrl2/data/linear_inequalities.h"
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace data
23 : {
24 :
25 : namespace detail
26 : {
27 :
28 0 : inline data_expression negate_inequality(const data_expression& e)
29 : {
30 0 : if (is_equal_to_application(e))
31 : {
32 0 : return not_equal_to(data::binary_left(atermpp::down_cast<application>(e)),data::binary_right(atermpp::down_cast<application>(e)));
33 : }
34 0 : if (is_not_equal_to_application(e))
35 : {
36 0 : return equal_to(data::binary_left(atermpp::down_cast<application>(e)),data::binary_right(atermpp::down_cast<application>(e)));
37 : }
38 0 : else if (is_less_application(e))
39 : {
40 0 : return greater_equal(data::binary_left(atermpp::down_cast<application>(e)),data::binary_right(atermpp::down_cast<application>(e)));
41 : }
42 0 : else if (is_less_equal_application(e))
43 : {
44 0 : return data::greater(data::binary_left(atermpp::down_cast<application>(e)),data::binary_right(atermpp::down_cast<application>(e)));
45 : }
46 0 : else if (is_greater_application(e))
47 : {
48 0 : return less_equal(data::binary_left(atermpp::down_cast<application>(e)),data::binary_right(atermpp::down_cast<application>(e)));
49 : }
50 0 : else if (is_greater_equal_application(e))
51 : {
52 0 : return data::less(data::binary_left(atermpp::down_cast<application>(e)),data::binary_right(atermpp::down_cast<application>(e)));
53 : }
54 : else
55 : {
56 0 : throw mcrl2::runtime_error("Expression " + data::pp(e) + " is expected to be an inequality over sort Real");
57 : }
58 : }
59 :
60 :
61 : /// \brief Determine whether a data expression is an inequality
62 : /// \param e A data expression
63 : /// \return true iff e is a data application of ==, <, <=, > or >= to
64 : /// two arguments.
65 :
66 23 : inline bool is_inequality(const data_expression& e)
67 : {
68 40 : return is_equal_to_application(e) || is_less_application(e) ||
69 51 : is_less_equal_application(e) || is_greater_application(e) ||
70 34 : is_greater_equal_application(e);
71 : }
72 :
73 : // Functions below should have been defined in the data library.
74 0 : inline const data_expression& condition_part(const data_expression& e)
75 : {
76 0 : assert(is_if_application(e));
77 0 : const data::application& a = atermpp::down_cast<const application>(e);
78 0 : data::application::const_iterator i = a.begin();
79 0 : return *i;
80 : }
81 :
82 0 : inline const data_expression& then_part(const data_expression& e)
83 : {
84 0 : assert(is_if_application(e));
85 0 : const data::application& a = atermpp::down_cast<const application>(e);
86 0 : data::application::const_iterator i = a.begin();
87 0 : return *(++i);
88 : }
89 :
90 0 : inline const data_expression& else_part(const data_expression& e)
91 : {
92 0 : assert(is_if_application(e));
93 0 : const data::application& a = atermpp::down_cast<const application>(e);
94 0 : data::application::const_iterator i = a.begin();
95 0 : return *(++(++i));
96 : }
97 :
98 :
99 :
100 : /// \brief Splits a condition in expressions ranging over reals and the others
101 : /// \details Conceptually, the condition is first transformed to disjunctive
102 : /// normal form. For each disjunct, there will be an entry in both
103 : /// resulting std::vectors, where the real conditions are in "real_conditions",
104 : /// and the others in non_real_conditions. If there are conjuncts with
105 : /// both real and non-real variables an exception is thrown. If negate
106 : /// is true the result will be negated.
107 : /// \param e A data expression of sort bool.
108 : /// \param real_condition Those parts of e with only variables over sort Real.
109 : /// \param non_real_condition Those parts of e with only variables not of sort Real.
110 : /// \param negate A boolean variable that indicates whether the result must be negated.
111 : /// \return True when e contains real variables
112 : /// \pre The parameter e must be of sort Bool.
113 :
114 38 : static bool split_condition_aux(
115 : const data_expression& e,
116 : std::vector < data_expression_list >& real_conditions,
117 : std::vector < data_expression_list >& non_real_conditions,
118 : const bool negate=false)
119 : {
120 38 : assert(real_conditions.empty());
121 38 : assert(non_real_conditions.empty());
122 :
123 : // In these three cases, we rewrite the expression and call this function recursively
124 : // with the rewritten expression
125 38 : if (sort_bool::is_implies_application(e))
126 : {
127 0 : data_expression rewritten = sort_bool::or_(sort_bool::not_(sort_bool::left(e)), sort_bool::right(e));
128 0 : return split_condition_aux(rewritten, real_conditions, non_real_conditions, negate);
129 0 : }
130 38 : else if (is_if_application(e))
131 : {
132 0 : return split_condition_aux(sort_bool::or_(sort_bool::and_(condition_part(e),then_part(e)),
133 0 : sort_bool::and_(sort_bool::not_(condition_part(e)),else_part(e))),
134 0 : real_conditions,non_real_conditions,negate);
135 : }
136 38 : else if (sort_bool::is_not_application(e))
137 : {
138 0 : return split_condition_aux(sort_bool::arg(e),real_conditions,non_real_conditions,!negate);
139 : }
140 :
141 38 : if(sort_bool::is_and_application(e) || sort_bool::is_or_application(e))
142 : {
143 : // Recursive case
144 15 : std::vector < data_expression_list > real_conditions_aux1, non_real_conditions_aux1;
145 15 : bool left_is_real = split_condition_aux(sort_bool::left(e),real_conditions_aux1,non_real_conditions_aux1,negate);
146 15 : std::vector < data_expression_list > real_conditions_aux2, non_real_conditions_aux2;
147 15 : bool right_is_real = split_condition_aux(sort_bool::right(e),real_conditions_aux2,non_real_conditions_aux2,negate);
148 15 : if(!left_is_real && !right_is_real)
149 : {
150 : // There are no real variables on either side so we can
151 : // just store the expression e in non_real_conditions
152 5 : real_conditions.push_back(data_expression_list());
153 10 : non_real_conditions.push_back(data_expression_list({ negate ? data_expression(sort_bool::not_(e)) : e }));
154 : }
155 10 : else if ((!negate && sort_bool::is_and_application(e)) || (negate && sort_bool::is_or_application(e)))
156 : {
157 : // Combine the recursive results (whis are disjunctiosn of conjunctions)
158 : // of the left and right sides of e (which is a conjunction or negated disjunction)
159 : // by using the distributivity of && and || to obtain a result
160 : // which is again a disjunction of conjuctions.
161 5 : for (std::vector < data_expression_list >::const_iterator
162 5 : i1r=real_conditions_aux1.begin(), i1n=non_real_conditions_aux1.begin() ;
163 12 : i1r!=real_conditions_aux1.end(); ++i1r, ++i1n)
164 : {
165 7 : for (std::vector < data_expression_list >::const_iterator
166 7 : i2r=real_conditions_aux2.begin(), i2n=non_real_conditions_aux2.begin() ;
167 19 : i2r!=real_conditions_aux2.end(); ++i2r, ++i2n)
168 : {
169 12 : real_conditions.push_back(*i1r + *i2r);
170 12 : non_real_conditions.push_back(*i1n + *i2n);
171 : }
172 : }
173 : }
174 : else
175 : {
176 5 : assert((!negate && sort_bool::is_or_application(e)) || (negate && sort_bool::is_and_application(e)));
177 :
178 : // Combine the recursive results of the left and right sides
179 : // of the disjunction (or negated conjunction) by concatenating
180 : // them.
181 5 : real_conditions.insert(real_conditions.end(), real_conditions_aux1.begin(), real_conditions_aux1.end());
182 5 : real_conditions.insert(real_conditions.end(), real_conditions_aux2.begin(), real_conditions_aux2.end());
183 5 : non_real_conditions.insert(non_real_conditions.end(), non_real_conditions_aux1.begin(), non_real_conditions_aux1.end());
184 5 : non_real_conditions.insert(non_real_conditions.end(), non_real_conditions_aux2.begin(), non_real_conditions_aux2.end());
185 : }
186 15 : return left_is_real || right_is_real;
187 15 : }
188 23 : else if (is_inequality(e) && (data::binary_left(atermpp::down_cast<application>(e)).sort() == sort_real::real_() || data::binary_right(atermpp::down_cast<application>(e)).sort() == sort_real::real_()))
189 : {
190 : // Base case 1: an inequality over real numbers
191 12 : std::set < variable > vars=data::find_all_variables(e);
192 27 : for (const variable& v: vars)
193 : {
194 15 : if (v.sort() != sort_real::real_())
195 : {
196 0 : throw mcrl2::runtime_error("Expression " + data::pp(e) + " contains variable " +
197 0 : data::pp(v) + " not of sort Real.");
198 : }
199 : }
200 24 : real_conditions.push_back(data_expression_list({ negate ? negate_inequality(e) : e }));
201 12 : non_real_conditions.push_back(data_expression_list());
202 12 : return true;
203 12 : }
204 : else
205 : {
206 : // Base case 2: an expression not containing real numbers
207 : // e is assumed to be a non_real expression.
208 11 : std::set < variable > vars=data::find_all_variables(e);
209 22 : for (const variable& v: vars)
210 : {
211 11 : if (v.sort() == sort_real::real_())
212 : {
213 0 : throw mcrl2::runtime_error("Expression " + data::pp(e) + " contains variable " +
214 0 : data::pp(v) + " of sort Real.");
215 : }
216 : }
217 22 : non_real_conditions.push_back(data_expression_list({ negate ? data_expression(sort_bool::not_(e)) : e }));
218 11 : real_conditions.push_back(data_expression_list());
219 11 : return false;
220 11 : }
221 : }
222 :
223 : /// \brief This function first splits the given condition e into real conditions and
224 : /// non real conditions.
225 : /// \detail This function first uses split_condition_aux to split the condition e. Then
226 : // it merges equal real conditions by merging the non-real conditions. No further
227 : // calculations take place with the non-real conditions, but if the non-real conditions
228 : // lead to unnecessary copying, this may lead to a huge overhead in removing the
229 : // real conditions.
230 8 : inline void split_condition(
231 : const data_expression& e,
232 : std::vector < data_expression_list >& real_conditions,
233 : std::vector < data_expression >& non_real_conditions)
234 : {
235 8 : std::vector < data_expression_list > aux_real_conditions;
236 8 : std::vector < data_expression_list > aux_non_real_conditions;
237 :
238 8 : split_condition_aux(e,aux_real_conditions, aux_non_real_conditions);
239 8 : assert(aux_non_real_conditions.size()==aux_real_conditions.size() && aux_non_real_conditions.size()>0);
240 :
241 : // For every list of real expressions, gather the corresponding non real expressions
242 8 : std::map< data_expression_list, data_expression > non_real_expression_map;
243 8 : for(std::vector < data_expression_list >::const_iterator i=aux_real_conditions.begin(), j=aux_non_real_conditions.begin();
244 23 : i!=aux_real_conditions.end(); ++i, ++j)
245 : {
246 : // Find the entry for *i, inserting false if it does not exist yet
247 : std::map< data_expression_list, data_expression >::iterator insert_result =
248 15 : non_real_expression_map.insert(std::make_pair(*i, sort_bool::false_())).first;
249 15 : insert_result->second = lazy::or_(insert_result->second, lazy::join_and(j->begin(), j->end()));
250 : }
251 : // Convert the map to a pair of vectors
252 23 : for(const std::pair<const data_expression_list, data_expression >& expr_pair: non_real_expression_map)
253 : {
254 15 : real_conditions.push_back(expr_pair.first);
255 15 : non_real_conditions.push_back(expr_pair.second);
256 : }
257 8 : assert(non_real_conditions.size()==real_conditions.size() && non_real_conditions.size()>0);
258 8 : }
259 :
260 : } // end namespace detail
261 :
262 :
263 : } // namespace data
264 :
265 : } // namespace mcrl2
266 :
267 : #endif // MCRL2_LPSREALELM_DETAIL_LINEAR_INEQUALITY_UTILITIES_H
|