From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 27 Jan 2022 23:35:13 +0000 (-0600)
Subject: Document substitute in API (#7904)
X-Git-Tag: cvc5-1.0.0~498
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8e3892ebe308712ad645848b551219f95e550b61;p=cvc5.git

Document substitute in API (#7904)
---

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index ad0054606..901bc9f64 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -589,6 +589,13 @@ class CVC5_EXPORT Sort
    * Substitution of Sorts.
    * @param sort the subsort to be substituted within this sort.
    * @param replacement the sort replacing the substituted subsort.
+   *
+   * Note that this replacement is applied during a pre-order traversal and
+   * only once to the sort. It is not run until fix point.
+   *
+   * For example,
+   * (Array A B).substitute({A, C}, {(Array C D), (Array A B)}) will
+   * return (Array (Array C D) B).
    */
   Sort substitute(const Sort& sort, const Sort& replacement) const;
 
@@ -596,6 +603,11 @@ class CVC5_EXPORT Sort
    * Simultaneous substitution of Sorts.
    * @param sorts the subsorts to be substituted within this sort.
    * @param replacements the sort replacing the substituted subsorts.
+   *
+   * Note that this replacement is applied during a pre-order traversal and
+   * only once to the sort. It is not run until fix point. In the case that
+   * sorts contains duplicates, the replacement earliest in the vector takes
+   * priority.
    */
   Sort substitute(const std::vector<Sort>& sorts,
                   const std::vector<Sort>& replacements) const;
@@ -1130,13 +1142,23 @@ class CVC5_EXPORT Term
   Sort getSort() const;
 
   /**
-   * @return the result of replacing 'term' by 'replacement' in this term
+   * @return the result of replacing 'term' by 'replacement' in this term.
+   *
+   * Note that this replacement is applied during a pre-order traversal and
+   * only once to the term. It is not run until fix point.
    */
   Term substitute(const Term& term, const Term& replacement) const;
 
   /**
    * @return the result of simultaneously replacing 'terms' by 'replacements'
    * in this term
+   *
+   * Note that this replacement is applied during a pre-order traversal and
+   * only once to the term. It is not run until fix point. In the case that
+   * terms contains duplicates, the replacement earliest in the vector takes
+   * priority. For example, calling substitute on f(x,y) with
+   *   terms = { x, z }, replacements = { g(z), w }
+   * results in the term f(g(z),y).
    */
   Term substitute(const std::vector<Term>& terms,
                   const std::vector<Term>& replacements) const;
diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java
index 326920a4e..549ad6c25 100644
--- a/src/api/java/io/github/cvc5/api/Sort.java
+++ b/src/api/java/io/github/cvc5/api/Sort.java
@@ -454,6 +454,9 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
    * Substitution of Sorts.
    * @param sort the subsort to be substituted within this sort.
    * @param replacement the sort replacing the substituted subsort.
+   *
+   * Note that this replacement is applied during a pre-order traversal and
+   * only once to the sort. It is not run until fix point.
    */
   public Sort substitute(Sort sort, Sort replacement)
   {
@@ -467,6 +470,15 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
    * Simultaneous substitution of Sorts.
    * @param sorts the subsorts to be substituted within this sort.
    * @param replacements the sort replacing the substituted subsorts.
+   *
+   * Note that this replacement is applied during a pre-order traversal and
+   * only once to the sort. It is not run until fix point. In the case that
+   * sorts contains duplicates, the replacement earliest in the list takes
+   * priority.
+   *
+   * For example,
+   * (Array A B).substitute({A, C}, {(Array C D), (Array A B)}) will
+   * return (Array (Array C D) B).
    */
   public Sort substitute(Sort[] sorts, Sort[] replacements)
   {
diff --git a/src/api/java/io/github/cvc5/api/Term.java b/src/api/java/io/github/cvc5/api/Term.java
index be792548e..7fddc49be 100644
--- a/src/api/java/io/github/cvc5/api/Term.java
+++ b/src/api/java/io/github/cvc5/api/Term.java
@@ -137,6 +137,9 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable<
 
   /**
    * @return the result of replacing 'term' by 'replacement' in this term
+   *
+   * Note that this replacement is applied during a pre-order traversal and
+   * only once to the term. It is not run until fix point.
    */
   public Term substitute(Term term, Term replacement)
   {
@@ -149,6 +152,13 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable<
   /**
    * @return the result of simultaneously replacing 'terms' by 'replacements'
    * in this term
+   *
+   * Note that this replacement is applied during a pre-order traversal and
+   * only once to the term. It is not run until fix point. In the case that
+   * terms contains duplicates, the replacement earliest in the vector takes
+   * priority. For example, calling substitute on f(x,y) with
+   *   terms = { x, z }, replacements = { g(z), w }
+   * results in the term f(g(z),y).
    */
   public Term substitute(List<Term> terms, List<Term> replacements)
   {
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index d5aedd0a4..10f697196 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2631,6 +2631,15 @@ cdef class Sort:
 
 	    :param sort_or_list_1: the subsort or subsorts to be substituted within this sort.
             :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort.
+
+        Note that this replacement is applied during a pre-order traversal and
+        only once to the sort. It is not run until fix point. In the case that
+        sort_or_list_1 contains duplicates, the replacement earliest in the list
+        takes priority.
+
+        For example,
+        (Array A B) .substitute([A, C], [(Array C D), (Array A B)]) will
+        return (Array (Array C D) B).
         """
 
         # The resulting sort after substitution
@@ -2953,6 +2962,13 @@ cdef class Term:
     def substitute(self, term_or_list_1, term_or_list_2):
         """
 	   :return: the result of simultaneously replacing the term(s) stored in ``term_or_list_1`` by the term(s) stored in ``term_or_list_2`` in this term.
+	   
+      Note that this replacement is applied during a pre-order traversal and
+      only once to the term. It is not run until fix point. In the case that
+      terms contains duplicates, the replacement earliest in the list takes
+      priority. For example, calling substitute on f(x,y) with
+        term_or_list_1 = [ x, z ], term_or_list_2 = [ g(z), w ]
+      results in the term f(g(z),y).
 	"""
         # The resulting term after substitution
         cdef Term term = Term(self.solver)