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                 :            :  * Iterators for traversing nodes.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "node_traversal.h"
      14                 :            : 
      15                 :            : #include <functional>
      16                 :            : 
      17                 :            : namespace cvc5::internal {
      18                 :            : 
      19                 :     169533 : NodeDfsIterator::NodeDfsIterator(TNode n,
      20                 :            :                                  VisitOrder order,
      21                 :     169533 :                                  std::function<bool(TNode)> skipIf)
      22                 :     339066 :     : d_stack{n},
      23                 :     169533 :       d_visited(),
      24                 :     169533 :       d_order(order),
      25                 :     169533 :       d_current(TNode()),
      26                 :     169533 :       d_skipIf(skipIf)
      27                 :            : {
      28                 :     169533 : }
      29                 :            : 
      30                 :     169533 : NodeDfsIterator::NodeDfsIterator(VisitOrder order)
      31                 :     169533 :     : d_stack(),
      32                 :     169533 :       d_visited(),
      33                 :     169533 :       d_order(order),
      34                 :     169533 :       d_current(TNode()),
      35                 :     169533 :       d_skipIf([](TNode) { return false; })
      36                 :            : {
      37                 :     169533 : }
      38                 :            : 
      39                 :     173150 : NodeDfsIterator& NodeDfsIterator::operator++()
      40                 :            : {
      41                 :            :   // If we were just constructed, advance to first visit, **before**
      42                 :            :   // advancing past it to the next visit (below).
      43                 :     173150 :   initializeIfUninitialized();
      44                 :            : 
      45                 :            :   // Advance to the next visit
      46                 :     173150 :   advanceToNextVisit();
      47                 :     173150 :   return *this;
      48                 :            : }
      49                 :            : 
      50                 :          6 : NodeDfsIterator NodeDfsIterator::operator++(int)
      51                 :            : {
      52                 :          6 :   NodeDfsIterator copyOfOld(*this);
      53                 :          6 :   ++*this;
      54                 :          6 :   return copyOfOld;
      55                 :          0 : }
      56                 :            : 
      57                 :     173156 : TNode& NodeDfsIterator::operator*()
      58                 :            : {
      59                 :            :   // If we were just constructed, advance to first visit
      60                 :     173156 :   initializeIfUninitialized();
      61 [ -  + ][ -  + ]:     173156 :   Assert(!d_current.isNull());
                 [ -  - ]
      62                 :            : 
      63                 :     173156 :   return d_current;
      64                 :            : }
      65                 :            : 
      66                 :     342677 : bool NodeDfsIterator::operator==(NodeDfsIterator& other)
      67                 :            : {
      68                 :            :   // Unitialize this node, and the other, before comparing.
      69                 :     342677 :   initializeIfUninitialized();
      70                 :     342677 :   other.initializeIfUninitialized();
      71                 :            :   // The stack and current node uniquely represent traversal state. We need not
      72                 :            :   // use the scheduled node set.
      73                 :            :   //
      74                 :            :   // Users should not compare iterators for traversals of different nodes, or
      75                 :            :   // traversals with different skipIfs.
      76 [ -  + ][ -  + ]:     342677 :   Assert(d_order == other.d_order);
                 [ -  - ]
      77 [ +  + ][ +  + ]:     342677 :   return d_stack == other.d_stack && d_current == other.d_current;
      78                 :            : }
      79                 :            : 
      80                 :     342666 : bool NodeDfsIterator::operator!=(NodeDfsIterator& other)
      81                 :            : {
      82                 :     342666 :   return !(*this == other);
      83                 :            : }
      84                 :            : 
      85                 :     760778 : void NodeDfsIterator::advanceToNextVisit()
      86                 :            : {
      87                 :            :   // While a node is enqueued and we're not at the right visit type
      88         [ +  + ]:    1180771 :   while (!d_stack.empty())
      89                 :            :   {
      90                 :     593151 :     TNode back = d_stack.back();
      91                 :     593151 :     auto visitEntry = d_visited.find(back);
      92         [ +  + ]:     593151 :     if (visitEntry == d_visited.end())
      93                 :            :     {
      94                 :            :       // if we haven't pre-visited this node, pre-visit it
      95         [ +  + ]:     404922 :       if (d_skipIf(back))
      96                 :            :       {
      97                 :            :         // actually, skip it if the skip predicate says so...
      98                 :     231750 :         d_stack.pop_back();
      99                 :     231750 :         continue;
     100                 :            :       }
     101                 :     173172 :       d_visited[back] = false;
     102                 :     173172 :       d_current = back;
     103                 :            :       // Use integer underflow to reverse-iterate
     104         [ +  + ]:     423641 :       for (size_t n = back.getNumChildren(), i = n - 1; i < n; --i)
     105                 :            :       {
     106                 :     250469 :         d_stack.push_back(back[i]);
     107                 :            :       }
     108         [ +  + ]:     173172 :       if (d_order == VisitOrder::PREORDER)
     109                 :            :       {
     110                 :         24 :         return;
     111                 :            :       }
     112                 :            :     }
     113 [ +  + ][ +  + ]:     188229 :     else if (d_order == VisitOrder::PREORDER || visitEntry->second)
                 [ +  + ]
     114                 :            :     {
     115                 :            :       // if we're previsiting or we've already post-visited this node: skip it
     116                 :      15095 :       d_stack.pop_back();
     117                 :            :     }
     118                 :            :     else
     119                 :            :     {
     120                 :            :       // otherwise, this is a post-visit
     121                 :     173134 :       visitEntry->second = true;
     122                 :     173134 :       d_current = back;
     123                 :     173134 :       d_stack.pop_back();
     124                 :     173134 :       return;
     125                 :            :     }
     126    [ +  + ][ + ]:     593151 :   }
     127                 :            :   // We're at the end of the traversal: nullify the current node to agree
     128                 :            :   // with the "end" iterator.
     129                 :     587620 :   d_current = TNode();
     130                 :            : }
     131                 :            : 
     132                 :    1031660 : void NodeDfsIterator::initializeIfUninitialized()
     133                 :            : {
     134         [ +  + ]:    1031660 :   if (d_current.isNull())
     135                 :            :   {
     136                 :     587628 :     advanceToNextVisit();
     137                 :            :   }
     138                 :    1031660 : }
     139                 :            : 
     140                 :     169533 : NodeDfsIterable::NodeDfsIterable(TNode n,
     141                 :            :                                  VisitOrder order,
     142                 :     169533 :                                  std::function<bool(TNode)> skipIf)
     143                 :     169533 :     : d_node(n), d_order(order), d_skipIf(skipIf)
     144                 :            : {
     145                 :     169533 : }
     146                 :            : 
     147                 :     169533 : NodeDfsIterator NodeDfsIterable::begin() const
     148                 :            : {
     149                 :     169533 :   return NodeDfsIterator(d_node, d_order, d_skipIf);
     150                 :            : }
     151                 :            : 
     152                 :     169533 : NodeDfsIterator NodeDfsIterable::end() const
     153                 :            : {
     154                 :     169533 :   return NodeDfsIterator(d_order);
     155                 :            : }
     156                 :            : 
     157                 :            : }  // namespace cvc5::internal