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                 :            :  * Implementation of a trie class for Nodes and TNodes.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "expr/node_trie.h"
      14                 :            : 
      15                 :            : namespace cvc5::internal {
      16                 :            : 
      17                 :            : template <bool ref_count>
      18                 :    8756376 : NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::existsTerm(
      19                 :            :     const std::vector<NodeTemplate<ref_count>>& reps) const
      20                 :            : {
      21                 :    8756376 :   const NodeTemplateTrie<ref_count>* tnt = this;
      22                 :            :   typename std::map<NodeTemplate<ref_count>,
      23                 :    8756376 :                     NodeTemplateTrie<ref_count>>::const_iterator it;
      24         [ +  + ]:   22750256 :   for (const NodeTemplate<ref_count>& r : reps)
      25                 :            :   {
      26                 :   16375488 :     it = tnt->d_data.find(r);
      27         [ +  + ]:   16375488 :     if (it == tnt->d_data.end())
      28                 :            :     {
      29                 :            :       // didn't find this child, return null
      30                 :    2381608 :       return Node::null();
      31                 :            :     }
      32                 :   13993880 :     tnt = &it->second;
      33                 :            :   }
      34         [ +  + ]:    6374768 :   if (tnt->d_data.empty())
      35                 :            :   {
      36                 :       2184 :     return Node::null();
      37                 :            :   }
      38                 :   12745168 :   return tnt->d_data.begin()->first;
      39                 :            : }
      40                 :            : 
      41                 :            : template TNode NodeTemplateTrie<false>::existsTerm(
      42                 :            :     const std::vector<TNode>& reps) const;
      43                 :            : template Node NodeTemplateTrie<true>::existsTerm(
      44                 :            :     const std::vector<Node>& reps) const;
      45                 :            : 
      46                 :            : template <bool ref_count>
      47                 :    3557247 : NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::addOrGetTerm(
      48                 :            :     NodeTemplate<ref_count> n, const std::vector<NodeTemplate<ref_count>>& reps)
      49                 :            : {
      50                 :    3557247 :   NodeTemplateTrie<ref_count>* tnt = this;
      51         [ +  + ]:    9932866 :   for (const NodeTemplate<ref_count>& r : reps)
      52                 :            :   {
      53                 :    6375619 :     tnt = &(tnt->d_data[r]);
      54                 :            :   }
      55         [ +  + ]:    3557247 :   if (tnt->d_data.empty())
      56                 :            :   {
      57                 :            :     // Store n in d_data. This should be interpreted as the "data" and not as a
      58                 :            :     // reference to a child.
      59                 :    2767928 :     tnt->d_data[n].clear();
      60                 :    2767928 :     return n;
      61                 :            :   }
      62                 :    1578638 :   return tnt->d_data.begin()->first;
      63                 :            : }
      64                 :            : 
      65                 :            : template TNode NodeTemplateTrie<false>::addOrGetTerm(
      66                 :            :     TNode n, const std::vector<TNode>& reps);
      67                 :            : template Node NodeTemplateTrie<true>::addOrGetTerm(
      68                 :            :     Node n, const std::vector<Node>& reps);
      69                 :            : 
      70                 :            : template <bool ref_count>
      71                 :          0 : void NodeTemplateTrie<ref_count>::debugPrint(const char* c,
      72                 :            :                                              unsigned depth) const
      73                 :            : {
      74         [ -  - ]:          0 :   for (const std::pair<const NodeTemplate<ref_count>,
      75                 :            :                        NodeTemplateTrie<ref_count>>& p : d_data)
      76                 :            :   {
      77         [ -  - ]:          0 :     for (unsigned i = 0; i < depth; i++)
      78                 :            :     {
      79         [ -  - ]:          0 :       Trace(c) << "  ";
      80                 :            :     }
      81         [ -  - ]:          0 :     Trace(c) << p.first << std::endl;
      82                 :          0 :     p.second.debugPrint(c, depth + 1);
      83                 :            :   }
      84                 :          0 : }
      85                 :            : 
      86                 :            : template void NodeTemplateTrie<false>::debugPrint(const char* c,
      87                 :            :                                                   unsigned depth) const;
      88                 :            : template void NodeTemplateTrie<true>::debugPrint(const char* c,
      89                 :            :                                                  unsigned depth) const;
      90                 :            : 
      91                 :            : template <bool ref_count>
      92                 :       1182 : std::vector<Node> NodeTemplateTrie<ref_count>::getLeaves(size_t depth) const
      93                 :            : {
      94 [ -  + ][ -  + ]:       1182 :   Assert(depth > 0);
                 [ -  - ]
      95                 :       1182 :   std::vector<Node> vec;
      96                 :       1182 :   std::vector<std::pair<const NodeTemplateTrie<ref_count>*, size_t>> visit;
      97                 :       1182 :   visit.emplace_back(this, depth);
      98                 :            :   do
      99                 :            :   {
     100                 :       2578 :     std::pair<const NodeTemplateTrie<ref_count>*, size_t> curr = visit.back();
     101                 :       2578 :     visit.pop_back();
     102                 :       2578 :     size_t currDepth = curr.second;
     103         [ +  + ]:       3974 :     for (const std::pair<const NodeTemplate<ref_count>,
     104                 :       2578 :                          NodeTemplateTrie<ref_count>>& p : curr.first->d_data)
     105                 :            :     {
     106         [ +  + ]:       2578 :       if (currDepth == 0)
     107                 :            :       {
     108                 :            :         // we are at a leaf
     109                 :       1182 :         vec.push_back(p.first);
     110                 :       1182 :         break;
     111                 :            :       }
     112                 :       1396 :       visit.emplace_back(&p.second, currDepth - 1);
     113                 :            :     }
     114         [ +  + ]:       2578 :   } while (!visit.empty());
     115                 :       2364 :   return vec;
     116                 :       1182 : }
     117                 :            : 
     118                 :            : template std::vector<Node> NodeTemplateTrie<false>::getLeaves(
     119                 :            :     size_t depth) const;
     120                 :            : template std::vector<Node> NodeTemplateTrie<true>::getLeaves(
     121                 :            :     size_t depth) const;
     122                 :            : 
     123                 :            : }  // namespace cvc5::internal