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 fourier_motzkin.h
10 : /// \brief Contains functions to apply Fourier-Motzkin on linear inequalities
11 : /// and data expressions.
12 :
13 :
14 : #ifndef MCRL2_DATA_FOURIER_MOTZKIN_H
15 : #define MCRL2_DATA_FOURIER_MOTZKIN_H
16 :
17 : #include "mcrl2/data/optimized_boolean_operators.h"
18 : #include "mcrl2/data/detail/linear_inequalities_utilities.h"
19 :
20 : namespace mcrl2
21 : {
22 :
23 : namespace data
24 : {
25 :
26 :
27 : template < class Data_variable_iterator >
28 3 : inline void fourier_motzkin(const std::vector < linear_inequality >& inequalities_in,
29 : Data_variable_iterator variables_begin,
30 : Data_variable_iterator variables_end,
31 : std::vector < linear_inequality >& resulting_inequalities,
32 : const rewriter& r)
33 : {
34 3 : assert(resulting_inequalities.empty());
35 3 : if (mCRL2logEnabled(log::trace))
36 : {
37 0 : mCRL2log(log::trace) << "Starting Fourier-Motzkin elimination on " + pp_vector(inequalities_in) + " on variables ";
38 0 : for (Data_variable_iterator i=variables_begin;
39 0 : i!=variables_end; ++i)
40 : {
41 0 : mCRL2log(log::trace) << " " << pp(*i) ;
42 : }
43 0 : mCRL2log(log::trace) << std::endl;
44 : }
45 :
46 3 : std::vector < linear_inequality > inequalities;
47 3 : std::vector < linear_inequality > equalities;
48 3 : std::set < variable > vars=
49 : gauss_elimination(inequalities_in,
50 : equalities, // Store all resulting equalities here.
51 : inequalities, // Store all resulting non equalities here.
52 : variables_begin,
53 : variables_end,
54 : r);
55 :
56 : // At this stage, the variables that should be eliminated only occur in
57 : // inequalities. Group the inequalities into positive, 0, and negative
58 : // occurrences of each variable, and create a new system.
59 10 : for (std::set < variable >::const_iterator i = vars.begin(); i != vars.end(); ++i)
60 : {
61 3 : std::map < variable, std::size_t> nr_positive_occurrences;
62 3 : std::map < variable, std::size_t> nr_negative_occurrences;
63 3 : count_occurrences(inequalities,nr_positive_occurrences,nr_negative_occurrences,r);
64 :
65 3 : bool found=false;
66 3 : std::size_t best_choice=0;
67 3 : variable best_variable;
68 6 : for (std::set < variable >::const_iterator k = vars.begin(); k != vars.end(); ++k)
69 : {
70 3 : const std::size_t p=nr_positive_occurrences[*k];
71 3 : const std::size_t n=nr_negative_occurrences[*k];
72 3 : if ((p!=0) || (n!=0))
73 : {
74 2 : if (found)
75 : {
76 0 : if (n*p<best_choice)
77 : {
78 0 : best_choice=n*p;
79 0 : best_variable=*k;
80 : }
81 : }
82 : else
83 : {
84 : // found is false
85 2 : best_choice=n*p;
86 2 : best_variable=*k;
87 2 : found=true;
88 : }
89 : }
90 3 : if (found && (best_choice==0))
91 : {
92 : // Stop searching, we cannot find a better candidate.
93 0 : break;
94 : }
95 : }
96 :
97 3 : mCRL2log(log::trace) << "Best variable " << pp(best_variable) << "\n";
98 :
99 3 : if (!found)
100 : {
101 : // There are no variables anymore that can be removed from inequalities
102 1 : break;
103 : }
104 2 : std::vector < linear_inequality > new_inequalities;
105 2 : std::vector < linear_inequality> inequalities_with_positive_variable;
106 2 : std::vector < linear_inequality> inequalities_with_negative_variable; // Idem.
107 :
108 8 : for (const linear_inequality& e: inequalities)
109 : {
110 6 : const detail::lhs_t::const_iterator factor_it=e.lhs().find(best_variable);
111 6 : if (factor_it==e.lhs().end()) // variable best_variable does not occur in inequality e.
112 : {
113 0 : new_inequalities.push_back(e);
114 : }
115 : else
116 : {
117 6 : data_expression f=factor_it->factor();
118 6 : if (is_positive(f,r))
119 : {
120 2 : inequalities_with_positive_variable.push_back(e);
121 : }
122 4 : else if (is_negative(f,r))
123 : {
124 4 : inequalities_with_negative_variable.push_back(e);
125 : }
126 : else
127 : {
128 0 : assert(0);
129 : }
130 6 : }
131 : }
132 :
133 2 : mCRL2log(log::trace) << "Positive :" << pp_vector(inequalities_with_positive_variable) << "\n";
134 2 : mCRL2log(log::trace) << "Negative :" << pp_vector(inequalities_with_negative_variable) << "\n";
135 2 : mCRL2log(log::trace) << "Equalities :" << pp_vector(equalities) << "\n";
136 2 : mCRL2log(log::trace) << "Rest :" << pp_vector(new_inequalities) << "\n";
137 :
138 : // Variables are grouped, now construct new inequalities as follows:
139 : // Keep the zero occurrences
140 : // Combine each positive and negative equation as follows with x the best variable:
141 : // Given inequalities N + bi * x <= ci
142 : // M - bj * x <= cj
143 : // This is equivalent to N/bi + M/bj <= ci/bi + cj/bj
144 4 : for (const linear_inequality& e1: inequalities_with_positive_variable)
145 : {
146 10 : for (const linear_inequality& e2: inequalities_with_negative_variable)
147 : {
148 4 : const detail::lhs_t::const_iterator e1_best_variable_it=e1.lhs().find(best_variable);
149 4 : const data_expression& e1_factor=e1_best_variable_it->factor();
150 4 : const data_expression& e1_reduced_rhs=real_divides(e1.rhs(),e1_factor);
151 4 : const detail::lhs_t e1_reduced_lhs=detail::remove_variable_and_divide(e1.lhs(),best_variable,e1_factor,r);
152 :
153 4 : const detail::lhs_t::const_iterator e2_best_variable_it=e2.lhs().find(best_variable);
154 4 : const data_expression& e2_factor=e2_best_variable_it->factor();
155 4 : const data_expression& e2_reduced_rhs=real_divides(e2.rhs(),e2_factor);
156 4 : const detail::lhs_t e2_reduced_lhs=detail::remove_variable_and_divide(e2.lhs(),best_variable,e2_factor,r);
157 8 : const linear_inequality new_inequality(subtract(e1_reduced_lhs,e2_reduced_lhs,r),
158 : rewrite_with_memory(real_minus(e1_reduced_rhs,e2_reduced_rhs), r),
159 4 : (e1.comparison()==detail::less_eq) && (e2.comparison()==detail::less_eq)?
160 : detail::less_eq:
161 : detail::less,r);
162 4 : if (new_inequality.is_false(r))
163 : {
164 0 : resulting_inequalities.push_back(linear_inequality()); // This is a single contraditory inequality;
165 0 : return;
166 : }
167 4 : if (!new_inequality.is_true(r))
168 : {
169 3 : new_inequalities.push_back(new_inequality);
170 : }
171 : }
172 : }
173 2 : inequalities.swap(new_inequalities);
174 : }
175 :
176 3 : resulting_inequalities.swap(inequalities);
177 : // Add the equalities to the inequalities and return the result
178 3 : for (std::vector < linear_inequality > :: const_iterator i=equalities.begin();
179 3 : i!=equalities.end(); ++i)
180 : {
181 0 : assert(!i->is_false(r));
182 0 : if (!i->is_true(r))
183 : {
184 0 : resulting_inequalities.push_back(*i);
185 : }
186 : }
187 3 : mCRL2log(log::trace) << "Fourier-Motzkin elimination yields " << pp_vector(resulting_inequalities) << std::endl;
188 3 : }
189 :
190 : /// \brief Eliminate variables from a data expression using Gauss elimination and
191 : /// Fourier-Motzkin elimination.
192 : /// \details Deliver a data_expression e_out and a set of variables vars_out such that
193 : /// exists vars_in.e_in is equivalent to exists vars_out.e_out.
194 : /// If the resulting list of inequalities is inconsistent, then [false] is
195 : /// returned.
196 : /// \param e_in An input data_expression of sort Bool.
197 : /// \param vars_in A container with variables. Supports iterating over these variables.
198 : /// \param e_out The output data expression of sort Bool.
199 : /// \param vars_out A list of variables to store resulting variables. Initially empty.
200 : /// \param r A rewriter.
201 : /// \post exists vars_out.e_out == exists vars_in.e_in.
202 :
203 1151 : inline void fourier_motzkin(const data_expression& e_in,
204 : const variable_list& vars_in,
205 : data_expression& e_out,
206 : variable_list& vars_out,
207 : const rewriter& r)
208 : {
209 1151 : assert(e_in.sort()==sort_bool::bool_());
210 1151 : assert(vars_out.empty());
211 :
212 1151 : const std::set<variable>& all_free_variables = find_free_variables(e_in);
213 : // First check whether there are variables of sort real in vars_in.
214 : // Also check whether the variables in vars_in occur freely in e_in
215 : // If either is not the case, fourier motzkin does not make sense.
216 1151 : if (std::find_if(vars_in.begin(),vars_in.end(),[&](variable v){
217 2456 : return v.sort()==sort_real::real_() && all_free_variables.find(v) != all_free_variables.end();})==vars_in.end())
218 : {
219 1149 : vars_out=vars_in;
220 1149 : e_out=e_in;
221 1149 : return;
222 : }
223 :
224 2 : std::vector <data_expression_list> real_conditions;
225 2 : std::vector <data_expression> non_real_conditions;
226 2 : detail::split_condition(e_in,real_conditions,non_real_conditions);
227 :
228 : // Determine all variables that occur in the sum operator, but not in the
229 : // next state. We can apply Fourier-Motzkin to eliminate these variables from
230 : // this sum operator and the condition.
231 :
232 2 : const std::set < variable> non_eliminatable_variables=data::find_all_variables(non_real_conditions);
233 :
234 2 : variable_list real_sum_variables;
235 2 : variable_list eliminatable_real_sum_variables;
236 4 : for (const variable& v: vars_in)
237 : {
238 2 : if (non_eliminatable_variables.count(v)==0)
239 : {
240 : // The variable does not occur in the parameters. We can eliminate it using Fourier-Motzkin
241 2 : eliminatable_real_sum_variables.push_front(v);
242 : }
243 : else
244 : {
245 0 : vars_out.push_front(v);
246 : }
247 : }
248 2 : if (vars_out.size()==vars_in.size())
249 : {
250 : // No variables can be eliminated. Stop here.
251 0 : e_out=e_in;
252 0 : return;
253 : }
254 :
255 : // Now apply fourier-motzkin to each conjunct of linear inequalities.
256 2 : std::vector <data_expression>::const_iterator j_n=non_real_conditions.begin();
257 2 : std::set< data_expression > result_disjunction_set;
258 :
259 2 : for (std::vector <data_expression_list>::const_iterator j_r=real_conditions.begin();
260 3 : j_r!=real_conditions.end(); ++j_r, ++j_n)
261 : {
262 2 : const data_expression non_real_condition=*j_n;
263 2 : if (!sort_bool::is_false_function_symbol(non_real_condition))
264 : {
265 : try
266 : {
267 2 : std::vector < linear_inequality > inequalities;
268 : // Collect all real conditions from the condition from this summand and put them
269 : // into inequalities.
270 4 : for (data_expression_list::const_iterator k=j_r->begin(); k!=j_r->end(); k++)
271 : {
272 3 : inequalities.push_back(linear_inequality(*k,r));
273 : }
274 :
275 1 : std::vector < linear_inequality > new_inequalities;
276 1 : fourier_motzkin(inequalities,
277 1 : eliminatable_real_sum_variables.begin(),
278 1 : eliminatable_real_sum_variables.end(),
279 : new_inequalities,
280 : r);
281 1 : inequalities.clear();
282 1 : remove_redundant_inequalities(new_inequalities,inequalities,r);
283 : // Save the result in the output expression.
284 1 : data_expression partial_result=*j_n;
285 :
286 2 : for(const linear_inequality& l: inequalities)
287 : {
288 1 : optimized_and(partial_result, partial_result, l.transform_to_data_expression());
289 : }
290 1 : result_disjunction_set.insert(partial_result);
291 2 : }
292 1 : catch (mcrl2::runtime_error& )
293 : {
294 : // Something went wrong, most likely that the inequalities in the input were not linear.
295 : // Return the original expression.
296 1 : vars_out=vars_in;
297 1 : e_out=e_in;
298 1 : return;
299 1 : }
300 : }
301 2 : }
302 :
303 1 : e_out=lazy::join_or(result_disjunction_set.begin(),result_disjunction_set.end());
304 1157 : }
305 :
306 :
307 : /// \brief A unary function that can be used in combination with
308 : /// replace_data_expressions to eliminate real numbers from all
309 : /// quantifiers in an expression.
310 : /// It is adviced to first push the quantifiers inside and
311 : /// apply the one point rule, since that reduces the time spent on
312 : /// the Fourier-Motzkin procedure for large expression.
313 : /// Apply this function innermost first if the expresion contains
314 : /// nested quantifiers.
315 : /// \author Thomas Neele
316 : struct fourier_motzkin_sigma
317 : {
318 :
319 : protected:
320 : rewriter rewr;
321 :
322 : const data_expression apply(const abstraction& d, bool negate) const
323 : {
324 : const variable_list& variables = d.variables();
325 : const data_expression body = rewr(negate ? sort_bool::not_(d.body()) : d.body());
326 :
327 : variable_list new_variables;
328 : data_expression new_body;
329 : fourier_motzkin(body, variables, new_body, new_variables, rewr);
330 :
331 : if (negate)
332 : {
333 : return (new_variables.empty() ? rewr(sort_bool::not_(new_body)) : rewr(forall(new_variables, sort_bool::not_(new_body))));
334 : }
335 : else
336 : {
337 : return rewr(new_variables.empty() ? new_body : exists(new_variables, new_body));
338 : }
339 : }
340 :
341 : public:
342 :
343 : fourier_motzkin_sigma(const rewriter& rewr_)
344 : : rewr(rewr_)
345 : {}
346 :
347 : const data_expression operator()(const data_expression& d) const
348 : {
349 : return is_forall(d) || is_exists(d) ? apply(atermpp::down_cast<abstraction>(d), is_forall(d)) : d;
350 : }
351 : };
352 :
353 : } // namespace data
354 :
355 : } // namespace mcrl2
356 :
357 : #endif // MCRL2_DATA_FOURIER_MOTZKIN_H
|