LCOV - code coverage report
Current view: top level - data/source - data_specification.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 337 358 94.1 %
Date: 2020-02-28 00:44:21 Functions: 20 22 90.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             : #include "mcrl2/core/load_aterm.h"
      11             : #include "mcrl2/data/data_specification.h"
      12             : #include "mcrl2/data/detail/data_utility.h"
      13             : #include "mcrl2/data/detail/io.h"
      14             : #include "mcrl2/data/replace.h"
      15             : #include "mcrl2/data/substitutions/sort_expression_assignment.h"
      16             : 
      17             : // Predefined datatypes
      18             : #include "mcrl2/data/function_update.h"
      19             : #include "mcrl2/data/list.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : namespace data
      24             : {
      25             : 
      26        1491 : class finiteness_helper
      27             : {
      28             :   protected:
      29             : 
      30             :     const data_specification& m_specification;
      31             :     std::set< sort_expression > m_visiting;
      32             : 
      33        1915 :     bool is_finite_aux(const sort_expression& s)
      34             :     {
      35        3830 :       function_symbol_vector constructors(m_specification.constructors(s));
      36        1915 :       if(constructors.empty())
      37             :       {
      38           7 :         return false;
      39             :       }
      40             : 
      41        5436 :       for(const function_symbol& f: constructors)
      42             :       {
      43        3814 :         if (is_function_sort(f.sort()))
      44             :         {
      45         298 :           const function_sort f_sort(f.sort());
      46         292 :           const sort_expression_list& l=f_sort.domain();
      47             : 
      48         458 :           for(const sort_expression& e: l)
      49             :           {
      50         452 :             if (!is_finite(e))
      51             :             {
      52         286 :               return false;
      53             :             }
      54             :           }
      55             :         }
      56             :       }
      57        1622 :       return true;
      58             :     }
      59             : 
      60             :   public:
      61             : 
      62        1491 :     finiteness_helper(const data_specification& specification) : m_specification(specification)
      63        1491 :     { }
      64             : 
      65        2319 :     bool is_finite(const sort_expression& s)
      66             :     {
      67        2319 :       assert(s==normalize_sorts(s,m_specification));
      68        2319 :       if (m_visiting.count(s)>0)
      69             :       {
      70         166 :         return false;
      71             :       }
      72             : 
      73        2153 :       m_visiting.insert(s);
      74             : 
      75        2153 :       bool result=false;
      76        2153 :       if (is_basic_sort(s))
      77             :       {
      78        1915 :         result=is_finite(basic_sort(s));
      79             :       }
      80         238 :       else if (is_container_sort(s))
      81             :       {
      82          86 :         result=is_finite(container_sort(s));
      83             :       }
      84         152 :       else if (is_function_sort(s))
      85             :       {
      86         152 :         result=is_finite(function_sort(s));
      87             :       }
      88           0 :       else if (is_structured_sort(s))
      89             :       {
      90           0 :         result=is_finite(structured_sort(s));
      91             :       }
      92             : 
      93        2153 :       m_visiting.erase(s);
      94        2153 :       return result;
      95             :     }
      96             : 
      97        1915 :     bool is_finite(const basic_sort& s)
      98             :     {
      99        1915 :       return is_finite_aux(s);
     100             :     }
     101             : 
     102         152 :     bool is_finite(const function_sort& s)
     103             :     {
     104         350 :       for(const sort_expression& sort: s.domain())
     105             :       {
     106         201 :         if (!is_finite(sort))
     107             :         {
     108           3 :           return false;
     109             :         }
     110             :       }
     111             : 
     112         149 :       return is_finite(s.codomain());
     113             :     }
     114             : 
     115          86 :     bool is_finite(const container_sort& s)
     116             :     {
     117          86 :       return (s.container_name() == set_container()) ? is_finite(s.element_sort()) : false;
     118             :     }
     119             : 
     120             :     bool is_finite(const alias&)
     121             :     {
     122             :       assert(0);
     123             :       return false;
     124             :     }
     125             : 
     126           0 :     bool is_finite(const structured_sort& s)
     127             :     {
     128           0 :       return is_finite_aux(s);
     129             :     }
     130             : };
     131             : 
     132             : /// \brief Checks whether a sort is certainly finite.
     133             : ///
     134             : /// \param[in] s A sort expression
     135             : /// \return true if s can be determined to be finite,
     136             : ///      false otherwise.
     137        1491 : bool data_specification::is_certainly_finite(const sort_expression& s) const
     138             : {
     139        1491 :   const bool result=finiteness_helper(*this).is_finite(s);
     140        1491 :   return result;
     141             : }
     142             : 
     143             : 
     144             : // The function below checks whether there is an alias loop, e.g. aliases
     145             : // of the form A=B; B=A; or more complex A=B->C; B=Set(D); D=List(A); Loops
     146             : // through structured sorts are allowed. If a loop is detected, an exception
     147             : // is thrown.
     148        9178 : void sort_specification::check_for_alias_loop(
     149             :   const sort_expression& s,
     150             :   std::set<sort_expression> sorts_already_seen,
     151             :   const bool toplevel) const
     152             : {
     153        9178 :   if (is_basic_sort(s))
     154             :   {
     155        5201 :     if (sorts_already_seen.count(s)>0)
     156             :     {
     157           6 :       throw mcrl2::runtime_error("Sort alias " + pp(s) + " is defined in terms of itself.");
     158             :     }
     159       11102 :     for(const alias& a: m_user_defined_aliases)
     160             :     {
     161       10382 :       if (a.name() == s)
     162             :       {
     163        4475 :         sorts_already_seen.insert(s);
     164        4484 :         check_for_alias_loop(a.reference(), sorts_already_seen, true);
     165        4466 :         sorts_already_seen.erase(s);
     166        4466 :         return;
     167             :       }
     168             :     }
     169         720 :     return;
     170             :   }
     171             : 
     172        3977 :   if (is_container_sort(s))
     173             :   {
     174         415 :     check_for_alias_loop(container_sort(s).element_sort(),sorts_already_seen,false);
     175         411 :     return;
     176             :   }
     177             : 
     178        3564 :   if (is_function_sort(s))
     179             :   {
     180         236 :     sort_expression_list s_domain(function_sort(s).domain());
     181         235 :     for(const sort_expression& sort: s_domain)
     182             :     {
     183         119 :       check_for_alias_loop(sort,sorts_already_seen,false);
     184             :     }
     185             : 
     186         118 :     check_for_alias_loop(function_sort(s).codomain(),sorts_already_seen,false);
     187         116 :     return;
     188             :   }
     189             : 
     190             :   // A sort declaration with a struct on toplevel can be recursive. Otherwise a
     191             :   // check needs to be made.
     192        3446 :   if (is_structured_sort(s) && !toplevel)
     193             :   {
     194          10 :     const structured_sort ss(s);
     195          10 :     structured_sort_constructor_list constructors=ss.constructors();
     196          11 :     for(const structured_sort_constructor& constructor: constructors)
     197             :     {
     198          16 :       structured_sort_constructor_argument_list ssca=constructor.arguments();
     199          11 :       for(const structured_sort_constructor_argument& a: ssca)
     200             :       {
     201           7 :         check_for_alias_loop(a.sort(),sorts_already_seen,false);
     202             :       }
     203             :     }
     204             :   }
     205             : 
     206             : }
     207             : 
     208             : 
     209             : // This function returns the normal form of e, under the the map map1.
     210             : // This normal form is obtained by repeatedly applying map1, until this
     211             : // is not possible anymore. It is assumed that this procedure terminates. There is
     212             : // no check for loops.
     213       14441 : static sort_expression find_normal_form(
     214             :   const sort_expression& e,
     215             :   const std::multimap< sort_expression, sort_expression >& map1,
     216             :   std::set < sort_expression > sorts_already_seen = std::set < sort_expression >())
     217             : {
     218       14441 :   assert(sorts_already_seen.find(e)==sorts_already_seen.end()); // e has not been seen already.
     219       14441 :   assert(!is_untyped_sort(e));
     220       14441 :   assert(!is_untyped_possible_sorts(e));
     221             : 
     222       14441 :   if (is_function_sort(e))
     223             :   {
     224         314 :     const function_sort fs(e);
     225             :     const sort_expression normalised_codomain=
     226         314 :       find_normal_form(fs.codomain(),map1,sorts_already_seen);
     227         157 :     const sort_expression_list& domain=fs.domain();
     228         314 :     sort_expression_list normalised_domain;
     229         314 :     for(const sort_expression& s: domain)
     230             :     {
     231         157 :       normalised_domain.push_front(find_normal_form(s,map1,sorts_already_seen));
     232             :     }
     233         157 :     return function_sort(reverse(normalised_domain),normalised_codomain);
     234             :   }
     235             : 
     236       14284 :   if (is_container_sort(e))
     237             :   {
     238        1084 :     const container_sort cs(e);
     239         542 :     return container_sort(cs.container_name(),find_normal_form(cs.element_sort(),map1,sorts_already_seen));
     240             :   }
     241             : 
     242       27484 :   sort_expression result_sort;
     243             : 
     244       13742 :   if (is_structured_sort(e))
     245             :   {
     246        6474 :     const structured_sort ss(e);
     247        6474 :     structured_sort_constructor_list constructors=ss.constructors();
     248        6474 :     structured_sort_constructor_list normalised_constructors;
     249        9332 :     for(const structured_sort_constructor& constructor: constructors)
     250             :     {
     251       12190 :       structured_sort_constructor_argument_list normalised_ssa;
     252        8391 :       for(const structured_sort_constructor_argument& a: constructor.arguments())
     253             :       {
     254        2296 :         normalised_ssa.push_front(structured_sort_constructor_argument(a.name(),
     255        4592 :                                       find_normal_form(a.sort(),map1,sorts_already_seen)));
     256             :       }
     257             : 
     258        6095 :       normalised_constructors.push_front(
     259       24380 :                                 structured_sort_constructor(
     260        6095 :                                   constructor.name(),
     261       12190 :                                   reverse(normalised_ssa),
     262        6095 :                                   constructor.recogniser()));
     263             : 
     264             :     }
     265        3237 :     result_sort=structured_sort(reverse(normalised_constructors));
     266             :   }
     267             : 
     268       13742 :   if (is_basic_sort(e))
     269             :   {
     270       10505 :     result_sort=e;
     271             :   }
     272             : 
     273             : 
     274       13742 :   assert(is_basic_sort(result_sort) || is_structured_sort(result_sort));
     275       13742 :   const std::multimap< sort_expression, sort_expression >::const_iterator i1=map1.find(result_sort);
     276       13742 :   if (i1!=map1.end()) // found
     277             :   {
     278             : #ifndef NDEBUG
     279         843 :     sorts_already_seen.insert(result_sort);
     280             : #endif
     281         843 :     return find_normal_form(i1->second,map1,sorts_already_seen);
     282             :   }
     283       12899 :   return result_sort;
     284             : }
     285             : 
     286       18569 : void sort_specification::add_predefined_basic_sorts()
     287             : {
     288       18569 :     add_system_defined_sort(sort_bool::bool_());
     289       18569 :     add_system_defined_sort(sort_pos::pos());
     290       18569 : }
     291             : 
     292      113446 : void sort_specification::import_system_defined_sort(const sort_expression& sort)
     293             : {
     294             : 
     295      113446 :   if (is_untyped_sort(sort) || is_untyped_possible_sorts(sort))
     296             :   {
     297         144 :     mCRL2log(mcrl2::log::debug) << "Erroneous attempt to insert an untyped sort into the a sort specification\n";
     298         144 :     return;
     299             :   }
     300             :   // Add an element, and stop if it was already added.
     301      113302 :   if (!m_sorts_in_context.insert(sort).second)
     302             :   {
     303       57532 :     return;
     304             :   }
     305             : 
     306       55770 :   sorts_are_not_necessarily_normalised_anymore();
     307             :   // add the sorts on which this sorts depends.
     308       55770 :   if (sort == sort_real::real_())
     309             :   {
     310             :     // Int is required as the rewrite rules of Real rely on it.
     311         746 :     import_system_defined_sort(sort_int::int_());
     312             :   }
     313       55024 :   else if (sort == sort_int::int_())
     314             :   {
     315             :     // See above, Int requires Nat.
     316         799 :     import_system_defined_sort(sort_nat::nat());
     317             :   }
     318       54225 :   else if (sort == sort_nat::nat())
     319             :   {
     320             :     // Nat requires NatPair.
     321        1748 :     import_system_defined_sort(sort_nat::natpair());
     322             :   }
     323       52477 :   else if (is_function_sort(sort))
     324             :   {
     325        9136 :     const function_sort& fsort=atermpp::down_cast<function_sort>(sort);
     326        9136 :     import_system_defined_sorts(fsort.domain());
     327        9136 :     import_system_defined_sort(fsort.codomain());
     328             :   }
     329       43341 :   else if (is_container_sort(sort))
     330             :   {
     331        1466 :     const sort_expression element_sort(container_sort(sort).element_sort());
     332             :     // Import the element sort (which may be a complex sort also).
     333         733 :     import_system_defined_sort(element_sort);
     334         733 :     if (sort_list::is_list(sort))
     335             :     {
     336         356 :       import_system_defined_sort(sort_nat::nat()); // Required for lists.
     337             :     }
     338         377 :     else if (sort_set::is_set(sort))
     339             :     {
     340         145 :       import_system_defined_sort(sort_fset::fset(element_sort));
     341             :       // Import the functions from element_sort->Bool.
     342         290 :       sort_expression_list element_sorts;
     343         145 :       element_sorts.push_front(element_sort);
     344         145 :       import_system_defined_sort(function_sort(element_sorts,sort_bool::bool_()));
     345             :     }
     346         232 :     else if (sort_fset::is_fset(sort))
     347             :     {
     348             :     }
     349          63 :     else if (sort_bag::is_bag(sort))
     350             :     {
     351             :       // Add the sorts Nat and set_(element_sort) to the specification.
     352          22 :       import_system_defined_sort(sort_nat::nat()); // Required for bags.
     353          22 :       import_system_defined_sort(sort_set::set_(element_sort));
     354          22 :       import_system_defined_sort(sort_fbag::fbag(element_sort));
     355             :       
     356             :       // Add the function sort element_sort->Nat to the specification
     357          44 :       sort_expression_list element_sorts ;
     358          22 :       element_sorts.push_front(element_sort);
     359          22 :       import_system_defined_sort(function_sort(element_sorts,sort_nat::nat()));
     360             :     }
     361          41 :     else if (sort_fbag::is_fbag(sort))
     362             :     {
     363          41 :       import_system_defined_sort(sort_nat::nat()); // Required for bags.
     364             :     }
     365             :   }
     366       42608 :   else if (is_structured_sort(sort))
     367             :   {
     368        3084 :     structured_sort s_sort(sort);
     369        3084 :     function_symbol_vector f(s_sort.constructor_functions(sort));
     370        4561 :     for(const function_symbol& f: s_sort.constructor_functions(sort))
     371             :     {
     372        3019 :       import_system_defined_sort(f.sort());
     373             :     }
     374             :   }
     375             : }
     376             : 
     377             : // The function below recalculates m_normalised_aliases, such that
     378             : // it forms a confluent terminating rewriting system using which
     379             : // sorts can be normalised.
     380             : // This algorithm is described in the document: algorithm-for-sort-equivalence.tex in
     381             : // the developers library of the mCRL2 toolset.
     382       10104 : void sort_specification::reconstruct_m_normalised_aliases() const
     383             : {
     384             :   // First reset the normalised aliases and the mappings and constructors that have been
     385             :   // inherited to basic sort aliases during a previous round of sort normalisation.
     386       10104 :   m_normalised_aliases.clear();
     387             : 
     388             :   // This is the first step of the algorithm.
     389             :   // Check for loops in the aliases. The type checker should already have done this,
     390             :   // but we check it again here. If there is a loop m_normalised_aliases will not be
     391             :   // built.
     392       14148 :     for(const alias& a: m_user_defined_aliases)
     393             :     {
     394        8094 :       std::set < sort_expression > sorts_already_seen; // Empty set.
     395             :     try
     396             :     {
     397        4056 :       check_for_alias_loop(a.name(),sorts_already_seen,true);
     398             :     }
     399          12 :     catch (mcrl2::runtime_error &)
     400             :     {
     401           6 :       mCRL2log(log::debug) << "Encountered an alias loop in the alias for " << a.name() <<". The normalised aliases are not constructed\n";
     402           6 :       return;
     403             :     }
     404             :   }
     405             : 
     406             :   // This is the second step of the algorithm.
     407             :   // Copy m_normalised_aliases. All aliases are stored from left to right,
     408             :   // except structured sorts, which are stored from right to left. The reason is
     409             :   // that structured sorts can be recursive, and therefore, they cannot be
     410             :   // rewritten from left to right, as this can cause sorts to be infinitely rewritten.
     411             : 
     412       20196 :   std::multimap< sort_expression, sort_expression > sort_aliases_to_be_investigated;
     413       20196 :   std::multimap< sort_expression, sort_expression > resulting_normalized_sort_aliases;
     414             : 
     415       14142 :   for(const alias& a: m_user_defined_aliases)
     416             :   {
     417        4044 :     if (is_structured_sort(a.reference()))
     418             :     {
     419        3159 :       sort_aliases_to_be_investigated.insert(std::pair<sort_expression,sort_expression>(a.reference(),a.name()));
     420             :     }
     421             :     else
     422             :     {
     423         885 :       resulting_normalized_sort_aliases.insert(std::pair<sort_expression,sort_expression>(a.name(),a.reference()));
     424             :     }
     425             :   }
     426             : 
     427             :   // Apply Knuth-Bendix completion to the rules in m_normalised_aliases.
     428       16444 :   for(; !sort_aliases_to_be_investigated.empty() ;)
     429             :   {
     430        3173 :     const std::multimap< sort_expression, sort_expression >::iterator it=sort_aliases_to_be_investigated.begin();
     431        6346 :     const sort_expression lhs=it->first;
     432        6346 :     const sort_expression rhs=it->second;
     433        3173 :     sort_aliases_to_be_investigated.erase(it);
     434             : 
     435        6197 :     for(const std::pair<const sort_expression, sort_expression >& p: resulting_normalized_sort_aliases)
     436             :     {
     437        6048 :       const sort_expression s1=data::replace_sort_expressions(lhs,sort_expression_assignment(p.first,p.second), true);
     438             : 
     439        3024 :       if (s1!=lhs)
     440             :       {
     441             :         // There is a conflict between the two sort rewrite rules.
     442          69 :         assert(is_basic_sort(rhs));
     443             :         // Choose the normal form on the basis of a lexicographical ordering. This guarantees
     444             :         // uniqueness of normal forms over different tools. Ordering on addresses (as used previously)
     445             :         // proved to be unstable over different tools.
     446          69 :         const bool rhs_to_s1 = is_basic_sort(s1) && pp(basic_sort(s1))<=pp(rhs);
     447         138 :         const sort_expression left_hand_side=(rhs_to_s1?rhs:s1);
     448         138 :         const sort_expression pre_normal_form=(rhs_to_s1?s1:rhs);
     449          69 :         assert(is_basic_sort(pre_normal_form));
     450          69 :         const sort_expression& e1=pre_normal_form;
     451          69 :         if (e1!=left_hand_side)
     452             :         {
     453         112 :           const sort_expression normalised_lhs=find_normal_form(left_hand_side,resulting_normalized_sort_aliases);
     454             :           // Check whether the inserted sort rewrite rule is already in sort_aliases_to_be_investigated.
     455         168 :           if (std::find_if(sort_aliases_to_be_investigated.lower_bound(normalised_lhs),
     456             :                         sort_aliases_to_be_investigated.upper_bound(normalised_lhs),
     457          98 :                         [&rhs](const std::pair<sort_expression,sort_expression>& x){ return x.second==rhs; })
     458         168 :                    == sort_aliases_to_be_investigated.upper_bound(normalised_lhs)) // Not found.
     459             :           {
     460          14 :             sort_aliases_to_be_investigated.insert(
     461          28 :                   std::pair<sort_expression,sort_expression > (normalised_lhs, e1));
     462             :           }
     463             :         }
     464             :       }
     465             :       else
     466             :       {
     467        5910 :         const sort_expression s2 = data::replace_sort_expressions(p.first,sort_expression_assignment(lhs,rhs), true);
     468        2955 :         if (s2!=p.first)
     469             :         {
     470           0 :           assert(is_basic_sort(p.second));
     471             :           // Choose the normal form on the basis of a lexicographical ordering. This guarantees
     472             :           // uniqueness of normal forms over different tools.
     473           0 :           const bool i_second_to_s2 = is_basic_sort(s2) && pp(basic_sort(s2))<=pp(p.second);
     474           0 :           const sort_expression left_hand_side=(i_second_to_s2?p.second:s2);
     475           0 :           const sort_expression pre_normal_form=(i_second_to_s2?s2:p.second);
     476           0 :           assert(is_basic_sort(pre_normal_form));
     477           0 :           const sort_expression& e2=pre_normal_form;
     478           0 :           if (e2!=left_hand_side)
     479             :           {
     480           0 :             const sort_expression normalised_lhs=find_normal_form(left_hand_side,resulting_normalized_sort_aliases);
     481             :             // Check whether the inserted sort rewrite rule is already in sort_aliases_to_be_investigated.
     482           0 :             if (std::find_if(sort_aliases_to_be_investigated.lower_bound(normalised_lhs),
     483             :                           sort_aliases_to_be_investigated.upper_bound(normalised_lhs),
     484           0 :                           [&rhs](const std::pair<sort_expression,sort_expression>& x){ return x.second==rhs; })
     485           0 :                      == sort_aliases_to_be_investigated.upper_bound(normalised_lhs)) // Not found.
     486             :             {
     487           0 :               sort_aliases_to_be_investigated.insert(
     488           0 :                     std::pair<sort_expression,sort_expression > (normalised_lhs,e2));
     489             :             }
     490             :           }
     491             :         }
     492             :       }
     493             :     }
     494        3173 :     assert(lhs!=rhs);
     495        6346 :     const sort_expression normalised_lhs = find_normal_form(lhs,resulting_normalized_sort_aliases);
     496        6346 :     const sort_expression normalised_rhs = find_normal_form(rhs,resulting_normalized_sort_aliases);
     497        3173 :     if (normalised_lhs!=normalised_rhs)
     498             :     {
     499        3159 :       resulting_normalized_sort_aliases.insert(std::pair<sort_expression,sort_expression >(normalised_lhs,normalised_rhs));
     500             :     }
     501             :   }
     502             :   // Copy resulting_normalized_sort_aliases into m_normalised_aliases, i.e. from multimap to map.
     503             :   // If there are rules with equal left hand side, only one is arbitrarily chosen. Rewrite the
     504             :   // right hand side to normal form.
     505             : 
     506       14142 :   for(const std::pair<const sort_expression,sort_expression>& p: resulting_normalized_sort_aliases)
     507             :   {
     508        8088 :     const sort_expression normalised_rhs = find_normal_form(p.second,resulting_normalized_sort_aliases);
     509        4044 :     m_normalised_aliases[p.first]=normalised_rhs;
     510             : 
     511        4044 :     assert(p.first!=normalised_rhs);
     512             :   }
     513             : }
     514             : 
     515             : ///\brief Adds the system defined sorts to the sets with constructors, mappings, and equations for
     516             : //        a given sort. If the boolean skip_equations is true, no equations are added.
     517       56705 : void data_specification::find_associated_system_defined_data_types_for_a_sort(
     518             :                    const sort_expression& sort,
     519             :                    std::set < function_symbol >& constructors,
     520             :                    std::set < function_symbol >& mappings,
     521             :                    std::set < data_equation >& equations,
     522             :                    const bool skip_equations) const
     523             : {
     524             :   // add sorts, constructors, mappings and equations
     525       56705 :   if (sort == sort_bool::bool_())
     526             :   {
     527       18564 :     function_symbol_vector f(sort_bool::bool_generate_constructors_code());
     528        9282 :     constructors.insert(f.begin(), f.end());
     529        9282 :     f = sort_bool::bool_generate_functions_code();
     530        9282 :     mappings.insert(f.begin(), f.end());
     531        9282 :     if (!skip_equations)
     532             :     {
     533       18562 :       data_equation_vector e(sort_bool::bool_generate_equations_code());
     534        9281 :       equations.insert(e.begin(),e.end());
     535             :     }
     536             :   }
     537       47423 :   else if (sort == sort_real::real_())
     538             :   {
     539        6260 :     function_symbol_vector f(sort_real::real_generate_constructors_code());
     540        3130 :     constructors.insert(f.begin(),f.end());
     541        3130 :     f = sort_real::real_generate_functions_code();
     542        3130 :     mappings.insert(f.begin(),f.end());
     543        3130 :     if (!skip_equations)
     544             :     {
     545        6258 :       data_equation_vector e(sort_real::real_generate_equations_code());
     546        3129 :       equations.insert(e.begin(),e.end());
     547             :     }
     548             :   }
     549       44293 :   else if (sort == sort_int::int_())
     550             :   {
     551        6384 :     function_symbol_vector f(sort_int::int_generate_constructors_code());
     552        3192 :     constructors.insert(f.begin(),f.end());
     553        3192 :     f = sort_int::int_generate_functions_code();
     554        3192 :     mappings.insert(f.begin(),f.end());
     555        3192 :     if (!skip_equations)
     556             :     {
     557        6382 :       data_equation_vector e(sort_int::int_generate_equations_code());
     558        3191 :       equations.insert(e.begin(),e.end());
     559             :     }
     560             :   }
     561       41101 :   else if (sort == sort_nat::nat())
     562             :   {
     563        8260 :     function_symbol_vector f(sort_nat::nat_generate_constructors_code());
     564        4130 :     constructors.insert(f.begin(),f.end());
     565        4130 :     f = sort_nat::nat_generate_functions_code();
     566        4130 :     mappings.insert(f.begin(),f.end());
     567        4130 :     if (!skip_equations)
     568             :     {
     569        8258 :       data_equation_vector e(sort_nat::nat_generate_equations_code());
     570        4129 :       equations.insert(e.begin(),e.end());
     571             :     }
     572             :   }
     573       36971 :   else if (sort == sort_pos::pos())
     574             :   {
     575       18892 :     function_symbol_vector f(sort_pos::pos_generate_constructors_code());
     576        9446 :     constructors.insert(f.begin(),f.end());
     577        9446 :     f = sort_pos::pos_generate_functions_code();
     578        9446 :     mappings.insert(f.begin(),f.end());
     579        9446 :     if (!skip_equations)
     580             :     {
     581       18890 :       data_equation_vector e(sort_pos::pos_generate_equations_code());
     582        9445 :       equations.insert(e.begin(),e.end());
     583             :     }
     584             :   }
     585       27525 :   else if (is_function_sort(sort))
     586             :   {
     587       14475 :     const sort_expression& t=function_sort(sort).codomain();
     588       14475 :     const sort_expression_list& l=function_sort(sort).domain();
     589       14475 :     if (l.size()==1)
     590             :     {
     591       11692 :       const function_symbol_vector f = function_update_generate_functions_code(l.front(),t);
     592        5846 :       mappings.insert(f.begin(),f.end());
     593             : 
     594        5846 :       if (!skip_equations)
     595             :       {
     596       11692 :         data_equation_vector e(function_update_generate_equations_code(l.front(),t));
     597        5846 :         equations.insert(e.begin(),e.end());
     598             :       }
     599             :     }
     600             :   }
     601       13050 :   else if (is_container_sort(sort))
     602             :   {
     603        4130 :     sort_expression element_sort(container_sort(sort).element_sort());
     604        2065 :     if (sort_list::is_list(sort))
     605             :     {
     606        2184 :       function_symbol_vector f(sort_list::list_generate_constructors_code(element_sort));
     607        1092 :       constructors.insert(f.begin(),f.end());
     608        1092 :       f = sort_list::list_generate_functions_code(element_sort);
     609        1092 :       mappings.insert(f.begin(),f.end());
     610        1092 :       if (!skip_equations)
     611             :       {
     612        2182 :         data_equation_vector e(sort_list::list_generate_equations_code(element_sort));
     613        1091 :         equations.insert(e.begin(),e.end());
     614             :       }
     615             :     }
     616         973 :     else if (sort_set::is_set(sort))
     617             :     {
     618         700 :       sort_expression_list element_sorts;
     619         350 :       element_sorts.push_front(element_sort);
     620         700 :       function_symbol_vector f(sort_set::set_generate_constructors_code(element_sort));
     621         350 :       constructors.insert(f.begin(),f.end());
     622         350 :       f = sort_set::set_generate_functions_code(element_sort);
     623         350 :       mappings.insert(f.begin(),f.end());
     624         350 :       if (!skip_equations)
     625             :       {
     626         698 :         data_equation_vector e(sort_set::set_generate_equations_code(element_sort));
     627         349 :         equations.insert(e.begin(),e.end());
     628             :       }
     629             :     }
     630         623 :     else if (sort_fset::is_fset(sort))
     631             :     {
     632         954 :       function_symbol_vector f = sort_fset::fset_generate_constructors_code(element_sort);
     633         477 :       constructors.insert(f.begin(),f.end());
     634         477 :       f = sort_fset::fset_generate_functions_code(element_sort);
     635         477 :       mappings.insert(f.begin(),f.end());
     636         477 :       if (!skip_equations)
     637             :       {
     638         952 :         data_equation_vector e = sort_fset::fset_generate_equations_code(element_sort);
     639         476 :         equations.insert(e.begin(),e.end());
     640             :       }
     641             :     }
     642         146 :     else if (sort_bag::is_bag(sort))
     643             :     {
     644         142 :       sort_expression_list element_sorts;
     645          71 :       element_sorts.push_front(element_sort);
     646         142 :       function_symbol_vector f(sort_bag::bag_generate_constructors_code(element_sort));
     647          71 :       constructors.insert(f.begin(),f.end());
     648          71 :       f = sort_bag::bag_generate_functions_code(element_sort);
     649          71 :       mappings.insert(f.begin(),f.end());
     650          71 :       if (!skip_equations)
     651             :       {
     652         140 :         data_equation_vector e(sort_bag::bag_generate_equations_code(element_sort));
     653          70 :         equations.insert(e.begin(),e.end());
     654             :       }
     655             :     }
     656          75 :     else if (sort_fbag::is_fbag(sort))
     657             :     {
     658         150 :       function_symbol_vector f = sort_fbag::fbag_generate_constructors_code(element_sort);
     659          75 :       constructors.insert(f.begin(),f.end());
     660          75 :       f = sort_fbag::fbag_generate_functions_code(element_sort);
     661          75 :       mappings.insert(f.begin(),f.end());
     662          75 :       if (!skip_equations)
     663             :       {
     664         148 :         data_equation_vector e = sort_fbag::fbag_generate_equations_code(element_sort);
     665          74 :         equations.insert(e.begin(),e.end());
     666             :       }
     667             :     }
     668             :   }
     669       10985 :   else if (is_structured_sort(sort))
     670             :   {
     671        3192 :     insert_mappings_constructors_for_structured_sort(
     672             :                     atermpp::down_cast<structured_sort>(sort),
     673             :                     constructors, mappings, equations, skip_equations);
     674             :   }
     675       56705 :   add_standard_mappings_and_equations(sort, mappings, equations, skip_equations);
     676       56705 : }
     677             : 
     678           1 : void data_specification::get_system_defined_sorts_constructors_and_mappings(
     679             :             std::set < sort_expression >& sorts,
     680             :             std::set < function_symbol >& constructors,
     681             :             std::set <function_symbol >& mappings) const
     682             : {
     683           1 :   sorts.insert(sort_bool::bool_());
     684           1 :   sorts.insert(sort_pos::pos());
     685           1 :   sorts.insert(sort_nat::nat());
     686           1 :   sorts.insert(sort_int::int_());
     687           1 :   sorts.insert(sort_real::real_());
     688           1 :   sorts.insert(sort_list::list(sort_pos::pos()));
     689           1 :   sorts.insert(sort_fset::fset(sort_pos::pos()));
     690           1 :   sorts.insert(sort_set::set_(sort_pos::pos()));
     691           1 :   sorts.insert(sort_fbag::fbag(sort_pos::pos()));
     692           1 :   sorts.insert(sort_bag::bag(sort_pos::pos()));
     693             : 
     694           2 :   std::set < data_equation > dummy_equations;
     695          11 :   for(const sort_expression& s: sorts)
     696             :   {
     697          10 :     find_associated_system_defined_data_types_for_a_sort(s, constructors, mappings, dummy_equations, true);
     698             :   }
     699           1 :   assert(dummy_equations.size()==0);
     700           1 : }
     701             : 
     702         140 : bool data_specification::is_well_typed() const
     703             : {
     704             :   // check 1)
     705         140 :   if (!detail::check_data_spec_sorts(constructors(), sorts()))
     706             :   {
     707             :     std::clog << "data_specification::is_well_typed() failed: not all of the sorts appearing in the constructors "
     708           0 :               << data::pp(constructors()) << " are declared in " << data::pp(sorts()) << std::endl;
     709           0 :     return false;
     710             :   }
     711             : 
     712             :   // check 2)
     713         140 :   if (!detail::check_data_spec_sorts(mappings(), sorts()))
     714             :   {
     715             :     std::clog << "data_specification::is_well_typed() failed: not all of the sorts appearing in the mappings "
     716           0 :               << data::pp(mappings()) << " are declared in " << data::pp(sorts()) << std::endl;
     717           0 :     return false;
     718             :   }
     719             : 
     720         140 :   return true;
     721             : }
     722             : /// \endcond
     723             : 
     724             : /// There are two types of representations of ATerms:
     725             : ///  - the bare specification that does not contain constructor, mappings
     726             : ///    and equations for system defined sorts
     727             : ///  - specification that includes all system defined information (legacy)
     728             : /// The last type must eventually disappear but is unfortunately still in
     729             : /// use in a substantial amount of source code.
     730             : /// Note, all sorts with name prefix \@legacy_ are eliminated
     731         124 : void data_specification::build_from_aterm(const atermpp::aterm_appl& term)
     732             : {
     733         124 :   assert(core::detail::check_rule_DataSpec(term));
     734             : 
     735             :   // Note backwards compatibility measure: alias is no longer a sort_expression
     736             :   const atermpp::term_list<atermpp::aterm_appl> term_sorts=
     737         248 :                  atermpp::down_cast<atermpp::term_list<atermpp::aterm_appl> >(atermpp::down_cast<atermpp::aterm_appl>(term[0])[0]);
     738             :   const data::function_symbol_list term_constructors=
     739         248 :                  atermpp::down_cast<data::function_symbol_list>(atermpp::down_cast<atermpp::aterm_appl>(term[1])[0]);
     740             :   const data::function_symbol_list term_mappings=
     741         248 :                  atermpp::down_cast<data::function_symbol_list>(atermpp::down_cast<atermpp::aterm_appl>(term[2])[0]);
     742             :   const data::data_equation_list term_equations=
     743         248 :                  atermpp::down_cast<data::data_equation_list>(atermpp::down_cast<atermpp::aterm_appl>(term[3])[0]);
     744             : 
     745             :   // Store the sorts and aliases.
     746         206 :   for(const atermpp::aterm_appl& t: term_sorts)
     747             :   {
     748          82 :     if (data::is_alias(t)) // Compatibility with legacy code
     749             :     {
     750          81 :       add_alias(atermpp::down_cast<data::alias>(t));
     751             :     }
     752             :     else
     753             :     {
     754           1 :       add_sort(atermpp::down_cast<basic_sort>(t));
     755             :     }
     756             :   }
     757             : 
     758             :   // Store the constructors.
     759         125 :   for(const function_symbol& f: term_constructors)
     760             :   {
     761           1 :     add_constructor(f);
     762             :   }
     763             : 
     764             :   // Store the mappings.
     765         164 :   for(const function_symbol& f: term_mappings)
     766             :   {
     767          40 :     add_mapping(f);
     768             :   }
     769             : 
     770             :   // Store the equations.
     771         155 :   for(const data_equation& e: term_equations)
     772             :   {
     773          31 :     add_equation(e);
     774             :   }
     775         124 : }
     776             : 
     777             : } // namespace data
     778         366 : } // namespace mcrl2

Generated by: LCOV version 1.13