LCOV - code coverage report
Current view: top level - data/include/mcrl2/data - representative_generator.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 75 79 94.9 %
Date: 2024-03-08 02:52:28 Functions: 5 5 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 mcrl2/data/representative_generator.h
      10             : /// \brief Component for generating representatives of sorts
      11             : 
      12             : #ifndef MCRL2_DATA_REPRESENTATIVE_GENERATOR_H
      13             : #define MCRL2_DATA_REPRESENTATIVE_GENERATOR_H
      14             : 
      15             : #include "mcrl2/data/data_specification.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace data
      21             : {
      22             : /// \brief Components for generating an arbitrary element of a sort
      23             : /// \details This component is not deterministic. So, it is not guaranteed
      24             : ///          to deliver the same element each time it is run.
      25             : ///
      26             : /// A representative is an arbitrary element of a given sort. This
      27             : /// component takes a specification and generates representatives for sorts
      28             : /// defined by the specification. An important property is that for the
      29             : /// same sort the same representative is returned. For this it assumes
      30             : /// that the context -constructors and mappings for the sort- remain
      31             : /// unchanged.
      32             : ///
      33             : /// The general aim is to keep the representative expression as simple. Use of
      34             : /// constructors is preferred above mappings and constructors or
      35             : /// mappings representing constants are preferred over those that have
      36             : /// non-empty domain.
      37             : ///
      38             : /// Constructors and functions that have arrows in their target sorts
      39             : /// (e.g. f:A->(B->C)) are not used to construct default terms. Once an
      40             : /// element is generated it is kept for later requests, which is done for
      41             : /// performance when used frequently on the same specification. At some
      42             : /// point a sufficiently advanced enumerator may be used to replace the
      43             : /// current implementation.
      44             : ///
      45             : /// This component will evolve through time, in the sense that more
      46             : /// complex expressions will be generated over time to act as
      47             : /// representative a certain sort, for instance containing function symbols
      48             : /// with complex target sorts, containing explicit function constructors
      49             : /// (lambda's). So, no reliance is possible on the particular shape of the
      50             : /// terms that are generated.
      51             : 
      52             : class representative_generator
      53             : {
      54             : 
      55             :   protected:
      56             : 
      57             :     /// \brief Data specification context
      58             :     const data_specification& m_specification;
      59             : 
      60             :     /// \brief Serves as a cache for later find operations
      61             :     std::map< sort_expression, data_expression > m_representatives_cache;
      62             : 
      63             :   protected:
      64             : 
      65             :     /// \brief Sets a data expression as representative of the sort
      66             :     /// \param[in] sort the sort of which to set the representative
      67             :     /// \param[in] representative the data expression that serves as representative
      68         696 :     void set_representative(const sort_expression& sort, const data_expression& representative)
      69             :     {
      70         696 :       assert(sort==representative.sort());
      71         696 :       m_representatives_cache[sort] = representative;
      72         696 :     }
      73             : 
      74             :     /// \brief Finds a representative of the form f(t1,...,tn) where f is the function symbol.
      75             :     /// \param[in] symbol The function symbol f using which the representative is constructed.
      76             :     /// \param[in] visited_sorts A set of sorts for which no representative can be constructed. This is used to prevent 
      77             :     //                           an infinite circular search through the sorts.
      78             :     /// \param[out] result The representative of the shape f(t1,...,tn). This is only set if this function yields true.
      79             :     /// \return a boolean indicating whether a representative has successfully been found.
      80             :     /// \pre symbol.sort() is of type function_sort
      81          39 :     bool find_representative(
      82             :                        const function_symbol& symbol, 
      83             :                        std::set < sort_expression >& visited_sorts,
      84             :                        data_expression& result) 
      85             :     {
      86          39 :       assert(is_function_sort(symbol.sort()));
      87             : 
      88          39 :       data_expression_vector arguments;
      89             : 
      90          81 :       for (const sort_expression& s: static_cast<const function_sort&>(symbol.sort()).domain())
      91             :       {
      92          47 :         data_expression representative;
      93          47 :         if (find_representative(s, visited_sorts, representative))
      94             :         {
      95          42 :           arguments.push_back(representative);
      96             :         }
      97             :         else
      98             :         {
      99             :           // a representative for this argument could not be found.
     100           5 :           return false;
     101             :         }
     102          47 :       }
     103             : 
     104             :       // a suitable set of arguments is found
     105          34 :       result=application(symbol, arguments);
     106          34 :       return true;
     107          39 :     }
     108             : 
     109             :     /// \brief Finds a representative element for an arbitrary sort expression
     110             :     /// \param[in] sort the sort for which to find the representative
     111             :     /// \param[in] visited_sorts A set of sorts for which no representative can be constructed. This is used to prevent 
     112             :     //                           an infinite circular search through the sorts.
     113             :     /// \param[out] result The representative of the shape f(t1,...,tn). This is only set if this function yields true.
     114             :     /// \return a boolean indicating whether a representative has successfully been found.
     115         710 :     bool find_representative(
     116             :                     const sort_expression& sort, 
     117             :                     std::set < sort_expression >& visited_sorts, 
     118             :                     data_expression& result)
     119             :     {
     120         710 :       if (visited_sorts.count(sort)>0)
     121             :       {
     122             :         // This sort is already visited. We are looking to find a representative term of this sort
     123             :         // within the scope of finding a term of this sort. If this is to be succesful, a more compact
     124             :         // term can be found. Hence, stop searching further.
     125           5 :         return false;
     126             :       }
     127             : 
     128         705 :       const std::map< sort_expression, data_expression >::iterator i=m_representatives_cache.find(sort);
     129         705 :       if (i!=m_representatives_cache.end())
     130             :       {
     131           3 :         assert(i->second.sort()==sort);
     132           3 :         result=i->second;
     133           3 :         return true;
     134             :       }
     135             :       
     136         702 :       if (is_function_sort(sort))
     137             :       {
     138             :         // s is a function sort. 
     139             :         // First check if there is a mapping with sort s (constructors with sort s cannot exist).
     140           9 :         const function_sort& fs=atermpp::down_cast<function_sort>(sort);
     141         188 :         for (const function_symbol& f: m_specification.mappings(fs.codomain()))
     142             :         {
     143         187 :           if (f.sort()==sort)
     144             :           {
     145           8 :             result=f;
     146           8 :             set_representative(sort, result);
     147           8 :             return true;
     148             :           }
     149             :         }
     150             :         // If no explicit constant is found of this sort, we know that its shape is "s0#..#sn -> s". 
     151             :         // We search a term t of sort s and if found, construct a lambda term of the shape 
     152             :         // lambda x0:s0,...,xn:sn.t. Note that this can be strengthened slightly by incorporating
     153             :         // the variables xi in generating t, e.g. generating for D->D  the reprentant lambd d:D.d. 
     154             :         // Incorporating the variables in the generation of terms requires adapting all algorithms,
     155             :         // and is not done. Until now the need for such representant generators has not been felt. 
     156             : 
     157           1 :         const sort_expression& s2=fs.codomain();
     158           1 :         data_expression t;
     159           1 :         if (find_representative(s2, visited_sorts, t))
     160             :         {
     161           1 :           variable_vector bound_variables;
     162           1 :           std::size_t variable_index=0;
     163           3 :           for(const sort_expression& s: fs.domain())
     164             :           {
     165           2 :             bound_variables.emplace_back("x" + std::to_string(variable_index), s);
     166           2 :             variable_index++;
     167             :           }
     168           1 :           result=abstraction(lambda_binder(),variable_list(bound_variables.begin(),bound_variables.end()),t);
     169           1 :           return true;
     170           1 :         }
     171           1 :       }
     172             :       else
     173             :       {
     174             :         // s is a constant (not a function sort).
     175             :         // check if there is a constant constructor for s
     176             : 
     177         744 :         for (const function_symbol& f: m_specification.constructors(sort))
     178             :         {
     179         705 :           if (f.sort()==sort)
     180             :           { 
     181         654 :             result=f;
     182         654 :             set_representative(sort, result);
     183         654 :             return true;
     184             :           }
     185             :         }
     186             : 
     187          39 :         visited_sorts.insert(sort);
     188             : 
     189             :         // Check whether there is a representative f(t1,...,tn) for s, where f is a constructor function. 
     190             :         // We prefer this over a constant mapping, as a constant mapping generally does not have appropriate
     191             :         // rewrite rules.
     192             :         
     193             :         // recursively traverse constructor functions of the form f:s1#...#sn -> sort.
     194             :         // operators with f:s1#...#sn->G where G is a complex sort expression are ignored
     195          39 :         for (const function_symbol& f: m_specification.constructors(sort))
     196             :         {
     197          32 :           if (find_representative(f, visited_sorts, result))
     198             :           {
     199          32 :             set_representative(sort, result);
     200          32 :             visited_sorts.erase(sort);
     201          32 :             return true;
     202             :           }
     203             :         }
     204             : 
     205             :         // check if there is a constant mapping for s
     206          58 :         for (const function_symbol& f: m_specification.mappings(sort))
     207             :         {
     208          51 :           if (f.sort()==sort)
     209             :           {
     210           0 :             result=f;
     211           0 :             set_representative(sort, result);
     212           0 :             visited_sorts.erase(sort);
     213           0 :             return true;
     214             :           }
     215             :         }
     216             : 
     217             :         // Try to check whether there is a representative f(t1,...,tn) where f is a mapping. 
     218          12 :         for (const function_symbol& f: m_specification.mappings(sort))
     219             :         {
     220           7 :           if (find_representative(f, visited_sorts, result))
     221             :           {
     222           2 :             set_representative(sort, result);
     223           2 :             visited_sorts.erase(sort);
     224           2 :             return true;
     225             :           }
     226             :         }
     227             :         
     228           5 :         visited_sorts.erase(sort);
     229             : 
     230             :       }
     231             : 
     232             :       // No representative has been found.
     233           5 :       return false;
     234             :     }
     235             : 
     236             :   public:
     237             : 
     238             :     /// \brief Constructor with data specification as context
     239         782 :     representative_generator(const data_specification& specification) : m_specification(specification)
     240             :     {
     241         782 :     }
     242             : 
     243             :     /// \brief Returns a representative of a sort
     244             :     /// \param[in] sort sort of which to find a representatitive
     245        1129 :     data_expression operator()(const sort_expression& sort)
     246             :     {
     247             :       // First see whether a term of this sort has already been constructed and resides in the representatives_cache. If yes return it. 
     248        1129 :       const std::map< sort_expression, data_expression >::iterator i=m_representatives_cache.find(sort);
     249        1129 :       if (i!=m_representatives_cache.end())
     250             :       {
     251         467 :         return i->second;
     252             :       }
     253             :       
     254         662 :       data_expression result;
     255         662 :       std::set<sort_expression> visited_sorts;
     256         662 :       if (find_representative(sort, visited_sorts, result))
     257             :       {
     258             :         // A term of the requested sort is found. Return it. 
     259         657 :         return result;
     260             :       }
     261             :       else 
     262             :       {
     263           5 :         throw mcrl2::runtime_error("Cannot find a term of sort " + data::pp(sort));
     264             :       }
     265             :      
     266         667 :     }
     267             : };
     268             : 
     269             : } // namespace data
     270             : } // namespace mcrl2
     271             : #endif
     272             : 

Generated by: LCOV version 1.14