diff options
Diffstat (limited to 'src/api/cpp/cvc5_kind.h')
| -rw-r--r-- | src/api/cpp/cvc5_kind.h | 24 |
1 files changed, 8 insertions, 16 deletions
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 0ff05022f..a01f84c3f 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -43,7 +43,7 @@ namespace api { * depends on the size of `cvc5::Kind` (`NodeValue::NBITS_KIND`, currently 10 * bits, see expr/node_value.h). */ -enum CVC5_EXPORT Kind : int32_t +enum Kind : int32_t { /** * Internal kind. @@ -331,22 +331,7 @@ enum CVC5_EXPORT Kind : int32_t * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` */ CARDINALITY_CONSTRAINT, - /** - * Cardinality value for uninterpreted sort S. - * An operator that returns an integer indicating the value of the cardinality - * of sort S. - * - * Parameters: - * - 1: Term of sort S - * - * Create with: - * - `Solver::mkTerm(Kind kind, const Term& child1) const` - * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const` - */ - CARDINALITY_VALUE, #if 0 - /* Combined cardinality constraint. */ - COMBINED_CARDINALITY_CONSTRAINT, /* Partial uninterpreted function application. */ PARTIAL_APPLY_UF, #endif @@ -766,6 +751,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 +2216,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` */ |