api: Improve documentation for special cases with nullary ops. (#7433)

Fixes #7430.

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index ded477a9d191e899553f8b0fb83252e476cab5dc..e6a19c77185b256158604c37f5dcd4a7324e65ec 100644 (file)
--- 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 0ff05022f048a45f73df947d73d940c69a74341c..fe87df934780020f8897a96700e5b71c06effcbb 100644 (file)
--- 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 eb839e1c020fd90bfd102b5755d6dbfd148147f2..35d06a510fe76fd70b48d708da7de694550534ac 100644 (file)
--- 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