diff options
Diffstat (limited to 'src/api/cpp/cvc5_kind.h')
| -rw-r--r-- | src/api/cpp/cvc5_kind.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 0ff05022f..fe87df934 100644 --- 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` */ |