src/expr/node_algorithm.h

   1 /*********************                                                        */
   2 /*! \file node_algorithm.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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.\endverbatim
  11  **
  12  ** \brief Common algorithms on nodes
  13  **
  14  ** This file implements common algorithms applied to nodes, such as checking if
  15  ** a node contains a free or a bound variable. This file should generally only
  16  ** be included in source files.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef CVC4__EXPR__NODE_ALGORITHM_H
  22 #define CVC4__EXPR__NODE_ALGORITHM_H
  23
  24 #include <unordered_map>
  25 #include <vector>
  26
  27 #include "expr/node.h"
  28 #include "expr/type_node.h"
  29
  30 namespace CVC4 {
  31 namespace expr {
  32
  33 /**
  34  * Check if the node n has a subterm t.
  35  * @param n The node to search in
  36  * @param t The subterm to search for
  37  * @param strict If true, a term is not considered to be a subterm of itself
  38  * @return true iff t is a subterm in n
  39  */
  40 bool hasSubterm(TNode n, TNode t, bool strict = false);
  41
  42 /**
  43  * Check if the node n has >1 occurrences of a subterm t.
  44  */
  45 bool hasSubtermMulti(TNode n, TNode t);
  46
  47 /**
  48  * Returns true iff the node n contains a bound variable, that is a node of
  49  * kind BOUND_VARIABLE. This bound variable may or may not be free.
  50  * @param n The node under investigation
  51  * @return true iff this node contains a bound variable
  52  */
  53 bool hasBoundVar(TNode n);
  54
  55 /**
  56  * Returns true iff the node n contains a free variable, that is, a node
  57  * of kind BOUND_VARIABLE that is not bound in n.
  58  * @param n The node under investigation
  59  * @return true iff this node contains a free variable.
  60  */
  61 bool hasFreeVar(TNode n);
  62
  63 /**
  64  * Get the free variables in n, that is, the subterms of n of kind
  65  * BOUND_VARIABLE that are not bound in n, adds these to fvs.
  66  * @param n The node under investigation
  67  * @param fvs The set which free variables are added to
  68  * @param computeFv If this flag is false, then we only return true/false and
  69  * do not add to fvs.
  70  * @return true iff this node contains a free variable.
  71  */
  72 bool getFreeVariables(TNode n,
  73                       std::unordered_set<Node, NodeHashFunction>& fvs,
  74                       bool computeFv = true);
  75
  76 /**
  77  * Get all variables in n.
  78  * @param n The node under investigation
  79  * @param vs The set which free variables are added to
  80  * @return true iff this node contains a free variable.
  81  */
  82 bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs);
  83
  84 /**
  85  * For term n, this function collects the symbols that occur as a subterms
  86  * of n. A symbol is a variable that does not have kind BOUND_VARIABLE.
  87  * @param n The node under investigation
  88  * @param syms The set which the symbols of n are added to
  89  */
  90 void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms);
  91
  92 /**
  93  * For term n, this function collects the symbols that occur as a subterms
  94  * of n. A symbol is a variable that does not have kind BOUND_VARIABLE.
  95  * @param n The node under investigation
  96  * @param syms The set which the symbols of n are added to
  97  * @param visited A cache to be used for visited nodes.
  98  */
  99 void getSymbols(TNode n,
 100                 std::unordered_set<Node, NodeHashFunction>& syms,
 101                 std::unordered_set<TNode, TNodeHashFunction>& visited);
 102
 103 /**
 104  * For term n, this function collects the operators that occur in n.
 105  * @param n The node under investigation
 106  * @param ops The map (from each type to operators of that type) which the
 107  * operators of n are added to
 108  */
 109 void getOperatorsMap(
 110     TNode n,
 111     std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops);
 112
 113 /**
 114  * For term n, this function collects the operators that occur in n.
 115  * @param n The node under investigation
 116  * @param ops The map (from each type to operators of that type) which the
 117  * operators of n are added to
 118  * @param visited A cache to be used for visited nodes.
 119  */
 120 void getOperatorsMap(
 121     TNode n,
 122     std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops,
 123     std::unordered_set<TNode, TNodeHashFunction>& visited);
 124
 125 /**
 126  * Substitution of Nodes in a capture avoiding way.
 127  */
 128 Node substituteCaptureAvoiding(TNode n, Node src, Node dest);
 129
 130 /**
 131  * Simultaneous substitution of Nodes in a capture avoiding way.  Elements in
 132  * source will be replaced by their corresponding element in dest.  Both
 133  * vectors should have the same size.
 134  */
 135 Node substituteCaptureAvoiding(TNode n,
 136                                std::vector<Node>& src,
 137                                std::vector<Node>& dest);
 138
 139 }  // namespace expr
 140 }  // namespace CVC4
 141
 142 #endif