From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 18 Nov 2021 01:18:06 +0000 (-0800)
Subject: api: Fix kind documentation for BAG_MAKE. (#7663)
X-Git-Tag: cvc5-1.0.0~801
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1f0ad7ba72e3081a3ead8960bc6dabfa1ccd7898;p=cvc5.git

api: Fix kind documentation for BAG_MAKE. (#7663)
---

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<Term>& 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);