LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail/prover - info.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 81 84 96.4 %
Date: 2020-02-13 00:44:47 Functions: 15 15 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Luc Engelen
       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 mcrl2/data/detail/prover/info.h
      10             : /// \brief Interface to classes Info
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_PROVER_INFO_H
      13             : #define MCRL2_DATA_DETAIL_PROVER_INFO_H
      14             : 
      15             : #include "mcrl2/atermpp/algorithm.h"
      16             : #include "mcrl2/data/rewriter.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : namespace data
      21             : {
      22             : namespace detail
      23             : {
      24             : 
      25             : enum Compare_Result
      26             : {
      27             :   compare_result_smaller,
      28             :   compare_result_equal,
      29             :   compare_result_bigger
      30             : };
      31             : 
      32             : /// \brief Base class for classes that provide information about the structure of
      33             : /// \brief data expressions in one of the internal formats of the rewriter.
      34             : class Info
      35             : {
      36             :   protected:
      37             : 
      38             :     /// \brief Flag indicating whether or not the arguments of equality functions are taken into account
      39             :     /// \brief when determining the order of expressions.
      40             :     const bool f_full;
      41             : 
      42             :     /// \brief Flag indicating whether or not the result of the comparison between the first two arguments
      43             :     /// \brief weighs stronger than the result of the comparison between the second pair of arguments of an
      44             :     /// \brief equation, when determining the order of expressions.
      45             :     const bool f_reverse;
      46             : 
      47         927 :     inline Compare_Result lexico(
      48             :               const Compare_Result& a_result1,
      49             :               const Compare_Result& a_result2) const
      50             :     {
      51         927 :       return (a_result1 != compare_result_equal) ? a_result1 : a_result2;
      52             :     }
      53             : 
      54         349 :     Compare_Result compare_address(
      55             :               const atermpp::aterm& a_term1,
      56             :               const atermpp::aterm& a_term2) const
      57             :     {
      58         349 :       if (a_term1 < a_term2)
      59             :       {
      60          98 :         return compare_result_smaller;
      61             :       }
      62         251 :       if (a_term2 < a_term1)
      63             :       {
      64         182 :         return compare_result_bigger;
      65             :       }
      66          69 :       return compare_result_equal;
      67             :     }
      68             : 
      69             :         /// \brief Returns an integer corresponding to the structure of the guard passed as argument \c a_guard.
      70         642 :     int get_guard_structure(const data_expression& a_guard) const
      71             :     {
      72         642 :       if (is_variable(a_guard))
      73             :       {
      74         372 :         return 0;
      75             :       }
      76         270 :       if (is_equal_to_application(a_guard))
      77             :       {
      78         540 :         data_expression v_term1, v_term2;
      79             : 
      80         270 :         v_term1 = get_argument(a_guard, 0);
      81         270 :         v_term2 = get_argument(a_guard, 1);
      82         270 :         if(find_free_variables(v_term1).empty() && is_variable(v_term2))
      83             :         {
      84         267 :           return 1;
      85             :         }
      86           3 :         if (is_variable(v_term1) && is_variable(v_term2))
      87             :         {
      88           0 :           return 2;
      89             :         }
      90           3 :         return 3;
      91             :       }
      92           0 :       return 4;
      93             :     }
      94             : 
      95             :     /// \brief Compares the structure of two guards.
      96         171 :     Compare_Result compare_guard_structure(const data_expression& a_guard1, const data_expression& a_guard2) const
      97             :     {
      98         171 :       if (get_guard_structure(a_guard1) < get_guard_structure(a_guard2))
      99             :       {
     100          21 :         return compare_result_smaller;
     101             :       }
     102         150 :       if (get_guard_structure(a_guard1) > get_guard_structure(a_guard2))
     103             :       {
     104          25 :         return compare_result_bigger;
     105             :       }
     106         125 :       return compare_result_equal;
     107             :     }
     108             : 
     109             :     /// \brief Compares two guards by their arguments.
     110         171 :     Compare_Result compare_guard_equality(const data_expression& a_guard1, const data_expression& a_guard2) const
     111             :     {
     112         171 :       if (f_full && is_equal_to_application(a_guard1) && is_equal_to_application(a_guard2))
     113             :       {
     114         102 :         data_expression v_g1a0, v_g1a1, v_g2a0, v_g2a1;
     115             : 
     116          51 :         v_g1a0 = get_argument(a_guard1, 0);
     117          51 :         v_g1a1 = get_argument(a_guard1, 1);
     118          51 :         v_g2a0 = get_argument(a_guard2, 0);
     119          51 :         v_g2a1 = get_argument(a_guard2, 1);
     120          51 :         if (f_reverse)
     121             :         {
     122          51 :           return lexico(compare_term(v_g1a1, v_g2a1), compare_term(v_g1a0, v_g2a0));
     123             :         }
     124             :         else
     125             :         {
     126           0 :           return lexico(compare_term(v_g1a0, v_g2a0), compare_term(v_g1a1, v_g2a1));
     127             :         }
     128             :       }
     129         120 :       return compare_result_equal;
     130             :     }
     131             : 
     132         178 :     Compare_Result compare_term_free_variables(const data_expression& a_term1, const data_expression& a_term2) const
     133             :     {
     134         178 :       bool term1_is_closed = find_free_variables(a_term1).empty();
     135         178 :       bool term2_is_closed = find_free_variables(a_term2).empty();
     136         178 :       if(term1_is_closed && !term2_is_closed)
     137             :       {
     138          29 :         return compare_result_smaller;
     139             :       }
     140         149 :       if(!term1_is_closed && term2_is_closed)
     141             :       {
     142          42 :         return compare_result_bigger;
     143             :       }
     144         107 :       return compare_result_equal;
     145             :     }
     146             : 
     147             :     /// \brief Compares terms by their type.
     148         178 :     Compare_Result compare_term_type(const data_expression& a_term1, const data_expression& a_term2) const
     149             :     {
     150         178 :       if (is_variable(a_term1) && !is_variable(a_term2))
     151             :       {
     152          40 :         return compare_result_bigger;
     153             :       }
     154         138 :       if (!is_variable(a_term1) && is_variable(a_term2))
     155             :       {
     156          33 :         return compare_result_smaller;
     157             :       }
     158         105 :       return compare_result_equal;
     159             :     }
     160             : 
     161             :     /// \brief Compares terms by checking whether one is a part of the other.
     162         178 :     Compare_Result compare_term_occurs(const data_expression& a_term1, const data_expression& a_term2) const
     163             :     {
     164         178 :       if (occurs(a_term1, a_term2))
     165             :       {
     166          41 :         return compare_result_bigger;
     167             :       }
     168         137 :       if (occurs(a_term2, a_term1))
     169             :       {
     170          10 :         return compare_result_smaller;
     171             :       }
     172         127 :       return compare_result_equal;
     173             :     }
     174             : 
     175             :   public:
     176             :     /// \brief Constructor that initializes the rewriter.
     177          18 :     constexpr Info(bool a_full, bool a_reverse)
     178          18 :     : f_full(a_full)
     179          18 :     , f_reverse(a_reverse)
     180          18 :     {}
     181             : 
     182             :     // Perform an occur check of expression t2 in expression t1.
     183         315 :     static bool occurs(const data_expression& t1, const data_expression& t2)
     184             :     {
     185        2688 :       return atermpp::find_if(t1,[&](const atermpp::aterm_appl& t){return t == t2;}) != atermpp::aterm_appl();
     186             :     }
     187             : 
     188             :     /// \brief Compares two guards.
     189         171 :     Compare_Result compare_guard(const data_expression& a_guard1, const data_expression& a_guard2) const
     190             :     {
     191             :       return lexico(
     192         342 :                lexico(
     193         342 :                  compare_guard_structure(a_guard1, a_guard2),
     194         342 :                  compare_guard_equality(a_guard1, a_guard2)
     195             :                ),
     196         342 :                compare_address(a_guard1, a_guard2)
     197         342 :              );
     198             :     }
     199             : 
     200             :     /// \brief Compares two terms.
     201         178 :     Compare_Result compare_term(const data_expression& a_term1, const data_expression& a_term2) const
     202             :     {
     203             :       return lexico(
     204         356 :                 lexico(
     205         356 :                   lexico(
     206         356 :                     compare_term_free_variables(a_term1, a_term2),
     207         356 :                     compare_term_occurs(a_term1, a_term2)
     208             :                   ),
     209         356 :                   compare_term_type(a_term1, a_term2)
     210             :                 ),
     211         356 :                 compare_address(a_term1, a_term2)
     212         356 :              );
     213             :     }
     214             : 
     215             :     /// \brief Returns the number of arguments of the main operator of a term.
     216             :     /// \param a_term An expression in the internal format of the rewriter with the jitty strategy.
     217             :     /// \return 0, if \c aterm is a constant or a variable.
     218             :     ///         The number of arguments of the main operator, otherwise.
     219         384 :     std::size_t get_number_of_arguments(const data_expression& a_term) const
     220             :     {
     221         384 :       if (!is_variable(a_term) && !is_function_symbol(a_term) && !is_abstraction(a_term))
     222             :       {
     223         334 :         return a_term.size() - 1;
     224             :       }
     225             :       else
     226             :       {
     227          50 :         return 0;
     228             :       }
     229             :     }
     230             : 
     231             :     /// \brief Returns the main operator of the term \c a_term;
     232             :     data_expression get_operator(const data_expression& a_term) const
     233             :     {
     234             :       if (is_function_symbol(a_term))
     235             :       {
     236             :         return a_term;
     237             :       }
     238             :       if (is_abstraction(a_term))
     239             :       {
     240             :         return get_operator(atermpp::down_cast<abstraction>(a_term).body());
     241             :       }
     242             :       const application& a = atermpp::down_cast<application>(a_term);
     243             :       return get_operator(a.head());
     244             :     }
     245             : 
     246             :     /// \brief Returns the argument with number \c a_number of the main operator of term \c a_term.
     247        1388 :     data_expression get_argument(const data_expression& a_term, const std::size_t a_number) const
     248             :     {
     249        1388 :       return data_expression(a_term[a_number + 1]);
     250             :     }
     251             : };
     252             : 
     253             : } // namespace detail
     254             : } // namespace data
     255             : } // namespace mcrl2
     256             : 
     257             : #endif

Generated by: LCOV version 1.13