src/expr/node_algorithm.h

   1 /*********************                                                        */
   2 /*! \file node_algorithm.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Andres Noetzli, Yoni Zohar
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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  * @param k The kind of node to check
  49  * @param n The node to search in.
  50  * @return true iff there is a term in n that has kind k
  51  */
  52 bool hasSubtermKind(Kind k, Node n);
  53
  54 /**
  55  * @param ks The kinds of node to check
  56  * @param n The node to search in.
  57  * @return true iff there is a term in n that has any kind ks
  58  */
  59 bool hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
  60                      Node n);
  61
  62 /**
  63  * Check if the node n has a subterm that occurs in t.
  64  * @param n The node to search in
  65  * @param t The set of subterms to search for
  66  * @param strict If true, a term is not considered to be a subterm of itself
  67  * @return true iff there is a term in t that is a subterm in n
  68  */
  69 bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict = false);
  70
  71 /**
  72  * Returns true iff the node n contains a bound variable, that is a node of
  73  * kind BOUND_VARIABLE. This bound variable may or may not be free.
  74  * @param n The node under investigation
  75  * @return true iff this node contains a bound variable
  76  */
  77 bool hasBoundVar(TNode n);
  78
  79 /**
  80  * Returns true iff the node n contains a free variable, that is, a node
  81  * of kind BOUND_VARIABLE that is not bound in n.
  82  * @param n The node under investigation
  83  * @return true iff this node contains a free variable.
  84  */
  85 bool hasFreeVar(TNode n);
  86
  87 /**
  88  * Returns true iff the node n contains a closure, that is, a node
  89  * whose kind is FORALL, EXISTS, WITNESS, LAMBDA, or any other closure currently
  90  * supported.
  91  * @param n The node under investigation
  92  * @return true iff this node contains a closure.
  93  */
  94 bool hasClosure(Node n);
  95
  96 /**
  97  * Get the free variables in n, that is, the subterms of n of kind
  98  * BOUND_VARIABLE that are not bound in n, adds these to fvs.
  99  * @param n The node under investigation
 100  * @param fvs The set which free variables are added to
 101  * @param computeFv If this flag is false, then we only return true/false and
 102  * do not add to fvs.
 103  * @return true iff this node contains a free variable.
 104  */
 105 bool getFreeVariables(TNode n,
 106                       std::unordered_set<Node, NodeHashFunction>& fvs,
 107                       bool computeFv = true);
 108
 109 /**
 110  * Get all variables in n.
 111  * @param n The node under investigation
 112  * @param vs The set which free variables are added to
 113  * @return true iff this node contains a free variable.
 114  */
 115 bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs);
 116
 117 /**
 118  * For term n, this function collects the symbols that occur as a subterms
 119  * of n. A symbol is a variable that does not have kind BOUND_VARIABLE.
 120  * @param n The node under investigation
 121  * @param syms The set which the symbols of n are added to
 122  */
 123 void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms);
 124
 125 /**
 126  * For term n, this function collects the symbols that occur as a subterms
 127  * of n. A symbol is a variable that does not have kind BOUND_VARIABLE.
 128  * @param n The node under investigation
 129  * @param syms The set which the symbols of n are added to
 130  * @param visited A cache to be used for visited nodes.
 131  */
 132 void getSymbols(TNode n,
 133                 std::unordered_set<Node, NodeHashFunction>& syms,
 134                 std::unordered_set<TNode, TNodeHashFunction>& visited);
 135
 136 /**
 137  * For term n, this function collects the operators that occur in n.
 138  * @param n The node under investigation
 139  * @param ops The map (from each type to operators of that type) which the
 140  * operators of n are added to
 141  */
 142 void getOperatorsMap(
 143     TNode n,
 144     std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops);
 145
 146 /**
 147  * For term n, this function collects the operators that occur in n.
 148  * @param n The node under investigation
 149  * @param ops The map (from each type to operators of that type) which the
 150  * operators of n are added to
 151  * @param visited A cache to be used for visited nodes.
 152  */
 153 void getOperatorsMap(
 154     TNode n,
 155     std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops,
 156     std::unordered_set<TNode, TNodeHashFunction>& visited);
 157
 158 /*
 159  * Substitution of Nodes in a capture avoiding way.
 160  * If x occurs free in n and it is substituted by a term t
 161  * and t includes some variable y that is bound in n,
 162  * then using alpha conversion y is replaced with a fresh bound variable
 163  * before the substitution.
 164  *
 165  */
 166 Node substituteCaptureAvoiding(TNode n, Node src, Node dest);
 167
 168 /**
 169  * Same as substituteCaptureAvoiding above, but with a
 170  * simultaneous substitution of a vector of variables.
 171  * Elements in source will be replaced by their corresponding element in dest.
 172  * Both vectors should have the same size.
 173  */
 174 Node substituteCaptureAvoiding(TNode n,
 175                                std::vector<Node>& src,
 176                                std::vector<Node>& dest);
 177
 178 /**
 179  * Get component types in type t. This adds all types that are subterms of t
 180  * when viewed as a term. For example, if t is (Array T1 T2), then
 181  * (Array T1 T2), T1 and T2 are component types of t.
 182  * @param t The type node under investigation
 183  * @param types The set which component types are added to.
 184  */
 185 void getComponentTypes(
 186     TypeNode t, std::unordered_set<TypeNode, TypeNodeHashFunction>& types);
 187
 188 /** match
 189  *
 190  * Given two terms `n1` and `n2` containing free variables, match returns true
 191  * if `n2` is an instance of `n1`. In which case, `subs` is a mapping from the
 192  * free variables in `n1` to corresponding terms in `n2` such that:
 193  *
 194  * n1 * subs = n2 (where * denotes application of substitution).
 195  *
 196  * For example, given:
 197  * n1 = (+ a (* x 2)) (x denotes a free variable)
 198  * n2 = (+ a (* b 2))
 199  * a call to match should return `true` with subs = {(x, b)}
 200  *
 201  * @param n1 the term (containing free vars) to compare an instance term
 202  * against
 203  * @param n2 the instance term in question
 204  * @param subs the mapping from free vars in `n1` to terms in `n2`
 205  * @return whether or not `n2` is an instance of `n1`
 206  */
 207 bool match(Node n1,
 208            Node n2,
 209            std::unordered_map<Node, Node, NodeHashFunction>& subs);
 210
 211 }  // namespace expr
 212 }  // namespace CVC4
 213
 214 #endif