From: yoni206 <yoni206@users.noreply.github.com>
Date: Wed, 4 Sep 2019 20:52:43 +0000 (-0700)
Subject: More details in substitution function documentation (#3244)
X-Git-Tag: cvc5-1.0.0~3979
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9d5aa1d53f715288acef81100e17908d838047a6;p=cvc5.git

More details in substitution function documentation (#3244)
---

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,