From ef48e42744b158a077abdf1299ce9e53da87379f Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 30 Mar 2022 18:47:05 -0700 Subject: [PATCH] api: Mark experimental kinds. (#8464) --- src/api/cpp/cvc5_kind.h | 137 ++++++++++++++++++++++++++++++++++++++-- 1 file changed, 133 insertions(+), 4 deletions(-) diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 8f3d65744..50b44d0f4 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -137,6 +137,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ SEXPR, /** @@ -2086,6 +2091,10 @@ enum Kind : int32_t * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ EQ_RANGE, @@ -2305,6 +2314,11 @@ enum Kind : int32_t * * - Create Term of this Kind with: * - Solver::mkSepNil(const Sort&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ SEP_NIL, /** @@ -2312,6 +2326,11 @@ enum Kind : int32_t * * - Create Term of this Kind with: * - Solver::mkSepEmp() const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ SEP_EMP, /** @@ -2327,6 +2346,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ SEP_PTO, /** @@ -2342,6 +2366,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ SEP_STAR, /** @@ -2359,6 +2388,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ SEP_WAND, @@ -2547,6 +2581,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ SET_COMPREHENSION, /** @@ -2566,6 +2605,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ SET_CHOOSE, /** @@ -2580,6 +2624,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ SET_IS_SINGLETON, /** @@ -2600,6 +2649,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ SET_MAP, @@ -2673,6 +2727,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ RELATION_JOIN_IMAGE, /** @@ -2687,6 +2746,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ RELATION_IDEN, @@ -2832,6 +2896,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ BAG_DUPLICATE_REMOVAL, /** @@ -2863,6 +2932,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ BAG_CARD, /** @@ -2884,6 +2958,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ BAG_CHOOSE, /** @@ -2898,6 +2977,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ BAG_IS_SINGLETON, /** @@ -2912,6 +2996,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ BAG_FROM_SET, /** @@ -2926,6 +3015,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ BAG_TO_SET, /** @@ -2946,6 +3040,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ BAG_MAP, /** @@ -2968,6 +3067,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ BAG_FILTER, /** @@ -2988,6 +3092,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ BAG_FOLD, /** @@ -3002,6 +3111,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ TABLE_PRODUCT, @@ -4052,26 +4166,31 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ INST_POOL, /** * A instantantiation-add-to-pool annotation. * * @note Should only be used as a child of #INST_PATTERN_LIST. - * + * * An instantantiation-add-to-pool annotation indicates that when a quantified * formula is instantiated, the instantiated version of a term should be * added to the given pool. - * + * * For example, consider a quantified formula: - * + * * \rst * .. code:: lisp * * (FORALL (VARIABLE_LIST x) F * (INST_PATTERN_LIST (INST_ADD_TO_POOL (ADD x 1) p))) * \endrst - * + * * where assume that @f$x@f$ has type Int. When this quantified formula is * instantiated with, e.g., the term @f$t@f$, the term `(ADD t 1)` is added to pool @f$p@f$. * @@ -4086,6 +4205,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ INST_ADD_TO_POOL, /** @@ -4121,6 +4245,11 @@ enum Kind : int32_t * * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const + * + * \rst + * .. warning:: This kind is experimental and may be changed or removed in + * future versions. + * \endrst */ SKOLEM_ADD_TO_POOL, /** -- 2.30.2