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& term1,
      56             :               const atermpp::aterm& term2) const
      57             :     {
      58         349 :       if (term1 < term2)
      59             :       {
      60         101 :         return compare_result_smaller;
      61             :       }
      62         248 :       if (term2 < term1)
      63             :       {
      64         179 :         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 guard.
      70         642 :     int get_guard_structure(const data_expression& guard) const
      71             :     {
      72         642 :       if (is_variable(guard))
      73             :       {
      74         372 :         return 0;
      75             :       }
      76         270 :       if (is_equal_to_application(guard))
      77             :       {
      78         270 :         const application& guard_appl=atermpp::down_cast<application>(guard);
      79         270 :         const data_expression& v_term1 = guard_appl[0]; 
      80         270 :         const data_expression& v_term2 = guard_appl[1]; 
      81         270 :         if (find_free_variables(v_term1).empty() && is_variable(v_term2))
      82             :         {
      83         267 :           return 1;
      84             :         }
      85           3 :         if (is_variable(v_term1) && is_variable(v_term2))
      86             :         {
      87           0 :           return 2;
      88             :         }
      89           3 :         return 3;
      90             :       }
      91           0 :       return 4;
      92             :     }
      93             : 
      94             :     /// \brief Compares the structure of two guards.
      95         171 :     Compare_Result compare_guard_structure(const data_expression& guard1, const data_expression& guard2) const
      96             :     {
      97         171 :       if (get_guard_structure(guard1) < get_guard_structure(guard2))
      98             :       {
      99          21 :         return compare_result_smaller;
     100             :       }
     101         150 :       if (get_guard_structure(guard1) > get_guard_structure(guard2))
     102             :       {
     103          25 :         return compare_result_bigger;
     104             :       }
     105         125 :       return compare_result_equal;
     106             :     }
     107             : 
     108             :     /// \brief Compares two guards by their arguments.
     109         171 :     Compare_Result compare_guard_equality(const data_expression& guard1, const data_expression& guard2) const
     110             :     {
     111         171 :       if (f_full && is_equal_to_application(guard1) && is_equal_to_application(guard2))
     112             :       {
     113          51 :         const application& guard1_appl=atermpp::down_cast<application>(guard1);
     114          51 :         const application& guard2_appl=atermpp::down_cast<application>(guard2);
     115          51 :         const data_expression& v_g1a0 = guard1_appl[0];
     116          51 :         const data_expression& v_g1a1 = guard1_appl[1];
     117          51 :         const data_expression& v_g2a0 = guard2_appl[0];
     118          51 :         const data_expression& v_g2a1 = guard2_appl[1];
     119          51 :         if (f_reverse)
     120             :         {
     121          51 :           return lexico(compare_term(v_g1a1, v_g2a1), compare_term(v_g1a0, v_g2a0));
     122             :         }
     123             :         else
     124             :         {
     125           0 :           return lexico(compare_term(v_g1a0, v_g2a0), compare_term(v_g1a1, v_g2a1));
     126             :         }
     127             :       }
     128         120 :       return compare_result_equal;
     129             :     }
     130             : 
     131         178 :     Compare_Result compare_term_free_variables(const data_expression& term1, const data_expression& term2) const
     132             :     {
     133         178 :       bool term1_is_closed = find_free_variables(term1).empty();
     134         178 :       bool term2_is_closed = find_free_variables(term2).empty();
     135         178 :       if (term1_is_closed && !term2_is_closed)
     136             :       {
     137          29 :         return compare_result_smaller;
     138             :       }
     139         149 :       if (!term1_is_closed && term2_is_closed)
     140             :       {
     141          42 :         return compare_result_bigger;
     142             :       }
     143         107 :       return compare_result_equal;
     144             :     }
     145             : 
     146             :     /// \brief Compares terms by their type.
     147         178 :     Compare_Result compare_term_type(const data_expression& term1, const data_expression& term2) const
     148             :     {
     149         178 :       if (is_variable(term1) && !is_variable(term2))
     150             :       {
     151          40 :         return compare_result_bigger;
     152             :       }
     153         138 :       if (!is_variable(term1) && is_variable(term2))
     154             :       {
     155          33 :         return compare_result_smaller;
     156             :       }
     157         105 :       return compare_result_equal;
     158             :     }
     159             : 
     160             :     /// \brief Compares terms by checking whether one is a part of the other.
     161         178 :     Compare_Result compare_term_occurs(const data_expression& term1, const data_expression& term2) const
     162             :     {
     163         178 :       if (occurs(term1, term2))
     164             :       {
     165          41 :         return compare_result_bigger;
     166             :       }
     167         137 :       if (occurs(term2, term1))
     168             :       {
     169          10 :         return compare_result_smaller;
     170             :       }
     171         127 :       return compare_result_equal;
     172             :     }
     173             : 
     174             :   public:
     175             :     /// \brief Constructor that initializes the rewriter.
     176          18 :     constexpr Info(bool a_full, bool a_reverse)
     177          18 :     : f_full(a_full)
     178          18 :     , f_reverse(a_reverse)
     179          18 :     {}
     180             : 
     181             :     // Perform an occur check of expression t2 in expression t1.
     182         315 :     static bool occurs(const data_expression& t1, const data_expression& t2)
     183             :     {
     184        2688 :       return atermpp::find_if(t1,[&](const atermpp::aterm_appl& t){return t == t2;}) != atermpp::aterm_appl();
     185             :     }
     186             : 
     187             :     /// \brief Compares two guards.
     188         171 :     Compare_Result compare_guard(const data_expression& guard1, const data_expression& guard2) const
     189             :     {
     190         171 :       return lexico(
     191         171 :                lexico(
     192         171 :                  compare_guard_structure(guard1, guard2),
     193         171 :                  compare_guard_equality(guard1, guard2)
     194             :                ),
     195         342 :                compare_address(guard1, guard2)
     196         342 :              );
     197             :     }
     198             : 
     199             :     /// \brief Compares two terms.
     200         178 :     Compare_Result compare_term(const data_expression& term1, const data_expression& term2) const
     201             :     {
     202         178 :       return lexico(
     203         178 :                 lexico(
     204         178 :                   lexico(
     205         178 :                     compare_term_free_variables(term1, term2),
     206         178 :                     compare_term_occurs(term1, term2)
     207             :                   ),
     208         178 :                   compare_term_type(term1, term2)
     209             :                 ),
     210         356 :                 compare_address(term1, term2)
     211         356 :              );
     212             :     }
     213             : 
     214             :     /// \brief Returns the main operator of the term \c term;
     215             :     data_expression get_operator(const data_expression& term) const
     216             :     {
     217             :       if (is_function_symbol(term))
     218             :       {
     219             :         return term;
     220             :       }
     221             :       if (is_abstraction(term))
     222             :       {
     223             :         return get_operator(atermpp::down_cast<abstraction>(term).body());
     224             :       }
     225             :       const application& a = atermpp::down_cast<application>(term);
     226             :       return get_operator(a.head());
     227             :     }
     228             : };
     229             : 
     230             : } // namespace detail
     231             : } // namespace data
     232             : } // namespace mcrl2
     233             : 
     234             : #endif