More details in substitution function documentation (#3244)

diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 3686b6686c48e7f5b0adc914fa606d09d7a33b80..17d7d951b61373ce502975b7a388ae44ba9772bb 100644 (file)
--- 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,