diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-05-19 16:24:59 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-19 16:24:59 -0500 |
commit | c8f149fa83fa16f821f37687fedfa778808809bd (patch) | |
tree | 8808ec522b58c0d8273280923b984a72e0b7bb29 /src/api/cvc4cppkind.h | |
parent | 6bb98062a5578d126db6a3e8cdca083881893b32 (diff) |
Renamed operator CHOICE to WITNESS (#4207)
Renamed operator CHOICE to WITNESS, and removed it from the front end
Diffstat (limited to 'src/api/cvc4cppkind.h')
-rw-r--r-- | src/api/cvc4cppkind.h | 33 |
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 --------------------------------------------------------------- */ |