LCOV - code coverage report
Current view: top level - smt/source - recursive_function_definition.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 165 0.0 %
Date: 2019-06-26 00:32:26 Functions: 0 10 0.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Ruud Koolen
       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             : #include <map>
      10             : #include <set>
      11             : 
      12             : #include "mcrl2/data/find.h"
      13             : #include "mcrl2/data/join.h"
      14             : #include "mcrl2/data/replace.h"
      15             : #include "mcrl2/data/set_identifier_generator.h"
      16             : #include "mcrl2/data/standard.h"
      17             : #include "mcrl2/data/substitutions/map_substitution.h"
      18             : #include "mcrl2/data/substitutions/variable_substitution.h"
      19             : #include "mcrl2/smt/recursive_function_definition.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : 
      24             : namespace smt
      25             : {
      26             : 
      27             : /*
      28             :  * A rule describes a partially pattern-matched rewrite rule.
      29             :  * match_criteria is a set of data_expression pairs (A, B)
      30             :  * where A is a data_expression over variables in the left hand
      31             :  * side of a function definition, and B is a pattern consisting of
      32             :  * constructor applications over free variables.
      33             :  *
      34             :  * The rule match_criteria = { (A, B), (C, D) }, condition = E, rhs = R
      35             :  * describes the following rewrite proposition:
      36             :  *
      37             :  *  "if the data expression A pattern-matches to pattern B, and the
      38             :  *   data expression C pattern-matches to pattern D, and the condition
      39             :  *   E is true after substituting the proper pattern-matching variables,
      40             :  *   then the right hand side R applies (again with substitution of
      41             :  *   pattern-matched variables."
      42             :  *
      43             :  * Pattern matching can then be performed by deconstructing the patterns
      44             :  * in the right hand sides of match_criteria, and rewriting rules accordingly.
      45             :  * As an example, the following rewrite rule:
      46             :  *
      47             :  *   is_even(n) -> sign_of_list_sum(n |> l) = sign_of_list_sum(l)
      48             :  *
      49             :  * Can be represented as the following rule:
      50             :  *
      51             :  *   match_criteria = { v1 -> n |> l }, condition = is_even(n), rhs = sign_of_list_sum(l)
      52             :  *
      53             :  * Which, after one step of pattern matching, gets simplified to the following rule:
      54             :  *
      55             :  *   match_criteria = { head(v1) -> n, tail(v1) -> l }, condition = is_even(n), rhs = sign_of_list_sum(l)
      56             :  */
      57           0 : struct rule
      58             : {
      59             :   std::map<data::data_expression, data::data_expression> match_criteria;
      60             :   data::data_expression rhs;
      61             :   data::data_expression condition;
      62             :   std::set<data::variable> variables;
      63             : };
      64             : 
      65             : /*
      66             :  * For a list of rules with equal left hand sides of match_criteria and only variables in
      67             :  * the right hand sides of match_criteria, construct a right hand side based on the
      68             :  * conditions and right hand sides of the rules.
      69             :  */
      70           0 : static data::data_expression construct_condition_rhs(data_specification *data_specification, const std::vector<rule>& rules, const data::sort_expression& sort)
      71             : {
      72           0 :   data::data_expression_vector negated_conditions;
      73           0 :   for (std::vector<rule>::const_iterator i = rules.begin(); i != rules.end(); i++)
      74             :   {
      75           0 :     negated_conditions.push_back(data::sort_bool::not_(i->condition));
      76             :   }
      77           0 :   data::data_expression else_clause = data::join_and(negated_conditions.begin(), negated_conditions.end());
      78             : 
      79             :   // TODO: Check whether else_clause is equivalent to false. Can we use the enumerator for this?
      80           0 :   bool conditions_are_complete = false;
      81           0 :   if (rules.size() == 1 && rules[0].condition == data::sort_bool::true_())
      82             :   {
      83           0 :     conditions_are_complete = true;
      84             :   }
      85           0 :   data::data_expression result;
      86           0 :   if (!conditions_are_complete)
      87             :   {
      88           0 :     result = data_specification->representative(sort);
      89             :   }
      90             : 
      91           0 :   for (std::vector<rule>::const_iterator i = rules.begin(); i != rules.end(); i++)
      92             :   {
      93           0 :     std::map<data::variable, data::data_expression> substitution_map;
      94           0 :     for (std::map<data::data_expression, data::data_expression>::const_iterator j = i->match_criteria.begin(); j != i->match_criteria.end(); j++)
      95             :     {
      96           0 :       assert(data::is_variable(j->second));
      97           0 :       substitution_map[data::variable(j->second)] = j->first;
      98             :     }
      99           0 :     data::map_substitution<std::map<data::variable, data::data_expression> > substitution(substitution_map);
     100             : 
     101           0 :     data::data_expression condition = data::replace_free_variables(i->condition, substitution);
     102           0 :     data::data_expression rhs = data::replace_free_variables(i->rhs, substitution);
     103             : 
     104           0 :     if (result == data::data_expression())
     105             :     {
     106           0 :       result = rhs;
     107             :     }
     108             :     else
     109             :     {
     110           0 :       result = data::if_(condition, rhs, result);
     111             :     }
     112             :   }
     113             : 
     114           0 :   return result;
     115             : }
     116             : 
     117             : /*
     118             :  * For a list of rules with equal left hand sides of match_criteria, construct a right hand side.
     119             :  */
     120           0 : static data::data_expression construct_rhs(data_specification *data_specification, const std::vector<rule>& rules, const data::sort_expression& sort)
     121             : {
     122           0 :   if (rules.empty())
     123             :   {
     124           0 :     return construct_condition_rhs(data_specification, rules, sort);
     125             :   }
     126             : 
     127             :   /*
     128             :    * For each matching rule LHS, check whether pattern matching needs to happen on that LHS.
     129             :    *
     130             :    * We prefer to match on an expression such that *all* rules perform matching on that expression.
     131             :    * For example, for a ruleset representing the following rewrite rules:
     132             :    *
     133             :    *   optionally_remove_first_element(false, l) = l
     134             :    *   optionally_remove_first_element(true, []) = []
     135             :    *   optionally_remove_first_element(true, x |> l) = l
     136             :    *
     137             :    * We prefer to pattern match on the first parameter, not the second. Pattern matching on the 
     138             :    * second parameter will (recursively) happen only on the true-branch, not the false-branch.
     139             :    * Pattern matching on the second parameter is still possible if there is no other option, but
     140             :    * it requires splitting the first rewrite rule into different cases for different 
     141             :    * constructors -- suboptimal.
     142             :    */
     143           0 :   data::data_expression matching_target;
     144             :   enum matching_type_t { MATCHING_NONE, MATCHING_INCOMPLETE, MATCHING_PARTIAL, MATCHING_FULL };
     145           0 :   matching_type_t matching_type = MATCHING_NONE;
     146           0 :   for (std::map<data::data_expression, data::data_expression>::const_iterator i = rules[0].match_criteria.begin(); i != rules[0].match_criteria.end(); i++)
     147             :   {
     148           0 :     bool variable_seen = false;
     149           0 :     std::set<data::function_symbol> constructors_seen;
     150           0 :     for (std::vector<rule>::const_iterator j = rules.begin(); j != rules.end(); j++)
     151             :     {
     152           0 :       data::data_expression pattern = j->match_criteria.at(i->first);
     153           0 :       if (data::is_variable(pattern))
     154             :       {
     155           0 :         variable_seen = true;
     156             :       }
     157           0 :       else if (data::is_function_symbol(pattern))
     158             :       {
     159           0 :         assert(data_specification->is_constructor(data::function_symbol(pattern)));
     160           0 :         constructors_seen.insert(data::function_symbol(pattern));
     161             :       }
     162           0 :       else if (data::is_application(pattern))
     163             :       {
     164           0 :         data::application application(pattern);
     165           0 :         assert(data::is_function_symbol(application.head()));
     166           0 :         assert(data_specification->is_constructor(data::function_symbol(application.head())));
     167           0 :         constructors_seen.insert(data::function_symbol(application.head()));
     168             :       }
     169             :       else
     170             :       {
     171           0 :         assert(false);
     172             :       }
     173             :     }
     174             : 
     175           0 :     if (constructors_seen.empty())
     176             :     {
     177             :       // No pattern matching is possible on this variable.
     178           0 :       continue;
     179             :     }
     180           0 :     else if (variable_seen)
     181             :     {
     182             :       // There are both rules that match on this variable and rules that do not.
     183             :       // That's better than an incomplete matching but worse than a full matching.
     184           0 :       if (matching_type == MATCHING_NONE || matching_type == MATCHING_INCOMPLETE)
     185             :       {
     186           0 :         matching_target = i->first;
     187           0 :         matching_type = MATCHING_PARTIAL;
     188             :       }
     189             :     }
     190           0 :     else if (constructors_seen.size() != data_specification->constructors(i->first.sort()).size())
     191             :     {
     192             :       // There are constructors for which there are no rules.
     193             :       // Thus, we have an incomplete function definition, that needs to be completed artificially.
     194             :       // A partial matching would be a better choice.
     195           0 :       if (matching_type == MATCHING_NONE)
     196             :       {
     197           0 :         matching_target = i->first;
     198           0 :         matching_type = MATCHING_INCOMPLETE;
     199             :       }
     200             :     }
     201             :     else
     202             :     {
     203             :       // There is a matching rule for each constructor, and no rule with a plain variable.
     204             :       // This variable is a perfect pattern matching candidate.
     205           0 :       matching_target = i->first;
     206           0 :       matching_type = MATCHING_FULL;
     207           0 :       break;
     208             :     }
     209             :   }
     210             : 
     211           0 :   if (matching_type == MATCHING_NONE)
     212             :   {
     213             :     // No constructor-based matching needs to happen. 
     214             :     // All that needs to happen is incorporating the rule conditions.
     215           0 :     return construct_condition_rhs(data_specification, rules, sort);
     216             :   }
     217             : 
     218             :   /*
     219             :    * For each constructor, find the set of rules that apply to it, rewritten to match the constructor.
     220             :    */
     221           0 :   std::map<data::function_symbol, std::vector<rule> > constructor_rules;
     222           0 :   for (std::vector<rule>::const_iterator i = rules.begin(); i != rules.end(); i++)
     223             :   {
     224           0 :     data::data_expression pattern = i->match_criteria.at(matching_target);
     225           0 :     if (data::is_function_symbol(pattern) || data::is_application(pattern))
     226             :     {
     227             :       /*
     228             :        * For a rule with a constructor pattern, strip the constructor and
     229             :        * introduce patterns for the constructor parameters.
     230             :        */
     231           0 :       data::function_symbol constructor;
     232           0 :       data::data_expression_vector parameters;
     233             : 
     234           0 :       if (data::is_function_symbol(pattern))
     235             :       {
     236           0 :         constructor = data::function_symbol(pattern);
     237             :       }
     238             :       else
     239             :       {
     240           0 :         data::application application(pattern);
     241           0 :         assert(data::is_function_symbol(application.head()));
     242           0 :         constructor = data::function_symbol(application.head());
     243           0 :         parameters.insert(parameters.end(), application.begin(), application.end());
     244             :       }
     245             : 
     246           0 :       assert(data_specification->constructors(matching_target.sort()).count(constructor) != 0);
     247           0 :       rule rule = *i;
     248           0 :       rule.match_criteria.erase(matching_target);
     249           0 :       for (std::size_t j = 0; j < parameters.size(); j++)
     250             :       {
     251           0 :         data::function_symbol projection_function = data_specification->projection_function(constructor, j);
     252           0 :         data::data_expression lhs_expression = data::application(projection_function, matching_target);
     253           0 :         rule.match_criteria[lhs_expression] = parameters[j];
     254             :       }
     255           0 :       constructor_rules[constructor].push_back(rule);
     256             :     }
     257             :     else
     258             :     {
     259             :       /*
     260             :        * For a rule with a variable pattern that nonetheless needs to pattern match
     261             :        * against the possible constructors for that variable, copy the rule for each
     262             :        * possible constructor. Substitute the original un-matched term for the pattern
     263             :        * variable that disappears.
     264             :        */
     265           0 :       assert(data::is_variable(pattern));
     266           0 :       data::data_expression condition = data::replace_free_variables(i->condition, data::variable_substitution(data::variable(pattern), matching_target));
     267           0 :       data::data_expression rhs = data::replace_free_variables(i->rhs, data::variable_substitution(data::variable(pattern), matching_target));
     268             : 
     269           0 :       const std::set<data::function_symbol>& constructors = data_specification->constructors(matching_target.sort());
     270           0 :       for (std::set<data::function_symbol>::const_iterator j = constructors.begin(); j != constructors.end(); j++)
     271             :       {
     272           0 :         rule rule;
     273           0 :         rule.condition = condition;
     274           0 :         rule.rhs = rhs;
     275           0 :         rule.variables = i->variables;
     276           0 :         rule.match_criteria = i->match_criteria;
     277           0 :         rule.match_criteria.erase(matching_target);
     278             : 
     279           0 :         data::set_identifier_generator generator;
     280           0 :         for (std::set<data::variable>::const_iterator k = i->variables.begin(); k != i->variables.end(); k++)
     281             :         {
     282           0 :           generator.add_identifier(k->name());
     283             :         }
     284             : 
     285           0 :         if (data::is_function_sort(j->sort()))
     286             :         {
     287           0 :           data::function_sort sort(j->sort());
     288           0 :           std::size_t index = 0;
     289           0 :           for (data::sort_expression_list::const_iterator k = sort.domain().begin(); k != sort.domain().end(); k++)
     290             :           {
     291           0 :             data::variable variable(generator("v"), *k);
     292           0 :             data::function_symbol projection_function = data_specification->projection_function(*j, index);
     293           0 :             data::data_expression lhs_expression = data::application(projection_function, matching_target);
     294           0 :             rule.match_criteria[lhs_expression] = variable;
     295           0 :             index++;
     296             :           }
     297             :         }
     298             : 
     299           0 :         constructor_rules[*j].push_back(rule);
     300             :       }
     301             :     }
     302             :   }
     303             : 
     304             :   /*
     305             :    * Construct an rhs of the form if(is_cons1, rhs_cons1, if(is_cons2, rhs_cons2, ...))
     306             :    */
     307           0 :   std::set<data::function_symbol>::const_iterator i = data_specification->constructors(matching_target.sort()).begin();
     308           0 :   data::data_expression result = construct_rhs(data_specification, constructor_rules[*i], sort);
     309           0 :   for (i++; i != data_specification->constructors(matching_target.sort()).end(); i++)
     310             :   {
     311           0 :     data::data_expression term = construct_rhs(data_specification, constructor_rules[*i], sort);
     312           0 :     data::function_symbol recogniser_function = data_specification->recogniser_function(*i);
     313           0 :     data::data_expression condition = data::application(recogniser_function, matching_target);
     314           0 :     result = data::if_(condition, term, result);
     315             :   }
     316           0 :   return result;
     317             : }
     318             : 
     319           0 : bool recursive_function_definition::is_pattern_matching_rule(data_specification *data_specification, const data::data_equation& rewrite_rule)
     320             : {
     321             :   /*
     322             :    * For this rewrite rule to be usable in pattern matching, its lhs must only contain
     323             :    * constructor functions and *fresh* variables.
     324             :    */
     325           0 :   std::set<data::data_expression> subexpressions = data::find_data_expressions(rewrite_rule.lhs());
     326           0 :   subexpressions.erase(rewrite_rule.lhs());
     327           0 :   if (data::is_application(rewrite_rule.lhs()))
     328             :   {
     329           0 :     subexpressions.erase(data::application(rewrite_rule.lhs()).head());
     330             :   }
     331             : 
     332           0 :   for (std::set<data::data_expression>::const_iterator i = subexpressions.begin(); i != subexpressions.end(); i++)
     333             :   {
     334           0 :     if (data::is_variable(*i))
     335             :     {
     336             :       // Fine.
     337             :     }
     338           0 :     else if (data::is_function_symbol(*i))
     339             :     {
     340           0 :       if (!data_specification->is_constructor(data::function_symbol(*i)))
     341             :       {
     342           0 :         return false;
     343             :       }
     344             :     }
     345           0 :     else if (data::is_application(*i))
     346             :     {
     347           0 :       data::application application(*i);
     348           0 :       if (!data::is_function_symbol(application.head()))
     349             :       {
     350           0 :         return false;
     351             :       }
     352           0 :       if (!data_specification->is_constructor(data::function_symbol(application.head())))
     353             :       {
     354           0 :         return false;
     355             :       }
     356             :     }
     357             :     else
     358             :     {
     359           0 :       return false;
     360             :     }
     361             :   }
     362             : 
     363           0 :   std::set<data::variable> variable_set;
     364           0 :   std::multiset<data::variable> variable_multiset;
     365           0 :   data::find_all_variables(rewrite_rule.lhs(), std::inserter(variable_set, variable_set.end()));
     366           0 :   data::find_all_variables(rewrite_rule.lhs(), std::inserter(variable_multiset, variable_multiset.end()));
     367           0 :   return variable_set.size() == variable_multiset.size();
     368             : }
     369             : 
     370           0 : recursive_function_definition::recursive_function_definition(data_specification *data_specification, data::function_symbol function, const data::data_equation_vector& rewrite_rules):
     371           0 :   named_function_definition(data_specification, function)
     372             : {
     373             :   /*
     374             :    * This converts a collection of rewrite rules for a give function symbol into a
     375             :    * one-rule specification of the function, using recogniser and projection functions
     376             :    * to implement pattern matching.
     377             :    *
     378             :    * For example, the collection of rewrite rules below:
     379             :    *
     380             :    *   sign_of_list_sum([]) = false;
     381             :    *   is_even(n) -> sign_of_list_sum(n |> l) = sign_of_list_sum(l);
     382             :    *   !is_even(n) -> sign_of_list_sum(n |> l) = !sign_of_list_sum(l);
     383             :    *
     384             :    * gets translated into the following function specification:
     385             :    *
     386             :    *   sign_of_list_sum(l) = if(is_emptylist(l), false,
     387             :    *                            if(is_even(head(l)), sign_of_list_sum(tail(l)),
     388             :    *                               !sign_of_list_sum(tail(l))))
     389             :    *
     390             :    * Two complications can arise. The rewrite rule set may contain rules that do not
     391             :    * pattern-match on the function parameters, such as 'not(not(b)) = b`; rules like
     392             :    * these are discarded.
     393             :    * More problematically, the set of rewrite rules may not be complete, or may not
     394             :    * easily be proven complete; in the example above, if the rewriter cannot rewrite
     395             :    * 'is_even(n) || !is_even(n)' to 'true', the translation cannot tell that the
     396             :    * rewrite rule set is complete.
     397             :    * In cases where a (non-constructor )function invocation can genuinely not be
     398             :    * rewritten any further, the MCRL2 semantics are unspecified (TODO check this);
     399             :    * the translation resolves this situation by returning an arbitrary value in this
     400             :    * case. Thus, in practice, the function definion above might well be translated
     401             :    * into the following:
     402             :    *
     403             :    *   sign_of_list_sum(l) = if(is_emptylist(l), false,
     404             :    *                            if(is_even(head(l)), sign_of_list_sum(tail(l)),
     405             :    *                               if(!is_even(head(l)), !sign_of_list_sum(tail(l)),
     406             :    *                                  false)))
     407             :    *
     408             :    * Where 'false' is a representative of sort_bool.
     409             :    */
     410             : 
     411           0 :   data::sort_expression codomain;
     412           0 :   if (data::is_function_sort(function.sort()))
     413             :   {
     414           0 :     data::function_sort sort(function.sort());
     415           0 :     codomain = sort.codomain();
     416           0 :     for (data::sort_expression_list::const_iterator i = sort.domain().begin(); i != sort.domain().end(); i++)
     417             :     {
     418           0 :       m_parameters.push_back(data::variable(data_specification->identifier_generator()("parameter"), *i));
     419             :     }
     420             :   }
     421             :   else
     422             :   {
     423           0 :     codomain = function.sort();
     424             :   }
     425             : 
     426           0 :   std::vector<rule> rules;
     427           0 :   for (data::data_equation_vector::const_iterator i = rewrite_rules.begin(); i != rewrite_rules.end(); i++)
     428             :   {
     429           0 :     assert(is_pattern_matching_rule(data_specification, *i));
     430             : 
     431           0 :     data::data_expression_vector arguments;
     432           0 :     if (data::is_application(i->lhs()))
     433             :     {
     434           0 :       data::application function_application(i->lhs());
     435           0 :       assert(function_application.head() == function);
     436           0 :       arguments.insert(arguments.end(), function_application.begin(), function_application.end());
     437             :     }
     438           0 :     assert(m_parameters.size() == arguments.size());
     439             : 
     440           0 :     rule rule;
     441           0 :     rule.rhs = i->rhs();
     442           0 :     rule.condition = i->condition();
     443           0 :     rule.variables.insert(i->variables().begin(), i->variables().end());
     444           0 :     for (std::size_t j = 0; j < arguments.size(); j++)
     445             :     {
     446           0 :       rule.match_criteria[m_parameters[j]] = arguments[j];
     447             :     }
     448           0 :     rules.push_back(rule);
     449             :   }
     450             : 
     451           0 :   assert(rules.size() != 0);
     452           0 :   m_rhs = construct_rhs(data_specification, rules, codomain);
     453           0 :   m_function_dependencies = data::find_function_symbols(m_rhs);
     454           0 :   m_function_dependencies.erase(function);
     455           0 : }
     456             : 
     457             : } // namespace smt
     458           0 : } // namespace mcrl2

Generated by: LCOV version 1.12