Line data    Source code

       1             : // Author(s): Jeroen van der Wulp
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/data/selection.h
      10             : /// \brief Provides selection utility functionality
      11             : 
      12             : #ifndef MCRL2_DATA_SELECTION_H
      13             : #define MCRL2_DATA_SELECTION_H
      14             : 
      15             : #include "mcrl2/data/data_specification.h"
      16             : #include "mcrl2/data/find.h"
      17             : #include "mcrl2/data/fset.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace data
      23             : {
      24             : 
      25             : /** \brief Component for selecting a subset of equations that are actually used in an encompassing specification
      26             :  *
      27             :  * This component can be used with the constructor of data::rewriter
      28             :  * derived classes to select a smaller set of equations that are used as
      29             :  * rewrite rules. This limited set of rewrite rules should be enough for the
      30             :  * purpose of rewriting objects that occur in the encompassing
      31             :  * specification (the context).
      32             :  *
      33             :  * \note Use of this component can have a dramatic effect of rewriter
      34             :  * initialisation time and overall performance.
      35             :  **/
      36             : class used_data_equation_selector
      37             : {
      38             :   private:
      39             : 
      40             :     std::set< function_symbol > m_used_symbols;
      41             : 
      42             :     bool add_all;
      43             : 
      44         854 :     void add_symbol(const function_symbol &f)
      45             :     {
      46         854 :       m_used_symbols.insert(f);
      47         854 :     }
      48             : 
      49             :     template < typename Range >
      50         281 :     void add_symbols(Range const& r)
      51             :     {
      52         281 :       m_used_symbols.insert(r.begin(), r.end());
      53         281 :     }
      54             : 
      55             :   protected:
      56          32 :     void add_data_specification_symbols(const data_specification& specification)
      57             :     {
      58             :       // Always add if:Bool#Bool#Bool->Bool; This symbol is used in the prover.
      59          32 :       add_symbol(if_(sort_bool::bool_()));
      60             :       // Always add and,or:Bool#Bool->Bool and not:Bool->Bool; This symbol is generated when eliminating quantifiers
      61          32 :       add_symbol(sort_bool::and_());
      62          32 :       add_symbol(sort_bool::or_());
      63          32 :       add_symbol(sort_bool::not_());
      64             : 
      65             :       // Add all constructors of all sorts as they may be used when enumerating over these sorts
      66          32 :       std::set< sort_expression > sorts(specification.sorts().begin(),specification.sorts().end());
      67         274 :       for (const sort_expression& sort: sorts)
      68             :       {
      69         242 :         add_symbols(specification.constructors(sort));
      70             :         // Always add equality and inequality of each sort. The one point rewriter is using this for instance.
      71         242 :         add_symbol(equal_to(sort));
      72         242 :         add_symbol(not_equal_to(sort));
      73             : 
      74             :         // Always add insert for an FSet(S) function, as it is used when enumerating the elements of an FSet.
      75         242 :         if (sort_fset::is_fset(sort))
      76             :         {
      77           0 :           const container_sort &s = atermpp::down_cast<container_sort>(sort);
      78           0 :           add_symbol(sort_fset::insert(s.element_sort()));
      79             :         }
      80             : 
      81             :         // Always add the if:Bool#S#S->S for every sort as enumerating elements over function sorts S1 #... # S # ... # Sn -> S
      82             :         // rewriting over functions of this shape.
      83         242 :         add_symbol(if_(sort));
      84             :       }
      85             : 
      86          32 :       std::map< data_equation, std::set< function_symbol > > symbols_for_equation;
      87             : 
      88        8326 :       for (const data_equation& equation: specification.equations())
      89             :       {
      90        8294 :         std::set< function_symbol > used_symbols;
      91             : 
      92        8294 :         data::detail::make_find_function_symbols_traverser<data::data_expression_traverser>(std::inserter(used_symbols, used_symbols.end())).apply(equation.lhs());
      93        8294 :         symbols_for_equation[equation].swap(used_symbols);
      94        8294 :       }
      95             : 
      96             :       /* Calculate the closure under the function symbols that can be introduced by applying equations, such that all
      97             :          the function symbols that can occur during rewriting are present in the datatype */
      98          32 :       std::vector<bool> equations_of_which_symbols_have_been_added(specification.equations().size(),false);
      99          32 :       bool stable=false;
     100         124 :       while (!stable)
     101             :       {
     102          92 :         stable=true;
     103          92 :         std::size_t equation_count=0;
     104       26088 :         for (const data_equation& e: specification.equations())
     105             :         {
     106       45738 :           if (!equations_of_which_symbols_have_been_added[equation_count] &&
     107       19742 :               std::includes(m_used_symbols.begin(), m_used_symbols.end(), symbols_for_equation[e].begin(), symbols_for_equation[e].end()))
     108             :           {
     109        2916 :             add_function_symbols(e.rhs());
     110        2916 :             add_function_symbols(e.condition());
     111        2916 :             equations_of_which_symbols_have_been_added[equation_count]=true;
     112        2916 :             stable=false;
     113             :           }
     114       25996 :           equation_count++;
     115             :         }
     116             :       }
     117          32 :     }
     118             : 
     119             :   public:
     120             : 
     121             :     /// \brief Check whether the symbol is used.
     122      275586 :     bool operator()(const data::function_symbol& f) const
     123             :     {
     124      275586 :       if (add_all)
     125             :       {
     126      272738 :         return true;
     127             :       }
     128        2848 :       return m_used_symbols.count(f)>0;
     129             :     }
     130             : 
     131             :     /// \brief Check whether data equation relates to used symbols, and therefore is important.
     132      587538 :     bool operator()(const data_equation& e) const
     133             :     {
     134      587538 :       if (add_all)
     135             :       {
     136      581323 :         return true;
     137             :       }
     138             : 
     139        6215 :       std::set< function_symbol > used_symbols;
     140             : 
     141        6215 :       data::detail::make_find_function_symbols_traverser<data::data_expression_traverser>(std::inserter(used_symbols, used_symbols.end())).apply(e.lhs());
     142             : 
     143        6215 :       return std::includes(m_used_symbols.begin(), m_used_symbols.end(), used_symbols.begin(), used_symbols.end());
     144        6215 :     }
     145             : 
     146        5832 :     void add_function_symbols(const data_expression& t)
     147             :     {
     148        5832 :       data::detail::make_find_function_symbols_traverser<data::data_expression_traverser>(std::inserter(m_used_symbols, m_used_symbols.end())).apply(t);
     149        5832 :     }
     150             : 
     151             :     /// \brief default constructor
     152             :     used_data_equation_selector():
     153             :        add_all(true)
     154             :     {}
     155             : 
     156             :     /// \brief context is a range of function symbols
     157             :     template <typename Range>
     158           1 :     used_data_equation_selector(data_specification const& data_spec, Range const& context):
     159           1 :        add_all(false)
     160             :     {
     161           1 :       add_symbols(context);
     162           1 :       add_data_specification_symbols(data_spec);
     163           1 :     }
     164             : 
     165          31 :     used_data_equation_selector(const data_specification& specification,
     166             :                                 const std::set<function_symbol>& function_symbols,
     167             :                                 const std::set<data::variable>& global_variables,
     168             :                                 const bool do_not_remove_function_symbols
     169          31 :                                ):add_all(do_not_remove_function_symbols)
     170             :     {
     171             :       // Compensate for symbols that could be used as part of an instantiation of free variables
     172          50 :       for (const variable& global_variable: global_variables)
     173             :       {
     174          19 :         add_symbols(specification.constructors(global_variable.sort()));
     175          19 :         add_symbols(specification.mappings(global_variable.sort()));
     176             :       }
     177          31 :       m_used_symbols.insert(function_symbols.begin(), function_symbols.end());
     178          31 :       add_data_specification_symbols(specification);
     179          31 :     }
     180             : 
     181             :     /// \brief select all equations
     182        1769 :     used_data_equation_selector(const data_specification& /* specification */):
     183        1769 :        add_all(true)
     184             :     {
     185             :       /* add_symbols(specification.constructors());
     186             :       add_symbols(specification.mappings());
     187             :       add_data_specification_symbols(specification); */
     188        1769 :     }
     189             : };
     190             : 
     191             : } // namespace data
     192             : 
     193             : } // namespace mcrl2
     194             : 
     195             : #endif // MCRL2_DATA_SELECTION_H