2 files changed, 20 insertions, 0 deletions
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`
    */