LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail/rewrite - match_tree.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 229 243 94.2 %
Date: 2020-02-28 00:44:21 Functions: 92 93 98.9 %
Legend: Lines: hit not hit

          Line data    Source code
       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             : //
       9             : /// \file mcrl2/data/detail/rewrite/jittyc.h
      10             : 
      11             : #ifndef MCRL2_DATA_MATCH_TREE_H
      12             : #define MCRL2_DATA_MATCH_TREE_H
      13             : 
      14             : #include "mcrl2/data/function_symbol.h"
      15             : #include "mcrl2/atermpp/aterm_io.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : namespace data
      20             : {
      21             : namespace detail
      22             : {
      23             : 
      24             : /// This is a list where variables and aterm ints can be stored.
      25        5700 : class variable_or_number: public atermpp::aterm
      26             : {
      27             :   public:
      28             :     /// Default constructor
      29             :     variable_or_number()
      30             :     {}
      31             : 
      32             :     /// Constructor
      33        5700 :     variable_or_number(const atermpp::aterm& v):
      34        5700 :        atermpp::aterm(v)
      35             :     {
      36        5700 :       assert(is_variable(atermpp::down_cast<atermpp::aterm_appl>(v)) || v.type_is_int());
      37        5700 :     }
      38             : };
      39             : 
      40             : typedef atermpp::term_list<variable_or_number> variable_or_number_list;
      41             : 
      42      255330 : class match_tree:public atermpp::aterm_appl
      43             : {
      44             :   public:
      45             :     /// Default constructor
      46       23326 :     match_tree():
      47       23326 :       atermpp::aterm_appl(afunUndefined())
      48       23326 :     {}
      49             : 
      50             :   protected:
      51             :     /// Constructor based on an aterm.
      52       56476 :     match_tree(const atermpp::aterm_appl& t):
      53       56476 :       atermpp::aterm_appl(t)
      54       56476 :     {}
      55             :   
      56       33295 :     atermpp::function_symbol afunUndefined() const
      57             :     {
      58       33295 :       static atermpp::function_symbol afunUndefined("@@Match_tree_dummy",0); // Undefined match term. Used as default match term
      59       33295 :       return afunUndefined;
      60             :     }
      61             : 
      62       35017 :     atermpp::function_symbol afunS() const
      63             :     {
      64       35017 :       static atermpp::function_symbol afunS("@@S",2); // Store term ( target_variable, result_tree )
      65       35017 :       return afunS;
      66             :     }
      67             : 
      68        8599 :     atermpp::function_symbol afunA() const
      69             :     {
      70        8599 :       static atermpp::function_symbol afunA("@@A",1); // Rewrite argument ( number of an argument as an aterm_int  )
      71        8599 :       return afunA;
      72             :     }
      73             : 
      74             : 
      75       28361 :     atermpp::function_symbol afunM() const
      76             :     {
      77       28361 :       static atermpp::function_symbol afunM("@@M",3); // Match term ( match_variable, true_tree , false_tree )
      78       28361 :       return afunM;
      79             :     }
      80             : 
      81       16988 :     atermpp::function_symbol afunF() const
      82             :     {
      83       16988 :       static atermpp::function_symbol afunF("@@F",3); // Match function ( match_function, true_tree, false_tree )
      84       16988 :       return afunF;
      85             :     }
      86             : 
      87       25265 :     atermpp::function_symbol afunN() const
      88             :     {
      89       25265 :       static atermpp::function_symbol afunN("@@N",1); // Go to next parameter ( result_tree )
      90       25265 :       return afunN;
      91             :     }
      92             : 
      93       27444 :     atermpp::function_symbol afunD() const
      94             :     {
      95       27444 :       static atermpp::function_symbol afunD("@@D",1); // Go down a level ( result_tree )
      96       27444 :       return afunD;
      97             :     }
      98             : 
      99        6328 :     atermpp::function_symbol afunR() const
     100             :     {
     101        6328 :       static atermpp::function_symbol afunR("@@R",1); // End of tree ( matching_rule )
     102        6328 :       return afunR;
     103             :     }
     104             : 
     105        2365 :     atermpp::function_symbol afunC() const
     106             :     {
     107        2365 :       static atermpp::function_symbol afunC("@@C",3); // Check condition ( condition, true_tree, false_tree )
     108        2365 :       return afunC;
     109             :     }
     110             : 
     111        2278 :     atermpp::function_symbol afunX() const
     112             :     {
     113        2278 :       static atermpp::function_symbol afunX("@@X",0); // End of tree
     114        2278 :       return afunX;
     115             :     }
     116             : 
     117       33985 :     atermpp::function_symbol afunRe() const
     118             :     {
     119       33985 :       static atermpp::function_symbol afunRe("@@Re",2); // End of tree ( matching_rule , vars_of_rule)
     120       33985 :       return afunRe;
     121             :     }
     122             : 
     123       18723 :     atermpp::function_symbol afunCRe() const
     124             :     {
     125       18723 :       static atermpp::function_symbol afunCRe("@@CRe",4); // End of tree ( condition, matching_rule, vars_of_condition, vars_of_rule )
     126       18723 :       return afunCRe;
     127             :     }
     128             : 
     129        5028 :     atermpp::function_symbol afunMe() const
     130             :     {
     131        5028 :       static atermpp::function_symbol afunMe("@@Me",2); // Match term ( match_variable, variable_index )
     132        5028 :       return afunMe;
     133             :     }
     134             : 
     135             :   public:
     136        9969 :     bool is_defined() const
     137             :     {
     138        9969 :       return this->function()!=afunUndefined();
     139             :     }
     140             : 
     141       28897 :     bool isS() const
     142             :     {
     143       28897 :       return this->function()==afunS();
     144             :     }
     145             : 
     146        7501 :     bool isA() const
     147             :     {
     148        7501 :       return this->function()==afunA();
     149             :     }
     150             :       
     151       27015 :     bool isM() const
     152             :     {
     153       27015 :       return this->function()==afunM();
     154             :     }
     155             :       
     156       12136 :     bool isF() const
     157             :     {
     158       12136 :       return this->function()==afunF();
     159             :     }
     160             :       
     161       19619 :     bool isN() const
     162             :     {
     163       19619 :       return this->function()==afunN();
     164             :     }
     165             :       
     166       23643 :     bool isD() const
     167             :     {
     168       23643 :       return this->function()==afunD();
     169             :     }
     170             :       
     171        3442 :     bool isR() const
     172             :     {
     173        3442 :       return this->function()==afunR();
     174             :     }
     175             :       
     176        2309 :     bool isC() const
     177             :     {
     178        2309 :       return this->function()==afunC();
     179             :     }
     180             :       
     181         910 :     bool isX() const
     182             :     {
     183         910 :       return this->function()==afunX();
     184             :     }
     185             :       
     186       28046 :     bool isRe() const
     187             :     {
     188       28046 :       return this->function()==afunRe();
     189             :     }
     190             :       
     191       18555 :     bool isCRe() const
     192             :     {
     193       18555 :       return this->function()==afunCRe();
     194             :     }
     195             :       
     196        4596 :     bool isMe() const
     197             :     {
     198        4596 :       return this->function()==afunMe();
     199             :     }
     200             : };
     201             : 
     202             : // Store term ( target_variable, result_tree )
     203       17177 : class match_tree_S:public match_tree
     204             : {
     205             :   public:
     206             :     match_tree_S()
     207             :     {}
     208             : 
     209       11057 :     match_tree_S(const atermpp::aterm_appl& t):
     210       11057 :           match_tree(t)
     211             :     {
     212       11057 :       assert(isS());
     213       11057 :     }
     214             :     
     215        6120 :     match_tree_S(const variable& target_variable, const match_tree& result_tree):
     216        6120 :           match_tree(atermpp::aterm_appl(afunS(),target_variable,result_tree))
     217        6120 :     {}
     218             : 
     219       16875 :     const variable& target_variable() const
     220             :     {
     221       16875 :       return atermpp::down_cast<const variable>((*this)[0]);
     222             :     }
     223             : 
     224        3138 :     const match_tree& subtree() const
     225             :     {
     226        3138 :       return atermpp::down_cast<const match_tree>((*this)[1]);
     227             :     }
     228             : };
     229             : 
     230             : // Rewrite argument ( a number of an arguments as a aterm_int )
     231             : 
     232        2048 : class match_tree_A:public match_tree
     233             : {
     234             :   public:
     235             :     match_tree_A()
     236             :     {}
     237             : 
     238         950 :     match_tree_A(const atermpp::aterm_appl& t):
     239         950 :           match_tree(t)
     240             :     {
     241         950 :       assert(isA());
     242         950 :     }
     243             : 
     244        1098 :     match_tree_A(const std::size_t n):
     245        1098 :           match_tree(atermpp::aterm_appl(afunA(),atermpp::aterm_int(n)))
     246        1098 :     {}
     247             : 
     248        1489 :     std::size_t variable_index() const
     249             :     {
     250        1489 :       return atermpp::down_cast<const atermpp::aterm_int>((*this)[0]).value();
     251             :     }
     252             : };
     253             : 
     254             : 
     255             : // Match term ( match_variable, true_tree , false_tree )
     256        1882 : class match_tree_M:public match_tree
     257             : {
     258             :   public:
     259             :     match_tree_M()
     260             :     {}
     261             : 
     262         536 :     match_tree_M(const atermpp::aterm_appl& t):
     263         536 :           match_tree(t)
     264             :     {
     265         536 :       assert(isM());
     266         536 :     }
     267             :     
     268        1346 :     match_tree_M(const variable& match_variable, const match_tree& true_tree, const match_tree& false_tree):
     269        1346 :           match_tree(atermpp::aterm_appl(afunM(),match_variable,true_tree,false_tree))
     270        1346 :     {}
     271             : 
     272        1076 :     const variable& match_variable() const
     273             :     {
     274        1076 :       return atermpp::down_cast<const variable>((*this)[0]);
     275             :     }
     276             : 
     277         972 :     const match_tree& true_tree() const
     278             :     {
     279         972 :       return atermpp::down_cast<const match_tree>((*this)[1]);
     280             :     }
     281             : 
     282         972 :     const match_tree& false_tree() const
     283             :     {
     284         972 :       return atermpp::down_cast<const match_tree>((*this)[2]);
     285             :     }
     286             : };
     287             : 
     288             : // Match function ( match_function, true_tree, false_tree )
     289        7204 : class match_tree_F:public match_tree
     290             : {
     291             :   public:
     292             :     match_tree_F()
     293             :     {}
     294             : 
     295        2352 :     match_tree_F(const atermpp::aterm_appl& t):
     296        2352 :           match_tree(t)
     297             :     {
     298        2352 :       assert(isF());
     299        2352 :     }
     300             :     
     301        4852 :     match_tree_F(const data::function_symbol& function, const match_tree& true_tree, const match_tree& false_tree):
     302        4852 :           match_tree(atermpp::aterm_appl(afunF(),function,true_tree,false_tree))
     303        4852 :     {}
     304             : 
     305        4074 :     const data::function_symbol& function() const
     306             :     {
     307        4074 :       return atermpp::down_cast<const data::function_symbol>((*this)[0]);
     308             :     }
     309             : 
     310        1120 :     const match_tree& true_tree() const
     311             :     {
     312        1120 :       return atermpp::down_cast<const match_tree>((*this)[1]);
     313             :     }
     314             : 
     315        1120 :     const match_tree& false_tree() const
     316             :     {
     317        1120 :       return atermpp::down_cast<const match_tree>((*this)[2]);
     318             :     }
     319             : };
     320             : 
     321             : // Go to next parameter ( result_tree )
     322        5646 : class match_tree_N:public match_tree
     323             : {
     324             :   public:
     325             :     match_tree_N()
     326             :     {}
     327             : 
     328             :     match_tree_N(const atermpp::aterm_appl& t):
     329             :           match_tree(t)
     330             :     {
     331             :       assert(isN());
     332             :     }
     333             :     
     334             :     /// Constructor. Builds a new term around a match_tree.
     335             :     /// The extra non-used std::size_t is provided, to distinghuish this
     336             :     /// constructor from the default copy constructor.
     337        5646 :     match_tree_N(const match_tree& result_tree, std::size_t):
     338        5646 :           match_tree(atermpp::aterm_appl(afunN(),result_tree))
     339        5646 :     {}
     340             : 
     341        2454 :     const match_tree& subtree() const
     342             :     {
     343        2454 :       return atermpp::down_cast<const match_tree>((*this)[0]);
     344             :     }
     345             : };
     346             : 
     347             : // Go down a level ( result_tree )
     348        3801 : class match_tree_D:public match_tree
     349             : {
     350             :   public:
     351             :     match_tree_D()
     352             :     {}
     353             : 
     354             :     match_tree_D(const atermpp::aterm_appl& t):
     355             :           match_tree(t)
     356             :     {
     357             :       assert(isD());
     358             :     }
     359             :     
     360             :     /// Constructor. Builds a new term around a match_tree.
     361             :     /// The extra non-used std::size_t is provided, to distinghuish this
     362             :     /// constructor from the default copy constructor.
     363        3801 :     match_tree_D(const match_tree& result_tree, std::size_t):
     364        3801 :           match_tree(atermpp::aterm_appl(afunD(),result_tree))
     365        3801 :     {}
     366             : 
     367         736 :     const match_tree& subtree() const
     368             :     {
     369         736 :       return atermpp::down_cast<const match_tree>((*this)[0]);
     370             :     }
     371             : };
     372             : 
     373             : // End of tree ( matching_rule )
     374        2886 : class match_tree_R:public match_tree
     375             : {
     376             : 
     377             :   public:
     378             :     match_tree_R()
     379             :     {}
     380             : 
     381           0 :     match_tree_R(const atermpp::aterm_appl& t):
     382           0 :           match_tree(t)
     383             :     {
     384           0 :       assert(isR());
     385           0 :     }
     386             :     
     387        2886 :     match_tree_R(const data_expression& e):
     388        2886 :           match_tree(atermpp::aterm_appl(afunR(),e))
     389        2886 :     {}
     390             : 
     391        2628 :     const data_expression& result() const
     392             :     {
     393        2628 :       return atermpp::down_cast<const data_expression>((*this)[0]);
     394             :     }
     395             : };
     396             : 
     397             : // Check condition ( condition, true_tree, false_tree )
     398          56 : class match_tree_C:public match_tree
     399             : {
     400             :   public:
     401             :     match_tree_C()
     402             :     {}
     403             : 
     404             :     match_tree_C(const atermpp::aterm_appl& t):
     405             :           match_tree(t)
     406             :     {
     407             :       assert(isC());
     408             :     }
     409             :     
     410          56 :     match_tree_C(const data_expression& condition, const match_tree& true_tree, const match_tree& false_tree):
     411          56 :         match_tree(atermpp::aterm_appl(afunC(),condition,true_tree,false_tree))
     412          56 :     {}
     413             : 
     414          44 :     const data_expression& condition() const
     415             :     {
     416          44 :       return atermpp::down_cast<const data_expression>((*this)[0]);
     417             :     }
     418             : 
     419          44 :     const match_tree& true_tree() const
     420             :     {
     421          44 :       return atermpp::down_cast<const match_tree>((*this)[1]);
     422             :     }
     423             : 
     424          44 :     const match_tree& false_tree() const
     425             :     {
     426          44 :       return atermpp::down_cast<const match_tree>((*this)[2]);
     427             :     }
     428             : };
     429             : 
     430             : // End of tree
     431        1368 : class match_tree_X:public match_tree
     432             : {
     433             :   public:
     434             :     match_tree_X(const atermpp::aterm_appl& t):
     435             :           match_tree(t)
     436             :     {
     437             :       assert(isX());
     438             :     }
     439             :     
     440        1368 :     match_tree_X():
     441        1368 :         match_tree(atermpp::aterm_appl(afunX()))
     442        1368 :     {}
     443             : };
     444             : 
     445             : // End of tree ( matching_rule , vars_of_rule)
     446             : // The var_of_rule is a list with variables and aterm_ints.
     447       25623 : class match_tree_Re:public match_tree
     448             : {
     449             :   public:
     450        9969 :     match_tree_Re()
     451        9969 :     {}
     452             : 
     453        6787 :     match_tree_Re(const atermpp::aterm_appl& t):
     454        6787 :           match_tree(t)
     455             :     {
     456        6787 :       assert(isRe());
     457        6787 :     }
     458             :     
     459        5939 :     match_tree_Re(const data_expression& result, const variable_or_number_list& vars):
     460        5939 :            match_tree(atermpp::aterm_appl(afunRe(),result,vars))
     461        5939 :     {}
     462             : 
     463        6689 :     const data_expression& result() const
     464             :     {
     465        6689 :       return atermpp::down_cast<const data_expression>((*this)[0]);
     466             :     }
     467             : 
     468        6689 :     const variable_or_number_list& variables() const
     469             :     {
     470        6689 :       return atermpp::down_cast<const variable_or_number_list>((*this)[1]);
     471             :     }
     472             : };
     473             : 
     474             : // End of tree ( condition, matching_rule, vars_of_condition, vars_of_rule )
     475             : // The last two parameters consist of a list with variables and numbers.
     476         336 : class match_tree_CRe:public match_tree
     477             : {
     478             :   public:
     479             :     match_tree_CRe()
     480             :     {}
     481             : 
     482         168 :     match_tree_CRe(const atermpp::aterm_appl& t):
     483         168 :           match_tree(t)
     484             :     {
     485         168 :       assert(isCRe());
     486         168 :     }
     487             :     
     488         168 :     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):
     489         168 :            match_tree(atermpp::aterm_appl(afunCRe(),condition,result,vars_condition,vars_rule))
     490         168 :     {}
     491             : 
     492         168 :     const data_expression& condition() const
     493             :     {
     494         168 :       return atermpp::down_cast<const data_expression>((*this)[0]);
     495             :     }
     496             : 
     497         168 :     const data_expression& result() const
     498             :     {
     499         168 :       return atermpp::down_cast<const data_expression>((*this)[1]);
     500             :     }
     501             : 
     502         168 :     const variable_or_number_list& variables_condition() const
     503             :     {
     504         168 :       return atermpp::down_cast<const variable_or_number_list>((*this)[2]);
     505             :     }
     506             : 
     507         168 :     const variable_or_number_list& variables_result() const
     508             :     {
     509         168 :       return  atermpp::down_cast<const variable_or_number_list>((*this)[3]);
     510             :     }
     511             : };
     512             : 
     513             : // Match term ( match_variable, variable_index )
     514        1346 : class match_tree_Me:public match_tree
     515             : {
     516             :   public:
     517             :     match_tree_Me()
     518             :     {}
     519             : 
     520         914 :     match_tree_Me(const atermpp::aterm_appl& t):
     521         914 :           match_tree(t)
     522             :     {
     523         914 :       assert(isMe());
     524         914 :     }
     525             :     
     526         432 :     match_tree_Me(const variable& match_variable, const std::size_t variable_index):
     527         432 :            match_tree(atermpp::aterm_appl(afunMe(),match_variable,atermpp::aterm_int(variable_index)))
     528         432 :     {}
     529             : 
     530         914 :     const variable& match_variable() const
     531             :     {
     532         914 :       return atermpp::down_cast<const variable>((*this)[0]);
     533             :     }
     534             : 
     535         914 :     std::size_t variable_index() const
     536             :     {
     537         914 :       return (atermpp::down_cast<const atermpp::aterm_int>((*this)[1])).value();
     538             :     }
     539             : };
     540             : 
     541             : typedef atermpp::term_list < match_tree > match_tree_list;
     542             : typedef std::vector < match_tree > match_tree_vector;
     543             : typedef atermpp::term_list < match_tree_list > match_tree_list_list;
     544             : typedef atermpp::term_list < match_tree_list_list > match_tree_list_list_list;
     545             : 
     546             : inline
     547        5363 : std::ostream& operator<<(std::ostream& s, const match_tree& t)
     548             : {
     549             :   using atermpp::down_cast;
     550        5363 :   if (t.isS())
     551             :   {
     552        1046 :     const match_tree_S& tS = down_cast<match_tree_S>(t);
     553        1046 :     s << "@@S(" << tS.target_variable() << ", " << tS.subtree() << ")";
     554             :   }
     555             :   else
     556        4317 :   if (t.isA())
     557             :   {
     558         539 :     const match_tree_A& tA = down_cast<match_tree_A>(t);
     559         539 :     s << "@@A(" << tA.variable_index() << ")";
     560             :   }
     561             :   else
     562        3778 :   if (t.isM())
     563             :   {
     564         270 :     const match_tree_M& tM = down_cast<match_tree_M>(t);
     565         270 :     s << "@@M(" << tM.match_variable() << ", " << tM.true_tree() << ", " << tM.false_tree() << ")";
     566             :   }
     567             :   else
     568        3508 :   if (t.isF())
     569             :   {
     570         560 :     const match_tree_F& tF = down_cast<match_tree_F>(t);
     571         560 :     s << "@@F(" << tF.function() << ", " << tF.true_tree() << ", " << tF.false_tree() << ")";
     572             :   }
     573             :   else
     574        2948 :   if (t.isN())
     575             :   {
     576        1227 :     const match_tree_N& tN = down_cast<match_tree_N>(t);
     577        1227 :     s << "@@N(" << tN.subtree() << ")";
     578             :   }
     579             :   else
     580        1721 :   if (t.isD())
     581             :   {
     582         368 :     const match_tree_D& tD = down_cast<match_tree_D>(t);
     583         368 :     s << "@@D(" << tD.subtree() << ")";
     584             :   }
     585             :   else
     586        1353 :   if (t.isR())
     587             :   {
     588         876 :     const match_tree_R& tR = down_cast<match_tree_R>(t);
     589         876 :     s << "@@R(" << tR.result() << ")";
     590             :   }
     591             :   else
     592         477 :   if (t.isC())
     593             :   {
     594          22 :     const match_tree_C& tC = down_cast<match_tree_C>(t);
     595          22 :     s << "@@C(" << tC.condition() << ", " << tC.true_tree() << ", " << tC.false_tree() << ")";
     596             :   }
     597             :   else
     598         455 :   if (t.isX())
     599             :   {
     600         455 :     s << "@@X";
     601             :   }
     602             :   else
     603           0 :   if (t.isRe())
     604             :   {
     605           0 :     const match_tree_Re& tRe = down_cast<match_tree_Re>(t);
     606           0 :     s << "@@Re(" << tRe.result() << ", " << tRe.variables() << ")";
     607             :   }
     608             :   else
     609           0 :   if (t.isCRe())
     610             :   {
     611           0 :     const match_tree_CRe& tCRe = down_cast<match_tree_CRe>(t);
     612           0 :     s << "@@CRe(" << tCRe.condition() << ", " << tCRe.result() << ", "
     613           0 :       << tCRe.variables_condition() << ", " << tCRe.variables_result() << ")";
     614             :   }
     615             :   else
     616           0 :   if (t.isMe())
     617             :   {
     618           0 :     const match_tree_Me& tMe = down_cast<match_tree_Me>(t);
     619           0 :     s << "@@Me(" << tMe.match_variable() << ", " << tMe.variable_index() << ")";
     620             :   }
     621        5363 :   return s;
     622             : }
     623             : 
     624             : } // namespace detail
     625             : 
     626             : } // namespace data
     627             : 
     628             : } // namespace mcrl2
     629             : 
     630             : #endif // MCRL2_DATA_MATCH_TREE_H

Generated by: LCOV version 1.13