LCOV - code coverage report
Current view: top level - data/include/mcrl2/data - fourier_motzkin.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 109 128 85.2 %
Date: 2024-03-08 02:52:28 Functions: 3 3 100.0 %
Legend: Lines: hit not hit

          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

Generated by: LCOV version 1.14