mCRL2
Searching...
No Matches
fourier_motzkin.h
Go to the documentation of this file.
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//
6// (See accompanying file LICENSE_1_0.txt or copy at
8//
12
13
14#ifndef MCRL2_DATA_FOURIER_MOTZKIN_H
15#define MCRL2_DATA_FOURIER_MOTZKIN_H
16
18
19
20namespace mcrl2
21{
22
23namespace data
24{
25
26
27template < class Data_variable_iterator >
28inline 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 assert(resulting_inequalities.empty());
35 if (mCRL2logEnabled(log::trace))
36 {
37 mCRL2log(log::trace) << "Starting Fourier-Motzkin elimination on " + pp_vector(inequalities_in) + " on variables ";
38 for (Data_variable_iterator i=variables_begin;
39 i!=variables_end; ++i)
40 {
41 mCRL2log(log::trace) << " " << pp(*i) ;
42 }
43 mCRL2log(log::trace) << std::endl;
44 }
45
46 std::vector < linear_inequality > inequalities;
47 std::vector < linear_inequality > equalities;
48 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 for (std::set < variable >::const_iterator i = vars.begin(); i != vars.end(); ++i)
60 {
61 std::map < variable, std::size_t> nr_positive_occurrences;
62 std::map < variable, std::size_t> nr_negative_occurrences;
63 count_occurrences(inequalities,nr_positive_occurrences,nr_negative_occurrences,r);
64
65 bool found=false;
66 std::size_t best_choice=0;
67 variable best_variable;
68 for (std::set < variable >::const_iterator k = vars.begin(); k != vars.end(); ++k)
69 {
70 const std::size_t p=nr_positive_occurrences[*k];
71 const std::size_t n=nr_negative_occurrences[*k];
72 if ((p!=0) || (n!=0))
73 {
74 if (found)
75 {
76 if (n*p<best_choice)
77 {
78 best_choice=n*p;
79 best_variable=*k;
80 }
81 }
82 else
83 {
84 // found is false
85 best_choice=n*p;
86 best_variable=*k;
87 found=true;
88 }
89 }
90 if (found && (best_choice==0))
91 {
92 // Stop searching, we cannot find a better candidate.
93 break;
94 }
95 }
96
97 mCRL2log(log::trace) << "Best variable " << pp(best_variable) << "\n";
98
99 if (!found)
100 {
101 // There are no variables anymore that can be removed from inequalities
102 break;
103 }
104 std::vector < linear_inequality > new_inequalities;
105 std::vector < linear_inequality> inequalities_with_positive_variable;
106 std::vector < linear_inequality> inequalities_with_negative_variable; // Idem.
107
108 for (const linear_inequality& e: inequalities)
109 {
110 const detail::lhs_t::const_iterator factor_it=e.lhs().find(best_variable);
111 if (factor_it==e.lhs().end()) // variable best_variable does not occur in inequality e.
112 {
113 new_inequalities.push_back(e);
114 }
115 else
116 {
117 data_expression f=factor_it->factor();
118 if (is_positive(f,r))
119 {
120 inequalities_with_positive_variable.push_back(e);
121 }
122 else if (is_negative(f,r))
123 {
124 inequalities_with_negative_variable.push_back(e);
125 }
126 else
127 {
128 assert(0);
129 }
130 }
131 }
132
133 mCRL2log(log::trace) << "Positive :" << pp_vector(inequalities_with_positive_variable) << "\n";
134 mCRL2log(log::trace) << "Negative :" << pp_vector(inequalities_with_negative_variable) << "\n";
135 mCRL2log(log::trace) << "Equalities :" << pp_vector(equalities) << "\n";
136 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 for (const linear_inequality& e1: inequalities_with_positive_variable)
145 {
146 for (const linear_inequality& e2: inequalities_with_negative_variable)
147 {
148 const detail::lhs_t::const_iterator e1_best_variable_it=e1.lhs().find(best_variable);
149 const data_expression& e1_factor=e1_best_variable_it->factor();
150 const data_expression& e1_reduced_rhs=real_divides(e1.rhs(),e1_factor);
151 const detail::lhs_t e1_reduced_lhs=detail::remove_variable_and_divide(e1.lhs(),best_variable,e1_factor,r);
152
153 const detail::lhs_t::const_iterator e2_best_variable_it=e2.lhs().find(best_variable);
154 const data_expression& e2_factor=e2_best_variable_it->factor();
155 const data_expression& e2_reduced_rhs=real_divides(e2.rhs(),e2_factor);
156 const detail::lhs_t e2_reduced_lhs=detail::remove_variable_and_divide(e2.lhs(),best_variable,e2_factor,r);
157 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 (e1.comparison()==detail::less_eq) && (e2.comparison()==detail::less_eq)?
161 detail::less,r);
162 if (new_inequality.is_false(r))
163 {
164 resulting_inequalities.push_back(linear_inequality()); // This is a single contraditory inequality;
165 return;
166 }
167 if (!new_inequality.is_true(r))
168 {
169 new_inequalities.push_back(new_inequality);
170 }
171 }
172 }
173 inequalities.swap(new_inequalities);
174 }
175
176 resulting_inequalities.swap(inequalities);
177 // Add the equalities to the inequalities and return the result
178 for (std::vector < linear_inequality > :: const_iterator i=equalities.begin();
179 i!=equalities.end(); ++i)
180 {
181 assert(!i->is_false(r));
182 if (!i->is_true(r))
183 {
184 resulting_inequalities.push_back(*i);
185 }
186 }
187 mCRL2log(log::trace) << "Fourier-Motzkin elimination yields " << pp_vector(resulting_inequalities) << std::endl;
188}
189
202
203inline 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 assert(e_in.sort()==sort_bool::bool_());
210 assert(vars_out.empty());
211
212 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 if (std::find_if(vars_in.begin(),vars_in.end(),[&](variable v){
217 return v.sort()==sort_real::real_() && all_free_variables.find(v) != all_free_variables.end();})==vars_in.end())
218 {
219 vars_out=vars_in;
220 e_out=e_in;
221 return;
222 }
223
224 std::vector <data_expression_list> real_conditions;
225 std::vector <data_expression> non_real_conditions;
226 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 const std::set < variable> non_eliminatable_variables=data::find_all_variables(non_real_conditions);
233
234 variable_list real_sum_variables;
235 variable_list eliminatable_real_sum_variables;
236 for (const variable& v: vars_in)
237 {
238 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 eliminatable_real_sum_variables.push_front(v);
242 }
243 else
244 {
245 vars_out.push_front(v);
246 }
247 }
248 if (vars_out.size()==vars_in.size())
249 {
250 // No variables can be eliminated. Stop here.
251 e_out=e_in;
252 return;
253 }
254
255 // Now apply fourier-motzkin to each conjunct of linear inequalities.
256 std::vector <data_expression>::const_iterator j_n=non_real_conditions.begin();
257 std::set< data_expression > result_disjunction_set;
258
259 for (std::vector <data_expression_list>::const_iterator j_r=real_conditions.begin();
260 j_r!=real_conditions.end(); ++j_r, ++j_n)
261 {
262 const data_expression non_real_condition=*j_n;
263 if (!sort_bool::is_false_function_symbol(non_real_condition))
264 {
265 try
266 {
267 std::vector < linear_inequality > inequalities;
268 // Collect all real conditions from the condition from this summand and put them
269 // into inequalities.
270 for (data_expression_list::const_iterator k=j_r->begin(); k!=j_r->end(); k++)
271 {
272 inequalities.push_back(linear_inequality(*k,r));
273 }
274
275 std::vector < linear_inequality > new_inequalities;
276 fourier_motzkin(inequalities,
277 eliminatable_real_sum_variables.begin(),
278 eliminatable_real_sum_variables.end(),
279 new_inequalities,
280 r);
281 inequalities.clear();
282 remove_redundant_inequalities(new_inequalities,inequalities,r);
283 // Save the result in the output expression.
284 data_expression partial_result=*j_n;
285
286 for(const linear_inequality& l: inequalities)
287 {
288 optimized_and(partial_result, partial_result, l.transform_to_data_expression());
289 }
290 result_disjunction_set.insert(partial_result);
291 }
292 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 vars_out=vars_in;
297 e_out=e_in;
298 return;
299 }
300 }
301 }
302
303 e_out=lazy::join_or(result_disjunction_set.begin(),result_disjunction_set.end());
304}
305
306
317{
318
319 protected:
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
344 : rewr(rewr_)
345 {}
346
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
Iterator for term_appl.
Iterator for term_list.
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
Definition aterm_core.h:152
An abstraction expression.
Definition abstraction.h:26
const variable_list & variables() const
Definition abstraction.h:63
const data_expression & body() const
Definition abstraction.h:68
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
const_iterator begin() const
existential quantification.
Definition exists.h:26
universal quantification.
Definition forall.h:26
bool is_true(const rewriter &r) const
bool is_false(const rewriter &r) const
Rewriter that operates on data expressions.
Definition rewriter.h:81
\brief A data variable
Definition variable.h:28
Standard exception class for reporting runtime errors.
Definition exception.h:27
Contains utility functions for linear inequalities.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
void split_condition(const data_expression &e, std::vector< data_expression_list > &real_conditions, std::vector< data_expression > &non_real_conditions)
This function first splits the given condition e into real conditions and non real conditions....
const lhs_t remove_variable_and_divide(const lhs_t &lhs, const variable &v, const data_expression &f, const rewriter &r)
data_expression join_or(ForwardTraversalIterator first, ForwardTraversalIterator last)
Returns or applied to the sequence of data expressions [first, last)
bool is_false_function_symbol(const atermpp::aterm &e)
Recogniser for function false.
Definition bool.h:119
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
const function_symbol & not_()
Constructor for function symbol !.
Definition bool.h:173
linear_inequality subtract(const linear_inequality &e1, const linear_inequality &e2, const data_expression &f1, const data_expression &f2, const rewriter &r)
Subtract the given equality, multiplied by f1/f2. The result is e1-(f1/f2)e2,.
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:94
bool is_positive(const data_expression &e, const rewriter &r)
void count_occurrences(const std::vector< linear_inequality > &inequalities, std::map< variable, std::size_t > &nr_positive_occurrences, std::map< variable, std::size_t > &nr_negative_occurrences, const rewriter &r)
std::string pp_vector(const TYPE &inequalities)
Print the vector of inequalities to stderr in readable form.
void remove_redundant_inequalities(const std::vector< linear_inequality > &inequalities, std::vector< linear_inequality > &resulting_inequalities, const rewriter &r)
Remove every redundant inequality from a vector of inequalities.
application real_minus(const data_expression &arg0, const data_expression &arg1)
std::string pp(const abstraction &x)
Definition data.cpp:39
application real_divides(const data_expression &arg0, const data_expression &arg1)
std::set< variable > gauss_elimination(const std::vector< linear_inequality > &inequalities, std::vector< linear_inequality > &resulting_equalities, std::vector< linear_inequality > &resulting_inequalities, Variable_iterator variables_begin, Variable_iterator variables_end, const rewriter &r)
Try to eliminate variables from a system of inequalities using Gauss elimination.
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
void fourier_motzkin(const std::vector< linear_inequality > &inequalities_in, Data_variable_iterator variables_begin, Data_variable_iterator variables_end, std::vector< linear_inequality > &resulting_inequalities, const rewriter &r)
data_expression rewrite_with_memory(const data_expression &t, const rewriter &r)
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
bool is_negative(const data_expression &e, const rewriter &r)
void optimized_and(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72