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