From 80cdf28298c9190506f37721492680f432ef635d Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 20 Oct 2021 15:56:40 -0700
Subject: [PATCH] api: Improve documentation for special cases with nullary
 ops. (#7433)

Fixes #7430.
---
 src/api/cpp/cvc5.h            | 13 +++++++++++++
 src/api/cpp/cvc5_kind.h       |  7 +++++++
 src/theory/sets/normal_form.h |  2 +-
 3 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index ded477a9d..e6a19c771 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -1353,6 +1353,8 @@ class CVC5_EXPORT Term
   std::pair<int64_t, uint64_t> getReal64Value() const;
   /**
    * @return true if the term is a rational value.
+   *
+   * Note that a term of kind PI is not considered to be a real value.
    */
   bool isRealValue() const;
   /**
@@ -1448,6 +1450,17 @@ class CVC5_EXPORT Term
 
   /**
    * @return true if the term is a set value.
+   *
+   * A term is a set value if it is considered to be a (canonical) constant set
+   * value.  A canonical set value is one whose AST is:
+   * ```
+   *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
+   * ```
+   * where `c1 ... cn` are values ordered by id such that `c1 > ... > cn` (see
+   * also @ref Term::operator>(const Term&) const).
+   *
+   * Note that a universe set term (kind UNIVERSE_SET) is not considered to be
+   * a set value.
    */
   bool isSetValue() const;
   /**
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 0ff05022f..fe87df934 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -766,6 +766,9 @@ enum CVC5_EXPORT Kind : int32_t
   /**
    * Pi constant.
    *
+   * Note that PI is considered a special symbol of sort Real, but is not
+   * a real value, i.e., `Term::isRealValue() const` will return false.
+   *
    * Create with:
    *   - `Solver::mkPi() const`
    *   - `Solver::mkTerm(Kind kind) const`
@@ -2228,6 +2231,10 @@ enum CVC5_EXPORT Kind : int32_t
    * Finite universe set.
    * All set variables must be interpreted as subsets of it.
    *
+   * Note that UNIVERSE_SET is considered a special symbol of the theory of
+   * sets and is not considered as a set value,
+   * i.e., `Term::isSetValue() const` will return false.
+   *
    * Create with:
    *   - `Solver::mkUniverseSet(const Sort& sort) const`
    */
diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
index eb839e1c0..35d06a510 100644
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -58,7 +58,7 @@ class NormalForm {
   }
 
   /**
-   * Returns true if n is considered a to be a (canonical) constant set value.
+   * Returns true if n is considered to be a (canonical) constant set value.
    * A canonical set value is one whose AST is:
    *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
    * where c1 ... cn are constants and the node identifier of these constants
-- 
2.30.2