Branch data     Line data    Source code

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