1 files changed, 30 insertions, 3 deletions
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 6c1a2256b..05423a952 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -134,15 +134,42 @@ enum CVC4_PUBLIC Kind : int32_t
    */
   LAMBDA,
   /**
-   * Hilbert choice (epsilon) expression.
+   * The syntax of a witness term is similar to a quantified formula except that
+   * only one bound variable is allowed.
+   * The term (witness ((x T)) F) returns an element x of type T
+   * and asserts F.
+   *
+   * The witness operator behaves like the description operator
+   * (see https://planetmath.org/hilbertsvarepsilonoperator) if there is no x
+   * that satisfies F. But if such x exists, the witness operator does not
+   * enforce the axiom that ensures uniqueness up to logical equivalence:
+   * forall x. F \equiv G => witness x. F =  witness x. G
+   *
+   * For example if there are 2 elements of type T that satisfy F, then the
+   * following formula is satisfiable:
+   * (distinct
+   *    (witness ((x Int)) F)
+   *    (witness ((x Int)) F))
+   *
+   * This kind is primarily used internally, but may be returned in models
+   * (e.g. for arithmetic terms in non-linear queries). However, it is not
+   * supported by the parser. Moreover, the user of the API should be cautious
+   * when using this operator. In general, all witness terms
+   * (witness ((x Int)) F) should be such that (exists ((x Int)) F) is a valid
+   * formula. If this is not the case, then the semantics in formulas that use
+   * witness terms may be unintuitive. For example, the following formula is
+   * unsatisfiable:
+   * (or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int)) false) 0))
+   * whereas notice that (or (= z 0) (not (= z 0))) is true for any z.
+   *
    * Parameters: 2
    *   -[1]: BOUND_VAR_LIST
-   *   -[2]: Hilbert choice body
+   *   -[2]: Witness body
    * Create with:
    *   mkTerm(Kind kind, Term child1, Term child2)
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
-  CHOICE,
+  WITNESS,
 
   /* Boolean --------------------------------------------------------------- */