mCRL2
Searching...
No Matches
linear_inequalities.h
Go to the documentation of this file.
1// Author(s): Jeroen Keiren and 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//
14
15
16#ifndef MCRL2_DATA_LINEAR_INEQUALITY_H
17#define MCRL2_DATA_LINEAR_INEQUALITY_H
18
19#include "mcrl2/data/rewriter.h"
21
22namespace mcrl2
23{
24
25namespace data
26{
27
28// Functions below should be made available in the data library.
29data_expression& real_zero();
30data_expression& real_one();
31data_expression& real_minus_one();
32data_expression min(const data_expression& e1,const data_expression& e2,const rewriter&);
33data_expression max(const data_expression& e1,const data_expression& e2,const rewriter&);
34bool is_closed_real_number(const data_expression& e);
35bool is_negative(const data_expression& e,const rewriter& r);
36bool is_positive(const data_expression& e,const rewriter& r);
37bool is_zero(const data_expression& e);
38
39
40// Efficient construction of times on reals.
41// The functions times, divide, plus, minus, negate and abs in the data library are not efficient since they determine the sort at runtime.
43{
45 assert(arg0.sort()==sort_real::real_() && arg1.sort()==sort_real::real_());
46 return application(times_f,arg0,arg1);
47}
48
50{
52 assert(arg0.sort()==sort_real::real_() && arg1.sort()==sort_real::real_());
53 return application(plus_f,arg0,arg1);
54}
55
57{
59 assert(arg0.sort()==sort_real::real_() && arg1.sort()==sort_real::real_());
60 return application(divides_f,arg0,arg1);
61}
62
64{
66 assert(arg0.sort()==sort_real::real_() && arg1.sort()==sort_real::real_());
67 return application(minus_f,arg0,arg1);
68}
69
71{
73 assert(arg.sort()==sort_real::real_());
74 return application(negate_f,arg);
75}
76
78{
80 assert(arg.sort()==sort_real::real_());
81 return application(abs_f,arg);
82}
83
84// End of functions that ought to be defined elsewhere.
85
86
87inline data_expression rewrite_with_memory(const data_expression& t,const rewriter& r);
88
89// prototype
90class linear_inequality;
91namespace detail
92{
93 class lhs_t;
94}
95
96inline std::string pp(const linear_inequality& l);
97template <class TYPE>
98inline std::string pp_vector(const TYPE& inequalities);
99
100namespace detail
101{
103
104 inline std::string pp(const detail::lhs_t& lhs);
105
107 {
108 switch (t)
109 {
110 case detail::less: return detail::less_eq;
111 case detail::less_eq: return detail::less;
112 case detail::equal: return detail::equal;
113 };
114 return detail::equal; // This return statement should be unreachable. It is added to suppress a compiler warning.
115 }
116
117 inline std::string pp(const detail::comparison_t t)
118 {
119 switch (t)
120 {
121 case detail::less: return "<";
122 case detail::less_eq: return "<=";
123 case detail::equal: return "==";
124 };
125 return "##"; // This return statement should be unreachable. It is added to suppress a compiler warning.
126 }
127
129 {
130 static atermpp::function_symbol f("variable_with_a_rational_factor",2);
131 return f;
132 }
133
135 {
136 public:
137 // \brief default constructor
140 {
141 assert(f!=real_zero());
142 }
143
144 // \brief Get the variable in a variable/rational factor pair.
145 const variable& variable_name() const
146 {
148 return atermpp::down_cast<variable>((*this)[0]);
149 }
150
151 // \brief Get the rational factor in a variable/rational factor pair.
152 const data_expression& factor() const
153 {
155 return atermpp::down_cast<data_expression>((*this)[1]);
156 }
157
158 // \brief Check that a term is indeed a variable with a rational factor pair.
160 {
162 }
163
164 // \brief Transform the variable with factor to a data_expression.
166 {
167 return real_times(factor(),variable_name());
168 }
169 };
170
171 // typedef atermpp::term_list<variable_with_a_rational_factor> lhs_t;
172 typedef std::map < variable, data_expression > map_based_lhs_t;
173
174 class lhs_t: public atermpp::term_list<variable_with_a_rational_factor>
175 {
176 public:
180 {}
181
183 explicit lhs_t(const aterm& t)
185 {}
186
188 template <class ITERATOR>
189 lhs_t(const ITERATOR begin, const ITERATOR end)
191 {}
192
194 template <class ITERATOR, class TRANSFORMER>
195 lhs_t(const ITERATOR begin, const ITERATOR end, TRANSFORMER f)
197 {}
198
201 {
202 return std::find_if(begin(),
203 end(),
205 {return p.variable_name()==v;});
206 }
207
209 lhs_t erase(const variable& v) const
210 {
211 std::vector <variable_with_a_rational_factor> result;
212 for(const variable_with_a_rational_factor& p: *this)
213 {
214 if (p.variable_name()!=v)
215 {
216 result.push_back(p);
217 }
218 }
219 return lhs_t(result.begin(),result.end());
220 }
221
223 const data_expression& operator[](const variable& v) const
224 {
227 {
228 return real_zero();
229 }
230 return i->factor();
231 }
232
234 std::size_t count(const variable& v) const
235 {
238 {
239 return 0;
240 }
241 return 1;
242 }
243
245 template <typename SubstitutionFunction>
246 data_expression evaluate(const SubstitutionFunction& beta, const rewriter& r) const
247 {
248 data_expression result=real_zero();
249 bool result_defined=false; // save adding the initial zero.
250 for (const variable_with_a_rational_factor& p: *this)
251 {
252 if (result_defined)
253 {
254 result=rewrite_with_memory(real_plus(result,real_times(beta(p.variable_name()),p.factor())), r);
255 }
256 else
257 {
258 result=rewrite_with_memory(real_times(beta(p.variable_name()),p.factor()), r);
259 result_defined=true;
260 }
261
262 }
263 return result;
264 }
265
266 // \brief Transform this lhs to a data_expression.
268 {
269 if (size()==0)
270 {
271 return real_zero();
272 }
273 data_expression result=real_zero();
274
275 for(const variable_with_a_rational_factor& p: *this)
276 {
277 if (result==real_zero())
278 {
279 result=p.transform_to_data_expression();
280 }
281 else
282 {
283 result=real_plus(result,p.transform_to_data_expression());
284 }
285 }
286 return result;
287 }
288 };
289
291 {
292 assert(is_closed_real_number(e));
293 if (e==real_zero())
294 {
295 detail::map_based_lhs_t::iterator i=new_lhs.find(x);
296 if (i!=new_lhs.end())
297 {
298 new_lhs.erase(i);
299 }
300 }
301 else
302 {
303 new_lhs[x]=e;
304 }
305 }
306
307 inline lhs_t set_factor_for_a_variable(const lhs_t& lhs, const variable& x, const data_expression& e)
308 {
309 assert(is_closed_real_number(e));
310 bool inserted=false;
311 std::vector<variable_with_a_rational_factor> result;
312 for(const variable_with_a_rational_factor& p: lhs)
313 {
314 if (!inserted && x<=p.variable_name())
315 {
316 result.emplace_back(x,e);
317 inserted=true;
318 if (x!=p.variable_name())
319 {
320 result.emplace_back(p.variable_name(),p.factor());
321 }
322 }
323 else result.emplace_back(p.variable_name(),p.factor());
324 }
325 if (!inserted)
326 {
327 result.emplace_back(x,e);
328 }
329 assert(std::find(result.begin(),result.end(),variable_with_a_rational_factor(x,e))!=result.end());
330 return lhs_t(result.begin(),result.end());
331 }
332
333 inline const lhs_t map_to_lhs_type(const map_based_lhs_t& lhs)
334 {
335 lhs_t result;
336 for(map_based_lhs_t::const_reverse_iterator i=lhs.rbegin(); i!=lhs.rend(); ++i)
337 {
338 result.push_front(variable_with_a_rational_factor(i->first,i->second));
339 }
340 return result;
341 }
342
343 inline const lhs_t map_to_lhs_type(const map_based_lhs_t& lhs, const data_expression& factor, const rewriter& r)
344 {
345 assert(factor!=real_one() && factor!=real_minus_one());
346 lhs_t result;
347 for(map_based_lhs_t::const_reverse_iterator i=lhs.rbegin(); i!=lhs.rend(); ++i)
348 {
349 result.push_front(variable_with_a_rational_factor(i->first, rewrite_with_memory(real_divides(i->second,factor), r)));
350 }
351 return result;
352 }
353
354 inline bool is_well_formed(const lhs_t& lhs)
355 {
356 if (lhs.empty())
357 {
358 return true;
359 }
360 if (lhs.front().factor()!=real_one() && lhs.front().factor()!=real_minus_one())
361 {
362 return false;
363 }
364 variable last_variable_seen=lhs.front().variable_name();
365 bool first=true;
366 for(const variable_with_a_rational_factor& p: lhs)
367 {
368 if (!first)
369 {
370 first=false;
371 if (p.variable_name()<=last_variable_seen)
372 {
373 return false;
374 }
375 last_variable_seen=p.variable_name();
376 }
377 }
378 return true;
379 }
380
381 inline const lhs_t remove_variable_and_divide(const lhs_t& lhs, const variable& v, const data_expression& f, const rewriter& r)
382 {
383 std::vector <variable_with_a_rational_factor> result;
384 for(const variable_with_a_rational_factor& p: lhs)
385 {
386 if (p.variable_name()!=v)
387 {
388 result.emplace_back(p.variable_name(),rewrite_with_memory(real_divides(p.factor(),f), r));
389 }
390 }
391 return lhs_t(result.begin(),result.end());
392 }
393
394 inline void emplace_back_if_not_zero(std::vector<detail::variable_with_a_rational_factor>& r, const variable& v, const data_expression& f)
395 {
396 if (f!=real_zero())
397 {
398 r.emplace_back(v,f);
399 }
400 }
401
402
403 template < application Operation(const data_expression&, const data_expression&) >
404 inline const lhs_t meta_operation_constant(const lhs_t& argument, const data_expression& v, const rewriter& r)
405 {
406 std::vector<detail::variable_with_a_rational_factor> result;
407 result.reserve(argument.size());
408 for (const detail::variable_with_a_rational_factor& p: argument)
409 {
410 emplace_back_if_not_zero(result,p.variable_name(), rewrite_with_memory(Operation(v,p.factor()),r));
411 }
412 return lhs_t(result.begin(),result.end());
413 }
414
415 // Template method to add or subtract lhs_t's
416 // template < application Operation(const data_expression&, const data_expression&) >
417 template <class OPERATION>
418 inline lhs_t meta_operation_lhs(const lhs_t& argument1,
419 const lhs_t& argument2,
420 OPERATION operation,
421 const rewriter& r)
422 {
423 std::vector<detail::variable_with_a_rational_factor> result;
424 result.reserve(argument1.size()+argument2.size());
425
426 lhs_t::const_iterator i1=argument1.begin();
427 lhs_t::const_iterator i2=argument2.begin();
428
429 while (i1!=argument1.end() && i2!=argument2.end())
430 {
431 if (i1->variable_name()<i2->variable_name())
432 {
433 emplace_back_if_not_zero(result,i1->variable_name(), rewrite_with_memory(operation(i1->factor(),real_zero()),r));
434 ++i1;
435 }
436 else if (i1->variable_name()>i2->variable_name())
437 {
438 emplace_back_if_not_zero(result,i2->variable_name(), rewrite_with_memory(operation(real_zero(),i2->factor()),r));
439 ++i2;
440 }
441 else
442 {
443 assert(i1->variable_name()==i2->variable_name());
444 emplace_back_if_not_zero(result,i1->variable_name(), rewrite_with_memory(operation(i1->factor(),i2->factor()),r));
445 ++i1;
446 ++i2;
447 }
448 }
449
450 if (i1==argument1.end())
451 {
452 while (i2!=argument2.end())
453 {
454 emplace_back_if_not_zero(result,i2->variable_name(), rewrite_with_memory(operation(real_zero(),i2->factor()),r));
455 ++i2;
456 }
457 }
458 else
459 {
460 while (i1!=argument1.end())
461 {
462 emplace_back_if_not_zero(result,i1->variable_name(), rewrite_with_memory(operation(i1->factor(),real_zero()),r));
463 ++i1;
464 }
465 }
466 return lhs_t(result.begin(),result.end());
467 }
468
469 inline const lhs_t add(const data_expression& v, const lhs_t& argument, const rewriter& r)
470 {
471 return meta_operation_constant<real_plus>(argument,v,r);
472 }
473
474 inline const lhs_t subtract(const lhs_t& argument, const data_expression& v, const rewriter& r)
475 {
476 return meta_operation_constant<real_minus>(argument, v, r);
477 }
478
479 inline const lhs_t multiply(const lhs_t& argument, const data_expression& v, const rewriter& r)
480 {
481 return meta_operation_constant<real_times>(argument, v, r);
482 }
483
484 inline const lhs_t divide(const lhs_t& argument, const data_expression& v, const rewriter& r)
485 {
486 return meta_operation_constant<real_divides>(argument, v, r);
487 }
488
489 inline const lhs_t add(const lhs_t& argument, const lhs_t& e, const rewriter& r)
490 {
491 return meta_operation_lhs(argument,
492 e,
493 [](const data_expression& d1, const data_expression& d2)->data_expression
494 { return real_plus(d1,d2); },
495 r);
496 }
497
498 inline const lhs_t subtract(const lhs_t& argument, const lhs_t& e, const rewriter& r)
499 {
500 return meta_operation_lhs(argument,
501 e,
502 [](const data_expression& d1, const data_expression& d2)->data_expression
503 { return real_minus(d1,d2); },
504 r);
505 }
506
507 inline std::string pp(const lhs_t& lhs)
508 {
509 std::string s;
510 if (lhs.begin()==lhs.end())
511 {
512 s="0";
513 }
514 for (lhs_t::const_iterator i=lhs.begin(); i!=lhs.end(); ++i)
515 {
516 s=s + (i==lhs.begin()?"":" + ") ;
517
518 if (i->factor()==real_one())
519 {
520 s=s + pp(i->variable_name());
521 }
522 else if (i->factor()==real_minus_one())
523 {
524 s=s + "-" + pp(i->variable_name());
525 }
526 else
527 {
528 s=s + data::pp(i->factor()) + "*" + data::pp(i->variable_name());
529 }
530 }
531 return s;
532 }
533
535 {
536 static atermpp::function_symbol f("linear_inequality_less",2);
537 return f;
538 }
539
540
542 {
543 static atermpp::function_symbol f("linear_inequality_less_equal",2);
544 return f;
545 }
546
547
549 {
550 static atermpp::function_symbol f("linear_inequality_equal",2);
551 return f;
552 }
553
554} // end namespace detail
555
557{
558 // The structure of a linear equality is a function application
559 // to two arguments. The function application is either linear_inequality_less,
560 // linear_inequality_less_equal, or linear_inequality_equal. There are two arguments,
561 // namely an ordered list of pairs of a variable and a factor. This list is ordered
562 // on the variables, and a closed expression which forms the right hand side.
563 // The first variable in the list has a factor one or minus one.
564
565 protected:
566
568 const data_expression& e,
570 data_expression& new_rhs,
571 const rewriter& r,
572 const bool negate = false,
573 const data_expression& factor = real_one())
574 {
576 {
577 parse_and_store_expression(binary_left1(e),new_lhs,new_rhs,r,negate,factor);
578 parse_and_store_expression(binary_right1(e),new_lhs,new_rhs,r,!negate,factor);
579 }
581 {
582 parse_and_store_expression(unary_operand1(e),new_lhs,new_rhs,r,!negate,factor);
583 }
585 {
586 parse_and_store_expression(binary_left1(e),new_lhs,new_rhs,r,negate,factor);
587 parse_and_store_expression(binary_right1(e),new_lhs,new_rhs,r,negate,factor);
588 }
590 {
594 {
595 parse_and_store_expression(rhs,new_lhs,new_rhs,r,negate,real_times(lhs,factor));
596 }
597 else if (is_closed_real_number(rhs))
598 {
599 parse_and_store_expression(lhs,new_lhs,new_rhs,r,negate,real_times(rhs,factor));
600 }
601 else
602 {
603 throw mcrl2::runtime_error("Expect constant multiplies expression: " + pp(e) + "\n");
604 }
605 }
606 else if (is_variable(e))
607 {
608 const variable& v = atermpp::down_cast<variable>(e);
609 if(v.sort() != sort_real::real_())
610 {
611 throw mcrl2::runtime_error("Encountered a variable in a real expression which is not of sort real: " + pp(e) + "\n");
612 }
613 const detail::map_based_lhs_t::const_iterator var_factor = new_lhs.find(v);
614
615 const data_expression neg_factor(negate ? real_negate(factor) : factor);
616 const data_expression new_factor(var_factor == new_lhs.end() ? neg_factor : real_plus(var_factor->second, neg_factor));
617 detail::set_factor_for_a_variable(new_lhs, v, rewrite_with_memory(new_factor, r));
618 }
620 {
621 // We are reasoning about the rhs, so apply double negation in case 'negate' is true
622 data_expression add_to_rhs(negate ? e : real_negate(e));
623 if(factor != real_one())
624 {
626 }
627 new_rhs = rewrite_with_memory(real_plus(new_rhs, add_to_rhs), r);
628 }
629 else
630 {
631 throw mcrl2::runtime_error("Expect linear expression over reals: " + pp(e) + "\n");
632 }
633 }
634
635
636 public:
637
640 : linear_inequality(detail::lhs_t(),real_zero(),detail::less)
641 {}
642
645 : atermpp::aterm((t==detail::less?
646 detail::linear_inequality_less():
647 (t==detail::less_eq?detail::linear_inequality_less_equal():detail::linear_inequality_equal())),
648 lhs,r)
649 {
651 assert(t==detail::less || t==detail::less_eq || t==detail::equal);
652 }
653
656 {
657 if (lhs.empty())
658 {
660 return;
661 }
662 // Normalize the linear_inequality such that the first term has factor 1 or -1.
663 data_expression factor=lhs.begin()->factor();
664 if (factor==real_one() || factor==real_minus_one())
665 {
667 return;
668 }
669 factor=rewrite_with_memory(real_abs(factor), r);
670
671 *this=linear_inequality(divide(lhs,factor,r),rewrite_with_memory(real_divides(rhs,factor), r),comparison);
672 }
673
676 const data_expression& rhs,
678 const rewriter& r,
679 const bool negate=false)
680 {
682 data_expression new_rhs(real_zero());
683 parse_and_store_expression(lhs,new_lhs,new_rhs,r,negate);
684 parse_and_store_expression(rhs,new_lhs,new_rhs,r,!negate);
685
686 if (new_lhs.empty())
687 {
688 if ((comparison==detail::equal && new_rhs==real_zero()) ||
689 (comparison==detail::less_eq && (new_rhs == real_zero() || is_positive(new_rhs,r))) ||
690 (comparison==detail::less && is_positive(new_rhs,r)))
691 {
692 // The linear inequality represents true.
694 return;
695 }
696 // The linear inequality represents false.
698 return;
699 }
700
701 // Normalize the linear_inequality such that the first term has factor 1 or -1.
702 data_expression factor=new_lhs.begin()->second;
703 if (factor==real_one() || factor==real_minus_one())
704 {
706 return;
707 }
708 factor=rewrite_with_memory(real_abs(factor), r);
709
710 *this=linear_inequality(detail::map_to_lhs_type(new_lhs,factor,r),rewrite_with_memory(real_divides(new_rhs,factor), r),comparison);
711 }
712
713
714
722
724 const rewriter& r)
725 {
727 bool negate(false);
729 {
731 }
732 else if (is_less_application(e))
733 {
735 }
736 else if (is_less_equal_application(e))
737 {
739 }
740 else if (is_greater_application(e))
741 {
743 negate=true;
744 }
746 {
748 negate=true;
749 }
750 else
751 {
752 throw mcrl2::runtime_error("Unexpected equality or inequality: " + pp(e) + "\n") ;
753 }
754
755 data_expression lhs=data::binary_left(atermpp::down_cast<application>(e));
756 data_expression rhs=data::binary_right(atermpp::down_cast<application>(e));
757 *this=linear_inequality(lhs,rhs,comparison,r,negate);
758
759 }
760
761
763 {
764 return lhs().begin();
765 }
766
768 {
769 return lhs().end();
770 }
771
772 const detail::lhs_t& lhs() const
773 {
774 return atermpp::down_cast<detail::lhs_t>((*this)[0]);
775 }
776
777 const data_expression& rhs() const
778 {
779 return atermpp::down_cast<data_expression>((*this)[1]);
780 }
781
783 {
784 return lhs()[x];
785 }
786
788 {
790 {
791 return detail::less;
792 }
794 {
795 return detail::less_eq;
796 }
797 assert(this->function()==detail::linear_inequality_equal());
798 return detail::equal;
799 }
800
802 {
804 if (c==detail::less_eq)
805 {
807 }
808 if (c==detail::less)
809 {
811 }
812 assert(c==detail::equal);
814 }
815
816 bool is_false(const rewriter& r) const
817 {
818 return lhs().empty() &&
821 }
822
823 bool is_true(const rewriter& r) const
824 {
825 return lhs().empty() &&
828 }
829
834 data_expression& lhs_expression,
835 data_expression& rhs_expression,
836 detail::comparison_t& comparison_operator,
837 const rewriter& r) const
838 {
839 if (lhs_begin()==lhs_end())
840 {
841 lhs_expression=real_zero();
842 rhs_expression=rhs();
843 comparison_operator=comparison();
844 return false;
845 }
846
847 data_expression factor=lhs_begin()->factor();
848
850 {
851 variable v=i->variable_name();
853 data_expression(v));
854 if (i==lhs_begin())
855 {
856 lhs_expression=e;
857 }
858 else
859 {
860 lhs_expression=real_plus(lhs_expression,e);
861 }
862 }
863
864 rhs_expression=rewrite_with_memory(real_divides(rhs(),factor),r);
865 if (is_negative(factor,r))
866 {
867 comparison_operator=negate(comparison());
868 return true;
869 }
870 else
871 {
872 comparison_operator=comparison();
873 return false;
874 }
875 }
876
878 {
879 const detail::lhs_t new_lhs(lhs().begin(),
880 lhs().end(),
883 p.variable_name(),
885
888 {
889 // set_comparison(detail::less_eq);
890 return linear_inequality(new_lhs,new_rhs,detail::less_eq);
891 }
892 else if (comparison()==detail::less_eq)
893 {
894 // set_comparison(detail::less);
895 return linear_inequality(new_lhs,new_rhs,detail::less);
896 }
897 return linear_inequality(new_lhs,new_rhs,detail::equal);
898 }
899
900 void add_variables(std::set < variable >& variable_set) const
901 {
902 for (detail::lhs_t::const_iterator i=lhs().begin(); i!=lhs().end(); ++i)
903 {
904 variable_set.insert(i->variable_name());
905 }
906 }
907};
908
909inline std::string pp(const linear_inequality& l)
910{
911 return pp(l.lhs()) + " " + detail::pp(l.comparison()) + " " + pp(l.rhs());
912}
913
915// where the comparison operator of e1 is kept.
917 const linear_inequality& e2,
918 const data_expression& f1,
919 const data_expression& f2,
920 const rewriter& r)
921{
923 return linear_inequality(
925 [&](const data_expression& d1, const data_expression& d2)->data_expression
926 { return real_minus(d1,real_times(f,d2)); },r),
928 e1.comparison(),
929 r);
930}
931
932// Real zero and real one are an ad hoc solution. They should be provided by
933// the data type library.
934
936{
938 return real_zero;
939}
940
942{
944 return real_one;
945}
946
948{
950 return real_minus_one;
951}
952
953inline data_expression min(const data_expression& e1,const data_expression& e2,const rewriter& r)
954{
956 {
957 return e1;
958 }
960 {
961 return e2;
962 }
963 throw mcrl2::runtime_error("Fail to determine the minimum of: " + pp(e1) + " and " + pp(e2) + "\n");
964}
965
966inline data_expression max(const data_expression& e1,const data_expression& e2,const rewriter& r)
967{
969 {
970 return e1;
971 }
973 {
974 return e2;
975 }
976 throw mcrl2::runtime_error("Fail to determine the maximum of: " + pp(e1) + " and " + pp(e2) + "\n");
977}
978
980{
981 if (e.sort()!=sort_real::real_())
982 {
983 return false;
984 }
985
986 std::set < variable > s=find_all_variables(e);
987 return s.empty();
988}
989
990inline bool is_negative(const data_expression& e,const rewriter& r)
991{
993 if (result==sort_bool::true_())
994 {
995 return true;
996 }
997 if (result==sort_bool::false_())
998 {
999 return false;
1000 }
1001 throw mcrl2::runtime_error("Cannot determine that " + pp(e) + " is smaller than 0");
1002}
1003
1004inline bool is_positive(const data_expression& e,const rewriter& r)
1005{
1007 if (result==sort_bool::true_())
1008 {
1009 return true;
1010 }
1011 if (result==sort_bool::false_())
1012 {
1013 return false;
1014 }
1015 throw mcrl2::runtime_error("Cannot determine that " + pp(e) + " is larger than or equal to 0");
1016}
1017
1018inline bool is_zero(const data_expression& e)
1019{
1020 // Assume data_expression is in normal form.
1021 assert(is_closed_real_number(e));
1022 return (e==real_zero());
1023}
1024
1026template <class TYPE>
1027inline std::string pp_vector(const TYPE& inequalities)
1028{
1029 std::string s="[";
1030 bool first=true;
1031 for (const linear_inequality& l: inequalities)
1032 {
1033 s=s+ (first?"":", ") + pp(l);
1034 first=false;
1035 }
1036 s=s+ "]";
1037 return s;
1038}
1039
1040bool is_inconsistent(
1041 const std::vector < linear_inequality >& inequalities_in,
1042 const rewriter& r,
1043 const bool use_cache=true);
1044
1045
1046// Count the occurrences of variables that occur in inequalities.
1047inline
1049 const std::vector < linear_inequality >& inequalities,
1050 std::map < variable, std::size_t>& nr_positive_occurrences,
1051 std::map < variable, std::size_t>& nr_negative_occurrences,
1052 const rewriter& r)
1053{
1054 for (std::vector < linear_inequality >::const_iterator i=inequalities.begin();
1055 i!=inequalities.end(); ++i)
1056 {
1057 for (detail::lhs_t::const_iterator j=i->lhs_begin(); j!=i->lhs_end(); ++j)
1058 {
1059 if (is_positive(j->factor(),r))
1060 {
1061 nr_positive_occurrences[j->variable_name()]=nr_positive_occurrences[j->variable_name()]+1;
1062 }
1063 else
1064 {
1065 nr_negative_occurrences[j->variable_name()]=nr_negative_occurrences[j->variable_name()]+1;
1066 }
1067 }
1068 }
1069}
1070
1071template < class Variable_iterator >
1072std::set < variable > gauss_elimination(
1073 const std::vector < linear_inequality >& inequalities,
1074 std::vector < linear_inequality >& resulting_equalities,
1075 std::vector < linear_inequality >& resulting_inequalities,
1076 Variable_iterator variables_begin,
1077 Variable_iterator variables_end,
1078 const rewriter& r);
1079
1080
1081
1093 const std::vector < linear_inequality >& inequalities,
1094 const std::vector < linear_inequality > :: iterator i,
1095 const rewriter& r)
1096{
1097#ifndef NDEBUG
1098 // Check that i points to some position in inequalities.
1099 bool found=false;
1100 for (std::vector < linear_inequality >:: const_iterator j=inequalities.begin() ;
1101 j!=inequalities.end() ; ++j)
1102 {
1103 if (j==i)
1104 {
1105 found=true;
1106 break;
1107 }
1108 }
1109 assert(found);
1110#endif
1111 // Check whether the inequalities, with the i-th equality with a reversed comparison operator is inconsistent.
1112 // If yes, the i-th inequality is redundant.
1113 if (i->comparison()==detail::equal)
1114 {
1115 // An inequality t==u is only redundant for equalities if
1116 // t<u and t>u are both inconsistent
1117 const linear_inequality old_inequality=*i;
1118 *i=linear_inequality(i->lhs(),i->rhs(),detail::less);
1119 if (is_inconsistent(inequalities,r))
1120 {
1121 *i=i->invert(r);
1122 if (is_inconsistent(inequalities,r))
1123 {
1124 *i=old_inequality;
1125 return true;
1126 }
1127 }
1128 *i=old_inequality;
1129 return false;
1130 }
1131 else
1132 {
1133 // an inequality t<u, t<=u, t>u and t>=u is redundant in equalities
1134 // if its inversion is inconsistent.
1135 const linear_inequality old_inequality=*i;
1136 *i=i->invert(r);
1137 if (is_inconsistent(inequalities,r))
1138 {
1139 *i=old_inequality;
1140 return true;
1141 }
1142 else
1143 {
1144 *i=old_inequality;
1145 return false;
1146 }
1147 }
1148}
1149
1157// Initially this list must be empty.
1159
1161 const std::vector < linear_inequality >& inequalities,
1162 std::vector < linear_inequality >& resulting_inequalities,
1163 const rewriter& r)
1164{
1165 assert(resulting_inequalities.empty());
1166 if (inequalities.empty())
1167 {
1168 return;
1169 }
1170
1171 // If false is among the inequalities, [false] is the minimal result.
1172 if (is_inconsistent(inequalities,r))
1173 {
1174 resulting_inequalities.push_back(linear_inequality());
1175 return;
1176 }
1177
1178 resulting_inequalities=inequalities;
1179 for (std::size_t i=0; i<resulting_inequalities.size();)
1180 {
1181 // Check whether the inequalities, with the i-th equality with a reversed comparison operator is inconsistent.
1182 // If yes, the i-th inequality is redundant.
1183 if (resulting_inequalities[i].comparison()==detail::equal)
1184 {
1185 // Do nothing, as removing redundant inequalities is expensive.
1186 ++i;
1187 }
1188 else
1189 {
1190 if (is_a_redundant_inequality(resulting_inequalities,
1191 resulting_inequalities.begin()+i,
1192 r))
1193 {
1194 /* The code below does not preserve the ordering in inequalities.
1195 if (i+1<resulting_inequalities.size())
1196 {
1197 // Copy the last element to the current position.
1198 resulting_inequalities[i].swap(resulting_inequalities.back());
1199 }
1200 resulting_inequalities.pop_back(); */
1201 resulting_inequalities.erase(resulting_inequalities.begin()+i);
1202 }
1203 else
1204 {
1205 ++i;
1206 }
1207 }
1208 }
1209}
1210
1211//---------------------------------------------------------------------------------------------------
1212
1214 const variable& xi, // a basic variable
1215 const variable& xj, // a non basic variable
1216 const data_expression& v,
1217 const data_expression& v_delta_correction,
1218 std::map < variable,data_expression >& beta,
1219 std::map < variable,data_expression >& beta_delta_correction,
1220 std::set < variable >& basic_variables,
1221 std::map < variable, detail::lhs_t >& working_equalities,
1222 const rewriter& r)
1223{
1224 mCRL2log(log::trace) << "Pivoting " << pp(xi) << " " << pp(xj) << "\n";
1225 const data_expression aij=working_equalities[xi][xj];
1226 const data_expression theta=rewrite_with_memory(real_divides(real_minus(v,beta[xi]),aij),r);
1227 const data_expression theta_delta_correction=rewrite_with_memory(real_divides(real_minus(v,beta_delta_correction[xi]),aij),r);
1228 beta[xi]=v;
1229 beta_delta_correction[xi]=v_delta_correction;
1230 beta[xj]=rewrite_with_memory(real_plus(beta[xj],theta),r);
1231 beta_delta_correction[xj]=rewrite_with_memory(real_plus(beta_delta_correction[xj],theta_delta_correction),r);
1232
1233 mCRL2log(log::trace) << "Pivoting phase 0\n";
1234 for (std::set < variable >::const_iterator k=basic_variables.begin();
1235 k!=basic_variables.end(); ++k)
1236 {
1237 mCRL2log(log::trace) << "Working equalities " << *k << ": " << pp(working_equalities[*k]) << "\n";
1238 if ((*k!=xi) && (working_equalities[*k].count(xj)>0))
1239 {
1240 const data_expression akj=working_equalities[*k][xj];
1241 beta[*k]=rewrite_with_memory(real_plus(beta[*k],real_times(akj ,theta)),r);
1242 beta_delta_correction[*k]=rewrite_with_memory(real_plus(beta_delta_correction[*k],real_times(akj ,theta_delta_correction)),r);
1243 }
1244 }
1245 // Apply pivoting on variables xi and xj;
1246 mCRL2log(log::trace) << "Pivoting phase 1\n";
1247 basic_variables.erase(xi);
1248 basic_variables.insert(xj);
1249
1250 detail::lhs_t expression_for_xj=working_equalities[xi];
1251 expression_for_xj=expression_for_xj.erase(xj);
1252 expression_for_xj=set_factor_for_a_variable(expression_for_xj,xi,real_minus_one());
1253 expression_for_xj=multiply(expression_for_xj,real_divides(real_minus_one(),aij),r);
1254 mCRL2log(log::trace) << "Expression for xj:" << pp(expression_for_xj) << "\n";
1255 mCRL2log(log::trace) << "Pivoting phase 2\n";
1256 working_equalities.erase(xi);
1257
1258 for (std::map < variable, detail::lhs_t >::iterator j=working_equalities.begin();
1259 j!=working_equalities.end(); ++j)
1260 {
1261 if (j->second.count(xj)>0)
1262 {
1263 const data_expression factor=j->second[xj];
1264 mCRL2log(log::trace) << "VAR: " << pp(j->first) << " Factor " << pp(factor) << "\n";
1265 j->second=j->second.erase(xj);
1266 // We need a temporary copy of expression_for_xj as otherwise the multiply
1267 // below will change this expression.
1268 //detail::lhs_t temporary_expression_for_xj(expression_for_xj);
1270 }
1271 }
1272
1273 working_equalities[xj]=expression_for_xj;
1274
1275 mCRL2log(log::trace) << "Pivoting phase 3\n";
1276 // Calculate the values for beta and beta_delta_correction for the basic variables
1277 for (std::map < variable, detail::lhs_t >::const_iterator i=working_equalities.begin();
1278 i!=working_equalities.end() ; ++i)
1279 {
1280 beta[i->first]=i->second.evaluate(make_map_substitution(beta),r);
1281 beta_delta_correction[i->first]=i->second.evaluate(make_map_substitution(beta_delta_correction),r);
1282 }
1283
1284 mCRL2log(log::trace) << "End pivoting " << pp(xj) << "\n";
1285 if (mCRL2logEnabled(log::trace))
1286 {
1287 for (std::map < variable,data_expression >::const_iterator i=beta.begin();
1288 i!=beta.end(); ++i)
1289 {
1290 mCRL2log(log::trace) << "(1) beta[" << pp(i->first) << "]= " << pp(beta[i->first]) << "+ delta* " << pp(beta_delta_correction[i->first]) << "\n";
1291 }
1292 for (std::map < variable, detail::lhs_t >::const_iterator i=working_equalities.begin();
1293 i!=working_equalities.end() ; ++i)
1294 {
1295 mCRL2log(log::trace) << "EQ: " << pp(i->first) << " := " << pp(i->second) << "\n";
1296 }
1297 }
1298}
1299
1300namespace detail
1301{
1302 /* False end nodes could be associated with NULL */
1304 class inequality_inconsistency_cache;
1305 class inequality_consistency_cache;
1306
1308 {
1311
1312 protected:
1317
1318 public:
1319
1322
1325 {}
1326
1328 const node_type node,
1329 const linear_inequality& inequality,
1331 inequality_inconsistency_cache_base* non_present_branch)
1332 : m_node(node),
1333 m_inequality(inequality),
1334 m_present_branch(present_branch),
1335 m_non_present_branch(non_present_branch)
1336 {}
1337
1339 {
1340 if (m_present_branch!=nullptr)
1341 {
1342 delete m_present_branch;
1343 }
1344 if (m_non_present_branch!=nullptr)
1345 {
1346 delete m_non_present_branch;
1347 }
1348 }
1349 };
1350
1352 {
1353 protected:
1355
1358
1359 public:
1360
1363 {}
1364
1366 {
1367 if (m_cache!=nullptr)
1368 {
1369 delete m_cache;
1370 }
1371 }
1372
1373 bool is_inconsistent(const std::vector < linear_inequality >& inequalities_in_) const
1374 {
1375 std::set < linear_inequality > inequalities_in(inequalities_in_.begin(),inequalities_in_.end());
1376 const inequality_inconsistency_cache_base* current_root=m_cache;
1377 for(const linear_inequality& l: inequalities_in)
1378 {
1379 /* First walk down the three until an endnode is found
1380 that with l<=current_root.m_inequality. */
1381 while (current_root->m_node==intermediate_node && l>current_root->m_inequality)
1382 {
1383 current_root=current_root->m_non_present_branch;
1384 }
1385 if (current_root->m_node==intermediate_node)
1386 {
1387 if (l==current_root->m_inequality)
1388 {
1389 current_root=current_root->m_present_branch;
1390 }
1391 assert(current_root->m_node!=intermediate_node || l<current_root->m_inequality);
1392 }
1393 else
1394 {
1395 return current_root->m_node==true_end_node;
1396 }
1397 }
1398 return current_root->m_node==true_end_node;
1399 }
1400
1401 void add_inconsistent_inequality_set(const std::vector < linear_inequality >& inequalities_in_)
1402 {
1403 std::set < linear_inequality > inequalities_in(inequalities_in_.begin(),inequalities_in_.end());
1405 for(const linear_inequality& l: inequalities_in)
1406 {
1407 /* First walk down the tree until an endnode is found
1408 that with l<=current_root->m_inequality. */
1409 while ((*current_root)->m_node==intermediate_node && l>(*current_root)->m_inequality)
1410 {
1411 current_root=&((*current_root)->m_non_present_branch);
1412 }
1413 if ((*current_root)->m_node==intermediate_node)
1414 {
1415 if (l==(*current_root)->m_inequality)
1416 {
1417 current_root=&((*current_root)->m_present_branch);
1418 assert((*current_root)->m_node!=intermediate_node || l<(*current_root)->m_inequality);
1419 }
1420 else
1421 {
1425 *current_root=new_node;
1426 current_root = &(new_node->m_present_branch);
1427 }
1428 }
1429 else
1430 {
1431 if ((*current_root)->m_node==true_end_node)
1432 {
1433 // A shorter sequence than the linear inequality set is already inconsistent.
1434 // This should not occur, assuming that the linear inequality sequence is checked
1435 // in in this cache, before being proven inconsistent.
1436 assert(0);
1437 }
1438 else
1439 {
1440 // Add the remaining sequence.
1443 *current_root=new_node;
1444 current_root = &(new_node->m_present_branch);
1445 }
1446 }
1447 }
1448 // At this point the sequence of inequalities has been explored, but the tree has not ended.
1449 // We expect the current node to be a true_end_node. If not, we replace it by one.
1450 if ((*current_root)->m_node!=true_end_node)
1451 {
1452 assert(*current_root!=nullptr);
1453 delete *current_root;
1455 }
1456 }
1457 };
1458
1460 {
1461 protected:
1463
1466
1467 public:
1468
1471 {
1472 }
1473
1475 {
1476 if (m_cache!=nullptr)
1477 {
1478 delete m_cache;
1479 }
1480 }
1481
1482 // Sort the vector inequalities_in if not sorted.
1483 bool is_consistent(const std::vector < linear_inequality >& inequalities_in_) const
1484 {
1485 std::set < linear_inequality > inequalities_in(inequalities_in_.begin(),inequalities_in_.end());
1487 for(std::set < linear_inequality >::const_iterator i=inequalities_in.begin(); i!=inequalities_in.end(); ++i)
1488 {
1489 while (current_root->m_node==intermediate_node && *i>current_root->m_inequality)
1490 {
1491 current_root=current_root->m_non_present_branch;
1492 }
1493 if (current_root->m_node==intermediate_node)
1494 {
1495 if (*i==current_root->m_inequality)
1496 {
1497 current_root=current_root->m_present_branch;
1498 }
1499 else
1500 {
1501 return false; // there are more inequalities than available in the tree. We know nothing about it being consistent.
1502 }
1503 assert(current_root->m_node!=intermediate_node || *i<current_root->m_inequality);
1504 }
1505 else
1506 {
1507 return current_root->m_node!=false_end_node && i==inequalities_in.end();
1508 }
1509 }
1510 return true;
1511 }
1512
1513 void add_consistent_inequality_set(const std::vector < linear_inequality >& inequalities_in_)
1514 {
1515 std::set < linear_inequality > inequalities_in(inequalities_in_.begin(),inequalities_in_.end());
1517 for(const linear_inequality& l: inequalities_in)
1518 {
1519 /* First walk down the three until an endnode is found
1520 with l<=current_root->m_inequality. */
1521 while ((*current_root)->m_node==intermediate_node && l>(*current_root)->m_inequality)
1522 {
1523 current_root=&((*current_root)->m_non_present_branch);
1524 }
1525 if ((*current_root)->m_node==intermediate_node)
1526 {
1527 if (l==(*current_root)->m_inequality)
1528 {
1529 current_root=&((*current_root)->m_present_branch);
1530 assert((*current_root)->m_node!=intermediate_node || l<(*current_root)->m_inequality);
1531 }
1532 else
1533 {
1537 *current_root=new_node;
1538 current_root = &(new_node->m_present_branch);
1539 }
1540 }
1541 else
1542 {
1543 // Add the remaining sequence.
1546 *current_root=new_node;
1547 current_root = &(new_node->m_present_branch);
1548 }
1549 }
1550 }
1551 };
1552
1553}
1554
1555
1571 const std::vector < linear_inequality >& inequalities_in,
1572 const rewriter& r,
1573 const bool use_cache/*=true*/)
1574{
1575 // Transform the linear inequalities into a vector of equalities and a
1576 // sequence of constraints on variables. All variables, including
1577 // those that will be generated as slack variables will have values indicated
1578 // by beta, which must lie between the lowerbounds and the upperbounds.
1579
1580 // First remove all equalities by Gauss elimination and make a fresh variable
1581 // generator.
1582
1583 mCRL2log(log::trace) << "Starting an inconsistency check on " + pp_vector(inequalities_in) << "\n";
1584
1585 static detail::inequality_inconsistency_cache inconsistency_cache;
1586 static detail::inequality_consistency_cache consistency_cache;
1587
1588 if (use_cache && consistency_cache.is_consistent(inequalities_in))
1589 {
1590 assert(!is_inconsistent(inequalities_in,r,false));
1591 return false;
1592 }
1593 if (use_cache && inconsistency_cache.is_inconsistent(inequalities_in))
1594 {
1595 assert(is_inconsistent(inequalities_in,r,false));
1596 return true;
1597 }
1598 // The required data structures
1599 std::map < variable,data_expression > lowerbounds;
1600 std::map < variable,data_expression > upperbounds;
1601 std::map < variable,data_expression > beta;
1602 std::map < variable,data_expression > lowerbounds_delta_correction;
1603 std::map < variable,data_expression > upperbounds_delta_correction;
1604 std::map < variable,data_expression > beta_delta_correction;
1605 std::set < variable > non_basic_variables;
1606 std::set < variable > basic_variables;
1607 std::map < variable, detail::lhs_t > working_equalities;
1608
1609 set_identifier_generator fresh_variable_name;
1610
1611 for (std::vector < linear_inequality >::const_iterator i=inequalities_in.begin();
1612 i!=inequalities_in.end(); ++i)
1613 {
1614 if (i->is_false(r))
1615 {
1616 mCRL2log(log::trace) << "Inconsistent, because linear inequalities contains an inconsistent inequality\n";
1617 if (use_cache)
1618 {
1620 assert(inconsistency_cache.is_inconsistent(inequalities_in));
1621 }
1622 return true;
1623 }
1625 for (detail::lhs_t::const_iterator j=i->lhs_begin();
1626 j!=i->lhs_end(); ++j)
1627 {
1629 }
1630 }
1631
1632 std::vector < linear_inequality > inequalities;
1633 std::vector < linear_inequality > equalities;
1634 non_basic_variables=
1635 gauss_elimination(inequalities_in,
1636 equalities, // Store all resulting equalities here.
1637 inequalities, // Store all resulting non equalities here.
1638 non_basic_variables.begin(),
1639 non_basic_variables.end(),
1640 r);
1641
1642 assert(equalities.size()==0); // There are no resulting equalities left.
1643 non_basic_variables.clear(); // gauss_elimination has removed certain variables. So, we reconstruct the non
1644 // basic variables again below.
1645
1646 mCRL2log(log::trace) << "Resulting equalities " << pp_vector(equalities) << "\n";
1647 mCRL2log(log::trace) << "Resulting inequalities " << pp_vector(inequalities) << "\n";
1648
1649 // Now bring the linear equalities in the basic form described
1650 // in the article by Bruno Dutertre and Leonardo de Moura.
1651
1652 // First set lower and upperbounds, and introduce slack variables
1653 // if required.
1654 for (std::vector < linear_inequality >::iterator i=inequalities.begin();
1655 i!=inequalities.end(); ++i)
1656 {
1657 mCRL2log(log::trace) << "Investigate inequality: " << ":=" << pp(*i) << " || " << pp(i->lhs()) << "\n";
1658 if (i->is_false(r))
1659 {
1660 mCRL2log(log::trace) << "Inconsistent, because linear inequalities contains an inconsistent inequality after Gauss elimination\n";
1661 if (use_cache)
1662 {
1664 assert(inconsistency_cache.is_inconsistent(inequalities_in));
1665 }
1666 return true;
1667 }
1668 if (!i->is_true(r)) // This inequality is redundant and can be skipped.
1669 {
1670 assert(i->comparison()!=detail::equal);
1671 assert(i->lhs().size()>0); // this signals a redundant or an inconsistent inequality.
1673
1674 if (i->lhs().size()==1) // the left hand side consists of a single variable.
1675 {
1676 variable v=i->lhs_begin()->variable_name();
1677 data_expression factor=i->lhs_begin()->factor();
1678 assert(factor!=real_zero());
1679 data_expression bound=rewrite_with_memory(real_divides(i->rhs(),factor),r);
1680 if (is_positive(factor,r))
1681 {
1682 // The inequality has the shape factor*v<=c or factor*v<c with factor positive
1683 if ((upperbounds.count(v)==0) ||
1684 (rewrite_with_memory(less(bound,upperbounds[v]),r)==sort_bool::true_()))
1685 {
1686 upperbounds[v]=bound;
1687 upperbounds_delta_correction[v]=
1688 ((i->comparison()==detail::less)?real_minus_one():real_zero());
1689
1690 }
1691 else
1692 {
1693 if (bound==upperbounds[v])
1694 {
1695 upperbounds_delta_correction[v]=
1696 min(upperbounds_delta_correction[v],
1697 ((i->comparison()==detail::less)?real_minus_one():real_zero()),r);
1698 }
1699 }
1700 }
1701 else
1702 {
1703 // The inequality has the shape factor*v<=c or factor*v<c with factor negative
1704 if ((lowerbounds.count(v)==0) ||
1705 (rewrite_with_memory(less(lowerbounds[v],bound),r)==sort_bool::true_()))
1706 {
1707 lowerbounds[v]=bound;
1708 lowerbounds_delta_correction[v]=
1709 ((i->comparison()==detail::less)?real_one():real_zero());
1710 }
1711 else
1712 {
1713 if (bound==lowerbounds[v])
1714 {
1715 lowerbounds_delta_correction[v]=
1716 max(lowerbounds_delta_correction[v],
1717 ((i->comparison()==detail::less)?real_one():real_zero()),r);
1718 }
1719 }
1720 }
1721 }
1722 else
1723 {
1724 // The inequality has more than one variable at the left hand side.
1725 // We transform it into an equation with a new slack variable.
1726 variable new_basic_variable(fresh_variable_name("slack_var"), sort_real::real_());
1727 basic_variables.insert(new_basic_variable);
1728 upperbounds[new_basic_variable]=i->rhs();
1729 upperbounds_delta_correction[new_basic_variable]=
1730 ((i->comparison()==detail::less)?real_minus_one():real_zero());
1731 working_equalities[new_basic_variable]=i->lhs();
1732 mCRL2log(log::trace) << "New slack variable: " << pp(new_basic_variable) << ":=" << pp(*i) << " " << pp(i->lhs()) << "\n";
1733 }
1734 }
1735 }
1736 // Now set the values for beta:
1737 // The beta values for the non basic variables must satisfy the lower and
1738 // upperbounds.
1739 for (std::set < variable >::const_iterator i=non_basic_variables.begin();
1740 i!=non_basic_variables.end(); ++i)
1741 {
1742 if (lowerbounds.count(*i)>0)
1743 {
1744 if ((upperbounds.count(*i)>0) &&
1745 ((rewrite_with_memory(less(upperbounds[*i],lowerbounds[*i]),r)==sort_bool::true_()) ||
1746 ((upperbounds[*i]==lowerbounds[*i]) &&
1747 (rewrite_with_memory(less(upperbounds_delta_correction[*i],lowerbounds_delta_correction[*i]),r)==sort_bool::true_()))))
1748 {
1749 mCRL2log(log::trace) << "Inconsistent, preprocessing " << pp(*i) << "\n";
1750 if (use_cache)
1751 {
1753 assert(inconsistency_cache.is_inconsistent(inequalities_in));
1754 }
1755 return true; // Inconsistent.
1756 }
1757 beta[*i]=lowerbounds[*i];
1758 beta_delta_correction[*i]=lowerbounds_delta_correction[*i];
1759 }
1760 else if (upperbounds.count(*i)>0)
1761 {
1762 beta[*i]=upperbounds[*i];
1763 beta_delta_correction[*i]=upperbounds_delta_correction[*i];
1764 }
1765 else // *i has neither a lower or an upperbound
1766 {
1767 beta[*i]=real_zero();
1768 beta_delta_correction[*i]=real_zero();
1769 }
1770 mCRL2log(log::trace) << "(2) beta[" << pp(*i) << "]=" << pp(beta[*i])<< "+delta*" << pp(beta_delta_correction[*i]) <<"\n";
1771 }
1772
1773 // Subsequently set the values for the basic variables
1774 for (std::set < variable >::const_iterator i=basic_variables.begin();
1775 i!=basic_variables.end(); ++i)
1776 {
1777 beta[*i]=working_equalities[*i].evaluate(make_map_substitution(beta),r);
1778 beta_delta_correction[*i]=working_equalities[*i].
1779 evaluate(make_map_substitution(beta_delta_correction),r);
1780 mCRL2log(log::trace) << "(3) beta[" << pp(*i) << "]=" << pp(beta[*i])<< "+delta*" << pp(beta_delta_correction[*i]) <<"\n";
1781 }
1782
1783 // Now the basic data structure has been set up.
1784 // We must find the first basic variable that does not satisfy its
1785 // upper and bounds. This is essentially the check algorithm in the
1786 // article by Bruno Dutertre and Leonardo de Moura.
1787
1788 for (; true ;)
1789 {
1790 // select the smallest basic variable that does not satisfy the bounds.
1791 bool found=false;
1792 bool lowerbound_violation = false;
1793 variable xi;
1794 for (std::set < variable > :: const_iterator i=basic_variables.begin() ;
1795 i!=basic_variables.end() ; ++i)
1796 {
1797 mCRL2log(log::trace) << "Evaluate start\n";
1798 assert(!found);
1799 data_expression value=beta[*i]; // working_equalities[*i].evaluate(beta,r);
1800 data_expression value_delta_correction=beta_delta_correction[*i]; // working_equalities[*i].evaluate(beta_delta_correction,r);
1801 mCRL2log(log::trace) << "Evaluate end\n";
1802 if ((upperbounds.count(*i)>0) &&
1803 ((rewrite_with_memory(less(upperbounds[*i],value),r)==sort_bool::true_()) ||
1804 ((upperbounds[*i]==value) &&
1805 (rewrite_with_memory(less(upperbounds_delta_correction[*i],value_delta_correction),r)==sort_bool::true_()))))
1806 {
1807 // The value of variable *i does not satisfy its upperbound. This must
1808 // be corrected using pivoting.
1809 mCRL2log(log::trace) << "Upperbound violation " << pp(*i) << " bound: " << pp(upperbounds[*i]) << "\n";
1810 found=true;
1811 xi=*i;
1812 lowerbound_violation=false;
1813 break;
1814 }
1815 else if ((lowerbounds.count(*i)>0) &&
1816 ((rewrite_with_memory(less(value,lowerbounds[*i]),r)==sort_bool::true_()) ||
1817 ((lowerbounds[*i]==value) &&
1818 (rewrite_with_memory(less(value_delta_correction,lowerbounds_delta_correction[*i]),r)==sort_bool::true_()))))
1819 {
1820 // The value of variable *i does not satisfy its upperbound. This must
1821 // be corrected using pivoting.
1822 mCRL2log(log::trace) << "Lowerbound violation " << pp(*i) << " bound: " << pp(lowerbounds[*i]) << "\n";
1823 found=true;
1824 xi=*i;
1825 lowerbound_violation=true;
1826 break;
1827 }
1828 }
1829 if (!found)
1830 {
1831 // The inequalities are consistent. Return false.
1832 mCRL2log(log::trace) << "Consistent while pivoting\n";
1833 if (use_cache)
1834 {
1836 assert(consistency_cache.is_consistent(inequalities_in));
1837 }
1838 return false;
1839 }
1840
1841 mCRL2log(log::trace) << "The smallest basic variable that does not satisfy the bounds is " << pp(xi) << "\n";
1842 if (lowerbound_violation)
1843 {
1844 mCRL2log(log::trace) << "Lowerbound violation \n";
1845 // select the smallest non-basic variable with which pivoting can take place.
1846 bool found=false;
1847 const detail::lhs_t& lhs=working_equalities[xi];
1848 for (detail::lhs_t::const_iterator xj_it=lhs.begin(); xj_it!=lhs.end(); ++xj_it)
1849 {
1850 const variable xj=xj_it->variable_name();
1851 mCRL2log(log::trace) << pp(xj) << " -- " << pp(xj_it->factor()) << "\n";
1852 if ((is_positive(xj_it->factor(),r) &&
1853 ((upperbounds.count(xj)==0) ||
1854 ((rewrite_with_memory(less(beta[xj],upperbounds[xj]),r)==sort_bool::true_())||
1855 ((beta[xj]==upperbounds[xj])&& (rewrite_with_memory(less(beta_delta_correction[xj],upperbounds_delta_correction[xj]),r)==sort_bool::true_()))))) ||
1856 (is_negative(xj_it->factor(),r) &&
1857 ((lowerbounds.count(xj)==0) ||
1858 ((rewrite_with_memory(greater(beta[xj],lowerbounds[xj]),r)==sort_bool::true_())||
1859 ((beta[xj]==lowerbounds[xj]) && (rewrite_with_memory(greater(beta_delta_correction[xj],lowerbounds_delta_correction[xj]),r)==sort_bool::true_()))))))
1860 {
1861 found=true;
1862 pivot_and_update(xi,xj,lowerbounds[xi],lowerbounds_delta_correction[xi],
1863 beta, beta_delta_correction,
1864 basic_variables,working_equalities,r);
1865 break;
1866 }
1867 }
1868 if (!found)
1869 {
1870 // The inequalities are inconsistent.
1871 mCRL2log(log::trace) << "Inconsistent while pivoting\n";
1872 if (use_cache)
1873 {
1875 assert(inconsistency_cache.is_inconsistent(inequalities_in));
1876 }
1877 return true;
1878 }
1879
1880 }
1881 else // Upperbound violation.
1882 {
1883 mCRL2log(log::trace) << "Upperbound violation \n";
1884 // select the smallest non-basic variable with which pivoting can take place.
1885 bool found=false;
1886 for (detail::lhs_t::const_iterator xj_it=working_equalities[xi].begin();
1887 xj_it!=working_equalities[xi].end(); ++xj_it)
1888 {
1889 const variable xj=xj_it->variable_name();
1890 mCRL2log(log::trace) << pp(xj) << " -- " << pp(xj_it->factor()) << " POS " << is_positive(xj_it->factor(),r) << "\n";
1891 if ((is_negative(xj_it->factor(),r) &&
1892 ((upperbounds.count(xj)==0) ||
1893 ((rewrite_with_memory(less(beta[xj],upperbounds[xj]),r)==sort_bool::true_()) ||
1894 ((beta[xj]==upperbounds[xj])&& (rewrite_with_memory(less(beta_delta_correction[xj],upperbounds_delta_correction[xj]),r)==sort_bool::true_()))))) ||
1895 (is_positive(xj_it->factor(),r) &&
1896 ((lowerbounds.count(xj)==0) ||
1897 ((rewrite_with_memory(greater(beta[xj],lowerbounds[xj]),r)==sort_bool::true_()) ||
1898 ((beta[xj]==lowerbounds[xj]) && (rewrite_with_memory(greater(beta_delta_correction[xj],lowerbounds_delta_correction[xj]),r)==sort_bool::true_()))))))
1899 {
1900 found=true;
1901 pivot_and_update(xi,xj,upperbounds[xi],upperbounds_delta_correction[xi],
1902 beta,beta_delta_correction,
1903 basic_variables,working_equalities,r);
1904 break;
1905 }
1906 }
1907 if (!found)
1908 {
1909 // The inequalities are inconsistent.
1910 mCRL2log(log::trace) << "Inconsistent while pivoting (1)\n";
1911 if (use_cache)
1912 {
1914 assert(inconsistency_cache.is_inconsistent(inequalities_in));
1915 }
1916 return true;
1917 }
1918 }
1919 }
1920}
1921
1922//---------------------------------------------------------------------------------------------------
1923
1924
1942
1943template < class Variable_iterator >
1944std::set < variable > gauss_elimination(
1945 const std::vector < linear_inequality >& inequalities,
1946 std::vector < linear_inequality >& resulting_equalities,
1947 std::vector < linear_inequality >& resulting_inequalities,
1948 Variable_iterator variables_begin,
1949 Variable_iterator variables_end,
1950 const rewriter& r)
1951{
1952 std::set < variable > remaining_variables;
1953
1954 // First copy equalities to the resulting_equalities and the inequalites to resulting_inequalities.
1955 for (std::vector < linear_inequality > ::const_iterator j = inequalities.begin(); j != inequalities.end(); ++j)
1956 {
1957 if (j->is_false(r))
1958 {
1959 // The input contains false. Return false and stop.
1960 resulting_equalities.clear();
1961 resulting_inequalities.clear();
1962 resulting_inequalities.push_back(linear_inequality());
1963 return remaining_variables;
1964 }
1965 else if (!j->is_true(r)) // Do not consider redundant equations.
1966 {
1967 if (j->comparison()==detail::equal)
1968 {
1969 resulting_equalities.push_back(*j);
1970 }
1971 else
1972 {
1973 resulting_inequalities.push_back(*j);
1974 }
1975 }
1976 }
1977
1978 // Now find out whether there are variables that occur in an equality, so
1979 // that we can perform gauss elimination.
1980 for (Variable_iterator i = variables_begin; i != variables_end; ++i)
1981 {
1982 std::size_t j;
1983 for (j=0; j<resulting_equalities.size(); ++j)
1984 {
1985 bool check_equalities_for_redundant_inequalities(false);
1986 std::set < variable > vars;
1988 if (vars.count(*i)>0)
1989 {
1990 // Equality *j contains data variable *i.
1991 // Perform gauss elimination, and break the loop.
1992
1993 for (std::size_t k = 0; k < resulting_inequalities.size();)
1994 {
1995 resulting_inequalities[k]=subtract(resulting_inequalities[k],
1996 resulting_equalities[j],
1997 resulting_inequalities[k].get_factor_for_a_variable(*i),
1998 resulting_equalities[j].get_factor_for_a_variable(*i),
1999 r);
2000 if (resulting_inequalities[k].is_false(r))
2001 {
2002 // The input is inconsistent. Return false.
2003 resulting_equalities.clear();
2004 resulting_inequalities.clear();
2005 resulting_inequalities.push_back(linear_inequality());
2006 remaining_variables.clear();
2007 return remaining_variables;
2008 }
2009 else if (resulting_inequalities[k].is_true(r))
2010 {
2011 // Inequality k has become redundant, and can be removed.
2012 if ((k+1)<resulting_inequalities.size())
2013 {
2014 resulting_inequalities[k].swap(resulting_inequalities.back());
2015 }
2016 resulting_inequalities.pop_back();
2017 }
2018 else
2019 {
2020 ++k;
2021 }
2022 }
2023
2024 for (std::size_t k = 0; k<resulting_equalities.size();)
2025 {
2026 if (k==j)
2027 {
2028 ++k;
2029 }
2030 else
2031 {
2032 resulting_equalities[k]=subtract(
2033 resulting_equalities[k],
2034 resulting_equalities[j],
2035 resulting_equalities[k].get_factor_for_a_variable(*i),
2036 resulting_equalities[j].get_factor_for_a_variable(*i),
2037 r);
2038 if (resulting_equalities[k].is_false(r))
2039 {
2040 // The input is inconsistent. Return false.
2041 resulting_equalities.clear();
2042 resulting_inequalities.clear();
2043 resulting_inequalities.push_back(linear_inequality());
2044 remaining_variables.clear();
2045 return remaining_variables;
2046 }
2047 else if (resulting_equalities[k].is_true(r))
2048 {
2049 // Equality k has become redundant, and can be removed.
2050 if (j+1==resulting_equalities.size())
2051 {
2052 // It is not possible to move move the last element of resulting
2053 // inequalities to position k, because j is at this last position.
2054 // Hence, we must recall to check the resulting_equalities for inequalities
2055 // that are true.
2056 check_equalities_for_redundant_inequalities=true;
2057 }
2058 else
2059 {
2060 if ((k+1)<resulting_equalities.size())
2061 {
2062 resulting_equalities[k].swap(resulting_equalities.back());
2063 }
2064 resulting_equalities.pop_back();
2065 }
2066 }
2067 else
2068 {
2069 ++k;
2070 }
2071 }
2072 }
2073
2074 // Remove equation j.
2075
2076 if (j+1<resulting_equalities.size())
2077 {
2078 resulting_equalities[j].swap(resulting_equalities.back());
2079 }
2080 resulting_equalities.pop_back();
2081
2082 // If there are unremoved resulting equalities, remove them now.
2083 if (check_equalities_for_redundant_inequalities)
2084 {
2085 for (std::size_t k = 0; k<resulting_equalities.size();)
2086 {
2087 if (resulting_equalities[k].is_true(r))
2088 {
2089 // Equality k is redundant, and can be removed.
2090 if ((k+1)<resulting_equalities.size())
2091 {
2092 resulting_equalities[k].swap(resulting_equalities.back());
2093 }
2094 resulting_equalities.pop_back();
2095 }
2096 else
2097 {
2098 ++k;
2099 }
2100 }
2101 }
2102 }
2103 }
2104 remaining_variables.insert(*i);
2105 }
2106
2107 return remaining_variables;
2108}
2109
2110// The introduction of the function rewrite_with_memory using a
2111// hash table here is a temporary trick, to boost
2112// performance, which is slow due to translations necessary from and to
2113// rewrite format.
2114
2116 const data_expression& t,const rewriter& r)
2117{
2118 static std::map < data_expression, data_expression > rewrite_hash_table;
2119 std::map < data_expression, data_expression > :: iterator i=rewrite_hash_table.find(t);
2120 if (i==rewrite_hash_table.end())
2121 {
2122 data_expression t1=r(t);
2123 rewrite_hash_table.insert(std::make_pair(t, t1));
2124 return t1;
2125 }
2126 return i->second;
2127}
2128
2129} // namespace data
2130
2131} // namespace mcrl2
2132
2133#endif // MCRL2_DATA_LINEAR_INEQUALITY_H
const_iterator end() const
Returns a const_iterator pointing past the last argument.
Definition aterm.h:172
aterm()
Default constructor.
Definition aterm.h:48
const_iterator begin() const
Returns an iterator pointing to the first argument.
Definition aterm.h:165
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
Iterator for term_appl.
A list of aterm objects.
Definition aterm_list.h:24
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 Term & front() const
Returns the first element of the list.
Definition aterm_list.h:239
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.
term_list() noexcept
Default constructor. Creates an empty list.
Definition aterm_list.h:61
An application of a data expression to a number of arguments.
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
const_iterator begin() const
void add_consistent_inequality_set(const std::vector< linear_inequality > &inequalities_in_)
inequality_consistency_cache & operator=(const inequality_consistency_cache &)=delete
inequality_consistency_cache(const inequality_consistency_cache &)=delete
inequality_inconsistency_cache_base * m_cache
bool is_consistent(const std::vector< linear_inequality > &inequalities_in_) const
inequality_inconsistency_cache_base & operator=(const inequality_inconsistency_cache_base &)=delete
inequality_inconsistency_cache_base(const node_type node, const linear_inequality &inequality, inequality_inconsistency_cache_base *present_branch, inequality_inconsistency_cache_base *non_present_branch)
inequality_inconsistency_cache_base(const inequality_inconsistency_cache_base &)=delete
bool is_inconsistent(const std::vector< linear_inequality > &inequalities_in_) const
inequality_inconsistency_cache & operator=(const inequality_consistency_cache &)=delete
inequality_inconsistency_cache(const inequality_inconsistency_cache &)=delete
void add_inconsistent_inequality_set(const std::vector< linear_inequality > &inequalities_in_)
lhs_t(const aterm &t)
Constructor from an aterm.
const data_expression & operator[](const variable &v) const
Give the factor of variable v.
data_expression transform_to_data_expression() const
lhs_t erase(const variable &v) const
Erase a variable and its factor.
std::size_t count(const variable &v) const
Give the factor of variable v.
lhs_t(const ITERATOR begin, const ITERATOR end, TRANSFORMER f)
Constructor.
data_expression evaluate(const SubstitutionFunction &beta, const rewriter &r) const
Evaluate the variables in this lhs_t according to the subsitution function.
lhs_t::const_iterator find(const variable &v) const
Give an iterator of the factor/variable pair for v, or end() if v does not occur.
lhs_t(const ITERATOR begin, const ITERATOR end)
Constructor.
variable_with_a_rational_factor(const variable &v, const data_expression &f)
\brief A function symbol
const detail::lhs_t & lhs() const
linear_inequality invert(const rewriter &r)
bool typical_pair(data_expression &lhs_expression, data_expression &rhs_expression, detail::comparison_t &comparison_operator, const rewriter &r) const
Return this inequality as a typical pair of terms of the form <x1+c2 x2+...+cn xn,...
linear_inequality()
Constructor yielding an inconsistent inequality.
bool is_true(const rewriter &r) const
void add_variables(std::set< variable > &variable_set) const
bool is_false(const rewriter &r) const
linear_inequality(const data_expression &e, const rewriter &r)
Constructor that constructs a linear inequality out of a data expression.
linear_inequality(const data_expression &lhs, const data_expression &rhs, const detail::comparison_t comparison, const rewriter &r, const bool negate=false)
constructor.
data_expression transform_to_data_expression() const
static void parse_and_store_expression(const data_expression &e, detail::map_based_lhs_t &new_lhs, data_expression &new_rhs, const rewriter &r, const bool negate=false, const data_expression &factor=real_one())
linear_inequality(const detail::lhs_t &lhs, const data_expression &r, detail::comparison_t t)
Basic constructor.
detail::lhs_t::const_iterator lhs_begin() const
detail::lhs_t::const_iterator lhs_end() const
linear_inequality(const detail::lhs_t &lhs, const data_expression &rhs, detail::comparison_t comparison, const rewriter &r)
constructor.
const data_expression & rhs() const
data_expression get_factor_for_a_variable(const variable &x)
detail::comparison_t comparison() const
Rewriter that operates on data expressions.
Definition rewriter.h:81
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
Adds the identifier s to the context.
\brief A data variable
Definition variable.h:28
const sort_expression & sort() const
Definition variable.h:43
Standard exception class for reporting runtime errors.
Definition exception.h:27
The class rewriter.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
The main namespace for the aterm++ library.
Definition algorithm.h:21
atermpp::function_symbol linear_inequality_equal()
const lhs_t map_to_lhs_type(const map_based_lhs_t &lhs)
const lhs_t remove_variable_and_divide(const lhs_t &lhs, const variable &v, const data_expression &f, const rewriter &r)
atermpp::function_symbol linear_inequality_less()
void emplace_back_if_not_zero(std::vector< detail::variable_with_a_rational_factor > &r, const variable &v, const data_expression &f)
const lhs_t add(const data_expression &v, const lhs_t &argument, const rewriter &r)
bool is_well_formed(const lhs_t &lhs)
detail::comparison_t negate(const detail::comparison_t t)
std::map< variable, data_expression > map_based_lhs_t
atermpp::function_symbol linear_inequality_less_equal()
lhs_t meta_operation_lhs(const lhs_t &argument1, const lhs_t &argument2, OPERATION operation, const rewriter &r)
const lhs_t subtract(const lhs_t &argument, const data_expression &v, const rewriter &r)
std::string pp(const detail::lhs_t &lhs)
const lhs_t meta_operation_constant(const lhs_t &argument, const data_expression &v, const rewriter &r)
void set_factor_for_a_variable(detail::map_based_lhs_t &new_lhs, const variable &x, const data_expression &e)
const lhs_t multiply(const lhs_t &argument, const data_expression &v, const rewriter &r)
atermpp::function_symbol f_variable_with_a_rational_factor()
const lhs_t divide(const lhs_t &argument, const data_expression &v, const rewriter &r)
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1059
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1237
function_symbol divides(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1407
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition real1.h:1136
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1152
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:48
function_symbol abs(const sort_expression &s0)
Definition real1.h:735
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition real1.h:1306
function_symbol negate(const sort_expression &s0)
Definition real1.h:810
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:877
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:1221
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,.
bool is_greater_application(const DataExpression &e)
Recogniser for application of >
Definition standard.h:343
application real_times(const data_expression &arg0, const data_expression &arg1)
data_expression & real_one()
function_symbol less_equal(const sort_expression &s)
Constructor for function symbol <=.
Definition standard.h:277
const data_expression & binary_right(const application &x)
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
bool is_closed_real_number(const data_expression &e)
application real_plus(const data_expression &arg0, const data_expression &arg1)
data_expression & real_minus_one()
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:94
function_symbol less(const sort_expression &s)
Constructor for function symbol <.
Definition standard.h:240
bool is_positive(const data_expression &e, const rewriter &r)
bool is_false(const data_expression &x)
Test if x is false.
Definition consistency.h:37
application real_abs(const data_expression &arg)
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)
bool is_greater_equal_application(const DataExpression &e)
Recogniser for application of >=.
Definition standard.h:380
std::string pp_vector(const TYPE &inequalities)
Print the vector of inequalities to stderr in readable form.
const data_expression & binary_left(const application &x)
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)
bool is_true(const data_expression &x)
Test if x is true.
Definition consistency.h:29
std::string pp(const abstraction &x)
Definition data.cpp:39
static void pivot_and_update(const variable &xi, const variable &xj, const data_expression &v, const data_expression &v_delta_correction, std::map< variable, data_expression > &beta, std::map< variable, data_expression > &beta_delta_correction, std::set< variable > &basic_variables, std::map< variable, detail::lhs_t > &working_equalities, const rewriter &r)
map_substitution< AssociativeContainer > make_map_substitution(const AssociativeContainer &m)
Utility function for creating a map_substitution.
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.
const data_expression & unary_operand1(const data_expression &x)
bool is_zero(const data_expression &e)
data_expression rewrite_with_memory(const data_expression &t, const rewriter &r)
data_expression & real_zero()
const data_expression & binary_right1(const data_expression &x)
bool is_a_redundant_inequality(const std::vector< linear_inequality > &inequalities, const std::vector< linear_inequality > ::iterator i, const rewriter &r)
Indicate whether an inequality from a set of inequalities is redundant.
application real_negate(const data_expression &arg)
bool is_inconsistent(const std::vector< linear_inequality > &inequalities_in, const rewriter &r, const bool use_cache=true)
Determine whether a list of data expressions is inconsistent.
const data_expression & binary_left1(const data_expression &x)
data_expression max(const data_expression &e1, const data_expression &e2, const rewriter &)
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
bool is_negative(const data_expression &e, const rewriter &r)
bool is_less_application(const DataExpression &e)
Recogniser for application of <.
Definition standard.h:269
data_expression min(const data_expression &e1, const data_expression &e2, const rewriter &)
bool is_less_equal_application(const DataExpression &e)
Recogniser for application of <=.
Definition standard.h:306
bool is_equal_to_application(const DataExpression &e)
Recogniser for application of ==.
Definition standard.h:155
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
function_symbol greater(const sort_expression &s)
Constructor for function symbol >
Definition standard.h:314
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72