More details in substitution function documentation (#3244)

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,