Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Mathias Preiner
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Implements a match trie, also known as a discrimination tree.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "expr/match_trie.h"
      17                 :            : 
      18                 :            : using namespace cvc5::internal::kind;
      19                 :            : 
      20                 :            : namespace cvc5::internal {
      21                 :            : namespace expr {
      22                 :            : 
      23                 :       2267 : bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
      24                 :            : {
      25                 :       4534 :   std::vector<Node> vars;
      26                 :       4534 :   std::vector<Node> subs;
      27                 :       4534 :   std::map<Node, Node> smap;
      28                 :            : 
      29                 :       4534 :   std::vector<std::vector<Node> > visit;
      30                 :       4534 :   std::vector<MatchTrie*> visit_trie;
      31                 :       4534 :   std::vector<int> visit_var_index;
      32                 :       4534 :   std::vector<bool> visit_bound_var;
      33                 :            : 
      34                 :       4534 :   visit.push_back(std::vector<Node>{n});
      35                 :       2267 :   visit_trie.push_back(this);
      36                 :       2267 :   visit_var_index.push_back(-1);
      37                 :       2267 :   visit_bound_var.push_back(false);
      38         [ +  + ]:     260921 :   while (!visit.empty())
      39                 :            :   {
      40                 :     258654 :     std::vector<Node> cvisit = visit.back();
      41                 :     258654 :     MatchTrie* curr = visit_trie.back();
      42         [ +  + ]:     258654 :     if (cvisit.empty())
      43                 :            :     {
      44 [ -  + ][ -  + ]:      31472 :       Assert(n
                 [ -  - ]
      45                 :            :              == curr->d_data.substitute(
      46                 :            :                  vars.begin(), vars.end(), subs.begin(), subs.end()));
      47         [ +  - ]:      31472 :       Trace("match-debug") << "notify : " << curr->d_data << std::endl;
      48         [ -  + ]:      31472 :       if (!ntm->notify(n, curr->d_data, vars, subs))
      49                 :            :       {
      50                 :          0 :         return false;
      51                 :            :       }
      52                 :      31472 :       visit.pop_back();
      53                 :      31472 :       visit_trie.pop_back();
      54                 :      31472 :       visit_var_index.pop_back();
      55                 :      31472 :       visit_bound_var.pop_back();
      56                 :            :     }
      57                 :            :     else
      58                 :            :     {
      59                 :     454364 :       Node cn = cvisit.back();
      60         [ +  - ]:     454364 :       Trace("match-debug") << "traverse : " << cn << " at depth "
      61                 :     227182 :                            << visit.size() << std::endl;
      62                 :     227182 :       unsigned index = visit.size() - 1;
      63                 :     227182 :       int vindex = visit_var_index[index];
      64         [ +  + ]:     227182 :       if (vindex == -1)
      65                 :            :       {
      66         [ +  + ]:      70821 :         if (!cn.isVar())
      67                 :            :         {
      68         [ +  + ]:      49540 :           Node op = cn.hasOperator() ? cn.getOperator() : cn;
      69         [ +  + ]:      24770 :           unsigned nchild = cn.hasOperator() ? cn.getNumChildren() : 0;
      70                 :            :           std::map<unsigned, MatchTrie>::iterator itu =
      71                 :      24770 :               curr->d_children[op].find(nchild);
      72         [ +  + ]:      24770 :           if (itu != curr->d_children[op].end())
      73                 :            :           {
      74                 :            :             // recurse on the operator or self
      75                 :      18388 :             cvisit.pop_back();
      76         [ +  + ]:      18388 :             if (cn.hasOperator())
      77                 :            :             {
      78         [ +  + ]:      27424 :               for (const Node& cnc : cn)
      79                 :            :               {
      80                 :      19188 :                 cvisit.push_back(cnc);
      81                 :            :               }
      82                 :            :             }
      83         [ +  - ]:      18388 :             Trace("match-debug") << "recurse op : " << op << std::endl;
      84                 :      18388 :             visit.push_back(cvisit);
      85                 :      18388 :             visit_trie.push_back(&itu->second);
      86                 :      18388 :             visit_var_index.push_back(-1);
      87                 :      18388 :             visit_bound_var.push_back(false);
      88                 :            :           }
      89                 :            :         }
      90                 :      70821 :         visit_var_index[index]++;
      91                 :            :       }
      92                 :            :       else
      93                 :            :       {
      94                 :            :         // clean up if we previously bound a variable
      95         [ +  + ]:     156361 :         if (visit_bound_var[index])
      96                 :            :         {
      97 [ -  + ][ -  + ]:      81276 :           Assert(!vars.empty());
                 [ -  - ]
      98                 :      81276 :           smap.erase(vars.back());
      99                 :      81276 :           vars.pop_back();
     100                 :      81276 :           subs.pop_back();
     101                 :      81276 :           visit_bound_var[index] = false;
     102                 :            :         }
     103                 :            : 
     104         [ +  + ]:     156361 :         if (vindex == static_cast<int>(curr->d_vars.size()))
     105                 :            :         {
     106         [ +  - ]:     141642 :           Trace("match-debug")
     107                 :          0 :               << "finished checking " << curr->d_vars.size()
     108                 :      70821 :               << " variables at depth " << visit.size() << std::endl;
     109                 :            :           // finished
     110                 :      70821 :           visit.pop_back();
     111                 :      70821 :           visit_trie.pop_back();
     112                 :      70821 :           visit_var_index.pop_back();
     113                 :      70821 :           visit_bound_var.pop_back();
     114                 :            :         }
     115                 :            :         else
     116                 :            :         {
     117         [ +  - ]:     171080 :           Trace("match-debug") << "check variable #" << vindex << " at depth "
     118                 :      85540 :                                << visit.size() << std::endl;
     119 [ -  + ][ -  + ]:      85540 :           Assert(vindex < static_cast<int>(curr->d_vars.size()));
                 [ -  - ]
     120                 :            :           // recurse on variable?
     121                 :      85540 :           Node var = curr->d_vars[vindex];
     122                 :      85540 :           bool recurse = true;
     123                 :            :           // check if it is already bound
     124                 :      85540 :           std::map<Node, Node>::iterator its = smap.find(var);
     125         [ +  + ]:      85540 :           if (its != smap.end())
     126                 :            :           {
     127         [ +  + ]:       2274 :             if (its->second != cn)
     128                 :            :             {
     129                 :       1912 :               recurse = false;
     130                 :            :             }
     131                 :            :           }
     132         [ +  + ]:      83266 :           else if (var.getType() != cn.getType())
     133                 :            :           {
     134                 :       1990 :             recurse = false;
     135                 :            :           }
     136                 :            :           else
     137                 :            :           {
     138                 :      81276 :             vars.push_back(var);
     139                 :      81276 :             subs.push_back(cn);
     140                 :      81276 :             smap[var] = cn;
     141                 :      81276 :             visit_bound_var[index] = true;
     142                 :            :           }
     143         [ +  + ]:      85540 :           if (recurse)
     144                 :            :           {
     145         [ +  - ]:      81638 :             Trace("match-debug") << "recurse var : " << var << std::endl;
     146                 :      81638 :             cvisit.pop_back();
     147                 :      81638 :             visit.push_back(cvisit);
     148                 :      81638 :             visit_trie.push_back(&curr->d_children[var][0]);
     149                 :      81638 :             visit_var_index.push_back(-1);
     150                 :      81638 :             visit_bound_var.push_back(false);
     151                 :            :           }
     152                 :      85540 :           visit_var_index[index]++;
     153                 :            :         }
     154                 :            :       }
     155                 :            :     }
     156                 :            :   }
     157                 :       2267 :   return true;
     158                 :            : }
     159                 :            : 
     160                 :       2270 : void MatchTrie::addTerm(Node n)
     161                 :            : {
     162 [ -  + ][ -  + ]:       2270 :   Assert(!n.isNull());
                 [ -  - ]
     163                 :       4540 :   std::vector<Node> visit;
     164                 :       2270 :   visit.push_back(n);
     165                 :       2270 :   MatchTrie* curr = this;
     166         [ +  + ]:      17132 :   while (!visit.empty())
     167                 :            :   {
     168                 :      29724 :     Node cn = visit.back();
     169                 :      14862 :     visit.pop_back();
     170         [ +  + ]:      14862 :     if (cn.hasOperator())
     171                 :            :     {
     172                 :       5345 :       curr = &(curr->d_children[cn.getOperator()][cn.getNumChildren()]);
     173         [ +  + ]:      17937 :       for (const Node& cnc : cn)
     174                 :            :       {
     175                 :      12592 :         visit.push_back(cnc);
     176                 :            :       }
     177                 :            :     }
     178                 :            :     else
     179                 :            :     {
     180                 :       9517 :       if (cn.isVar()
     181 [ +  + ][ +  + ]:      22121 :           && std::find(curr->d_vars.begin(), curr->d_vars.end(), cn)
     182         [ +  + ]:      22121 :                  == curr->d_vars.end())
     183                 :            :       {
     184                 :       4342 :         curr->d_vars.push_back(cn);
     185                 :            :       }
     186                 :       9517 :       curr = &(curr->d_children[cn][0]);
     187                 :            :     }
     188                 :            :   }
     189                 :       2270 :   curr->d_data = n;
     190                 :       2270 : }
     191                 :            : 
     192                 :         54 : void MatchTrie::clear()
     193                 :            : {
     194                 :         54 :   d_children.clear();
     195                 :         54 :   d_vars.clear();
     196                 :         54 :   d_data = Node::null();
     197                 :         54 : }
     198                 :            : 
     199                 :            : }  // namespace expr
     200                 :            : }  // namespace cvc5::internal