LCOV - code coverage report
Current view: top level - data/source/detail/rewrite - rewrite.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 153 229 66.8 %
Date: 2020-02-28 00:44:21 Functions: 21 26 80.8 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg
       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 "mcrl2/data/detail/rewrite/jitty.h"
      10             : #include "mcrl2/data/detail/rewrite/jitty_jittyc.h"
      11             : #ifdef MCRL2_JITTYC_AVAILABLE
      12             : #include "mcrl2/data/detail/rewrite/jittyc.h"
      13             : #endif
      14             : 
      15             : #include "mcrl2/data/detail/rewrite/with_prover.h"
      16             : 
      17             : #include "mcrl2/data/detail/rewriter_wrapper.h"
      18             : #include "mcrl2/data/enumerator_with_iterator.h"
      19             : 
      20             : using namespace mcrl2::core;
      21             : using namespace mcrl2::core::detail;
      22             : using namespace mcrl2::log;
      23             : 
      24             : namespace mcrl2
      25             : {
      26             : namespace data
      27             : {
      28             : namespace detail
      29             : {
      30             : 
      31         441 : static std::size_t npos()
      32             : {
      33         441 :   return std::size_t(-1);
      34             : }
      35             : 
      36             : #ifndef NDEBUG
      37             : // function object to test if it is an aterm_appl with function symbol "f"
      38             : struct is_a_variable
      39             : {
      40           0 :   bool operator()(const atermpp::aterm& t) const
      41             :   {
      42           0 :     return is_variable(atermpp::down_cast<atermpp::aterm_appl>(t));
      43             :   }
      44             : };
      45             : 
      46             : static
      47           0 : bool occur_check(const variable& v, const atermpp::aterm_appl& e)
      48             : {
      49           0 :   if (v==e)
      50             :   {
      51             :     // The variable is reset. This is ok.
      52           0 :     return true;
      53             :   }
      54           0 :   std::set<variable> s;
      55           0 :   find_all_if(e,is_a_variable(),std::inserter(s,s.begin()));
      56           0 :   if (s.count(v)>0)
      57             :   {
      58           0 :     return false; // Occur check failed.
      59             :   }
      60           0 :   return true;
      61             : }
      62             : #endif
      63             : 
      64          45 : data_expression Rewriter::rewrite_where(
      65             :                       const where_clause& term,
      66             :                       substitution_type& sigma)
      67             : {
      68          45 :   const assignment_list& assignments = term.assignments();
      69          45 :   const data_expression& body=term.body();
      70             : 
      71          90 :   mutable_map_substitution<std::map < variable,data_expression> > variable_renaming;
      72          90 :   for (const assignment& a: assignments)
      73             :   {
      74          45 :     const variable& v=a.lhs();
      75          90 :     const variable v_fresh(m_generator(), v.sort());
      76          45 :     variable_renaming[v]=v_fresh;
      77          45 :     sigma[v_fresh]=rewrite(a.rhs(),sigma);
      78             :   }
      79          45 :   const data_expression result=rewrite(replace_variables(body,variable_renaming),sigma);
      80             : 
      81             :   // Reset variables in sigma
      82          90 :   for (mutable_map_substitution<std::map < variable,data_expression> >::const_iterator it=variable_renaming.begin();
      83          90 :       it!=variable_renaming.end(); ++it)
      84             :   {
      85          45 :     sigma[atermpp::down_cast<variable>(it->second)]=it->second;
      86             :   }
      87          90 :   return result;
      88             : }
      89             : 
      90        3549 : abstraction Rewriter::rewrite_single_lambda(
      91             :                       const variable_list& vl,
      92             :                       const data_expression& body,
      93             :                       const bool body_in_normal_form,
      94             :                       substitution_type& sigma)
      95             : {
      96        3549 :   assert(vl.size()>0);
      97             :   // A lambda term without arguments; Take care that the bound variable is made unique with respect to
      98             :   // the variables occurring in sigma. But in case vl is empty, just rewrite...
      99             : 
     100             :   // First filter the variables in vl by those occuring as left/right hand sides in sigma.
     101             : 
     102        3549 :   std::size_t number_of_renamed_variables=0;
     103        3549 :   std::size_t count=0;
     104        7098 :   std::vector<variable> new_variables(vl.size());
     105             :   {
     106             :     // Create new unique variables to replace the old and create storage for
     107             :     // storing old values for variables in vl.
     108       10171 :     for(const variable& v: vl)
     109             :     {
     110        6622 :       if (sigma(v)!=v || sigma.variable_occurs_in_a_rhs(v))
     111             :       {
     112           0 :         number_of_renamed_variables++;
     113           0 :         new_variables[count]=data::variable(m_generator(), v.sort());
     114           0 :         assert(occur_check(v, new_variables[count]));
     115             :       }
     116             :       else
     117             :       {
     118        6622 :         new_variables[count]=v;
     119             :       }
     120        6622 :       count++;
     121             :     }
     122             :   }
     123             : 
     124        3549 :   if (number_of_renamed_variables==0)
     125             :   {
     126        3549 :     return abstraction(lambda_binder(),vl,(body_in_normal_form?body:rewrite(body,sigma)));
     127             :   }
     128             : 
     129           0 :   data_expression result;
     130           0 :   variable_list::const_iterator v;
     131           0 :   if (body_in_normal_form)
     132             :   {
     133             :     // If the body is already in normal form, a simple replacement of the old variables
     134             :     // by the new ones will do
     135           0 :     mutable_map_substitution<std::map<variable,data_expression> > variable_renaming;
     136           0 :     for(v = vl.begin(), count = 0; v != vl.end(); ++v, ++count)
     137             :     {
     138           0 :       if (*v != new_variables[count])
     139             :       {
     140           0 :         variable_renaming[*v] = new_variables[count];
     141             :       }
     142             :     }
     143           0 :     result = replace_variables(body, variable_renaming);
     144             :   }
     145             :   else
     146             :   {
     147             :     // If the body is not in normal form, then we have to rewrite with an updated sigma.
     148             :     // We first change sigma and save the values in sigma we overwrote...
     149           0 :     std::vector<data_expression> saved_substitutions;
     150           0 :     for(v = vl.begin(), count = 0; v != vl.end(); ++v, ++count)
     151             :     {
     152           0 :       if (*v != new_variables[count])
     153             :       {
     154           0 :         saved_substitutions.push_back(sigma(*v));
     155           0 :         sigma[*v] = new_variables[count];
     156             :       }
     157             :     }
     158             :     // ... then we rewrite with the new sigma ...
     159           0 :     result = rewrite(body,sigma);
     160             :     // ... and then we restore sigma to its old state.
     161           0 :     std::size_t new_variable_count = 0;
     162           0 :     for(v = vl.begin(), count = 0; v != vl.end(); ++v, ++count)
     163             :     {
     164           0 :       if (*v != new_variables[count])
     165             :       {
     166           0 :         sigma[*v] = saved_substitutions[new_variable_count++];
     167             :       }
     168             :     }
     169             :   }
     170           0 :   variable_list new_variable_list(new_variables.begin(), new_variables.end());
     171           0 :   return abstraction(lambda_binder(),new_variable_list,result);
     172             : }
     173             : 
     174             : 
     175             : // The function rewrite_lambda_application assumes that t has the shape
     176             : // application(...application(lambda x:D...., arg1,...,argn),argn+1,...,argN).
     177             : // It applies the lambda term to its arguments, and rewrites the result to
     178             : // normal form.
     179             : 
     180           0 : data_expression Rewriter::rewrite_lambda_application(
     181             :                       const data_expression& t,
     182             :                       substitution_type& sigma)
     183             : {
     184           0 :   if (is_lambda(t))
     185             :   {
     186           0 :     const abstraction& ta(t);
     187           0 :     return rewrite_single_lambda(ta.variables(),ta.body(),false,sigma);
     188             :   }
     189             : 
     190           0 :   const application ta(t);
     191           0 :   if (is_lambda(ta.head()))
     192             :   {
     193           0 :     return rewrite_lambda_application(ta.head(),ta,sigma);
     194             :   }
     195             : 
     196           0 :   return rewrite(application(rewrite_lambda_application(ta.head(),sigma),ta.begin(),ta.end()),sigma);
     197             : }
     198             : 
     199             : 
     200             : 
     201             : // The function rewrite_lambda_application rewrites a lambda term to a set of
     202             : // arguments which are the arguments 1,...,n of t. If t has the shape
     203             : // #REWR#(t0,t1,....,tn) and the lambda term is L, we calculate the normal form
     204             : // in internal format for L(t1,...,tn). Note that the term t0 is ignored.
     205             : // Note that we assume that neither L, nor t is in normal form.
     206             : 
     207        4732 : data_expression Rewriter::rewrite_lambda_application(
     208             :                       const abstraction& lambda_term,
     209             :                       const application& t,
     210             :                       substitution_type& sigma)
     211             : {
     212        4732 :   assert(is_lambda(lambda_term));  // The function symbol in this position cannot be anything else than a lambda term.
     213        4732 :   const variable_list& vl=lambda_term.variables();
     214        4732 :   const data_expression& lambda_body=lambda_term.body();
     215        4732 :   std::size_t arity=t.size();
     216        4732 :   if (arity==0) // The term has shape application(lambda d..:D...t), i.e. without arguments.
     217             :   {
     218           0 :     data_expression r= rewrite_single_lambda(vl, lambda_body, true, sigma);
     219           0 :     return r;
     220             :   }
     221        4732 :   assert(vl.size()<=arity);
     222             : 
     223             :   // The variable vl_backup will be used to first store the values to be substituted
     224             :   // for the variables in vl. Subsequently, it will be used to temporarily save the values in sigma
     225             :   // assigned to vl.
     226        4732 :   data_expression* vl_backup = MCRL2_SPECIFIC_STACK_ALLOCATOR(data_expression,vl.size());
     227             : 
     228             :   // Calculate the values that must be substituted for the variables in vl and store these in vl_backup.
     229       15609 :   for(std::size_t count=0; count<vl.size(); count++)
     230             :   {
     231       10877 :     new (&vl_backup[count]) data_expression(rewrite(data_expression(t[count]),sigma));
     232             :   }
     233             : 
     234             :   // Swap the values assigned to variables in vl with those in vl_backup.
     235        4732 :   std::size_t count=0;
     236       15609 :   for(const variable& v: vl)
     237             :   {
     238       21754 :     const data_expression temp=sigma(v);
     239       10877 :     sigma[v]=vl_backup[count];
     240       10877 :     vl_backup[count]=temp;
     241       10877 :     count++;
     242             :   }
     243             : 
     244        9464 :   const data_expression result=rewrite(lambda_body,sigma);
     245             : 
     246             :   // Reset variables in sigma and destroy the elements in vl_backup.
     247        4732 :   count=0;
     248       15609 :   for(const variable& v: vl)
     249             :   {
     250       10877 :     sigma[v]=vl_backup[count];
     251       10877 :     vl_backup[count].~data_expression();
     252       10877 :     count++;
     253             :   }
     254             : 
     255        4732 :   if (vl.size()==arity)
     256             :   {
     257        4732 :     return result;
     258             :   }
     259             : 
     260             :   // There are more arguments than bound variables.
     261             :   // Rewrite the remaining arguments and apply the rewritten lambda term to them.
     262           0 :   return application(result,
     263           0 :                      t.begin()+vl.size(),
     264           0 :                      t.end(),
     265           0 :                      [this, &sigma](const data_expression& t) -> data_expression { return rewrite(t, sigma); });
     266             : }
     267             : 
     268          95 : data_expression Rewriter::existential_quantifier_enumeration(
     269             :      const abstraction& t,
     270             :      substitution_type& sigma)
     271             : {
     272             :   // This is a quantifier elimination that works on the existential quantifier as specified
     273             :   // in data types, i.e. without applying the implement function anymore.
     274             : 
     275          95 :   assert(is_exists(t));
     276          95 :   return existential_quantifier_enumeration(t.variables(), t.body(), false, sigma);
     277             : }
     278             : 
     279             : // Generate a term equivalent to exists vl.t1.
     280             : // The variable t1_is_normal_form indicates whether t1 is in normal
     281             : // form, but this information is not used as it stands.
     282          95 : data_expression Rewriter::existential_quantifier_enumeration(
     283             :       const variable_list& vl,
     284             :       const data_expression& t1,
     285             :       const bool t1_is_normal_form,
     286             :       substitution_type& sigma)
     287             : {
     288          95 :   return quantifier_enumeration(vl, t1, t1_is_normal_form, sigma, exists_binder(), &lazy::or_, sort_bool::false_(), sort_bool::true_());
     289             : }
     290             : 
     291             : 
     292         846 : data_expression Rewriter::universal_quantifier_enumeration(
     293             :      const abstraction& t,
     294             :      substitution_type& sigma)
     295             : {
     296         846 :   assert(is_forall(t));
     297         846 :   return universal_quantifier_enumeration(t.variables(),t.body(),false,sigma);
     298             : }
     299             : 
     300             : // Generate a term equivalent to forall vl.t1.
     301             : // The variable t1_is_normal_form indicates whether t1 is in normal
     302             : // form, but this information is not used as it stands.
     303         846 : data_expression Rewriter::universal_quantifier_enumeration(
     304             :       const variable_list& vl,
     305             :       const data_expression& t1,
     306             :       const bool t1_is_normal_form,
     307             :       substitution_type& sigma)
     308             : {
     309         846 :   return quantifier_enumeration(vl, t1, t1_is_normal_form, sigma, forall_binder(), &lazy::and_, sort_bool::true_(), sort_bool::false_());
     310             : }
     311             : 
     312         941 : data_expression Rewriter::quantifier_enumeration(
     313             :       const variable_list& vl,
     314             :       const data_expression& t1,
     315             :       const bool t1_is_normal_form,
     316             :       substitution_type& sigma,
     317             :       const binder_type& binder,
     318             :       data_expression (*lazy_op)(const data_expression&, const data_expression&),
     319             :       const data_expression& identity_element,
     320             :       const data_expression& absorbing_element
     321             :     )
     322             : {
     323             :   // Rename the bound variables to unique
     324             :   // variables, to avoid naming conflicts.
     325             : 
     326        1882 :   mutable_map_substitution<std::map < variable,data_expression> > variable_renaming;
     327        1882 :   variable_vector vl_new_v;
     328        1895 :   for(const variable& v: vl)
     329             :   {
     330         954 :     if (sigma(v)!=v)
     331             :     {
     332           0 :       const variable v_fresh(m_generator(), v.sort());
     333           0 :       variable_renaming[v]=v_fresh;
     334           0 :       vl_new_v.push_back(v_fresh);
     335             :     }
     336             :     else
     337             :     {
     338         954 :       vl_new_v.push_back(v);
     339             :     }
     340             :   }
     341             : 
     342        1882 :   const data_expression t2=replace_variables(t1,variable_renaming);
     343        1882 :   const data_expression t3=(t1_is_normal_form?t2:rewrite(t2,sigma));
     344             : 
     345             :   // Check whether the bound variables occur free in the rewritten body
     346        1882 :   std::set < variable > free_variables=find_free_variables(t3);
     347        1882 :   variable_list vl_new_l_enum;
     348        1882 :   variable_list vl_new_l_other;
     349             : 
     350         941 :   bool sorts_are_finite=true;
     351        1895 :   for(variable_vector::const_reverse_iterator i=vl_new_v.rbegin(); i!=vl_new_v.rend(); ++i)
     352             :   {
     353        1908 :     const variable v = *i;
     354         954 :     if (free_variables.count(v)>0)
     355             :     {
     356         535 :       if(is_enumerable(m_data_specification_for_enumeration, rewriter_wrapper(this), v.sort()))
     357             :       {
     358         531 :         vl_new_l_enum.push_front(v);
     359         531 :         sorts_are_finite = sorts_are_finite && m_data_specification_for_enumeration.is_certainly_finite(v.sort());
     360             :       }
     361             :       else
     362             :       {
     363           4 :         vl_new_l_other.push_front(v);
     364             :       }
     365             :     }
     366             :   }
     367             : 
     368         941 :   if (vl_new_l_enum.empty())
     369             :   {
     370         418 :     if(vl_new_l_other.empty())
     371             :     {
     372         415 :       return t3; // No quantified variables are bound.
     373             :     }
     374             :     else
     375             :     {
     376           3 :       return abstraction(binder, vl_new_l_other, t3);
     377             :     }
     378             :   }
     379             : 
     380             :   /* Find A solution*/
     381         523 :   rewriter_wrapper wrapped_rewriter(this);
     382         523 :   const std::size_t max_count = sorts_are_finite ? std::numeric_limits<std::size_t>::max() : data::detail::get_enumerator_iteration_limit();
     383             : 
     384       19467 :   struct is_not
     385             :   {
     386             :     data_expression m_expr;
     387         523 :     is_not(const data_expression& expr)
     388         523 :     : m_expr(expr)
     389         523 :     {}
     390             : 
     391        4984 :     bool operator()(const data_expression& expr)
     392             :     {
     393        4984 :       return expr != m_expr;
     394             :     }
     395             :   };
     396             : 
     397             :   typedef enumerator_algorithm_with_iterator<rewriter_wrapper,
     398             :                                              enumerator_list_element<>,
     399             :                                              is_not,
     400             :                                              rewriter_wrapper,
     401             :                                              rewriter_wrapper::substitution_type> enumerator_type;
     402             :   try
     403             :   {
     404             :     enumerator_type enumerator(wrapped_rewriter, m_data_specification_for_enumeration,
     405         588 :       wrapped_rewriter, m_generator, max_count, true, is_not(identity_element));
     406             : 
     407             :     /* Create a list to store solutions */
     408         588 :     data_expression partial_result = identity_element;
     409             : 
     410         523 :     std::size_t loop_upperbound = (sorts_are_finite ? npos() : 10);
     411         588 :     data::enumerator_queue<enumerator_list_element<> > enumerator_solution_deque(enumerator_list_element<>(vl_new_l_enum, t3));
     412             : 
     413         588 :     enumerator_type::iterator sol = enumerator.begin(sigma, enumerator_solution_deque);
     414        2991 :     for( ; loop_upperbound > 0 &&
     415        1128 :            sol != enumerator.end();
     416             :            ++sol)
     417             :     {
     418        1095 :       partial_result = lazy_op(partial_result, sol->expression());
     419        1095 :       loop_upperbound--;
     420        1095 :       if(partial_result == absorbing_element)
     421             :       {
     422             :         // We found a solution, so prevent the enumerator from doing any unnecessary work
     423             :         // Also prevents any further exceptions from the enumerator
     424         425 :         return absorbing_element;
     425             :       }
     426             :     }
     427             : 
     428          98 :     if (sol == enumerator.end())
     429             :     {
     430          33 :       if(vl_new_l_other.empty())
     431             :       {
     432          32 :         return partial_result;
     433             :       }
     434             :       else
     435             :       {
     436           1 :         return abstraction(binder, vl_new_l_other, partial_result);
     437             :       }
     438             :     }
     439             :     // One can consider to replace the variables by their original, in order to not show
     440             :     // internally generated variables in the output.
     441          65 :     assert(!sol->is_valid() || loop_upperbound == 0);
     442             :   }
     443           0 :   catch(const mcrl2::runtime_error&)
     444             :   {
     445             :     // It is not possible to enumerate one of the bound variables, so we just return
     446             :     // the simplified expression
     447             :   }
     448             : 
     449          65 :   return abstraction(binder,vl_new_l_enum+vl_new_l_other,rewrite(t3,sigma));
     450             : }
     451             : 
     452             : 
     453        1920 : std::shared_ptr<Rewriter> createRewriter(
     454             :             const data_specification& data_spec,
     455             :             const used_data_equation_selector& equations_selector,
     456             :             const rewrite_strategy strategy)
     457             : {
     458        1920 :   switch (strategy)
     459             :   {
     460        1916 :     case jitty:
     461        1916 :       return std::shared_ptr<Rewriter>(new RewriterJitty(data_spec,equations_selector));
     462             : #ifdef MCRL2_JITTYC_AVAILABLE
     463           4 :     case jitty_compiling:
     464           4 :       return std::shared_ptr<Rewriter>(new RewriterCompilingJitty(data_spec,equations_selector));
     465             : #endif
     466           0 :     case jitty_prover:
     467           0 :       return std::shared_ptr<Rewriter>(new RewriterProver(data_spec,jitty,equations_selector));
     468             : #ifdef MCRL2_JITTYC_AVAILABLE
     469           0 :     case jitty_compiling_prover:
     470           0 :       return std::shared_ptr<Rewriter>(new RewriterProver(data_spec,jitty_compiling,equations_selector));
     471             : #endif
     472           0 :     default: throw mcrl2::runtime_error("Cannot create a rewriter using strategy " + pp(strategy) + ".");
     473             :   }
     474             : }
     475             : 
     476             : //Prototype
     477             : static void check_vars(const data_expression& expr, const std::set <variable>& vars, std::set <variable>& used_vars);
     478             : 
     479     4317815 : static void check_vars(application::const_iterator begin,
     480             :                        const application::const_iterator& end,
     481             :                        const std::set <variable>& vars,
     482             :                        std::set <variable>& used_vars)
     483             : {
     484     7084160 :   while (begin != end)
     485             :   {
     486     2766345 :     check_vars(*begin++, vars, used_vars);
     487             :   }
     488     1551470 : }
     489             : 
     490     5907083 : static void check_vars(const data_expression& expr, const std::set <variable>& vars, std::set <variable>& used_vars)
     491             : {
     492     5907083 :   if (is_application(expr))
     493             :   {
     494     1551470 :     const application& a=atermpp::down_cast<application>(expr);
     495     1551470 :     check_vars(a.head(),vars,used_vars);
     496     1551470 :     check_vars(a.begin(),a.end(),vars,used_vars);
     497             :   }
     498     4355613 :   else if (is_variable(expr))
     499             :   {
     500     1784792 :     const variable& v=atermpp::down_cast<variable>(expr);
     501     1784792 :     used_vars.insert(v);
     502             : 
     503     1784792 :     if (vars.count(v)==0)
     504             :     {
     505           0 :       throw v;
     506             :     }
     507             :   }
     508     5907083 : }
     509             : 
     510             : //Prototype
     511             : static void checkPattern(const data_expression& p);
     512             : 
     513     2414719 : static void checkPattern(application::const_iterator begin,
     514             :                          const application::const_iterator& end)
     515             : {
     516     3984077 :   while (begin != end)
     517             :   {
     518     1569358 :     checkPattern(*begin++);
     519             :   }
     520      845361 : }
     521             : 
     522     2944475 : static void checkPattern(const data_expression& p)
     523             : {
     524     2944475 :   if (is_application(p))
     525             :   {
     526      845361 :     if (is_variable(atermpp::down_cast<application>(p).head()))
     527             :     {
     528           0 :       throw mcrl2::runtime_error(std::string("variable ") + data::pp(application(p).head()) +
     529           0 :                " is used as head symbol in an application, which is not supported");
     530             :     }
     531      845361 :     const application& a=atermpp::down_cast<application>(p);
     532      845361 :     checkPattern(a.head());
     533      845361 :     checkPattern(a.begin(),a.end());
     534             :   }
     535     2944475 : }
     536             : 
     537      529756 : void CheckRewriteRule(const data_equation& data_eqn)
     538             : {
     539      529756 :   const variable_list& rule_var_list = data_eqn.variables();
     540     1059512 :   const std::set <variable> rule_vars(rule_var_list.begin(),rule_var_list.end());
     541             : 
     542             :   // collect variables from lhs and check that they are in rule_vars
     543     1059512 :   std::set <variable> lhs_vars;
     544             :   try
     545             :   {
     546      529756 :     check_vars(data_eqn.lhs(),rule_vars,lhs_vars);
     547             :   }
     548           0 :   catch (variable& var)
     549             :   {
     550             :     // This should never occur if data_eqn is a valid data equation
     551           0 :     mCRL2log(log::error) << "Data equation: " << data_expression(data_eqn) << std::endl;
     552           0 :     assert(0);
     553             :     throw runtime_error("variable " + pp(var) + " occurs in left-hand side of equation but is not defined (in equation: " + pp(data_eqn) + ")");
     554             :   }
     555             : 
     556             :   // check that variables from the condition occur in the lhs
     557             :   try
     558             :   {
     559     1059512 :     std::set <variable> dummy;
     560      529756 :     check_vars(data_eqn.condition(),lhs_vars,dummy);
     561             :   }
     562           0 :   catch (variable& var)
     563             :   {
     564           0 :     throw runtime_error("variable " + pp(var) + " occurs in condition of equation but not in left-hand side (in equation: " +
     565           0 :                     pp(data_eqn) + "); equation cannot be used as rewrite rule");
     566             :   }
     567             : 
     568             :   // check that variables from the rhs are occur in the lhs
     569             :   try
     570             :   {
     571     1059512 :     std::set <variable> dummy;
     572      529756 :     check_vars(data_eqn.rhs(),lhs_vars,dummy);
     573             :   }
     574           0 :   catch (variable& var)
     575             :   {
     576           0 :     throw runtime_error("variable " + pp(var) + " occurs in right-hand side of equation but not in left-hand side (in equation: " +
     577           0 :                 pp(data_eqn) + "); equation cannot be used as rewrite rule");
     578             :   }
     579             : 
     580             :   // check that the lhs is a supported pattern
     581      529756 :   if (is_variable(data_eqn.lhs()))
     582             :   {
     583           0 :     throw runtime_error("left-hand side of equation is a variable; this is not allowed for rewriting");
     584             :   }
     585             :   try
     586             :   {
     587      529756 :     checkPattern(data_eqn.lhs());
     588             :   }
     589           0 :   catch (mcrl2::runtime_error& s)
     590             :   {
     591           0 :     throw runtime_error(std::string(s.what()) + " (in equation: " + pp(data_eqn) + "); equation cannot be used as rewrite rule");
     592             :   }
     593      529756 : }
     594             : 
     595           0 : bool isValidRewriteRule(const data_equation& data_eqn)
     596             : {
     597             :   try
     598             :   {
     599           0 :     CheckRewriteRule(data_eqn);
     600           0 :     return true;
     601             :   }
     602           0 :   catch (runtime_error&)
     603             :   {
     604           0 :     return false;
     605             :   }
     606             :   return false; // compiler warning
     607             : }
     608             : 
     609             : }
     610             : }
     611         366 : }

Generated by: LCOV version 1.13