LCOV - code coverage report
Current view: top level - data/include/mcrl2/data - data_specification.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 246 255 96.5 %
Date: 2020-02-19 00:44:21 Functions: 47 49 95.9 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jeroen Keiren, Jeroen van der Wulp, 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             : 
      10             : #ifndef MCRL2_DATA_DATA_SPECIFICATION_H
      11             : #define MCRL2_DATA_DATA_SPECIFICATION_H
      12             : 
      13             : #include "mcrl2/data/detail/data_functional.h"
      14             : #include "mcrl2/data/sort_specification.h"
      15             : 
      16             : namespace mcrl2
      17             : {
      18             : 
      19             : namespace data
      20             : {
      21             : 
      22             : // template function overloads
      23             : data_expression normalize_sorts(const data_expression& x, const data::sort_specification& sortspec);
      24             : variable_list normalize_sorts(const variable_list& x, const data::sort_specification& sortspec);
      25             : data::data_equation normalize_sorts(const data::data_equation& x, const data::sort_specification& sortspec);
      26             : data_equation_list normalize_sorts(const data_equation_list& x, const data::sort_specification& sortspec);
      27             : void normalize_sorts(data_equation_vector& x, const data::sort_specification& sortspec);
      28             : 
      29             : // prototype
      30             : class data_specification;
      31             : 
      32             : std::string pp(const data::data_specification& x);
      33             : 
      34             : /// \brief Test for a data specification expression
      35             : /// \param x A term
      36             : /// \return True if \a x is a data specification expression
      37             : inline
      38           0 : bool is_data_specification(const atermpp::aterm_appl& x)
      39             : {
      40           0 :   return x.function() == core::detail::function_symbols::DataSpec;
      41             : }
      42             : 
      43             : /// \brief data specification.
      44             : 
      45       30956 : class data_specification: public sort_specification
      46             : {
      47             :   private:
      48             : 
      49             :     /// \cond INTERNAL_DOCS
      50             :     /// \brief Cached constructors by target sort
      51       92902 :     struct target_sort_to_function_map
      52             :     {
      53             :       bool _outdated;
      54             :       std::map<sort_expression, std::vector<function_symbol> > _mapping;
      55             : 
      56       37136 :       target_sort_to_function_map()
      57       37136 :         : _outdated(true)
      58       37136 :       {}
      59             : 
      60             :       /// \brief Groups functions according to their target sorts.
      61             :       /// \param [in,out] c container in which the functions are stored grouped by target sort.
      62             :       /// \param [in] functions a container with function symbols
      63             :       template <typename Container>
      64         893 :       void group_functions_by_target_sort(std::map<sort_expression, std::vector<function_symbol> >& c, const Container& functions)
      65             :       {
      66       11222 :         for (typename Container::const_iterator i = functions.begin(); i != functions.end(); ++i)
      67             :         {
      68       20658 :           sort_expression index_sort(i->sort().target_sort());
      69       10329 :           if(c.find(index_sort) == c.end() || std::find(c[index_sort].begin(), c[index_sort].end(), *i) == c[index_sort].end())
      70             :           {
      71       10329 :             c[index_sort].push_back(*i);
      72             :           }
      73             :         }
      74         893 :       }
      75             : 
      76             :       template <typename FunctionContainer>
      77       15250 :       void reset(const FunctionContainer& c)
      78             :       {
      79       15250 :         if(_outdated)
      80             :         {
      81         893 :           _mapping.clear();
      82         893 :           group_functions_by_target_sort(_mapping, c);
      83         893 :           _outdated = false;
      84             :         }
      85       15250 :       }
      86             : 
      87       18562 :       void expire()
      88             :       {
      89       18562 :         _outdated = true;
      90       18562 :       }
      91             : 
      92       15250 :       std::map<sort_expression, std::vector<function_symbol> >&mapping()
      93             :       {
      94       15250 :         assert(!_outdated);
      95       15250 :         return _mapping;
      96             :       }
      97             :     };
      98             : 
      99             :     ///\brief Builds a specification from aterm
     100             :     void build_from_aterm(const atermpp::aterm_appl& term);
     101             :     /// \endcond
     102             : 
     103             :   protected:
     104             : 
     105             :     /// \brief A mapping of sort expressions to the constructors corresponding to that sort.
     106             :     function_symbol_vector m_user_defined_constructors;
     107             : 
     108             :     /// \brief The mappings of the specification.
     109             :     function_symbol_vector m_user_defined_mappings;
     110             : 
     111             :     /// \brief The equations of the specification.
     112             :     data_equation_vector m_user_defined_equations;
     113             : 
     114             :     /// \brief Set containing all constructors, including the system defined ones.
     115             :     /// The types in these constructors are normalised.
     116             :     mutable function_symbol_vector m_normalised_constructors;
     117             : 
     118             :     /// \brief Cache normalised constructors grouped by target sort.
     119             :     mutable target_sort_to_function_map m_grouped_normalised_constructors;
     120             : 
     121             :     /// \brief Set containing system defined all mappings, including the system defined ones.
     122             :     /// The types in these mappings are normalised.
     123             :     mutable function_symbol_vector m_normalised_mappings;
     124             : 
     125             :     /// \brief Cache normalised mappings grouped by target sort.
     126             :     mutable target_sort_to_function_map m_grouped_normalised_mappings;
     127             :     //
     128             :     /// \brief Table containing all equations, including the system defined ones.
     129             :     ///        The sorts in these equations are normalised.
     130             :     /// \details The normalised equations are a set as the number of equations
     131             :     ///          can become large, in which case removing duplicates while inserting equations can be
     132             :     ///          very time consuming.
     133             :     mutable std::set<data_equation> m_normalised_equations;
     134             : 
     135        3898 :     void data_is_not_necessarily_normalised_anymore() const
     136             :     {
     137        3898 :       m_normalised_data_is_up_to_date=false;
     138        3898 :     }
     139             : 
     140             :   protected:
     141             : 
     142             :     /// \brief Adds a constructor to this specification, and marks it as
     143             :     ///        system defined.
     144             :     ///
     145             :     /// \param[in] f A function symbol.
     146             :     /// \pre f does not yet occur in this specification.
     147             :     /// \post is_system_defined(f) == true
     148             :     /// \note this operation does not invalidate iterators of constructors_const_range
     149             :     inline
     150       66100 :     void add_normalised_constructor(const function_symbol& f) const
     151             :     {
     152      132200 :       function_symbol g(normalize_sorts(f, *this));
     153       66100 :       if (std::find(m_normalised_constructors.begin(),m_normalised_constructors.end(),g)==m_normalised_constructors.end()) // not found
     154             :       {
     155       65026 :         m_normalised_constructors.push_back(g);
     156             :       }
     157       66100 :     }
     158             : 
     159             :     /// \brief Adds a mapping to this specification, and marks it as system
     160             :     ///        defined.
     161             :     ///
     162             :     /// \param[in] f A function symbol.
     163             :     /// \pre f does not yet occur in this specification.
     164             :     /// \post is_system_defined(f) == true
     165             :     /// \note this operation does not invalidate iterators of mappings_const_range
     166      848111 :     void add_normalised_mapping(const function_symbol& f) const
     167             :     {
     168     1696222 :       function_symbol g(normalize_sorts(f, *this));
     169      848111 :       if (std::find(m_normalised_mappings.begin(),m_normalised_mappings.end(),g)==m_normalised_mappings.end()) // not found
     170             :       {
     171      813751 :         m_normalised_mappings.push_back(g);
     172             :       }
     173      848111 :     }
     174             : 
     175             :     /// \brief Adds an equation to this specification, and marks it as system
     176             :     ///        defined.
     177             :     ///
     178             :     /// \param[in] e An equation.
     179             :     /// \pre e does not yet occur in this specification.
     180             :     /// \post is_system_defined(f) == true
     181             :     /// \note this operation does not invalidate iterators of equations_const_range
     182     2052023 :     void add_normalised_equation(const data_equation& e) const
     183             :     {
     184     2052023 :       m_normalised_equations.insert(normalize_sorts(e,*this));
     185     2052023 :     }
     186             : 
     187             :     template < class Iterator >
     188       56695 :     void add_normalised_constructors(Iterator begin, Iterator end) const
     189             :     {
     190      122669 :       for(Iterator i=begin; i!=end; ++i)
     191             :       {
     192       65974 :         data_specification::add_normalised_constructor(*i);
     193             :       }
     194       56695 :     }
     195             : 
     196             :     template < class Iterator >
     197       56695 :     void add_normalised_mappings(Iterator begin, Iterator end) const
     198             :     {
     199      902695 :       for(Iterator i=begin; i!=end; ++i)
     200             :       {
     201      846000 :         data_specification::add_normalised_mapping(*i);
     202             :       }
     203       56695 :     }
     204             : 
     205             :     template < class Iterator >
     206       56695 :     void add_normalised_equations(Iterator begin, Iterator end) const
     207             :     {
     208     2105814 :       for(Iterator i=begin; i!=end; ++i)
     209             :       {
     210     2049119 :         data_specification::add_normalised_equation(*i);
     211             :       }
     212       56695 :     }
     213             : 
     214             :     /// \brief Adds constructors, mappings and equations for a structured sort
     215             :     ///        to this specification, and marks them as system defined.
     216             :     ///
     217             :     /// \param[in] sort A sort expression that is representing the structured sort.
     218             :     /// \param[out] constructors To this set the new constructors are added.
     219             :     /// \param[out] mappings     New mappings are added to this set.
     220             :     /// \param[out] equations    New equations for the structured sort are added to this set.
     221             :     /// \param[in]  skip_equations This boolean indicates whether equations are added.
     222             : 
     223        3192 :     void insert_mappings_constructors_for_structured_sort(
     224             :                        const structured_sort& sort,
     225             :                        std::set < function_symbol >& constructors,
     226             :                        std::set < function_symbol >& mappings,
     227             :                        std::set < data_equation >& equations,
     228             :                        const bool skip_equations) const
     229             :     {
     230        3192 :       const structured_sort& s_sort(sort);
     231        6384 :       function_symbol_vector f(s_sort.constructor_functions(sort));
     232        3192 :       constructors.insert(f.begin(),f.end());
     233        3192 :       f = s_sort.projection_functions(sort);
     234        3192 :       mappings.insert(f.begin(),f.end());
     235        3192 :       f = s_sort.recogniser_functions(sort);
     236        3192 :       mappings.insert(f.begin(),f.end());
     237        3192 :       f = s_sort.comparison_functions(sort);
     238        3192 :       mappings.insert(f.begin(),f.end());
     239             : 
     240        3192 :       if (!skip_equations)
     241             :       {
     242        6384 :         data_equation_vector e(s_sort.constructor_equations(sort));
     243        3192 :         equations.insert(e.begin(),e.end());
     244        3192 :         e = s_sort.projection_equations(sort);
     245        3192 :         equations.insert(e.begin(),e.end());
     246        3192 :         e = s_sort.recogniser_equations(sort);
     247        3192 :         equations.insert(e.begin(),e.end());
     248        3192 :         e = s_sort.comparison_equations(sort);
     249        3192 :         equations.insert(e.begin(),e.end());
     250             :       }
     251        3192 :     }
     252             : 
     253       56705 :     void add_standard_mappings_and_equations(
     254             :                        const sort_expression& sort,
     255             :                        std::set < function_symbol >& mappings,
     256             :                        std::set < data_equation >& equations,
     257             :                        const bool skip_equations) const
     258             :     {
     259      113410 :       function_symbol_vector f(standard_generate_functions_code(sort));
     260       56705 :       mappings.insert(f.begin(), f.end());
     261             : 
     262       56705 :       if (!skip_equations)
     263             :       {
     264      113390 :         const data_equation_vector eq(standard_generate_equations_code(sort));
     265       56695 :         equations.insert(eq.begin(), eq.end());
     266             :       }
     267       56705 :     }
     268             : 
     269             :   public:
     270             : 
     271             :     ///\brief Default constructor. Generate a data specification that contains
     272             :     ///       only booleans and positive numbers.
     273       18444 :     data_specification()
     274       18444 :     {
     275       18444 :     }
     276             : 
     277             :     ///\brief Constructor from an aterm.
     278             :     /// \param[in] t a term adhering to the internal format.
     279         124 :     data_specification(const atermpp::aterm_appl& t)
     280         124 :     {
     281         124 :       build_from_aterm(t);
     282         124 :     }
     283             : 
     284             :     /// \brief Indicates that the data specification is type checked.
     285             :     /// \details This builds up internal data structures and allows
     286             :     ///  access to the data specification using all the utility functions.
     287        4130 :     void declare_data_specification_to_be_type_checked()
     288             :     {
     289             :       // This is now an empty deprecated method.
     290        4130 :     }
     291             : 
     292             :     /// \brief Gets all constructors including those that are system defined.
     293             :     /// \details The time complexity is the same as for sorts().
     294             :     /// \return All constructors in this specification, including those for
     295             :     /// structured sorts.
     296             :     inline
     297       21592 :     const function_symbol_vector& constructors() const
     298             :     {
     299       21592 :       normalise_data_specification_if_required();
     300       21592 :       return m_normalised_constructors;
     301             :     }
     302             : 
     303             :     /// \brief Gets the constructors defined by the user, excluding those that
     304             :     /// are system defined.
     305             :     /// \details The time complexity for this operation is constant.
     306             :     inline
     307       11060 :     const function_symbol_vector& user_defined_constructors() const
     308             :     {
     309       11060 :       return m_user_defined_constructors;
     310             :     }
     311             : 
     312             :     /// \brief Gets all constructors of a sort including those that are system defined.
     313             :     ///
     314             :     /// \details The time complexity is the same as for sorts().
     315             :     /// \param[in] s A sort expression.
     316             :     /// \return The constructors for sort s in this specification.
     317             :     inline
     318       15150 :     const function_symbol_vector& constructors(const sort_expression& s) const
     319             :     {
     320       15150 :       normalise_data_specification_if_required();
     321       15150 :       m_grouped_normalised_constructors.reset(constructors());
     322       15150 :       return m_grouped_normalised_constructors.mapping()[normalize_sorts(s,*this)];
     323             :     }
     324             : 
     325             :     /// \brief Gets all mappings in this specification including those that are system defined.
     326             :     ///
     327             :     /// \brief The time complexity is the same as for sorts().
     328             :     /// \return All mappings in this specification, including recognisers and
     329             :     /// projection functions from structured sorts.
     330             :     inline
     331        2357 :     const function_symbol_vector& mappings() const
     332             :     {
     333        2357 :       normalise_data_specification_if_required();
     334        2357 :       return m_normalised_mappings;
     335             :     }
     336             : 
     337             :     /// \brief Gets all user defined mappings in this specification.
     338             :     ///
     339             :     /// \brief The time complexity is constant.
     340             :     /// \return All mappings in this specification, including recognisers and
     341             :     /// projection functions from structured sorts.
     342             :     inline
     343       11082 :     const function_symbol_vector& user_defined_mappings() const
     344             :     {
     345       11082 :       return m_user_defined_mappings;
     346             :     }
     347             : 
     348             :     /// \brief Gets all mappings of a sort including those that are system defined
     349             :     ///
     350             :     /// \param[in] s A sort expression.
     351             :     /// \return All mappings in this specification, for which s occurs as a
     352             :     /// right-hand side of the mapping's sort.
     353             :     inline
     354         100 :     const function_symbol_vector& mappings(const sort_expression& s) const
     355             :     {
     356         100 :       normalise_data_specification_if_required();
     357         100 :       m_grouped_normalised_mappings.reset(mappings());
     358         100 :       return m_grouped_normalised_mappings.mapping()[normalize_sorts(s, *this)];
     359             :     }
     360             : 
     361             :     /// \brief Gets all equations in this specification including those that are system defined
     362             :     ///
     363             :     /// \details The time complexity of this operation is the same as that for sort().
     364             :     /// \return All equations in this specification, including those for
     365             :     ///  structured sorts.
     366             :     inline
     367        3744 :     const std::set<data_equation>& equations() const
     368             :     {
     369        3744 :       normalise_data_specification_if_required();
     370        3744 :       return m_normalised_equations;
     371             :     }
     372             : 
     373             :     /// \brief Gets all user defined equations.
     374             :     ///
     375             :     /// \details The time complexity of this operation is constant.
     376             :     /// \return All equations in this specification, including those for
     377             :     ///  structured sorts.
     378             :     inline
     379       10980 :     const data_equation_vector& user_defined_equations() const
     380             :     {
     381       10980 :       return m_user_defined_equations;
     382             :     }
     383             : 
     384             :     /// \brief Adds a constructor to this specification
     385             :     ///
     386             :     /// \param[in] f A function symbol.
     387             :     /// \pre a mapping f does not yet occur in this specification.
     388             :     /// \note this operation does not invalidate iterators of constructors_const_range
     389         123 :     void add_constructor(const function_symbol& f)
     390             :     {
     391         123 :       if (std::find(m_user_defined_constructors.begin(),m_user_defined_constructors.end(),f)==m_user_defined_constructors.end())
     392             :       {
     393         120 :         m_user_defined_constructors.push_back(f);
     394         120 :         import_system_defined_sort(f.sort());
     395         120 :         data_is_not_necessarily_normalised_anymore();
     396             :       }
     397         123 :     }
     398             : 
     399             :     /// \brief Adds a mapping to this specification
     400             :     ///
     401             :     /// \param[in] f A function symbol.
     402             :     /// \pre a constructor f does not yet occur in this specification.
     403             :     /// \note this operation does not invalidate iterators of mappings_const_range
     404        1692 :     void add_mapping(const function_symbol& f)
     405             :     {
     406        1692 :       if (std::find(m_user_defined_mappings.begin(),m_user_defined_mappings.end(),f)==m_user_defined_mappings.end())
     407             :       {
     408        1689 :         m_user_defined_mappings.push_back(f);
     409        1689 :         import_system_defined_sort(f.sort());
     410        1689 :         data_is_not_necessarily_normalised_anymore();
     411             :       }
     412        1692 :     }
     413             : 
     414             :     /// \brief Adds an equation to this specification
     415             :     ///
     416             :     /// \param[in] e An equation.
     417             :     /// \pre e does not yet occur in this specification.
     418             :     /// \note this operation does not invalidate iterators of equations_const_range
     419        2093 :     void add_equation(const data_equation& e)
     420             :     {
     421        2093 :       if(std::find(m_user_defined_equations.begin(),m_user_defined_equations.end(),e)==m_user_defined_equations.end())
     422             :       {
     423        2089 :         m_user_defined_equations.push_back(e);
     424        2089 :         import_system_defined_sorts(find_sort_expressions(e));
     425        2089 :         data_is_not_necessarily_normalised_anymore();
     426             :       }
     427        2093 :     }
     428             : 
     429             :   private:
     430             : 
     431             :     ///\brief Puts the constructors, functions and equations in normalised form in
     432             :     ///       de data type.
     433             :     ///\details See the function normalise_sorts on arbitrary objects for a more detailed description.
     434             :     /// All sorts in the constructors, mappings and equations are normalised.
     435        9281 :     void add_data_types_for_sorts() const
     436             :     {
     437             :       // Normalise the sorts of the constructors.
     438        9281 :       m_normalised_constructors.clear();
     439        9281 :       m_normalised_mappings.clear();
     440        9281 :       m_normalised_equations.clear();
     441             : 
     442       61879 :       for (const sort_expression& sort: sorts())
     443             :       {
     444       52598 :         import_data_type_for_system_defined_sort(sort);
     445             :       }
     446             : 
     447       13378 :       for (const alias& a: user_defined_aliases())
     448             :       {
     449        4097 :         import_data_type_for_system_defined_sort(a.reference());
     450             :       }
     451             : 
     452             : 
     453             :       // Normalise the constructors.
     454        9407 :       for (const function_symbol& f: m_user_defined_constructors)
     455             :       {
     456         126 :         add_normalised_constructor(f);
     457             :       }
     458             : 
     459             :       // Normalise the sorts of the mappings.
     460       11392 :       for (const function_symbol& f: m_user_defined_mappings)
     461             :       {
     462        2111 :         add_normalised_mapping(f);
     463             :       }
     464             : 
     465             :       // Normalise the sorts of the expressions and variables in equations.
     466       12185 :       for (const data_equation& eq: m_user_defined_equations)
     467             :       {
     468        2904 :         add_normalised_equation(data::translate_user_notation(eq));
     469             :       }
     470        9281 :     }
     471             : 
     472             :     /// \brief
     473             :     /// \details
     474       54844 :     void normalise_data_specification_if_required() const
     475             :     {
     476       54844 :       if (!m_normalised_data_is_up_to_date)
     477             :       {
     478        9281 :         m_normalised_data_is_up_to_date=true;
     479        9281 :         m_grouped_normalised_constructors.expire();
     480        9281 :         m_grouped_normalised_mappings.expire();
     481        9281 :         add_data_types_for_sorts();
     482             :       }
     483       54844 :     }
     484             : 
     485             :     ///\brief Adds the system defined sorts to the sets with constructors, mappings, and equations for
     486             :     //        a given sort. If the boolean skip_equations is true, no equations are added.
     487             :     void find_associated_system_defined_data_types_for_a_sort(
     488             :                        const sort_expression& sort,
     489             :                        std::set < function_symbol >& constructors,
     490             :                        std::set < function_symbol >& mappings,
     491             :                        std::set < data_equation >& equations,
     492             :                        const bool skip_equations=false) const;
     493             : 
     494             :     ///\brief Adds the system defined sorts in a sequence.
     495             :     ///       The second argument is used to check which sorts are added, to prevent
     496             :     ///       useless repetitions of additions of sorts.
     497             :     /// The function normalise_sorts imports for the given sort_expression sort all sorts, constructors,
     498             :     /// mappings and equations that belong to this sort to the `normalised' sets in this
     499             :     /// data type. E.g. for the sort Nat of natural numbers, it is required that Pos
     500             :     /// (positive numbers) are defined.
     501       56695 :     void import_data_type_for_system_defined_sort(const sort_expression& sort) const
     502             :     {
     503      113390 :       std::set < function_symbol > constructors;
     504      113390 :       std::set < function_symbol > mappings;
     505      113390 :       std::set < data_equation > equations;
     506       56695 :       find_associated_system_defined_data_types_for_a_sort(sort, constructors, mappings, equations);
     507             : 
     508             :       // add normalised constructors, mappings and equations
     509       56695 :       add_normalised_constructors(constructors.begin(), constructors.end());
     510       56695 :       add_normalised_mappings(mappings.begin(), mappings.end());
     511       56695 :       add_normalised_equations(equations.begin(), equations.end());
     512       56695 :     }
     513             : 
     514             :   public:
     515             : 
     516             :     /// \brief This function provides a sample of all system defined sorts, constructors and mappings
     517             :     ///        that contains at least one specimen of each sort and function symbol. Because types
     518             :     ///        can be parameterised not all function symbols for all types are provided.
     519             :     /// \details The sorts, constructors and mappings for the following types are added:
     520             :     ///            Bool, Pos, Int, Nat, Real, List(Pos), FSet(Pos), FBag(Pos), Set(Pos), Bag(Pos).
     521             :     ///       How to deal with struct...
     522             :     void get_system_defined_sorts_constructors_and_mappings(
     523             :                 std::set < sort_expression >& sorts,
     524             :                 std::set < function_symbol >& constructors,
     525             :                 std::set <function_symbol >& mappings) const;
     526             : 
     527             :     /// \brief Removes constructor from specification.
     528             :     ///
     529             :     /// Note that this does not remove equations containing the constructor.
     530             :     /// \param[in] f A constructor.
     531             :     /// \pre f occurs in the specification as constructor.
     532             :     /// \post f does not occur as constructor.
     533             :     /// \note this operation does not invalidate iterators of constructors_const_range,
     534             :     /// only if they point to the element that is removed
     535           3 :     void remove_constructor(const function_symbol& f)
     536             :     {
     537           3 :       detail::remove(m_normalised_constructors, normalize_sorts(f,*this));
     538           3 :       detail::remove(m_user_defined_constructors, f);
     539           3 :     }
     540             : 
     541             :     /// \brief Removes mapping from specification.
     542             :     ///
     543             :     /// Note that this does not remove equations in which the mapping occurs.
     544             :     /// \param[in] f A function.
     545             :     /// \post f does not occur as constructor.
     546             :     /// \note this operation does not invalidate iterators of mappings_const_range,
     547             :     /// only if they point to the element that is removed
     548           2 :     void remove_mapping(const function_symbol& f)
     549             :     {
     550           2 :       detail::remove(m_normalised_mappings, normalize_sorts(f,*this));
     551           2 :       detail::remove(m_user_defined_mappings, f);
     552           2 :     }
     553             : 
     554             :     /// \brief Removes equation from specification.
     555             :     ///
     556             :     /// \param[in] e An equation.
     557             :     /// \post e is removed from this specification.
     558             :     /// \note this operation does not invalidate iterators of equations_const_range,
     559             :     /// only if they point to the element that is removed
     560           2 :     void remove_equation(const data_equation& e)
     561             :     {
     562           4 :       const data_equation e1=data::translate_user_notation(e);
     563             : 
     564           2 :       detail::remove(m_normalised_equations, normalize_sorts(e1,*this));
     565           2 :       detail::remove(m_user_defined_equations, e);
     566           2 :     }
     567             : 
     568             :     /// \brief Checks whether two sort expressions represent the same sort
     569             :     ///
     570             :     /// \param[in] s1 A sort expression
     571             :     /// \param[in] s2 A sort expression
     572       11897 :     bool equal_sorts(sort_expression const& s1, sort_expression const& s2) const
     573             :     {
     574       11897 :       normalise_data_specification_if_required();
     575       23794 :       const sort_expression normalised_sort1=normalize_sorts(s1,*this);
     576       23794 :       const sort_expression normalised_sort2=normalize_sorts(s2,*this);
     577       23794 :       return (normalised_sort1 == normalised_sort2);
     578             :     }
     579             : 
     580             :     /// \brief Checks whether a sort is certainly finite.
     581             :     ///
     582             :     /// \param[in] s A sort expression
     583             :     /// \return true if s can be determined to be finite,
     584             :     ///      false otherwise.
     585             :     bool is_certainly_finite(const sort_expression& s) const;
     586             : 
     587             :     /// \brief Checks whether a sort is a constructor sort
     588             :     ///
     589             :     /// \param[in] s A sort expression
     590             :     /// \return true if s is a constructor sort
     591             :     bool is_constructor_sort(const sort_expression& s) const
     592             :     {
     593             :       normalise_data_specification_if_required();
     594             :       const sort_expression normalised_sort=normalize_sorts(s,*this);
     595             :       return !is_function_sort(normalised_sort) && !constructors(normalised_sort).empty();
     596             :     }
     597             : 
     598             :     /// \brief Returns true if
     599             :     /// <ul>
     600             :     /// <li>the domain and range sorts of constructors are contained in the list of sorts</li>
     601             :     /// <li>the domain and range sorts of mappings are contained in the list of sorts</li>
     602             :     /// </ul>
     603             :     /// \return True if the data specification is well typed.
     604             :     bool is_well_typed() const;
     605             : 
     606           2 :     bool operator==(const data_specification& other) const
     607             :     {
     608           2 :       normalise_data_specification_if_required();
     609           2 :       other.normalise_data_specification_if_required();
     610             :       return
     611           4 :         sort_specification::operator==(other) &&
     612           4 :         m_normalised_constructors == other.m_normalised_constructors &&
     613           6 :         m_normalised_mappings == other.m_normalised_mappings &&
     614           4 :         m_normalised_equations == other.m_normalised_equations;
     615             :     }
     616             : 
     617       15495 :     data_specification& operator=(const data_specification& other)
     618             :     {
     619       15495 :       sort_specification::operator=(other);
     620       15495 :       m_user_defined_constructors=other.m_user_defined_constructors;
     621       15495 :       m_user_defined_mappings=other.m_user_defined_mappings;
     622       15495 :       m_user_defined_equations=other.m_user_defined_equations;
     623       15495 :       m_normalised_mappings=other.m_normalised_mappings;
     624       15495 :       m_normalised_constructors=other.m_normalised_constructors;
     625       15495 :       m_grouped_normalised_mappings=other.m_grouped_normalised_mappings;
     626       15495 :       m_grouped_normalised_constructors=other.m_grouped_normalised_constructors;
     627       15495 :       m_normalised_equations=other.m_normalised_equations;
     628       15495 :       return *this;
     629             :     }
     630             : 
     631             : }; // class data_specification
     632             : 
     633             : //--- start generated class data_specification ---//
     634             : // prototype declaration
     635             : std::string pp(const data_specification& x);
     636             : 
     637             : /// \brief Outputs the object to a stream
     638             : /// \param out An output stream
     639             : /// \param x Object x
     640             : /// \return The output stream
     641             : inline
     642           0 : std::ostream& operator<<(std::ostream& out, const data_specification& x)
     643             : {
     644           0 :   return out << data::pp(x);
     645             : }
     646             : //--- end generated class data_specification ---//
     647             : 
     648             : /// \brief Merges two data specifications into one.
     649             : /// \details It is assumed that the two specs can be merged. I.e.
     650             : ///          that the second is a safe extension of the first.
     651             : /// \param[in] spec1 One of the input specifications.
     652             : /// \param[in] spec2 The second input specification.
     653             : /// \return A specification that is merged.
     654          10 : inline data_specification operator +(data_specification spec1, const data_specification& spec2)
     655             : {
     656          10 :   for(const basic_sort& bsort: spec2.user_defined_sorts())
     657             :   {
     658           0 :     spec1.add_sort(bsort);
     659             :   }
     660             : 
     661          68 :   for(const sort_expression& sort: spec2.context_sorts())
     662             :   {
     663          58 :     spec1.add_context_sort(sort);
     664             :   }
     665             : 
     666          14 :   for(const alias& a: spec2.user_defined_aliases())
     667             :   {
     668           4 :     spec1.add_alias(a);
     669             :   }
     670             : 
     671          10 :   for(const function_symbol& f: spec2.user_defined_constructors())
     672             :   {
     673           0 :     spec1.add_constructor(f);
     674             :   }
     675             : 
     676          11 :   for(const function_symbol& f: spec2.user_defined_mappings())
     677             :   {
     678           1 :     spec1.add_mapping(f);
     679             :   }
     680             : 
     681          11 :   for(const data_equation& e: spec2.user_defined_equations())
     682             :   {
     683           1 :     spec1.add_equation(e);
     684             :   }
     685             : 
     686          10 :   return spec1;
     687             : }
     688             : 
     689             : /// \brief Finds a mapping in a data specification.
     690             : /// \param data A data specification
     691             : /// \param s A string
     692             : /// \return The found mapping
     693             : 
     694             : inline
     695          10 : function_symbol find_mapping(data_specification const& data, std::string const& s)
     696             : {
     697          10 :   const function_symbol_vector& r(data.mappings());
     698          10 :   function_symbol_vector::const_iterator i = std::find_if(r.begin(), r.end(), detail::function_symbol_has_name(s));
     699          10 :   return (i == r.end()) ? function_symbol() : *i;
     700             : }
     701             : 
     702             : /// \brief Finds a constructor in a data specification.
     703             : /// \param data A data specification
     704             : /// \param s A string
     705             : /// \return The found constructor
     706             : 
     707             : inline
     708             : function_symbol find_constructor(data_specification const& data, std::string const& s)
     709             : {
     710             :   const function_symbol_vector& r(data.constructors());
     711             :   function_symbol_vector::const_iterator i = std::find_if(r.begin(), r.end(), detail::function_symbol_has_name(s));
     712             :   return (i == r.end()) ? function_symbol() : *i;
     713             : }
     714             : 
     715             : /// \brief Finds a sort in a data specification.
     716             : /// \param data A data specification
     717             : /// \param s A string
     718             : /// \return The found sort
     719             : 
     720             : inline
     721             : sort_expression find_sort(data_specification const& data, std::string const& s)
     722             : {
     723             :   const std::set<sort_expression>& r(data.sorts());
     724             :   const std::set<sort_expression>::const_iterator i = std::find_if(r.begin(), r.end(), detail::sort_has_name(s));
     725             :   return (i == r.end()) ? sort_expression() : *i;
     726             : }
     727             : 
     728             : /// \brief Gets all equations with a data expression as head
     729             : /// on one of its sides.
     730             : ///
     731             : /// \param[in] specification A data specification.
     732             : /// \param[in] d A data expression.
     733             : /// \return All equations with d as head in one of its sides.
     734             : 
     735             : inline
     736           1 : data_equation_vector find_equations(data_specification const& specification, const data_expression& d)
     737             : {
     738           1 :   data_equation_vector result;
     739         127 :   for (const data_equation& eq: specification.equations())
     740             :   {
     741         126 :     if (eq.lhs() == d || eq.rhs() == d)
     742             :     {
     743           1 :       result.push_back(eq);
     744             :     }
     745         125 :     else if (is_application(eq.lhs()))
     746             :     {
     747         125 :       if (atermpp::down_cast<application>(eq.lhs()).head() == d)
     748             :       {
     749           1 :         result.push_back(eq);
     750             :       }
     751             :     }
     752           0 :     else if (is_application(eq.rhs()))
     753             :     {
     754           0 :       if (atermpp::down_cast<application>(eq.rhs()).head() == d)
     755             :       {
     756           0 :         result.push_back(eq);
     757             :       }
     758             :     }
     759             :   }
     760           1 :   return result;
     761             : }
     762             : 
     763             : 
     764             : 
     765             : /// \brief Order the variables in a variable list such that enumeration over these variables becomes more efficient.
     766             : //  \detail This routine is experimental, and may benefit from further investigation. The rule of thumb that is
     767             : //          now used is that first variables of enumerated types are put in the variable list. These are sorts with
     768             : //          constructors that have no arguments, typically resulting from declarations such as sort Enum = struct e1 | e2 | e3.
     769             : //          The variables with the largest number of elements are put in front.
     770             : //          Subsequently, the other data types with a finite number of elements are listed, in arbitrary sequence. At the
     771             : //          end all other variables are put in an arbitrary sequence.
     772             : /// \param[in] l A list of variables that are to be sorted.
     773             : /// \param[in] data_spec A data specification containing the constructors that are used to determine efficiency.
     774             : /// \return The same list of variables but ordered in such a way that
     775             : 
     776             : 
     777        1067 : inline variable_list order_variables_to_optimise_enumeration(const variable_list& l, const data_specification& data_spec)
     778             : {
     779             :   // Put variables with enumerated types with the largest number of elements in front.
     780             :   // Put variables of finite types as second.
     781             :   // Finally put the other variables in the list.
     782        2134 :   std::map < std::size_t,variable_list> vars_of_enumerated_type;
     783        2134 :   variable_list vars_of_finite_type;
     784        1067 :   variable_list rest_vars;
     785        1565 :   for(const variable& v: l)
     786             :   {
     787         498 :     if (data_spec.is_certainly_finite(v.sort()))
     788             :     {
     789         413 :       bool is_enumerated_type=true;
     790        1145 :       for(const function_symbol& f: data_spec.constructors(v.sort()))
     791             :       {
     792         756 :         if (is_function_sort(f.sort()) && function_sort(f.sort()).domain().size()>0)
     793             :         {
     794          24 :           is_enumerated_type=false;
     795          24 :           break;
     796             :         }
     797             :       }
     798         413 :       if (is_enumerated_type)
     799             :       {
     800         389 :         vars_of_enumerated_type[data_spec.constructors(v.sort()).size()].push_front(v);
     801             :       }
     802             :       else
     803             :       {
     804          24 :         vars_of_finite_type.push_front(v);
     805             :       }
     806             :     }
     807             :     else
     808             :     {
     809             :       // variable *i has no finite type
     810          85 :       rest_vars.push_front(v);
     811             :     }
     812             :   }
     813             : 
     814             :   // Accumulate the result in rest_vars
     815        1067 :   rest_vars=vars_of_finite_type + rest_vars;
     816        1456 :   for(std::map <std::size_t,variable_list>::const_reverse_iterator k=vars_of_enumerated_type.rbegin(); k!=vars_of_enumerated_type.rend(); ++k)
     817             :   {
     818         389 :     rest_vars = k->second + rest_vars;
     819             :   }
     820        2134 :   return rest_vars;
     821             : }
     822             : 
     823             : /// \brief Returns the names of functions and mappings that occur in a data specification.
     824             : /// \param[in] dataspec A data specification
     825             : inline
     826        1338 : std::set<core::identifier_string> function_and_mapping_identifiers(const data_specification& dataspec)
     827             : {
     828        1338 :   std::set<core::identifier_string> result;
     829        9928 :   for (auto const& f: dataspec.constructors())
     830             :   {
     831        8590 :     result.insert(f.name());
     832             :   }
     833      102127 :   for (auto const& f: dataspec.mappings())
     834             :   {
     835      100789 :     result.insert(f.name());
     836             :   }
     837        1338 :   return result;
     838             : }
     839             : 
     840             : } // namespace data
     841             : 
     842             : } // namespace mcrl2
     843             : 
     844             : #endif // MCRL2_DATA_DATA_SPECIFICATION_H

Generated by: LCOV version 1.13