Branch data     Line data    Source code

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