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                 :            :  * A simple visitor for nodes.
      11                 :            :  */
      12                 :            : 
      13                 :            : #pragma once
      14                 :            : 
      15                 :            : #include <vector>
      16                 :            : 
      17                 :            : #include "cvc5_private.h"
      18                 :            : #include "expr/node.h"
      19                 :            : 
      20                 :            : namespace cvc5::internal {
      21                 :            : 
      22                 :            : /**
      23                 :            :  * Traverses the nodes reverse-topologically (children before parents),
      24                 :            :  * calling the visitor in order.
      25                 :            :  */
      26                 :            : template <typename Visitor>
      27                 :            : class NodeVisitor
      28                 :            : {
      29                 :            :  public:
      30                 :            :   /**
      31                 :            :    * Element of the stack.
      32                 :            :    */
      33                 :            :   struct stack_element
      34                 :            :   {
      35                 :            :     /** The node to be visited */
      36                 :            :     TNode d_node;
      37                 :            :     /** The parent of the node */
      38                 :            :     TNode d_parent;
      39                 :            :     /** Have the children been queued up for visitation */
      40                 :            :     bool d_childrenAdded;
      41                 :   13204460 :     stack_element(TNode node, TNode parent)
      42                 :   13204460 :         : d_node(node), d_parent(parent), d_childrenAdded(false)
      43                 :            :     {
      44                 :   13204460 :     }
      45                 :            :   }; /* struct preprocess_stack_element */
      46                 :            : 
      47                 :            :   /**
      48                 :            :    * Performs the traversal.
      49                 :            :    */
      50                 :    2262999 :   static typename Visitor::return_type run(Visitor& visitor, TNode node)
      51                 :            :   {
      52                 :            :     // Notify of a start
      53                 :    2262999 :     visitor.start(node);
      54                 :            : 
      55                 :            :     // Do a reverse-topological sort of the subexpressions
      56                 :    2262999 :     std::vector<stack_element> toVisit;
      57                 :    2262999 :     toVisit.push_back(stack_element(node, node));
      58         [ +  + ]:   53883701 :     while (!toVisit.empty())
      59                 :            :     {
      60                 :   25810351 :       stack_element& stackHead = toVisit.back();
      61                 :            :       // The current node we are processing
      62                 :   25810351 :       TNode current = stackHead.d_node;
      63                 :   25810351 :       TNode parent = stackHead.d_parent;
      64                 :            : 
      65         [ +  + ]:   25810351 :       if (visitor.alreadyVisited(current, parent))
      66                 :            :       {
      67                 :            :         // If already visited, we're done
      68                 :     598543 :         toVisit.pop_back();
      69                 :            :       }
      70         [ +  + ]:   25211808 :       else if (stackHead.d_childrenAdded)
      71                 :            :       {
      72                 :            :         // Call the visitor
      73                 :   12605927 :         visitor.visit(current, parent);
      74                 :            :         // Done with this node, remove from the stack
      75                 :   12605879 :         toVisit.pop_back();
      76                 :            :       }
      77                 :            :       else
      78                 :            :       {
      79                 :            :         // Mark that we have added the children
      80                 :   12605913 :         stackHead.d_childrenAdded = true;
      81                 :            :         // We need to add the children
      82                 :   25463801 :         for (TNode::iterator child_it = current.begin();
      83         [ +  + ]:   25463801 :              child_it != current.end();
      84                 :   12857888 :              ++child_it)
      85                 :            :         {
      86                 :   12857888 :           TNode childNode = *child_it;
      87         [ +  + ]:   12857888 :           if (!visitor.alreadyVisited(childNode, current))
      88                 :            :           {
      89                 :   10941461 :             toVisit.push_back(stack_element(childNode, current));
      90                 :            :           }
      91                 :            :         }
      92                 :            :       }
      93                 :            :     }
      94                 :            : 
      95                 :            :     // Notify that we're done
      96                 :    4525966 :     return visitor.done(node);
      97                 :    2262999 :   }
      98                 :            : 
      99                 :            : }; /* class NodeVisitor<> */
     100                 :            : 
     101                 :            : }  // namespace cvc5::internal