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: 60 64 93.8 %
Date: 2020-02-19 00:44:21 Functions: 6 6 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         696 : 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         491 :     void set_representative(const sort_expression& sort, const data_expression& representative)
      69             :     {
      70         491 :       assert(sort==representative.sort());
      71         491 :       m_representatives_cache[sort] = representative;
      72         491 :     }
      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          78 :       data_expression_vector arguments;
      89             : 
      90          81 :       for (const sort_expression& s: function_sort(symbol.sort()).domain())
      91             :       {
      92          89 :         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             :       }
     103             : 
     104             :       // a suitable set of arguments is found
     105          34 :       result=application(symbol, arguments);
     106          34 :       return true;
     107             :     }
     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         503 :     bool find_representative(
     116             :                     const sort_expression& sort, 
     117             :                     std::set < sort_expression >& visited_sorts, 
     118             :                     data_expression& result)
     119             :     {
     120         503 :       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         498 :       const std::map< sort_expression, data_expression >::iterator i=m_representatives_cache.find(sort);
     129         498 :       if (i!=m_representatives_cache.end())
     130             :       {
     131           2 :         assert(i->second.sort()==sort);
     132           2 :         result=i->second;
     133           2 :         return true;
     134             :       }
     135             :       
     136         496 :       if (is_function_sort(sort))
     137             :       {
     138             :         // s is a function sort. We search for a constructor of mapping of this sort
     139             :         // Although in principle possible, we do not do a lot of effort to construct
     140             :         // a term of this sort. We just look whether a term of exactly this sort is
     141             :         // present.
     142             : 
     143             :         // check if there is a mapping with sort s (constructors with sort s cannot exist).
     144          12 :         for (const function_symbol& f: m_specification.mappings(atermpp::down_cast<function_sort>(sort).codomain()))
     145             :         {
     146          12 :           if (f.sort()==sort)
     147             :           {
     148           1 :             result=f;
     149           1 :             set_representative(sort, result);
     150           1 :             return true;
     151             :           }
     152             :         }
     153             :       }
     154             :       else
     155             :       {
     156             :         // s is a constant (not a function sort).
     157             :         // check if there is a constant constructor for s
     158             : 
     159         546 :         for (const function_symbol& f: m_specification.constructors(sort))
     160             :         {
     161         507 :           if (f.sort()==sort)
     162             :           { 
     163         456 :             result=f;
     164         456 :             set_representative(sort, result);
     165         456 :             return true;
     166             :           }
     167             :         }
     168             : 
     169          39 :         visited_sorts.insert(sort);
     170             : 
     171             :         // Check whether there is a representative f(t1,...,tn) for s, where f is a constructor function. 
     172             :         // We prefer this over a constant mapping, as a constant mapping generally does not have appropriate
     173             :         // rewrite rules.
     174             :         
     175             :         // recursively traverse constructor functions of the form f:s1#...#sn -> sort.
     176             :         // operators with f:s1#...#sn->G where G is a complex sort expression are ignored
     177          39 :         for (const function_symbol& f: m_specification.constructors(sort))
     178             :         {
     179          32 :           if (find_representative(f, visited_sorts, result))
     180             :           {
     181          32 :             set_representative(sort, result);
     182          32 :             visited_sorts.erase(sort);
     183          32 :             return true;
     184             :           }
     185             :         }
     186             : 
     187             :         // check if there is a constant mapping for s
     188          58 :         for (const function_symbol& f: m_specification.mappings(sort))
     189             :         {
     190          51 :           if (f.sort()==sort)
     191             :           {
     192           0 :             result=f;
     193           0 :             set_representative(sort, result);
     194           0 :             visited_sorts.erase(sort);
     195           0 :             return true;
     196             :           }
     197             :         }
     198             : 
     199             :         // Try to check whether there is a representative f(t1,...,tn) where f is a mapping. 
     200          12 :         for (const function_symbol& f: m_specification.mappings(sort))
     201             :         {
     202           7 :           if (find_representative(f, visited_sorts, result))
     203             :           {
     204           2 :             set_representative(sort, result);
     205           2 :             visited_sorts.erase(sort);
     206           2 :             return true;
     207             :           }
     208             :         }
     209             :         
     210           5 :         visited_sorts.erase(sort);
     211             : 
     212             :       }
     213             : 
     214             :       // No representative has been found.
     215           5 :       return false;
     216             :     }
     217             : 
     218             :   public:
     219             : 
     220             :     /// \brief Constructor with data specification as context
     221         696 :     representative_generator(const data_specification& specification) : m_specification(specification)
     222             :     {
     223         696 :     }
     224             : 
     225             :     /// \brief Returns a representative of a sort
     226             :     /// \param[in] sort sort of which to find a representatitive
     227        1179 :     data_expression operator()(const sort_expression& sort)
     228             :     {
     229             :       // First see whether a term of this sort has already been constructed and resides in the representatives_cache. If yes return it. 
     230        1179 :       const std::map< sort_expression, data_expression >::iterator i=m_representatives_cache.find(sort);
     231        1179 :       if (i!=m_representatives_cache.end())
     232             :       {
     233         723 :         return i->second;
     234             :       }
     235             :       
     236         912 :       data_expression result;
     237         912 :       std::set<sort_expression> visited_sorts;
     238         456 :       if (find_representative(sort, visited_sorts, result))
     239             :       {
     240             :         // A term of the requested sort is found. Return it. 
     241         451 :         return result;
     242             :       }
     243             :       else 
     244             :       {
     245           5 :         throw mcrl2::runtime_error("Cannot find a term of sort " + data::pp(sort));
     246             :       }
     247             :      
     248             :     }
     249             : };
     250             : 
     251             : } // namespace data
     252             : } // namespace mcrl2
     253             : #endif
     254             : 

Generated by: LCOV version 1.13