Branch data     Line data    Source code

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