From d61cf911d37ac6ddfec6b9a723a3152a88076e42 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 4 Apr 2022 18:03:09 -0700
Subject: [PATCH] api: Fixes in docs for Op. (#8565)

---
 src/api/cpp/cvc5.h                  | 19 +++++++++++--------
 src/api/java/io/github/cvc5/Op.java | 27 ++++++++++++++-------------
 2 files changed, 25 insertions(+), 21 deletions(-)

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 4fb86e25d..4f2bf0ba5 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -896,8 +896,9 @@ namespace cvc5 {
 
 /**
  * A cvc5 operator.
+ *
  * An operator is a term that represents certain operators, instantiated
- * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT.
+ * with its required parameters, e.g., a Term of kind #BITVECTOR_EXTRACT.
  */
 class CVC5_EXPORT Op
 {
@@ -918,19 +919,21 @@ class CVC5_EXPORT Op
 
   /**
    * Syntactic equality operator.
-   * Return true if both operators are syntactically identical.
-   * Both operators must belong to the same solver object.
+   *
+   * @note Both operators must belong to the same solver object.
+   *
    * @param t The operator to compare to for equality.
-   * @return True if the operators are equal.
+   * @return True if both operators are syntactically identical.
    */
   bool operator==(const Op& t) const;
 
   /**
    * Syntactic disequality operator.
-   * Return true if both operators differ syntactically.
-   * Both terms must belong to the same solver object.
+   *
+   * @note Both terms must belong to the same solver object.
+   *
    * @param t The operator to compare to for disequality.
-   * @return True if operators are disequal.
+   * @return True if operators differ syntactically.
    */
   bool operator!=(const Op& t) const;
 
@@ -955,7 +958,7 @@ class CVC5_EXPORT Op
   size_t getNumIndices() const;
 
   /**
-   * Get the index at position i.
+   * Get the index at position `i`.
    * @param i The position of the index to return.
    * @return The index at position i.
    */
diff --git a/src/api/java/io/github/cvc5/Op.java b/src/api/java/io/github/cvc5/Op.java
index 30dd50229..d5a123bfc 100644
--- a/src/api/java/io/github/cvc5/Op.java
+++ b/src/api/java/io/github/cvc5/Op.java
@@ -17,8 +17,10 @@ package io.github.cvc5;
 
 /**
  * A cvc5 operator.
+ *
  * An operator is a term that represents certain operators, instantiated
- * with its required parameters, e.g., a term of kind {@link Kind#BITVECTOR_EXTRACT}.
+ * with its required parameters, e.g., a Term of kind
+ * {@link Kind#BITVECTOR_EXTRACT}.
  */
 public class Op extends AbstractPointer
 {
@@ -39,10 +41,9 @@ public class Op extends AbstractPointer
 
   /**
    * Syntactic equality operator.
-   * Return true if both operators are syntactically identical.
-   * Both operators must belong to the same solver object.
-   * @param t the operator to compare to for equality
-   * @return true if the operators are equal
+   * @api.note Both operators must belong to the same solver object.
+   * @param t The operator to compare to for equality.
+   * @return True If the operators are syntactically identical.
    */
   @Override
   public boolean equals(Object t)
@@ -57,7 +58,7 @@ public class Op extends AbstractPointer
   private native boolean equals(long pointer1, long pointer2);
 
   /**
-   * @return the kind of this operator
+   * @return The Kind of this operator.
    */
   public Kind getKind()
   {
@@ -76,7 +77,7 @@ public class Op extends AbstractPointer
   private native int getKind(long pointer);
 
   /**
-   * @return true if this operator is a null term
+   * @return True If this operator is a null term.
    */
   public boolean isNull()
   {
@@ -86,7 +87,7 @@ public class Op extends AbstractPointer
   private native boolean isNull(long pointer);
 
   /**
-   * @return true iff this operator is indexed
+   * @return True Iff this operator is indexed.
    */
   public boolean isIndexed()
   {
@@ -96,7 +97,7 @@ public class Op extends AbstractPointer
   private native boolean isIndexed(long pointer);
 
   /**
-   * @return the number of indices of this op
+   * @return The Number of indices of this op.
    */
   public int getNumIndices()
   {
@@ -106,9 +107,9 @@ public class Op extends AbstractPointer
   private native int getNumIndices(long pointer);
 
   /**
-   * Get the index at position i.
-   * @param i the position of the index to return
-   * @return the index at position i
+   * Get the index at position {@code i}.
+   * @param i The position of the index to return.
+   * @return The Index at position i.
    */
   public Term get(int i) throws CVC5ApiException
   {
@@ -120,7 +121,7 @@ public class Op extends AbstractPointer
   private native long get(long pointer, int i);
 
   /**
-   * @return a string representation of this operator
+   * @return A String representation of this operator.
    */
   protected native String toString(long pointer);
 }
-- 
2.30.2