diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2019-09-04 13:52:43 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-04 15:52:43 -0500 |
commit | 9d5aa1d53f715288acef81100e17908d838047a6 (patch) | |
tree | 5621eade909231fa002a4b83613b586219b308ea /src | |
parent | d9ee2ae563b031547e76245d9f01fb24b95bc8cb (diff) |
More details in substitution function documentation (#3244)
Diffstat (limited to 'src')
-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, |