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: 233 240 97.1 %
Date: 2020-09-16 00:45:56 Functions: 50 51 98.0 %
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             : bool is_data_specification(const atermpp::aterm_appl& x)
      39             : {
      40             :   return x.function() == core::detail::function_symbols::DataSpec;
      41             : }
      42             : 
      43             : /// \brief data specification.
      44             : 
      45       86476 : class data_specification: public sort_specification
      46             : {
      47             :   private:
      48             : 
      49             :     /// \cond INTERNAL_DOCS
      50             :     /// \brief Cached constructors by target sort
      51      172952 :     struct target_sort_to_function_map
      52             :     {
      53             :       bool _outdated;
      54             :       std::map<sort_expression, std::vector<function_symbol> > _mapping;
      55             : 
      56      112388 :       target_sort_to_function_map()
      57      112388 :         : _outdated(true)
      58      112388 :       {}
      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         900 :       void group_functions_by_target_sort(std::map<sort_expression, std::vector<function_symbol> >& c, const Container& functions)
      65             :       {
      66       11268 :         for (typename Container::const_iterator i = functions.begin(); i != functions.end(); ++i)
      67             :         {
      68       20736 :           sort_expression index_sort(i->sort().target_sort());
      69       10368 :           if(c.find(index_sort) == c.end() || std::find(c[index_sort].begin(), c[index_sort].end(), *i) == c[index_sort].end())
      70             :           {
      71       10368 :             c[index_sort].push_back(*i);
      72             :           }
      73             :         }
      74         900 :       }
      75             : 
      76             :       template <typename FunctionContainer>
      77       15260 :       void reset(const FunctionContainer& c)
      78             :       {
      79       15260 :         if(_outdated)
      80             :         {
      81         900 :           _mapping.clear();
      82         900 :           group_functions_by_target_sort(_mapping, c);
      83         900 :           _outdated = false;
      84             :         }
      85       15260 :       }
      86             : 
      87       16164 :       void expire()
      88             :       {
      89       16164 :         _outdated = true;
      90       16164 :       }
      91             : 
      92       15260 :       std::map<sort_expression, std::vector<function_symbol> >&mapping()
      93             :       {
      94       15260 :         assert(!_outdated);
      95       15260 :         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        3906 :     void data_is_not_necessarily_normalised_anymore() const
     136             :     {
     137        3906 :       m_normalised_data_is_up_to_date=false;
     138        3906 :     }
     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       60011 :     void add_normalised_constructor(const function_symbol& f) const
     151             :     {
     152      120022 :       function_symbol g(normalize_sorts(f, *this));
     153       60011 :       if (std::find(m_normalised_constructors.begin(),m_normalised_constructors.end(),g)==m_normalised_constructors.end()) // not found
     154             :       {
     155       59115 :         m_normalised_constructors.push_back(g);
     156             :       }
     157       60011 :     }
     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      797801 :     void add_normalised_mapping(const function_symbol& f) const
     167             :     {
     168     1595602 :       function_symbol g(normalize_sorts(f, *this));
     169      797801 :       if (std::find(m_normalised_mappings.begin(),m_normalised_mappings.end(),g)==m_normalised_mappings.end()) // not found
     170             :       {
     171      767897 :         m_normalised_mappings.push_back(g);
     172             :       }
     173      797801 :     }
     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     1903066 :     void add_normalised_equation(const data_equation& e) const
     183             :     {
     184     1903066 :       m_normalised_equations.insert(normalize_sorts(e,*this));
     185     1903066 :     }
     186             : 
     187             :     template < class Iterator >
     188       52612 :     void add_normalised_constructors(Iterator begin, Iterator end) const
     189             :     {
     190      112497 :       for(Iterator i=begin; i!=end; ++i)
     191             :       {
     192       59885 :         data_specification::add_normalised_constructor(*i);
     193             :       }
     194       52612 :     }
     195             : 
     196             :     template < class Iterator >
     197       52612 :     void add_normalised_mappings(Iterator begin, Iterator end) const
     198             :     {
     199      848487 :       for(Iterator i=begin; i!=end; ++i)
     200             :       {
     201      795875 :         data_specification::add_normalised_mapping(*i);
     202             :       }
     203       52612 :     }
     204             : 
     205             :     template < class Iterator >
     206       52612 :     void add_normalised_equations(Iterator begin, Iterator end) const
     207             :     {
     208     1953015 :       for(Iterator i=begin; i!=end; ++i)
     209             :       {
     210     1900403 :         data_specification::add_normalised_equation(*i);
     211             :       }
     212       52612 :     }
     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        2815 :     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        2815 :       const structured_sort& s_sort(sort);
     231        5630 :       function_symbol_vector f(s_sort.constructor_functions(sort));
     232        2815 :       constructors.insert(f.begin(),f.end());
     233        2815 :       f = s_sort.projection_functions(sort);
     234        2815 :       mappings.insert(f.begin(),f.end());
     235        2815 :       f = s_sort.recogniser_functions(sort);
     236        2815 :       mappings.insert(f.begin(),f.end());
     237        2815 :       f = s_sort.comparison_functions(sort);
     238        2815 :       mappings.insert(f.begin(),f.end());
     239             : 
     240        2815 :       if (!skip_equations)
     241             :       {
     242        5630 :         data_equation_vector e(s_sort.constructor_equations(sort));
     243        2815 :         equations.insert(e.begin(),e.end());
     244        2815 :         e = s_sort.projection_equations(sort);
     245        2815 :         equations.insert(e.begin(),e.end());
     246        2815 :         e = s_sort.recogniser_equations(sort);
     247        2815 :         equations.insert(e.begin(),e.end());
     248        2815 :         e = s_sort.comparison_equations(sort);
     249        2815 :         equations.insert(e.begin(),e.end());
     250             :       }
     251        2815 :     }
     252             : 
     253       52622 :     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      105244 :       function_symbol_vector f(standard_generate_functions_code(sort));
     260       52622 :       mappings.insert(f.begin(), f.end());
     261             : 
     262       52622 :       if (!skip_equations)
     263             :       {
     264      105224 :         const data_equation_vector eq(standard_generate_equations_code(sort));
     265       52612 :         equations.insert(eq.begin(), eq.end());
     266             :       }
     267       52622 :     }
     268             : 
     269             :   public:
     270             : 
     271             :     ///\brief Default constructor. Generate a data specification that contains
     272             :     ///       only booleans and positive numbers.
     273       56066 :     data_specification()
     274       56066 :     {
     275       56066 :     }
     276             : 
     277             :     ///\brief Constructor from an aterm.
     278             :     /// \param[in] t a term adhering to the internal format.
     279           3 :     data_specification(const atermpp::aterm_appl& t)
     280           3 :     {
     281           3 :       build_from_aterm(t);
     282           3 :     }
     283             : 
     284             :     ///\brief Constructor from its members.
     285             :     data_specification(const basic_sort_vector& sorts,
     286             :       const alias_vector& aliases,
     287             :       const function_symbol_vector& constructors,
     288             :       const function_symbol_vector& user_defined_mappings,
     289             :       const data_equation_vector& user_defined_equations);
     290             : 
     291             :     /// \brief Gets all constructors including those that are system defined.
     292             :     /// \details The time complexity is the same as for sorts().
     293             :     /// \return All constructors in this specification, including those for
     294             :     /// structured sorts.
     295             :     inline
     296       21259 :     const function_symbol_vector& constructors() const
     297             :     {
     298       21259 :       normalise_data_specification_if_required();
     299       21259 :       return m_normalised_constructors;
     300             :     }
     301             : 
     302             :     /// \brief Gets the constructors defined by the user, excluding those that
     303             :     /// are system defined.
     304             :     /// \details The time complexity for this operation is constant.
     305             :     inline
     306       11016 :     const function_symbol_vector& user_defined_constructors() const
     307             :     {
     308       11016 :       return m_user_defined_constructors;
     309             :     }
     310             : 
     311             :     /// \brief Gets all constructors of a sort including those that are system defined.
     312             :     ///
     313             :     /// \details The time complexity is the same as for sorts().
     314             :     /// \param[in] s A sort expression.
     315             :     /// \return The constructors for sort s in this specification.
     316             :     inline
     317       15158 :     const function_symbol_vector& constructors(const sort_expression& s) const
     318             :     {
     319       15158 :       normalise_data_specification_if_required();
     320       15158 :       m_grouped_normalised_constructors.reset(constructors());
     321       15158 :       return m_grouped_normalised_constructors.mapping()[normalize_sorts(s,*this)];
     322             :     }
     323             : 
     324             :     /// \brief Gets all mappings in this specification including those that are system defined.
     325             :     ///
     326             :     /// \brief The time complexity is the same as for sorts().
     327             :     /// \return All mappings in this specification, including recognisers and
     328             :     /// projection functions from structured sorts.
     329             :     inline
     330        1987 :     const function_symbol_vector& mappings() const
     331             :     {
     332        1987 :       normalise_data_specification_if_required();
     333        1987 :       return m_normalised_mappings;
     334             :     }
     335             : 
     336             :     /// \brief Gets all user defined mappings in this specification.
     337             :     ///
     338             :     /// \brief The time complexity is constant.
     339             :     /// \return All mappings in this specification, including recognisers and
     340             :     /// projection functions from structured sorts.
     341             :     inline
     342       11038 :     const function_symbol_vector& user_defined_mappings() const
     343             :     {
     344       11038 :       return m_user_defined_mappings;
     345             :     }
     346             : 
     347             :     /// \brief Gets all mappings of a sort including those that are system defined
     348             :     ///
     349             :     /// \param[in] s A sort expression.
     350             :     /// \return All mappings in this specification, for which s occurs as a
     351             :     /// right-hand side of the mapping's sort.
     352             :     inline
     353         102 :     const function_symbol_vector& mappings(const sort_expression& s) const
     354             :     {
     355         102 :       normalise_data_specification_if_required();
     356         102 :       m_grouped_normalised_mappings.reset(mappings());
     357         102 :       return m_grouped_normalised_mappings.mapping()[normalize_sorts(s, *this)];
     358             :     }
     359             : 
     360             :     /// \brief Gets all equations in this specification including those that are system defined
     361             :     ///
     362             :     /// \details The time complexity of this operation is the same as that for sort().
     363             :     /// \return All equations in this specification, including those for
     364             :     ///  structured sorts.
     365             :     inline
     366        3788 :     const std::set<data_equation>& equations() const
     367             :     {
     368        3788 :       normalise_data_specification_if_required();
     369        3788 :       return m_normalised_equations;
     370             :     }
     371             : 
     372             :     /// \brief Gets all user defined equations.
     373             :     ///
     374             :     /// \details The time complexity of this operation is constant.
     375             :     /// \return All equations in this specification, including those for
     376             :     ///  structured sorts.
     377             :     inline
     378       10936 :     const data_equation_vector& user_defined_equations() const
     379             :     {
     380       10936 :       return m_user_defined_equations;
     381             :     }
     382             : 
     383             :     /// \brief Adds a constructor to this specification
     384             :     ///
     385             :     /// \param[in] f A function symbol.
     386             :     /// \pre a mapping f does not yet occur in this specification.
     387             :     /// \note this operation does not invalidate iterators of constructors_const_range
     388         123 :     void add_constructor(const function_symbol& f)
     389             :     {
     390         123 :       if (std::find(m_user_defined_constructors.begin(),m_user_defined_constructors.end(),f)==m_user_defined_constructors.end())
     391             :       {
     392         120 :         m_user_defined_constructors.push_back(f);
     393         120 :         import_system_defined_sort(f.sort());
     394         120 :         data_is_not_necessarily_normalised_anymore();
     395             :       }
     396         123 :     }
     397             : 
     398             :     /// \brief Adds a mapping to this specification
     399             :     ///
     400             :     /// \param[in] f A function symbol.
     401             :     /// \pre a constructor f does not yet occur in this specification.
     402             :     /// \note this operation does not invalidate iterators of mappings_const_range
     403        1696 :     void add_mapping(const function_symbol& f)
     404             :     {
     405        1696 :       if (std::find(m_user_defined_mappings.begin(),m_user_defined_mappings.end(),f)==m_user_defined_mappings.end())
     406             :       {
     407        1693 :         m_user_defined_mappings.push_back(f);
     408        1693 :         import_system_defined_sort(f.sort());
     409        1693 :         data_is_not_necessarily_normalised_anymore();
     410             :       }
     411        1696 :     }
     412             : 
     413             :     /// \brief Adds an equation to this specification
     414             :     ///
     415             :     /// \param[in] e An equation.
     416             :     /// \pre e does not yet occur in this specification.
     417             :     /// \note this operation does not invalidate iterators of equations_const_range
     418        2097 :     void add_equation(const data_equation& e)
     419             :     {
     420        2097 :       if(std::find(m_user_defined_equations.begin(),m_user_defined_equations.end(),e)==m_user_defined_equations.end())
     421             :       {
     422        2093 :         m_user_defined_equations.push_back(e);
     423        2093 :         import_system_defined_sorts(find_sort_expressions(e));
     424        2093 :         data_is_not_necessarily_normalised_anymore();
     425             :       }
     426        2097 :     }
     427             : 
     428             :   private:
     429             : 
     430             :     ///\brief Puts the constructors, functions and equations in normalised form in
     431             :     ///       de data type.
     432             :     ///\details See the function normalise_sorts on arbitrary objects for a more detailed description.
     433             :     /// All sorts in the constructors, mappings and equations are normalised.
     434        8082 :     void add_data_types_for_sorts() const
     435             :     {
     436             :       // Normalise the sorts of the constructors.
     437        8082 :       m_normalised_constructors.clear();
     438        8082 :       m_normalised_mappings.clear();
     439        8082 :       m_normalised_equations.clear();
     440             : 
     441       57119 :       for (const sort_expression& sort: sorts())
     442             :       {
     443       49037 :         import_data_type_for_system_defined_sort(sort);
     444             :       }
     445             : 
     446       11657 :       for (const alias& a: user_defined_aliases())
     447             :       {
     448        3575 :         import_data_type_for_system_defined_sort(a.reference());
     449             :       }
     450             : 
     451             : 
     452             :       // Normalise the constructors.
     453        8208 :       for (const function_symbol& f: m_user_defined_constructors)
     454             :       {
     455         126 :         add_normalised_constructor(f);
     456             :       }
     457             : 
     458             :       // Normalise the sorts of the mappings.
     459       10008 :       for (const function_symbol& f: m_user_defined_mappings)
     460             :       {
     461        1926 :         add_normalised_mapping(f);
     462             :       }
     463             : 
     464             :       // Normalise the sorts of the expressions and variables in equations.
     465       10745 :       for (const data_equation& eq: m_user_defined_equations)
     466             :       {
     467        2663 :         add_normalised_equation(data::translate_user_notation(eq));
     468             :       }
     469        8082 :     }
     470             : 
     471             :     /// \brief
     472             :     /// \details
     473       65983 :     void normalise_data_specification_if_required() const
     474             :     {
     475       65983 :       if (!m_normalised_data_is_up_to_date)
     476             :       {
     477        8082 :         m_normalised_data_is_up_to_date=true;
     478        8082 :         m_grouped_normalised_constructors.expire();
     479        8082 :         m_grouped_normalised_mappings.expire();
     480        8082 :         add_data_types_for_sorts();
     481             :       }
     482       65983 :     }
     483             : 
     484             :     ///\brief Adds the system defined sorts to the sets with constructors, mappings, and equations for
     485             :     //        a given sort. If the boolean skip_equations is true, no equations are added.
     486             :     void find_associated_system_defined_data_types_for_a_sort(
     487             :                        const sort_expression& sort,
     488             :                        std::set < function_symbol >& constructors,
     489             :                        std::set < function_symbol >& mappings,
     490             :                        std::set < data_equation >& equations,
     491             :                        const bool skip_equations=false) const;
     492             : 
     493             :     ///\brief Adds the system defined sorts in a sequence.
     494             :     ///       The second argument is used to check which sorts are added, to prevent
     495             :     ///       useless repetitions of additions of sorts.
     496             :     /// The function normalise_sorts imports for the given sort_expression sort all sorts, constructors,
     497             :     /// mappings and equations that belong to this sort to the `normalised' sets in this
     498             :     /// data type. E.g. for the sort Nat of natural numbers, it is required that Pos
     499             :     /// (positive numbers) are defined.
     500       52612 :     void import_data_type_for_system_defined_sort(const sort_expression& sort) const
     501             :     {
     502      105224 :       std::set < function_symbol > constructors;
     503      105224 :       std::set < function_symbol > mappings;
     504      105224 :       std::set < data_equation > equations;
     505       52612 :       find_associated_system_defined_data_types_for_a_sort(sort, constructors, mappings, equations);
     506             : 
     507             :       // add normalised constructors, mappings and equations
     508       52612 :       add_normalised_constructors(constructors.begin(), constructors.end());
     509       52612 :       add_normalised_mappings(mappings.begin(), mappings.end());
     510       52612 :       add_normalised_equations(equations.begin(), equations.end());
     511       52612 :     }
     512             : 
     513             :   public:
     514             : 
     515             :     /// \brief This function provides a sample of all system defined sorts, constructors and mappings
     516             :     ///        that contains at least one specimen of each sort and function symbol. Because types
     517             :     ///        can be parameterised not all function symbols for all types are provided.
     518             :     /// \details The sorts, constructors and mappings for the following types are added:
     519             :     ///            Bool, Pos, Int, Nat, Real, List(Pos), FSet(Pos), FBag(Pos), Set(Pos), Bag(Pos).
     520             :     ///       How to deal with struct...
     521             :     void get_system_defined_sorts_constructors_and_mappings(
     522             :                 std::set < sort_expression >& sorts,
     523             :                 std::set < function_symbol >& constructors,
     524             :                 std::set <function_symbol >& mappings) const;
     525             : 
     526             :     /// \brief Removes constructor from specification.
     527             :     ///
     528             :     /// Note that this does not remove equations containing the constructor.
     529             :     /// \param[in] f A constructor.
     530             :     /// \pre f occurs in the specification as constructor.
     531             :     /// \post f does not occur as constructor.
     532             :     /// \note this operation does not invalidate iterators of constructors_const_range,
     533             :     /// only if they point to the element that is removed
     534           3 :     void remove_constructor(const function_symbol& f)
     535             :     {
     536           3 :       detail::remove(m_normalised_constructors, normalize_sorts(f,*this));
     537           3 :       detail::remove(m_user_defined_constructors, f);
     538           3 :     }
     539             : 
     540             :     /// \brief Removes mapping from specification.
     541             :     ///
     542             :     /// Note that this does not remove equations in which the mapping occurs.
     543             :     /// \param[in] f A function.
     544             :     /// \post f does not occur as constructor.
     545             :     /// \note this operation does not invalidate iterators of mappings_const_range,
     546             :     /// only if they point to the element that is removed
     547           2 :     void remove_mapping(const function_symbol& f)
     548             :     {
     549           2 :       detail::remove(m_normalised_mappings, normalize_sorts(f,*this));
     550           2 :       detail::remove(m_user_defined_mappings, f);
     551           2 :     }
     552             : 
     553             :     /// \brief Removes equation from specification.
     554             :     ///
     555             :     /// \param[in] e An equation.
     556             :     /// \post e is removed from this specification.
     557             :     /// \note this operation does not invalidate iterators of equations_const_range,
     558             :     /// only if they point to the element that is removed
     559           2 :     void remove_equation(const data_equation& e)
     560             :     {
     561           4 :       const data_equation e1=data::translate_user_notation(e);
     562             : 
     563           2 :       detail::remove(m_normalised_equations, normalize_sorts(e1,*this));
     564           2 :       detail::remove(m_user_defined_equations, e);
     565           2 :     }
     566             : 
     567             :     /// \brief Checks whether two sort expressions represent the same sort
     568             :     ///
     569             :     /// \param[in] s1 A sort expression
     570             :     /// \param[in] s2 A sort expression
     571       23685 :     bool equal_sorts(sort_expression const& s1, sort_expression const& s2) const
     572             :     {
     573       23685 :       normalise_data_specification_if_required();
     574       47370 :       const sort_expression normalised_sort1=normalize_sorts(s1,*this);
     575       47370 :       const sort_expression normalised_sort2=normalize_sorts(s2,*this);
     576       47370 :       return (normalised_sort1 == normalised_sort2);
     577             :     }
     578             : 
     579             :     /// \brief Checks whether a sort is certainly finite.
     580             :     ///
     581             :     /// \param[in] s A sort expression
     582             :     /// \return true if s can be determined to be finite,
     583             :     ///      false otherwise.
     584             :     bool is_certainly_finite(const sort_expression& s) const;
     585             : 
     586             :     /// \brief Checks whether a sort is a constructor sort
     587             :     ///
     588             :     /// \param[in] s A sort expression
     589             :     /// \return true if s is a constructor sort
     590             :     bool is_constructor_sort(const sort_expression& s) const
     591             :     {
     592             :       normalise_data_specification_if_required();
     593             :       const sort_expression normalised_sort=normalize_sorts(s,*this);
     594             :       return !is_function_sort(normalised_sort) && !constructors(normalised_sort).empty();
     595             :     }
     596             : 
     597             :     /// \brief Returns true if
     598             :     /// <ul>
     599             :     /// <li>the domain and range sorts of constructors are contained in the list of sorts</li>
     600             :     /// <li>the domain and range sorts of mappings are contained in the list of sorts</li>
     601             :     /// </ul>
     602             :     /// \return True if the data specification is well typed.
     603             :     bool is_well_typed() const;
     604             : 
     605           2 :     bool operator==(const data_specification& other) const
     606             :     {
     607           2 :       normalise_data_specification_if_required();
     608           2 :       other.normalise_data_specification_if_required();
     609             :       return
     610           4 :         sort_specification::operator==(other) &&
     611           4 :         m_normalised_constructors == other.m_normalised_constructors &&
     612           6 :         m_normalised_mappings == other.m_normalised_mappings &&
     613           4 :         m_normalised_equations == other.m_normalised_equations;
     614             :     }
     615             : 
     616             : }; // class data_specification
     617             : 
     618             : //--- start generated class data_specification ---//
     619             : // prototype declaration
     620             : std::string pp(const data_specification& x);
     621             : 
     622             : /// \brief Outputs the object to a stream
     623             : /// \param out An output stream
     624             : /// \param x Object x
     625             : /// \return The output stream
     626             : inline
     627           0 : std::ostream& operator<<(std::ostream& out, const data_specification& x)
     628             : {
     629           0 :   return out << data::pp(x);
     630             : }
     631             : //--- end generated class data_specification ---//
     632             : 
     633             : /// \brief Merges two data specifications into one.
     634             : /// \details It is assumed that the two specs can be merged. I.e.
     635             : ///          that the second is a safe extension of the first.
     636             : /// \param[in] spec1 One of the input specifications.
     637             : /// \param[in] spec2 The second input specification.
     638             : /// \return A specification that is merged.
     639          10 : inline data_specification operator +(data_specification spec1, const data_specification& spec2)
     640             : {
     641          10 :   for(const basic_sort& bsort: spec2.user_defined_sorts())
     642             :   {
     643           0 :     spec1.add_sort(bsort);
     644             :   }
     645             : 
     646          68 :   for(const sort_expression& sort: spec2.context_sorts())
     647             :   {
     648          58 :     spec1.add_context_sort(sort);
     649             :   }
     650             : 
     651          14 :   for(const alias& a: spec2.user_defined_aliases())
     652             :   {
     653           4 :     spec1.add_alias(a);
     654             :   }
     655             : 
     656          10 :   for(const function_symbol& f: spec2.user_defined_constructors())
     657             :   {
     658           0 :     spec1.add_constructor(f);
     659             :   }
     660             : 
     661          11 :   for(const function_symbol& f: spec2.user_defined_mappings())
     662             :   {
     663           1 :     spec1.add_mapping(f);
     664             :   }
     665             : 
     666          11 :   for(const data_equation& e: spec2.user_defined_equations())
     667             :   {
     668           1 :     spec1.add_equation(e);
     669             :   }
     670             : 
     671          10 :   return spec1;
     672             : }
     673             : 
     674             : /// \brief Finds a mapping in a data specification.
     675             : /// \param data A data specification
     676             : /// \param s A string
     677             : /// \return The found mapping
     678             : 
     679             : inline
     680          10 : function_symbol find_mapping(data_specification const& data, std::string const& s)
     681             : {
     682          10 :   const function_symbol_vector& r(data.mappings());
     683          10 :   function_symbol_vector::const_iterator i = std::find_if(r.begin(), r.end(), detail::function_symbol_has_name(s));
     684          10 :   return (i == r.end()) ? function_symbol() : *i;
     685             : }
     686             : 
     687             : /// \brief Finds a constructor in a data specification.
     688             : /// \param data A data specification
     689             : /// \param s A string
     690             : /// \return The found constructor
     691             : 
     692             : inline
     693             : function_symbol find_constructor(data_specification const& data, std::string const& s)
     694             : {
     695             :   const function_symbol_vector& r(data.constructors());
     696             :   function_symbol_vector::const_iterator i = std::find_if(r.begin(), r.end(), detail::function_symbol_has_name(s));
     697             :   return (i == r.end()) ? function_symbol() : *i;
     698             : }
     699             : 
     700             : /// \brief Finds a sort in a data specification.
     701             : /// \param data A data specification
     702             : /// \param s A string
     703             : /// \return The found sort
     704             : 
     705             : inline
     706             : sort_expression find_sort(data_specification const& data, std::string const& s)
     707             : {
     708             :   const std::set<sort_expression>& r(data.sorts());
     709             :   const std::set<sort_expression>::const_iterator i = std::find_if(r.begin(), r.end(), detail::sort_has_name(s));
     710             :   return (i == r.end()) ? sort_expression() : *i;
     711             : }
     712             : 
     713             : /// \brief Gets all equations with a data expression as head
     714             : /// on one of its sides.
     715             : ///
     716             : /// \param[in] specification A data specification.
     717             : /// \param[in] d A data expression.
     718             : /// \return All equations with d as head in one of its sides.
     719             : 
     720             : inline
     721           1 : data_equation_vector find_equations(data_specification const& specification, const data_expression& d)
     722             : {
     723           1 :   data_equation_vector result;
     724         127 :   for (const data_equation& eq: specification.equations())
     725             :   {
     726         126 :     if (eq.lhs() == d || eq.rhs() == d)
     727             :     {
     728           1 :       result.push_back(eq);
     729             :     }
     730         125 :     else if (is_application(eq.lhs()))
     731             :     {
     732         125 :       if (atermpp::down_cast<application>(eq.lhs()).head() == d)
     733             :       {
     734           1 :         result.push_back(eq);
     735             :       }
     736             :     }
     737           0 :     else if (is_application(eq.rhs()))
     738             :     {
     739           0 :       if (atermpp::down_cast<application>(eq.rhs()).head() == d)
     740             :       {
     741           0 :         result.push_back(eq);
     742             :       }
     743             :     }
     744             :   }
     745           1 :   return result;
     746             : }
     747             : 
     748             : 
     749             : 
     750             : /// \brief Order the variables in a variable list such that enumeration over these variables becomes more efficient.
     751             : //  \detail This routine is experimental, and may benefit from further investigation. The rule of thumb that is
     752             : //          now used is that first variables of enumerated types are put in the variable list. These are sorts with
     753             : //          constructors that have no arguments, typically resulting from declarations such as sort Enum = struct e1 | e2 | e3.
     754             : //          The variables with the largest number of elements are put in front.
     755             : //          Subsequently, the other data types with a finite number of elements are listed, in arbitrary sequence. At the
     756             : //          end all other variables are put in an arbitrary sequence.
     757             : /// \param[in] l A list of variables that are to be sorted.
     758             : /// \param[in] data_spec A data specification containing the constructors that are used to determine efficiency.
     759             : /// \return The same list of variables but ordered in such a way that
     760             : 
     761             : 
     762        1091 : inline variable_list order_variables_to_optimise_enumeration(const variable_list& l, const data_specification& data_spec)
     763             : {
     764             :   // Put variables with enumerated types with the largest number of elements in front.
     765             :   // Put variables of finite types as second.
     766             :   // Finally put the other variables in the list.
     767        2182 :   std::map < std::size_t,variable_list> vars_of_enumerated_type;
     768        2182 :   variable_list vars_of_finite_type;
     769        1091 :   variable_list rest_vars;
     770        1589 :   for(const variable& v: l)
     771             :   {
     772         498 :     if (data_spec.is_certainly_finite(v.sort()))
     773             :     {
     774         413 :       bool is_enumerated_type=true;
     775        1145 :       for(const function_symbol& f: data_spec.constructors(v.sort()))
     776             :       {
     777         756 :         if (is_function_sort(f.sort()) && function_sort(f.sort()).domain().size()>0)
     778             :         {
     779          24 :           is_enumerated_type=false;
     780          24 :           break;
     781             :         }
     782             :       }
     783         413 :       if (is_enumerated_type)
     784             :       {
     785         389 :         vars_of_enumerated_type[data_spec.constructors(v.sort()).size()].push_front(v);
     786             :       }
     787             :       else
     788             :       {
     789          24 :         vars_of_finite_type.push_front(v);
     790             :       }
     791             :     }
     792             :     else
     793             :     {
     794             :       // variable *i has no finite type
     795          85 :       rest_vars.push_front(v);
     796             :     }
     797             :   }
     798             : 
     799             :   // Accumulate the result in rest_vars
     800        1091 :   rest_vars=vars_of_finite_type + rest_vars;
     801        1480 :   for(std::map <std::size_t,variable_list>::const_reverse_iterator k=vars_of_enumerated_type.rbegin(); k!=vars_of_enumerated_type.rend(); ++k)
     802             :   {
     803         389 :     rest_vars = k->second + rest_vars;
     804             :   }
     805        2182 :   return rest_vars;
     806             : }
     807             : 
     808             : /// \brief Returns the names of functions and mappings that occur in a data specification.
     809             : /// \param[in] dataspec A data specification
     810             : inline
     811         676 : std::set<core::identifier_string> function_and_mapping_identifiers(const data_specification& dataspec)
     812             : {
     813         676 :   std::set<core::identifier_string> result;
     814        5959 :   for (auto const& f: dataspec.constructors())
     815             :   {
     816        5283 :     result.insert(f.name());
     817             :   }
     818       75732 :   for (auto const& f: dataspec.mappings())
     819             :   {
     820       75056 :     result.insert(f.name());
     821             :   }
     822         676 :   return result;
     823             : }
     824             : 
     825             : } // namespace data
     826             : 
     827             : } // namespace mcrl2
     828             : 
     829             : #endif // MCRL2_DATA_DATA_SPECIFICATION_H

Generated by: LCOV version 1.13