Line data    Source code

       1             : // Author(s): Wieger Wesselink, Thomas Neele
       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/equality_one_point_substitution.h
      10             : 
      11             : 
      12             : #ifndef MCRL2_DATA_EQUALITY_ONE_POINT_SUBSTITUTION_H
      13             : #define MCRL2_DATA_EQUALITY_ONE_POINT_SUBSTITUTION_H
      14             : 
      15             : 
      16             : #include "mcrl2/data/replace.h"
      17             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      18             : 
      19             : namespace mcrl2::data
      20             : {
      21             : namespace detail
      22             : {
      23             : 
      24             : struct one_point_rule_substitution_algorithm
      25             : {
      26             :   std::map<data::variable, std::vector<data::data_expression> > equalities;
      27             :   data::mutable_map_substitution<> sigma;
      28             :   std::set<data::variable> sigma_lhs_variables;
      29             :   data::set_identifier_generator id_generator;
      30             : 
      31             :   // applies the substitution sigma to all right hand sides of equalities
      32       31569 :   void apply_sigma()
      33             :   {
      34       34257 :     for (auto& [_, exprs]: equalities)
      35             :     {
      36        5395 :       for (data::data_expression& e: exprs)
      37             :       {
      38        2707 :         e = data::replace_variables_capture_avoiding(e, sigma, id_generator);
      39             :       }
      40             :     }
      41       31569 :   }
      42             : 
      43             :   // finds all assignments to a constant, and adds them to sigma
      44             :   // returns true if any assignment was found
      45       14756 :   bool find_constant_assignments()
      46             :   {
      47       14756 :     std::vector<data::variable> to_be_removed;
      48       16944 :     for (const auto& [lhs, exprs]: equalities)
      49             :     {
      50        4400 :       for (const data::data_expression& e: exprs)
      51             :       {
      52        2212 :         if (data::is_constant(e))
      53             :         {
      54          45 :           sigma[lhs] = e;
      55          45 :           sigma_lhs_variables.insert(lhs);
      56          45 :           to_be_removed.push_back(lhs);
      57             :         }
      58             :       }
      59             :     }
      60             : 
      61             :     // remove entries for the assignments
      62       14801 :     for (const data::variable& v: to_be_removed)
      63             :     {
      64          45 :       equalities.erase(v);
      65             :     }
      66             : 
      67             :     // apply sigma to the right hand sides
      68       14756 :     apply_sigma();
      69             : 
      70       29512 :     return !to_be_removed.empty();
      71       14756 :   }
      72             : 
      73             :   // finds an arbitrary assignment and adds it to sigma
      74             :   // returns true if any assignment was found
      75       16813 :   bool find_assignment()
      76             :   {
      77       16813 :     std::set<data::variable> to_be_removed;
      78       16813 :     for (const auto& [lhs,exprs]: equalities)
      79             :     {
      80        2057 :       for (const data::data_expression& e: exprs)
      81             :       {
      82        2057 :         if (e != lhs)
      83             :         {
      84        2057 :           sigma[lhs] = e;
      85        2057 :           sigma_lhs_variables.insert(lhs);
      86        2057 :           std::set<data::variable> FV = data::find_free_variables(e);
      87        4580 :           for (const data::variable& v: FV)
      88             :           {
      89        2523 :             id_generator.add_identifier(v.name());
      90             :           }
      91        2057 :           to_be_removed.insert(lhs);
      92        2057 :           to_be_removed.insert(FV.begin(), FV.end());
      93        2057 :           break;
      94        2057 :         }
      95             :       }
      96        2057 :       if (!to_be_removed.empty())
      97             :       {
      98        2057 :         break;
      99             :       }
     100             :     }
     101             : 
     102             :     // remove entries for the assignments
     103       21393 :     for (const data::variable& v: to_be_removed)
     104             :     {
     105        4580 :       equalities.erase(v);
     106             :     }
     107             : 
     108             :     // apply sigma to the right hand sides
     109       16813 :     apply_sigma();
     110             : 
     111       33626 :     return !to_be_removed.empty();
     112       16813 :   }
     113             : 
     114       14756 :   void build_equality_map(const std::map<data::variable, std::set<data::data_expression> >& equalities_, bool check_vars, const data::variable_list& vars = data::variable_list())
     115             :   {
     116             :     using utilities::detail::contains;
     117       59218 :     for (const auto& [lhs,exprs]: equalities_)
     118             :     {
     119       44462 :       if (check_vars && !contains(vars, lhs))
     120             :       {
     121       42274 :         continue;
     122             :       }
     123        2188 :       std::vector<data::data_expression> E;
     124        4400 :       for (const data::data_expression& e: exprs)
     125             :       {
     126        2212 :         if (!contains(data::find_free_variables(e), lhs))
     127             :         {
     128        2212 :           E.push_back(e);
     129             :         }
     130             :       }
     131        2188 :       if (!E.empty())
     132             :       {
     133        2188 :         equalities[lhs] = E;
     134             :       }
     135        2188 :     }
     136       14756 :   }
     137             : 
     138             :   one_point_rule_substitution_algorithm(const std::map<data::variable, std::set<data::data_expression> >& equalities_)
     139             :   {
     140             :     build_equality_map(equalities_, false);
     141             :   }
     142             : 
     143       14756 :   one_point_rule_substitution_algorithm(const std::map<data::variable, std::set<data::data_expression> >& equalities_, const data::variable_list& quantifier_variables)
     144       14756 :   {
     145       14756 :     build_equality_map(equalities_, true, quantifier_variables);
     146       14756 :   }
     147             : 
     148       14756 :   data::mutable_map_substitution<> run(bool find_all_assignments = true)
     149             :   {
     150       14756 :     find_constant_assignments();
     151       16813 :     while (find_all_assignments)
     152             :     {
     153       16813 :       if (!find_assignment())
     154             :       {
     155       14756 :         break;
     156             :       }
     157             :     }
     158       14756 :     return sigma;
     159             :   }
     160             : 
     161             :   // creates a substitution from a set of (in-)equalities for a given list of quantifier variables
     162             :   // returns the substitution, and the subset of quantifier variables that are not used in the substitution
     163       14756 :   std::pair<data::mutable_map_substitution<>, std::vector<data::variable> > run(const data::variable_list& quantifier_variables, bool find_all_assignments = true)
     164             :   {
     165             :     using utilities::detail::contains;
     166             : 
     167       14756 :     run(find_all_assignments);
     168             : 
     169       14756 :     std::vector<data::variable> remaining_variables;
     170       44069 :     for (const data::variable& v: quantifier_variables)
     171             :     {
     172       29313 :       if (!contains(sigma_lhs_variables, v))
     173             :       {
     174       27213 :         remaining_variables.push_back(v);
     175             :       }
     176             :     }
     177             : 
     178       29512 :     return std::make_pair(sigma, remaining_variables);
     179       14756 :   }
     180             : };
     181             : 
     182             : } // namespace detail
     183             : 
     184             : 
     185             : /// @brief creates a substitution from a set of (in-)equalities for a given list of quantifier variables
     186             : /// @param quantifier_variables Consider only these variables
     187             : /// @param find_all_assignments True to find all assignments, false to find only constant assignments
     188             : /// @return the substitution, and the subset of quantifier variables that are not used in the substitution
     189             : inline
     190       14756 : std::pair<data::mutable_map_substitution<>, std::vector<data::variable> > make_one_point_rule_substitution(
     191             :   const std::map<data::variable, std::set<data::data_expression> >& equalities,
     192             :   const data::variable_list& quantifier_variables,
     193             :   bool find_all_assignments = true)
     194             : {
     195       14756 :   detail::one_point_rule_substitution_algorithm algorithm(equalities, quantifier_variables);
     196       29512 :   return algorithm.run(quantifier_variables, find_all_assignments);
     197       14756 : }
     198             : 
     199             : /// @brief creates a substitution from a set of (in-)equalities
     200             : /// @param find_all_assignments True to find all assignments, false to find only constant assignments
     201             : /// @return the substitution
     202             : inline
     203             : data::mutable_map_substitution<> make_one_point_rule_substitution(
     204             :   const std::map<data::variable, std::set<data::data_expression> >& equalities,
     205             :   bool find_all_assignments = true)
     206             : {
     207             :   detail::one_point_rule_substitution_algorithm algorithm(equalities);
     208             :   return algorithm.run(find_all_assignments);
     209             : }
     210             : 
     211             : } // namespace mcrl2::data
     212             : 
     213             : #endif // MCRL2_DATA_EQUALITY_ONE_POINT_SUBSTITUTION_H