From 8d3f80a5b6237037b2620b477b20187f7c37caea Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 16 Mar 2022 21:51:37 -0700 Subject: [PATCH] api: Fix documentation for UNINTERPRETED_SORT_VALUE kind. (#8330) --- src/api/cpp/cvc5_kind.h | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) 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 -- 2.30.2