diff options
| -rw-r--r-- | src/expr/node_algorithm.h | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 3686b6686..17d7d951b 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -122,15 +122,21 @@ void getOperatorsMap( std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops, std::unordered_set<TNode, TNodeHashFunction>& visited); -/** +/* * Substitution of Nodes in a capture avoiding way. + * If x occurs free in n and it is substituted by a term t + * and t includes some variable y that is bound in n, + * then using alpha conversion y is replaced with a fresh bound variable + * before the substitution. + * */ Node substituteCaptureAvoiding(TNode n, Node src, Node dest); /** - * Simultaneous substitution of Nodes in a capture avoiding way. Elements in - * source will be replaced by their corresponding element in dest. Both - * vectors should have the same size. + * Same as substituteCaptureAvoiding above, but with a + * simultaneous substitution of a vector of variables. + * Elements in source will be replaced by their corresponding element in dest. + * Both vectors should have the same size. */ Node substituteCaptureAvoiding(TNode n, std::vector<Node>& src, |