1 /********************* */
2 /*! \file node_algorithm.h
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
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 * @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
52 bool hasSubtermKind(Kind k
, Node n
);
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
59 bool hasSubtermKinds(const std::unordered_set
<Kind
, kind::KindHashFunction
>& ks
,
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
69 bool hasSubterm(TNode n
, const std::vector
<Node
>& t
, bool strict
= false);
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
77 bool hasBoundVar(TNode n
);
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.
85 bool hasFreeVar(TNode n
);
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
91 * @param n The node under investigation
92 * @return true iff this node contains a closure.
94 bool hasClosure(Node n
);
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
103 * @return true iff this node contains a free variable.
105 bool getFreeVariables(TNode n
,
106 std::unordered_set
<Node
, NodeHashFunction
>& fvs
,
107 bool computeFv
= true);
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.
115 bool getVariables(TNode n
, std::unordered_set
<TNode
, TNodeHashFunction
>& vs
);
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
123 void getSymbols(TNode n
, std::unordered_set
<Node
, NodeHashFunction
>& syms
);
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.
132 void getSymbols(TNode n
,
133 std::unordered_set
<Node
, NodeHashFunction
>& syms
,
134 std::unordered_set
<TNode
, TNodeHashFunction
>& visited
);
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
142 void getOperatorsMap(
144 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>>& ops
);
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.
153 void getOperatorsMap(
155 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>>& ops
,
156 std::unordered_set
<TNode
, TNodeHashFunction
>& visited
);
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.
166 Node
substituteCaptureAvoiding(TNode n
, Node src
, Node dest
);
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.
174 Node
substituteCaptureAvoiding(TNode n
,
175 std::vector
<Node
>& src
,
176 std::vector
<Node
>& dest
);
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.
185 void getComponentTypes(
186 TypeNode t
, std::unordered_set
<TypeNode
, TypeNodeHashFunction
>& types
);
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:
194 * n1 * subs = n2 (where * denotes application of substitution).
196 * For example, given:
197 * n1 = (+ a (* x 2)) (x denotes a free variable)
199 * a call to match should return `true` with subs = {(x, b)}
201 * @param n1 the term (containing free vars) to compare an instance term
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`
209 std::unordered_map
<Node
, Node
, NodeHashFunction
>& subs
);