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 
29 namespace CVC4 {
30 namespace expr {
31 
32 /**
33  * Check if the node n has a subterm t.
34  * @param n The node to search in
35  * @param t The subterm to search for
36  * @param strict If true, a term is not considered to be a subterm of itself
37  * @return true iff t is a subterm in n
38  */
39 bool hasSubterm(TNode n, TNode t, bool strict = false);
40 
41 /**
42  * Check if the node n has >1 occurrences of a subterm t.
43  */
44 bool hasSubtermMulti(TNode n, TNode t);
45 
46 /**
47  * Returns true iff the node n contains a bound variable, that is a node of
48  * kind BOUND_VARIABLE. This bound variable may or may not be free.
49  * @param n The node under investigation
50  * @return true iff this node contains a bound variable
51  */
52 bool hasBoundVar(TNode n);
53 
54 /**
55  * Returns true iff the node n contains a free variable, that is, a node
56  * of kind BOUND_VARIABLE that is not bound in n.
57  * @param n The node under investigation
58  * @return true iff this node contains a free variable.
59  */
60 bool hasFreeVar(TNode n);
61 
62 /**
63  * Get the free variables in n, that is, the subterms of n of kind
64  * BOUND_VARIABLE that are not bound in n, adds these to fvs.
65  * @param n The node under investigation
66  * @param fvs The set which free variables are added to
67  * @param computeFv If this flag is false, then we only return true/false and
68  * do not add to fvs.
69  * @return true iff this node contains a free variable.
70  */
71 bool getFreeVariables(TNode n,
72                       std::unordered_set<Node, NodeHashFunction>& fvs,
73                       bool computeFv = true);
74 
75 /**
76  * For term n, this function collects the symbols that occur as a subterms
77  * of n. A symbol is a variable that does not have kind BOUND_VARIABLE.
78  * @param n The node under investigation
79  * @param syms The set which the symbols of n are added to
80  */
81 void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms);
82 /** Same as above, with a visited cache */
83 void getSymbols(TNode n,
84                 std::unordered_set<Node, NodeHashFunction>& syms,
85                 std::unordered_set<TNode, TNodeHashFunction>& visited);
86 /**
87  * Substitution of Nodes in a capture avoiding way.
88  */
89 Node substituteCaptureAvoiding(TNode n, Node src, Node dest);
90 
91 /**
92  * Simultaneous substitution of Nodes in a capture avoiding way.  Elements in
93  * source will be replaced by their corresponding element in dest.  Both
94  * vectors should have the same size.
95  */
96 Node substituteCaptureAvoiding(TNode n,
97                                std::vector<Node>& src,
98                                std::vector<Node>& dest);
99 
100 }  // namespace expr
101 }  // namespace CVC4
102 
103 #endif
104