From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 17 Mar 2022 04:51:37 +0000 (-0700)
Subject: api: Fix documentation for UNINTERPRETED_SORT_VALUE kind. (#8330)
X-Git-Tag: cvc5-1.0.0~231
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8d3f80a5b6237037b2620b477b20187f7c37caea;p=cvc5.git

api: Fix documentation for UNINTERPRETED_SORT_VALUE kind. (#8330)
---

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index e4ddcaa00..414b0c093 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -64,14 +64,11 @@ enum Kind : int32_t
   /* Builtin --------------------------------------------------------------- */
 
   /**
-   * Abstract value.
+   * The value of an uninterpreted constant.
    *
-   * Parameters:
-   *   - 1: Index of the abstract value
-   *
-   * Create with:
-   *   - `Solver::mkUninterpretedSortValue(const std::string& index) const`
-   *   - `Solver::mkUninterpretedSortValue(uint64_t index) const`
+   * @note May be returned as the result of an API call, but terms of this kind
+   *       may not be created explicitly via the API. Terms of this kind may
+   *       further not appear in assertions.
    */
   UNINTERPRETED_SORT_VALUE,
 #if 0