From 2dfa487a5636b79b15afb5887b8859a0487242ed Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 4 Apr 2022 18:01:56 -0700
Subject: [PATCH] api: Fixes in docs for DatatypeConstructor. (#8561)

---
 src/api/cpp/cvc5.h                            | 16 +++--
 .../io/github/cvc5/DatatypeConstructor.java   | 65 ++++++++++---------
 src/api/python/cvc5.pxi                       |  9 +--
 3 files changed, 49 insertions(+), 41 deletions(-)

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index a2faf5a10..4fb86e25d 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2142,9 +2142,11 @@ class CVC5_EXPORT DatatypeConstructor
 
   /**
    * Get the constructor term of this datatype constructor whose return
-   * type is retSort. This method is intended to be used on constructors of
-   * parametric datatypes and can be seen as returning the constructor
-   * term that has been explicitly cast to the given sort.
+   * type is `retSort`.
+   *
+   * This method is intended to be used on constructors of parametric datatypes
+   * and can be seen as returning the constructor term that has been explicitly
+   * cast to the given sort.
    *
    * This method is required for constructors of parametric datatypes whose
    * return type cannot be determined by type inference. For example, given:
@@ -2166,12 +2168,12 @@ class CVC5_EXPORT DatatypeConstructor
    * \endverbatim
    *
    * This method is equivalent of applying the above, where this
-   * DatatypeConstructor is the one corresponding to nil, and retSort is
+   * DatatypeConstructor is the one corresponding to `nil`, and `retSort` is
    * `(List Int)`.
    *
-   * @note the returned constructor term `t` is the constructor, while
-   *       `Solver::mkTerm(APPLY_CONSTRUCTOR, {t})` is used to construct the
-   *       above (nullary) application of nil.
+   * @note The returned constructor term `t` is used to construct the above
+   *       (nullary) application of `nil` with
+   *       `Solver::mkTerm(APPLY_CONSTRUCTOR, {t})`.
    *
    * @warning This method is experimental and may change in future versions.
    *
diff --git a/src/api/java/io/github/cvc5/DatatypeConstructor.java b/src/api/java/io/github/cvc5/DatatypeConstructor.java
index 5a07d2c5e..1b0c94fa9 100644
--- a/src/api/java/io/github/cvc5/DatatypeConstructor.java
+++ b/src/api/java/io/github/cvc5/DatatypeConstructor.java
@@ -38,7 +38,7 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
 
   // endregion
 
-  /** @return the name of this Datatype constructor. */
+  /** @return The name of this Datatype constructor. */
   public String getName()
   {
     return getName(pointer);
@@ -50,16 +50,18 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
    * Get the constructor term of this datatype constructor.
    *
    * Datatype constructors are a special class of function-like terms whose sort
-   * is datatype constructor ({@link Sort#isDatatypeConstructor()}). All datatype
-   * constructors, including nullary ones, should be used as the
-   * first argument to Terms whose kind is APPLY_CONSTRUCTOR. For example,
-   * the nil list is represented by the term (APPLY_CONSTRUCTOR nil), where
-   * nil is the term returned by this method.
+   * is datatype constructor ({@link Sort#isDatatypeConstructor()}). All
+   * datatype constructors, including nullary ones, should be used as the
+   * first argument to Terms whose kind is {@link Kind#APPLY_CONSTRUCTOR}.
+   * For example, the nil list is represented by the term
+   * {@code (APPLY_CONSTRUCTOR nil)}, where {@code nil} is the term returned by
+   * this method.
    *
    * @api.note This method should not be used for parametric datatypes. Instead,
-   *           use the method {@link DatatypeConstructor#getInstantiatedTerm(Sort)} below.
+   *           use method
+   *           {@link DatatypeConstructor#getInstantiatedTerm(Sort)} below.
    *
-   * @return the constructor term
+   * @return The constructor term.
    */
   public Term getTerm()
   {
@@ -71,28 +73,31 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
 
   /**
    * Get the constructor term of this datatype constructor whose return
-   * type is retSort. This method is intended to be used on constructors of
-   * parametric datatypes and can be seen as returning the constructor
-   * term that has been explicitly cast to the given sort.
+   * type is {@code retSort}.
+   *
+   * This method is intended to be used on constructors of parametric datatypes
+   * and can be seen as returning the constructor term that has been explicitly
+   * cast to the given sort.
    *
    * This method is required for constructors of parametric datatypes whose
    * return type cannot be determined by type inference. For example, given:
-   *   (declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T))))))
+   *   {@code (declare-datatype List (par (T) ((nil) (cons (head T)
+   *          (tail (List T))))))}
    * The type of nil terms need to be provided by the user. In SMT version 2.6,
    * this is done via the syntax for qualified identifiers:
-   *   (as nil (List Int))
+   *   {@code (as nil (List Int))}
    * This method is equivalent of applying the above, where this
-   * DatatypeConstructor is the one corresponding to nil, and retSort is
-   * (List Int).
+   * DatatypeConstructor is the one corresponding to {@code nil}, and
+   * {@code retSort} is {@code (List Int)}.
    *
-   * Furthermore note that the returned constructor term t is the constructor,
-   * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above
-   * (nullary) application of nil.
+   * @api.note The returned constructor term {@code t} is used to construct the
+   *           above (nullary) application of {@code nil} with
+   *           {@code Solver.mkTerm(APPLY_CONSTRUCTOR, new Term[] {t})}.
    *
    * @api.note This method is experimental and may change in future versions.
    *
-   * @param retSort the desired return sort of the constructor
-   * @return the constructor term
+   * @param retSort The desired return sort of the constructor.
+   * @return The constructor term.
    */
   public Term getInstantiatedTerm(Sort retSort)
   {
@@ -106,10 +111,10 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
    * Get the tester term of this datatype constructor.
    *
    * Similar to constructors, testers are a class of function-like terms of
-   * tester sort ({@link Sort#isDatatypeTester()}), and should be used as the first
-   * argument of Terms of kind APPLY_TESTER.
+   * tester sort ({@link Sort#isDatatypeTester()}), and should be used as the
+   * first argument of Terms of kind {@link Kind#APPLY_TESTER}.
    *
-   * @return the tester term
+   * @return The tester term.
    */
   public Term getTesterTerm()
   {
@@ -119,7 +124,7 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
   private native long getTesterTerm(long pointer);
 
   /**
-   * @return the number of selectors (so far) of this Datatype constructor.
+   * @return The number of selectors (so far) of this Datatype constructor.
    */
   public int getNumSelectors()
   {
@@ -129,8 +134,8 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
 
   /**
    * Get the DatatypeSelector at the given index
-   * @param index the given index i
-   * @return the i^th DatatypeSelector
+   * @param index The given index i.
+   * @return The i^th DatatypeSelector.
    */
   public DatatypeSelector getSelector(int index)
   {
@@ -143,8 +148,8 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
    * Get the datatype selector with the given name.
    * This is a linear search through the selectors, so in case of
    * multiple, similarly-named selectors, the first is returned.
-   * @param name the name of the datatype selector
-   * @return the first datatype selector with the given name
+   * @param name The name of the datatype selector.
+   * @return The first datatype selector with the given name.
    */
   public DatatypeSelector getSelector(String name)
   {
@@ -154,7 +159,7 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
   private native long getSelector(long pointer, String name);
 
   /**
-   * @return true if this DatatypeConstructor is a null object
+   * @return True if this DatatypeConstructor is a null object.
    */
   public boolean isNull()
   {
@@ -164,7 +169,7 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
   private native boolean isNull(long pointer);
 
   /**
-   * @return a string representation of this datatype constructor
+   * @return A string representation of this datatype constructor.
    */
   protected native String toString(long pointer);
 
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 88f8682d4..cfd150e43 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -314,9 +314,9 @@ cdef class DatatypeConstructor:
 
             .. note::
 
-                The returned constructor term ``t`` is the constructor, while
-                ``Solver.mkTerm(APPLY_CONSTRUCTOR, [t])`` is used to construct
-                the above (nullary) application of nil.
+                The returned constructor term ``t`` is used to construct the
+                above (nullary) application of ``nil`` with
+                ``Solver.mkTerm(APPLY_CONSTRUCTOR, t)``.
 
             .. warning:: This method is experimental and may change in future
                          versions.
@@ -334,7 +334,8 @@ cdef class DatatypeConstructor:
 
             Similar to constructors, testers are a class of function-like terms
             of tester sort (:py:meth:`Sort.isDatatypeTester`), and should
-            be used as the first argument of Terms of kind APPLY_TESTER.
+            be used as the first argument of Terms of kind
+            :py:obj:`Kind.APPLY_TESTER`.
 
             :return: The tester term for this constructor.
         """
-- 
2.30.2