mCRL2
Loading...
Searching...
No Matches
match_tree.h
Go to the documentation of this file.
1// Author(s): Muck van Weerdenburg/Jan Friso Groote
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//
10
11#ifndef MCRL2_DATA_MATCH_TREE_H
12#define MCRL2_DATA_MATCH_TREE_H
13
16
17namespace mcrl2
18{
19namespace data
20{
21namespace detail
22{
23
26{
27 public:
30 {}
31
34 atermpp::aterm(v)
35 {
36 assert(is_variable(v) || v.type_is_int());
37 }
38};
39
41
43{
44 public:
47 : atermpp::aterm_appl(afunUndefined())
48 {}
49
52 atermpp::aterm_appl(t)
53 {
54 assert(!is_defined() || isS() || isA() || isM() || isF() ||
55 isN() || isD() || isR () || isC() || isX() || isRe() ||
56 isCRe() || isMe());
57 }
58
59 protected:
61 {
62 static atermpp::function_symbol afunUndefined("@@Match_tree_dummy",0); // Undefined match term. Used as default match term
63 return afunUndefined;
64 }
65
67 {
68 static atermpp::function_symbol afunS("@@S",2); // Store term ( target_variable, result_tree )
69 return afunS;
70 }
71
73 {
74 static atermpp::function_symbol afunA("@@A",1); // Rewrite argument ( number of an argument as an aterm_int )
75 return afunA;
76 }
77
78
80 {
81 static atermpp::function_symbol afunM("@@M",3); // Match term ( match_variable, true_tree , false_tree )
82 return afunM;
83 }
84
86 {
87 static atermpp::function_symbol afunF("@@F",3); // Match function ( match_function, true_tree, false_tree )
88 return afunF;
89 }
90
92 {
93 static atermpp::function_symbol afunN("@@N",1); // Go to next parameter ( result_tree )
94 return afunN;
95 }
96
98 {
99 static atermpp::function_symbol afunD("@@D",1); // Go down a level ( result_tree )
100 return afunD;
101 }
102
104 {
105 static atermpp::function_symbol afunR("@@R",1); // End of tree ( matching_rule )
106 return afunR;
107 }
108
110 {
111 static atermpp::function_symbol afunC("@@C",3); // Check condition ( condition, true_tree, false_tree )
112 return afunC;
113 }
114
116 {
117 static atermpp::function_symbol afunX("@@X",0); // End of tree
118 return afunX;
119 }
120
122 {
123 static atermpp::function_symbol afunRe("@@Re",2); // End of tree ( matching_rule , vars_of_rule)
124 return afunRe;
125 }
126
128 {
129 static atermpp::function_symbol afunCRe("@@CRe",4); // End of tree ( condition, matching_rule, vars_of_condition, vars_of_rule )
130 return afunCRe;
131 }
132
134 {
135 static atermpp::function_symbol afunMe("@@Me",2); // Match term ( match_variable, variable_index )
136 return afunMe;
137 }
138
139 public:
140 bool is_defined() const
141 {
142 return this->function()!=afunUndefined();
143 }
144
145 bool isS() const
146 {
147 return this->function()==afunS();
148 }
149
150 bool isA() const
151 {
152 return this->function()==afunA();
153 }
154
155 bool isM() const
156 {
157 return this->function()==afunM();
158 }
159
160 bool isF() const
161 {
162 return this->function()==afunF();
163 }
164
165 bool isN() const
166 {
167 return this->function()==afunN();
168 }
169
170 bool isD() const
171 {
172 return this->function()==afunD();
173 }
174
175 bool isR() const
176 {
177 return this->function()==afunR();
178 }
179
180 bool isC() const
181 {
182 return this->function()==afunC();
183 }
184
185 bool isX() const
186 {
187 return this->function()==afunX();
188 }
189
190 bool isRe() const
191 {
192 return this->function()==afunRe();
193 }
194
195 bool isCRe() const
196 {
197 return this->function()==afunCRe();
198 }
199
200 bool isMe() const
201 {
202 return this->function()==afunMe();
203 }
204};
205
206// Store term ( target_variable, result_tree )
208{
209 public:
211 {}
212
214 : match_tree(t)
215 {
216 assert(isS());
217 }
218
220 : match_tree(atermpp::aterm_appl(afunS(),target_variable,result_tree))
221 {}
222
224 {
225 return atermpp::down_cast<const variable>((*this)[0]);
226 }
227
228 const match_tree& subtree() const
229 {
230 return atermpp::down_cast<const match_tree>((*this)[1]);
231 }
232};
233
234// Rewrite argument ( a number of an arguments as a aterm_int )
235
237{
238 public:
240 {}
241
243 : match_tree(t)
244 {
245 assert(isA());
246 }
247
248 match_tree_A(const std::size_t n)
249 : match_tree(atermpp::aterm_appl(afunA(),atermpp::aterm_int(n)))
250 {}
251
252 std::size_t variable_index() const
253 {
254 return atermpp::down_cast<const atermpp::aterm_int>((*this)[0]).value();
255 }
256};
257
258
259// Match term ( match_variable, true_tree , false_tree )
261{
262 public:
264 {}
265
267 : match_tree(t)
268 {
269 assert(isM());
270 }
271
274 {}
275
277 {
278 return atermpp::down_cast<const variable>((*this)[0]);
279 }
280
281 const match_tree& true_tree() const
282 {
283 return atermpp::down_cast<const match_tree>((*this)[1]);
284 }
285
286 const match_tree& false_tree() const
287 {
288 return atermpp::down_cast<const match_tree>((*this)[2]);
289 }
290};
291
292// Match function ( match_function, true_tree, false_tree )
294{
295 public:
297 {}
298
300 : match_tree(t)
301 {
302 assert(isF());
303 }
304
307 {}
308
310 {
311 return atermpp::down_cast<const data::function_symbol>((*this)[0]);
312 }
313
314 const match_tree& true_tree() const
315 {
316 return atermpp::down_cast<const match_tree>((*this)[1]);
317 }
318
319 const match_tree& false_tree() const
320 {
321 return atermpp::down_cast<const match_tree>((*this)[2]);
322 }
323};
324
325// Go to next parameter ( result_tree )
327{
328 public:
330 {}
331
333 : match_tree(t)
334 {
335 assert(isN());
336 }
337
341 match_tree_N(const match_tree& result_tree, std::size_t)
342 : match_tree(atermpp::aterm_appl(afunN(),result_tree))
343 {}
344
345 const match_tree& subtree() const
346 {
347 return atermpp::down_cast<const match_tree>((*this)[0]);
348 }
349};
350
351// Go down a level ( result_tree )
353{
354 public:
356 {}
357
359 : match_tree(t)
360 {
361 assert(isD());
362 }
363
367 match_tree_D(const match_tree& result_tree, std::size_t)
368 : match_tree(atermpp::aterm_appl(afunD(),result_tree))
369 {}
370
371 const match_tree& subtree() const
372 {
373 return atermpp::down_cast<const match_tree>((*this)[0]);
374 }
375};
376
377// End of tree ( matching_rule )
379{
380
381 public:
383 {}
384
386 : match_tree(t)
387 {
388 assert(isR());
389 }
390
392 : match_tree(atermpp::aterm_appl(afunR(),e))
393 {}
394
395 const data_expression& result() const
396 {
397 return atermpp::down_cast<const data_expression>((*this)[0]);
398 }
399};
400
401// Check condition ( condition, true_tree, false_tree )
403{
404 public:
406 {}
407
409 : match_tree(t)
410 {
411 assert(isC());
412 }
413
416 {}
417
419 {
420 return atermpp::down_cast<const data_expression>((*this)[0]);
421 }
422
423 const match_tree& true_tree() const
424 {
425 return atermpp::down_cast<const match_tree>((*this)[1]);
426 }
427
428 const match_tree& false_tree() const
429 {
430 return atermpp::down_cast<const match_tree>((*this)[2]);
431 }
432};
433
434// End of tree
436{
437 public:
439 : match_tree(t)
440 {
441 assert(isX());
442 }
443
445 : match_tree(atermpp::aterm_appl(afunX()))
446 {}
447};
448
449// End of tree ( matching_rule , vars_of_rule)
450// The var_of_rule is a list with variables and aterm_ints.
452{
453 public:
455 {}
456
458 : match_tree(t)
459 {
460 assert(isRe());
461 }
462
464 : match_tree(atermpp::aterm_appl(afunRe(),result,vars))
465 {}
466
467 const data_expression& result() const
468 {
469 return atermpp::down_cast<const data_expression>((*this)[0]);
470 }
471
473 {
474 return atermpp::down_cast<const variable_or_number_list>((*this)[1]);
475 }
476};
477
478// End of tree ( condition, matching_rule, vars_of_condition, vars_of_rule )
479// The last two parameters consist of a list with variables and numbers.
481{
482 public:
484 {}
485
487 : match_tree(t)
488 {
489 assert(isCRe());
490 }
491
493 : match_tree(atermpp::aterm_appl(afunCRe(),condition,result,vars_condition,vars_rule))
494 {}
495
497 {
498 return atermpp::down_cast<const data_expression>((*this)[0]);
499 }
500
501 const data_expression& result() const
502 {
503 return atermpp::down_cast<const data_expression>((*this)[1]);
504 }
505
507 {
508 return atermpp::down_cast<const variable_or_number_list>((*this)[2]);
509 }
510
512 {
513 return atermpp::down_cast<const variable_or_number_list>((*this)[3]);
514 }
515};
516
517// Match term ( match_variable, variable_index )
519{
520 public:
522 {}
523
525 : match_tree(t)
526 {
527 assert(isMe());
528 }
529
531 : match_tree(atermpp::aterm_appl(afunMe(),match_variable,atermpp::aterm_int(variable_index)))
532 {}
533
535 {
536 return atermpp::down_cast<const variable>((*this)[0]);
537 }
538
539 std::size_t variable_index() const
540 {
541 return (atermpp::down_cast<const atermpp::aterm_int>((*this)[1])).value();
542 }
543};
544
545typedef atermpp::term_list < match_tree > match_tree_list;
546typedef std::vector < match_tree > match_tree_vector;
547typedef atermpp::term_list < match_tree_list > match_tree_list_list;
548typedef atermpp::term_list < match_tree_list_list > match_tree_list_list_list;
549
550// Structure for build_tree parameters
552{
553public:
554 match_tree_list_list Flist; // List of sequences of which the first action is an F
555 match_tree_list_list Slist; // List of sequences of which the first action is an S
556 match_tree_list_list Mlist; // List of sequences of which the first action is an M
557 match_tree_list_list_list stack; // Stack to maintain the sequences that do not have to
558 // do anything in the current term
559 match_tree_list_list upstack; // List of sequences that have done an F at the current
560 // level
561
562 // Initialise.
564 : Flist(),
565 Slist(),
566 Mlist(),
568 upstack()
569
570 {
571 }
572};
573
574
575inline
576std::ostream& operator<<(std::ostream& s, const match_tree& t)
577{
578 using atermpp::down_cast;
579 if (t.isS())
580 {
581 const match_tree_S& tS = down_cast<match_tree_S>(t);
582 s << "@@S(" << tS.target_variable() << ", " << tS.subtree() << ")";
583 }
584 else
585 if (t.isA())
586 {
587 const match_tree_A& tA = down_cast<match_tree_A>(t);
588 s << "@@A(" << tA.variable_index() << ")";
589 }
590 else
591 if (t.isM())
592 {
593 const match_tree_M& tM = down_cast<match_tree_M>(t);
594 s << "@@M(" << tM.match_variable() << ", " << tM.true_tree() << ", " << tM.false_tree() << ")";
595 }
596 else
597 if (t.isF())
598 {
599 const match_tree_F& tF = down_cast<match_tree_F>(t);
600 s << "@@F(" << tF.function() << ", " << tF.true_tree() << ", " << tF.false_tree() << ")";
601 }
602 else
603 if (t.isN())
604 {
605 const match_tree_N& tN = down_cast<match_tree_N>(t);
606 s << "@@N(" << tN.subtree() << ")";
607 }
608 else
609 if (t.isD())
610 {
611 const match_tree_D& tD = down_cast<match_tree_D>(t);
612 s << "@@D(" << tD.subtree() << ")";
613 }
614 else
615 if (t.isR())
616 {
617 const match_tree_R& tR = down_cast<match_tree_R>(t);
618 s << "@@R(" << tR.result() << ")";
619 }
620 else
621 if (t.isC())
622 {
623 const match_tree_C& tC = down_cast<match_tree_C>(t);
624 s << "@@C(" << tC.condition() << ", " << tC.true_tree() << ", " << tC.false_tree() << ")";
625 }
626 else
627 if (t.isX())
628 {
629 s << "@@X";
630 }
631 else
632 if (t.isRe())
633 {
634 const match_tree_Re& tRe = down_cast<match_tree_Re>(t);
635 s << "@@Re(" << tRe.result() << ", " << tRe.variables() << ")";
636 }
637 else
638 if (t.isCRe())
639 {
640 const match_tree_CRe& tCRe = down_cast<match_tree_CRe>(t);
641 s << "@@CRe(" << tCRe.condition() << ", " << tCRe.result() << ", "
642 << tCRe.variables_condition() << ", " << tCRe.variables_result() << ")";
643 }
644 else
645 if (t.isMe())
646 {
647 const match_tree_Me& tMe = down_cast<match_tree_Me>(t);
648 s << "@@Me(" << tMe.match_variable() << ", " << tMe.variable_index() << ")";
649 }
650 return s;
651}
652
653} // namespace detail
654
655} // namespace data
656
657} // namespace mcrl2
658
659#endif // MCRL2_DATA_MATCH_TREE_H
The aterm base class that provides protection of the underlying shared terms.
Definition aterm.h:186
aterm() noexcept
Default constructor.
const function_symbol & function() const
Returns the function symbol belonging to an aterm_appl.
Definition aterm_appl.h:174
A list of aterm objects.
Definition aterm_list.h:23
bool type_is_int() const noexcept
Dynamic check whether the term is an aterm_int.
Definition aterm.h:67
match_tree_list_list Slist
Definition match_tree.h:555
match_tree_list_list upstack
Definition match_tree.h:559
match_tree_list_list Flist
Definition match_tree.h:554
match_tree_list_list Mlist
Definition match_tree.h:556
match_tree_list_list_list stack
Definition match_tree.h:557
std::size_t variable_index() const
Definition match_tree.h:252
match_tree_A(const std::size_t n)
Definition match_tree.h:248
match_tree_A(const atermpp::aterm &t)
Definition match_tree.h:242
match_tree_CRe(const data_expression &condition, const data_expression &result, const variable_or_number_list &vars_condition, const variable_or_number_list &vars_rule)
Definition match_tree.h:492
match_tree_CRe(const atermpp::aterm &t)
Definition match_tree.h:486
const variable_or_number_list & variables_condition() const
Definition match_tree.h:506
const data_expression & condition() const
Definition match_tree.h:496
const data_expression & result() const
Definition match_tree.h:501
const variable_or_number_list & variables_result() const
Definition match_tree.h:511
const data_expression & condition() const
Definition match_tree.h:418
match_tree_C(const atermpp::aterm &t)
Definition match_tree.h:408
const match_tree & false_tree() const
Definition match_tree.h:428
match_tree_C(const data_expression &condition, const match_tree &true_tree, const match_tree &false_tree)
Definition match_tree.h:414
const match_tree & true_tree() const
Definition match_tree.h:423
match_tree_D(const atermpp::aterm &t)
Definition match_tree.h:358
const match_tree & subtree() const
Definition match_tree.h:371
match_tree_D(const match_tree &result_tree, std::size_t)
Definition match_tree.h:367
match_tree_F(const data::function_symbol &function, const match_tree &true_tree, const match_tree &false_tree)
Definition match_tree.h:305
const data::function_symbol & function() const
Definition match_tree.h:309
const match_tree & false_tree() const
Definition match_tree.h:319
const match_tree & true_tree() const
Definition match_tree.h:314
match_tree_F(const atermpp::aterm &t)
Definition match_tree.h:299
const match_tree & false_tree() const
Definition match_tree.h:286
const match_tree & true_tree() const
Definition match_tree.h:281
const variable & match_variable() const
Definition match_tree.h:276
match_tree_M(const atermpp::aterm &t)
Definition match_tree.h:266
match_tree_M(const variable &match_variable, const match_tree &true_tree, const match_tree &false_tree)
Definition match_tree.h:272
const variable & match_variable() const
Definition match_tree.h:534
match_tree_Me(const variable &match_variable, const std::size_t variable_index)
Definition match_tree.h:530
std::size_t variable_index() const
Definition match_tree.h:539
match_tree_Me(const atermpp::aterm &t)
Definition match_tree.h:524
match_tree_N(const atermpp::aterm &t)
Definition match_tree.h:332
const match_tree & subtree() const
Definition match_tree.h:345
match_tree_N(const match_tree &result_tree, std::size_t)
Definition match_tree.h:341
match_tree_R(const atermpp::aterm &t)
Definition match_tree.h:385
const data_expression & result() const
Definition match_tree.h:395
match_tree_R(const data_expression &e)
Definition match_tree.h:391
match_tree_Re(const data_expression &result, const variable_or_number_list &vars)
Definition match_tree.h:463
match_tree_Re(const atermpp::aterm &t)
Definition match_tree.h:457
const variable_or_number_list & variables() const
Definition match_tree.h:472
const data_expression & result() const
Definition match_tree.h:467
match_tree_S(const atermpp::aterm &t)
Definition match_tree.h:213
const variable & target_variable() const
Definition match_tree.h:223
match_tree_S(const variable &target_variable, const match_tree &result_tree)
Definition match_tree.h:219
const match_tree & subtree() const
Definition match_tree.h:228
match_tree_X(const atermpp::aterm &t)
Definition match_tree.h:438
atermpp::function_symbol afunUndefined() const
Definition match_tree.h:60
atermpp::function_symbol afunD() const
Definition match_tree.h:97
atermpp::function_symbol afunN() const
Definition match_tree.h:91
match_tree(const atermpp::aterm &t)
Constructor based on an aterm.
Definition match_tree.h:51
match_tree()
Default constructor.
Definition match_tree.h:46
atermpp::function_symbol afunRe() const
Definition match_tree.h:121
atermpp::function_symbol afunF() const
Definition match_tree.h:85
atermpp::function_symbol afunCRe() const
Definition match_tree.h:127
atermpp::function_symbol afunM() const
Definition match_tree.h:79
atermpp::function_symbol afunX() const
Definition match_tree.h:115
atermpp::function_symbol afunMe() const
Definition match_tree.h:133
atermpp::function_symbol afunC() const
Definition match_tree.h:109
atermpp::function_symbol afunS() const
Definition match_tree.h:66
atermpp::function_symbol afunA() const
Definition match_tree.h:72
atermpp::function_symbol afunR() const
Definition match_tree.h:103
This is a list where variables and aterm ints can be stored.
Definition match_tree.h:26
variable_or_number(const atermpp::aterm &v)
Constructor.
Definition match_tree.h:33
variable_or_number()
Default constructor.
Definition match_tree.h:29
\brief A function symbol
\brief A data variable
Definition variable.h:28
The class function symbol.
The main namespace for the aterm++ library.
Definition algorithm.h:21
const Derived & down_cast(const Base &t, typename std::enable_if< is_convertible< Base, Derived >::value &&!std::is_base_of< Derived, Base >::value >::type *=nullptr)
A cheap cast from one aterm based type to another When casting one aterm based type into another,...
Definition aterm.h:259
atermpp::term_list< match_tree > match_tree_list
Definition match_tree.h:545
atermpp::term_list< match_tree_list > match_tree_list_list
Definition match_tree.h:547
atermpp::term_list< variable_or_number > variable_or_number_list
Definition match_tree.h:40
std::ostream & operator<<(std::ostream &os, smt_solver_type s)
standard conversion from solvert type to stream
Definition solver_type.h:71
std::vector< match_tree > match_tree_vector
Definition match_tree.h:546
atermpp::term_list< match_tree_list_list > match_tree_list_list_list
Definition match_tree.h:548
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72