Line data    Source code

       1             : // Author: 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 mcrl2/data/cardinality.h
      10             : /// \brief This file provides a class that can determine the cardinality of a sort in a datatype
      11             : 
      12             : #ifndef MCRL2_DATA_CARDINALIY_H
      13             : #define MCRL2_DATA_CARDINALIY_H
      14             : 
      15             : #include "mcrl2/data/enumerator.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : namespace data
      20             : {
      21             : 
      22             : class cardinality_calculator
      23             : {
      24             :   protected:
      25             : 
      26             :     const data_specification& m_specification;
      27             :     const rewriter& m_rewriter;
      28             : 
      29             :     // Determine whether f is a new unique element of sort s. If this cannot be determined,
      30             :     // the boolean determined is set to false, and the function yields false. 
      31           0 :     bool is_a_new_unique_element(const data_expression& t, 
      32             :                                  const std::vector<data_expression> already_found_elements,
      33             :                                  bool& determined) const
      34             :     {
      35           0 :       data_expression result;
      36           0 :       for(const data_expression& u: already_found_elements)
      37             :       {
      38           0 :         result=m_rewriter(equal_to(t,u));
      39           0 :         if (result==sort_bool::true_())
      40             :         {
      41           0 :           determined=true;
      42           0 :           return false;
      43             :         }
      44           0 :         else if (result!=sort_bool::false_())
      45             :         {
      46           0 :           determined=false;
      47           0 :           return false;
      48             :         }
      49             :         // else result==false and the element can still be unique.
      50             :       }
      51           0 :       determined=true;
      52           0 :       return true; 
      53           0 :     }
      54             :     
      55             :   public:
      56             : 
      57           0 :     cardinality_calculator(const data_specification& specification, const rewriter& r) 
      58           0 :       : m_specification(specification),
      59           0 :         m_rewriter(r)
      60           0 :     {}
      61             : 
      62             :     /// \brief Counts the number of elements in a sort. 
      63             :     /// \details The returned value is either the number of elements, or zero if
      64             :     ///          the number of elements cannot be determined, or is infinite.
      65             :     /// \param s The sort expression to be determined.
      66           0 :     std::size_t operator()(const sort_expression& s) const
      67             :     {
      68           0 :       if (s==sort_bool::bool_()) // Special case that occurs often. 
      69             :       {
      70           0 :         return 2;
      71             :       }
      72             :       /* if (!m_specification.is_certainly_finite(s))
      73             :       {
      74             :         return 0;
      75             :       } */
      76           0 :       std::vector<data_expression> found_elements(enumerate_expressions(s, m_specification, m_rewriter));
      77           0 :       std::vector<data_expression> unique_found_elements;  
      78             :      
      79           0 :       for(const data_expression& t: found_elements)
      80             :       {
      81             :         bool determined;
      82           0 :         if (is_a_new_unique_element(t, unique_found_elements, determined))
      83             :         {
      84           0 :           unique_found_elements.push_back(t);
      85             :         }
      86           0 :         else if (!determined)
      87             :         {
      88             :           // It is not possible to determine whether the found element is equal to any earlier element. 
      89           0 :           return 0;
      90             :         }
      91             :       }
      92           0 :       return unique_found_elements.size();
      93           0 :     }
      94             : };
      95             : 
      96             : } // namespace data
      97             : } // namespace mcrl2
      98             :       
      99             : #endif // MCRL2_DATA_CARDINALITY_H