From 1f0ad7ba72e3081a3ead8960bc6dabfa1ccd7898 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 17 Nov 2021 17:18:06 -0800 Subject: [PATCH] api: Fix kind documentation for BAG_MAKE. (#7663) --- src/api/cpp/cvc5_kind.h | 8 +++++--- test/unit/api/cpp/solver_black.cpp | 2 ++ 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 1c1819889..e6a03cbe4 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -2459,13 +2459,15 @@ enum Kind : int32_t */ BAG_DUPLICATE_REMOVAL, /** - * The bag of the single element given as a parameter. + * Construct a bag with the given element and given multiplicity. * * Parameters: - * - 1: Single element + * - 1: The element + * - 2: The multiplicity of the element. * * Create with: - * - `Solver::mkTerm(Kind kind, const Term& child) const` + * - `Solver::mkTerm(Kind kind, const Term& child, const Term& child) const` + * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ BAG_MAKE, /** diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index ba5bd655a..cf6b29017 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -659,6 +659,8 @@ TEST_F(TestApiBlackSolver, mkTerm) // mkTerm(Kind kind, Term child) const ASSERT_NO_THROW(d_solver.mkTerm(NOT, d_solver.mkTrue())); + ASSERT_NO_THROW( + d_solver.mkTerm(BAG_MAKE, d_solver.mkTrue(), d_solver.mkInteger(1))); ASSERT_THROW(d_solver.mkTerm(NOT, Term()), CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(NOT, a), CVC5ApiException); ASSERT_THROW(slv.mkTerm(NOT, d_solver.mkTrue()), CVC5ApiException); -- 2.30.2