1 /********************* */
2 /*! \file node_algorithm.h
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
12 ** \brief Common algorithms on nodes
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.
19 #include "cvc4_private.h"
21 #ifndef CVC4__EXPR__NODE_ALGORITHM_H
22 #define CVC4__EXPR__NODE_ALGORITHM_H
24 #include <unordered_map>
27 #include "expr/node.h"
28 #include "expr/type_node.h"
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
40 bool hasSubterm(TNode n
, TNode t
, bool strict
= false);
43 * Check if the node n has >1 occurrences of a subterm t.
45 bool hasSubtermMulti(TNode n
, TNode t
);
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
53 bool hasBoundVar(TNode n
);
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.
61 bool hasFreeVar(TNode n
);
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
70 * @return true iff this node contains a free variable.
72 bool getFreeVariables(TNode n
,
73 std::unordered_set
<Node
, NodeHashFunction
>& fvs
,
74 bool computeFv
= true);
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.
82 bool getVariables(TNode n
, std::unordered_set
<TNode
, TNodeHashFunction
>& vs
);
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
90 void getSymbols(TNode n
, std::unordered_set
<Node
, NodeHashFunction
>& syms
);
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.
99 void getSymbols(TNode n
,
100 std::unordered_set
<Node
, NodeHashFunction
>& syms
,
101 std::unordered_set
<TNode
, TNodeHashFunction
>& visited
);
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
109 void getOperatorsMap(
111 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>>& ops
);
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.
120 void getOperatorsMap(
122 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>>& ops
,
123 std::unordered_set
<TNode
, TNodeHashFunction
>& visited
);
126 * Substitution of Nodes in a capture avoiding way.
128 Node
substituteCaptureAvoiding(TNode n
, Node src
, Node dest
);
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.
135 Node
substituteCaptureAvoiding(TNode n
,
136 std::vector
<Node
>& src
,
137 std::vector
<Node
>& dest
);