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

Generated by: LCOV version 1.14