New C++ API: Get rid of mkConst functions (simplify API). (#2783)

3 files changed, 56 insertions, 409 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index f9dfaa143..5321a90ec 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2303,254 +2303,74 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
 }
 
-Term Solver::mkConst(RoundingMode rm) const
+Term Solver::mkRoundingMode(RoundingMode rm) const
 {
   return mkConstHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
 }
 
-Term Solver::mkConst(Kind kind, Sort arg) const
+Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const
 {
-  try
-  {
-    CVC4_API_ARG_CHECK_EXPECTED(
-        (kind == EMPTYSET && arg.isNull()) || arg.isSet(), arg)
-        << "null sort or set sort";
-    CVC4_API_KIND_CHECK_EXPECTED(kind == EMPTYSET || kind == UNIVERSE_SET, kind)
-        << "EMPTY_SET or UNIVERSE_SET";
-    if (kind == EMPTYSET)
-    {
-      return mkConstHelper<CVC4::EmptySet>(CVC4::EmptySet(*arg.d_type));
-    }
-    else
-    {
-      Term res = d_exprMgr->mkNullaryOperator(*arg.d_type, extToIntKind(kind));
-      (void)res.d_expr->getType(true); /* kick off type checking */
-      return res;
-    }
-  }
-  catch (const CVC4::TypeCheckingException& e)
-  {
-    throw CVC4ApiException(e.getMessage());
-  }
-}
-
-Term Solver::mkConst(Kind kind, Sort arg1, int32_t arg2) const
-{
-  CVC4_API_ARG_CHECK_EXPECTED(!arg1.isNull(), arg1) << "non-null sort";
-  CVC4_API_KIND_CHECK_EXPECTED(kind == UNINTERPRETED_CONSTANT, kind)
-      << "UNINTERPRETED_CONSTANT";
+  CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
   return mkConstHelper<CVC4::UninterpretedConstant>(
-      CVC4::UninterpretedConstant(*arg1.d_type, arg2));
-}
-
-Term Solver::mkConst(Kind kind, bool arg) const
-{
-  CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_BOOLEAN, kind) << "CONST_BOOLEAN";
-  return mkConstHelper<bool>(arg);
-}
-
-/* Split out to avoid nested API calls (problematic with API tracing). */
-Term Solver::mkConstFromStrHelper(Kind kind, std::string s) const
-{
-  CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
-  CVC4_API_KIND_CHECK_EXPECTED(
-      kind == ABSTRACT_VALUE || kind == CONST_RATIONAL || kind == CONST_STRING,
-      kind)
-      << "ABSTRACT_VALUE or CONST_RATIONAL or CONST_STRING";
-  if (kind == ABSTRACT_VALUE)
-  {
-    try
-    {
-      return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(s, 10)));
-      // do not call getType(), for abstract values, type can not be computed
-      // until it is substituted away
-    }
-    catch (const std::invalid_argument& e)
-    {
-      throw CVC4ApiException(e.what());
-    }
-    catch (const CVC4::TypeCheckingException& e)
-    {
-      throw CVC4ApiException(e.getMessage());
-    }
-  }
-  else if (kind == CONST_RATIONAL)
-  {
-    return mkRealFromStrHelper(s);
-  }
-  return mkConstHelper<CVC4::String>(CVC4::String(s));
-}
-
-Term Solver::mkConst(Kind kind, const char* arg) const
-{
-  CVC4_API_ARG_CHECK_NOT_NULL(arg);
-  return mkConstFromStrHelper(kind, std::string(arg));
-}
-
-Term Solver::mkConst(Kind kind, const std::string& arg) const
-{
-  return mkConstFromStrHelper(kind, arg);
+      CVC4::UninterpretedConstant(*sort.d_type, index));
 }
 
-/* Split out to avoid nested API calls (problematic with API tracing). */
-Term Solver::mkConstFromStrHelper(Kind kind, std::string s, uint32_t a) const
-{
-  CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
-  CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_BITVECTOR, kind)
-      << "CONST_BITVECTOR";
-  return mkBVFromStrHelper(s, a);
-}
-
-Term Solver::mkConst(Kind kind, const char* arg1, uint32_t arg2) const
-{
-  CVC4_API_ARG_CHECK_NOT_NULL(arg1);
-  return mkConstFromStrHelper(kind, std::string(arg1), arg2);
-}
-
-Term Solver::mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const
+Term Solver::mkAbstractValue(const std::string& index) const
 {
-  return mkConstFromStrHelper(kind, arg1, arg2);
-}
-
-/* Split out to avoid nested API calls (problematic with API tracing). */
-template <typename T>
-Term Solver::mkConstFromIntHelper(Kind kind, T a) const
-{
-  CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL,
-                               kind)
-      << "ABSTRACT_VALUE or CONST_RATIONAL";
-  if (kind == ABSTRACT_VALUE)
-  {
-    try
-    {
-      return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(a)));
-      // do not call getType(), for abstract values, type can not be computed
-      // until it is substituted away
-    }
-    catch (const std::invalid_argument& e)
-    {
-      throw CVC4ApiException(e.what());
-    }
-    catch (const CVC4::TypeCheckingException& e)
-    {
-      throw CVC4ApiException(e.getMessage());
-    }
-  }
+  CVC4_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string";
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(a));
+    CVC4::Integer idx(index, 10);
+    CVC4_API_ARG_CHECK_EXPECTED(idx > 0, index)
+        << "a string representing an integer > 0";
+    return d_exprMgr->mkConst(CVC4::AbstractValue(idx));
+    // do not call getType(), for abstract values, type can not be computed
+    // until it is substituted away
   }
   catch (const std::invalid_argument& e)
   {
     throw CVC4ApiException(e.what());
   }
-}
-
-Term Solver::mkConst(Kind kind, int32_t arg) const
-{
-  return mkConstFromIntHelper<int64_t>(kind, static_cast<int64_t>(arg));
-}
-
-Term Solver::mkConst(Kind kind, int64_t arg) const
-{
-  return mkConstFromIntHelper<int64_t>(kind, arg);
-}
-
-Term Solver::mkConst(Kind kind, uint32_t arg) const
-{
-  return mkConstFromIntHelper<uint64_t>(kind, static_cast<uint64_t>(arg));
-}
-
-Term Solver::mkConst(Kind kind, uint64_t arg) const
-{
-  return mkConstFromIntHelper<uint64_t>(kind, arg);
-}
-
-Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const
-{
-  CVC4_API_KIND_CHECK_EXPECTED(
-      kind == CONST_BITVECTOR || kind == CONST_RATIONAL, kind)
-      << "CONST_BITVECTOR or CONST_RATIONAL";
-  if (kind == CONST_BITVECTOR)
-  {
-    return mkBVFromIntHelper(arg1, arg2);
-  }
-  try
-  {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
-  }
-  catch (const std::invalid_argument& e)
-  {
-    throw CVC4ApiException(e.what());
-  }
-}
-
-Term Solver::mkConst(Kind kind, int32_t arg1, int32_t arg2) const
-{
-  CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind)
-      << "CONST_RATIONAL";
-  try
-  {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
-  }
-  catch (const std::invalid_argument& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
-    throw CVC4ApiException(e.what());
+    throw CVC4ApiException(e.getMessage());
   }
 }
 
-Term Solver::mkConst(Kind kind, int64_t arg1, int64_t arg2) const
+Term Solver::mkAbstractValue(uint64_t index) const
 {
-  CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind)
-      << "CONST_RATIONAL";
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
+    CVC4_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0";
+    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index)));
+    // do not call getType(), for abstract values, type can not be computed
+    // until it is substituted away
   }
   catch (const std::invalid_argument& e)
   {
     throw CVC4ApiException(e.what());
   }
-}
-
-Term Solver::mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const
-{
-  CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind)
-      << "CONST_RATIONAL";
-  try
-  {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
-  }
-  catch (const std::invalid_argument& e)
+  catch (const CVC4::TypeCheckingException& e)
   {
-    throw CVC4ApiException(e.what());
+    throw CVC4ApiException(e.getMessage());
   }
 }
 
-Term Solver::mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const
-{
-  CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_BITVECTOR, kind)
-      << "CONST_BITVECTOR";
-  return mkBVFromIntHelper(arg1, arg2);
-}
-
-Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const
+Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_FLOATINGPOINT, kind)
-      << "CONST_FLOATINGPOINT";
-  CVC4_API_ARG_CHECK_EXPECTED(arg1 > 0, arg1) << "a value > 0";
-  CVC4_API_ARG_CHECK_EXPECTED(arg2 > 0, arg2) << "a value > 0";
-  uint32_t bw = arg1 + arg2;
-  CVC4_API_ARG_CHECK_EXPECTED(bw == arg3.getSort().getBVSize(), arg3)
+  CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0";
+  CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0";
+  uint32_t bw = exp + sig;
+  CVC4_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val)
       << "a bit-vector constant with bit-width '" << bw << "'";
-  CVC4_API_ARG_CHECK_EXPECTED(!arg3.isNull(), arg3) << "non-null term";
+  CVC4_API_ARG_CHECK_EXPECTED(!val.isNull(), val) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(
-      arg3.getSort().isBitVector() && arg3.d_expr->isConst(), arg3)
+      val.getSort().isBitVector() && val.d_expr->isConst(), val)
       << "bit-vector constant";
   return mkConstHelper<CVC4::FloatingPoint>(
-      CVC4::FloatingPoint(arg1, arg2, arg3.d_expr->getConst<BitVector>()));
+      CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>()));
 }
 
 /* Create variables                                                           */
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index ef82a9174..1d98f127d 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2088,183 +2088,38 @@ class CVC4_PUBLIC Solver
   Term mkNegZero(uint32_t exp, uint32_t sig) const;
 
   /**
-   * Create constant of kind:
-   *   - CONST_ROUNDINGMODE
+   * Create a roundingmode constant.
    * @param rm the floating point rounding mode this constant represents
    */
-  Term mkConst(RoundingMode rm) const;
-
-  /*
-   * Create constant of kind:
-   *   - EMPTYSET
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg the argument to this kind
-   */
-  Term mkConst(Kind kind, Sort arg) const;
-
-  /**
-   * Create constant of kind:
-   *   - UNINTERPRETED_CONSTANT
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg1 the first argument to this kind
-   * @param arg2 the second argument to this kind
-   */
-  Term mkConst(Kind kind, Sort arg1, int32_t arg2) const;
-
-  /**
-   * Create constant of kind:
-   *   - BOOLEAN
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg the argument to this kind
-   */
-  Term mkConst(Kind kind, bool arg) const;
-
-  /**
-   * Create constant of kind:
-   *   - ABSTRACT_VALUE
-   *   - CONST_RATIONAL (for integers, reals)
-   *   - CONST_STRING
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg the argument to this kind
-   */
-  Term mkConst(Kind kind, const char* arg) const;
-
-  /**
-   * Create constant of kind:
-   *   - ABSTRACT_VALUE
-   *   - CONST_RATIONAL (for integers, reals)
-   *   - CONST_STRING
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg the argument to this kind
-   */
-  Term mkConst(Kind kind, const std::string& arg) const;
-
-  /**
-   * Create constant of kind:
-   *   - CONST_BITVECTOR
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg1 the first argument to this kind
-   * @param arg2 the second argument to this kind
-   */
-  Term mkConst(Kind kind, const char* arg1, uint32_t arg2) const;
+  Term mkRoundingMode(RoundingMode rm) const;
 
   /**
-   * Create constant of kind:
-   *   - CONST_BITVECTOR
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg1 the first argument to this kind
-   * @param arg2 the second argument to this kind
+   * Create uninterpreted constant.
+   * @param arg1 Sort of the constant
+   * @param arg2 Index of the constant
    */
-  Term mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const;
+  Term mkUninterpretedConst(Sort sort, int32_t index) const;
 
   /**
-   * Create constant of kind:
-   *   - ABSTRACT_VALUE
-   *   - CONST_RATIONAL (for integers, reals)
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg the argument to this kind
+   * Create an abstract value constant.
+   * @param index Index of the abstract value
    */
-  Term mkConst(Kind kind, uint32_t arg) const;
+  Term mkAbstractValue(const std::string& index) const;
 
   /**
-   * Create constant of kind:
-   *   - ABSTRACT_VALUE
-   *   - CONST_RATIONAL (for integers, reals)
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg the argument to this kind
+   * Create an abstract value constant.
+   * @param index Index of the abstract value
    */
-  Term mkConst(Kind kind, int32_t arg) const;
+  Term mkAbstractValue(uint64_t index) const;
 
   /**
-   * Create constant of kind:
-   *   - ABSTRACT_VALUE
-   *   - CONST_RATIONAL (for integers, reals)
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg the argument to this kind
-   */
-  Term mkConst(Kind kind, int64_t arg) const;
-
-  /**
-   * Create constant of kind:
-   *   - ABSTRACT_VALUE
-   *   - CONST_RATIONAL (for integers, reals)
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg the argument to this kind
-   */
-  Term mkConst(Kind kind, uint64_t arg) const;
-
-  /**
-   * Create constant of kind:
-   *   - CONST_RATIONAL (for rationals)
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg1 the first argument to this kind
-   * @param arg2 the second argument to this kind
-   */
-  Term mkConst(Kind kind, int32_t arg1, int32_t arg2) const;
-
-  /**
-   * Create constant of kind:
-   *   - CONST_RATIONAL (for rationals)
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg1 the first argument to this kind
-   * @param arg2 the second argument to this kind
-   */
-  Term mkConst(Kind kind, int64_t arg1, int64_t arg2) const;
-
-  /**
-   * Create constant of kind:
-   *   - CONST_RATIONAL (for rationals)
-   *   - CONST_BITVECTOR
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg1 the first argument to this kind
-   * @param arg2 the second argument to this kind
-   */
-  Term mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const;
-
-  /**
-   * Create constant of kind:
-   *   - CONST_RATIONAL (for rationals)
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg1 the first argument to this kind
-   * @param arg2 the second argument to this kind
-   */
-  Term mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const;
-
-  /**
-   * Create constant of kind:
-   *   - CONST_BITVECTOR
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg1 the first argument to this kind
-   * @param arg2 the second argument to this kind
-   */
-  Term mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const;
-
-  /**
-   * Create constant of kind:
-   *   - CONST_FLOATINGPOINT (requires CVC4 to be compiled with symFPU support)
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the constant
-   * @param arg1 the first argument to this kind
-   * @param arg2 the second argument to this kind
-   * @param arg3 the third argument to this kind
+   * Create a floating-point constant (requires CVC4 to be compiled with symFPU
+   * support).
+   * @param exp Size of the exponent
+   * @param sig Size of the significand
+   * @param val Value of the floating-point constant as a bit-vector term
    */
-  Term mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const;
+  Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const;
 
   /* .................................................................... */
   /* Create Variables                                                     */
@@ -2644,12 +2499,6 @@ class CVC4_PUBLIC Solver
   Term mkBVFromStrHelper(uint32_t size, std::string s, uint32_t base) const;
   /* Helper for mkBitVector functions that take an integer as argument. */
   Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
-  /* Helper for mkConst functions that take a string as argument. */
-  Term mkConstFromStrHelper(Kind kind, std::string s) const;
-  Term mkConstFromStrHelper(Kind kind, std::string s, uint32_t a) const;
-  /* Helper for mkConst functions that take an integer as argument. */
-  template <typename T>
-  Term mkConstFromIntHelper(Kind kind, T a) const;
 
   /**
    * Helper function that ensures that a given term is of sort real (as opposed
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index a940dbefa..a7f6926bb 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -62,7 +62,7 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[1]: Sort of the constant
    *   -[2]: Index of the constant
    * Create with:
-   *   mkConst(Kind, Sort, int32_t)
+   *   mkUninterpretedConst(Sort sort, int32_t index)
    */
   UNINTERPRETED_CONSTANT,
   /**
@@ -70,12 +70,8 @@ enum CVC4_PUBLIC Kind : int32_t
    * Parameters: 1
    *   -[1]: Index of the abstract value
    * Create with:
-   *   mkConst(Kind kind, const char* arg)
-   *   mkConst(Kind kind, const std::string& arg)
-   *   mkConst(Kind kind, uint32_t arg)
-   *   mkConst(Kind kind, int32_t arg)
-   *   mkConst(Kind kind, int64_t arg)
-   *   mkConst(Kind kind, uint64_t arg)
+   *   mkAbstractValue(const std::string& index);
+   *   mkAbstractValue(uint64_t index);
    */
   ABSTRACT_VALUE,
 #if 0
@@ -204,7 +200,6 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTrue()
    *   mkFalse()
    *   mkBoolean(bool val)
-   *   mkConst(Kind kind, bool arg)
    */
   CONST_BOOLEAN,
   /* Logical not.
@@ -568,20 +563,10 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkReal(int64_t val)
    *   mkReal(uint32_t val)
    *   mkReal(uint64_t val)
-   *   mkRational(int32_t num, int32_t den)
-   *   mkRational(int64_t num, int64_t den)
-   *   mkRational(uint32_t num, uint32_t den)
-   *   mkRational(uint64_t num, uint64_t den)
-   *   mkConst(Kind kind, const char* s, uint32_t base = 10)
-   *   mkConst(Kind kind, const std::string& s, uint32_t base = 10)
-   *   mkConst(Kind kind, uint32_t arg)
-   *   mkConst(Kind kind, int64_t arg)
-   *   mkConst(Kind kind, uint64_t arg)
-   *   mkConst(Kind kind, int32_t arg)
-   *   mkConst(Kind kind, int32_t arg1, int32_t arg2)
-   *   mkConst(Kind kind, int64_t arg1, int64_t arg2)
-   *   mkConst(Kind kind, uint32_t arg1, uint32_t arg2)
-   *   mkConst(Kind kind, uint64_t arg1, uint64_t arg2)
+   *   mkReal(int32_t num, int32_t den)
+   *   mkReal(int64_t num, int64_t den)
+   *   mkReal(uint32_t num, uint32_t den)
+   *   mkReal(uint64_t num, uint64_t den)
    */
   CONST_RATIONAL,
   /**
@@ -661,9 +646,6 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkBitVector(uint32_t size, uint64_t val)
    *   mkBitVector(const char* s, uint32_t base = 2)
    *   mkBitVector(std::string& s, uint32_t base = 2)
-   *   mkConst(Kind kind, const char* s, uint32_t base = 10)
-   *   mkConst(Kind kind, const std::string& s, uint32_t base = 10)
-   *   mkConst(Kind kind, uint32_t arg1, uint64_t arg2)
    */
   CONST_BITVECTOR,
   /**
@@ -1166,13 +1148,13 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[2]: Size of the significand
    *   -[3]: Value of the floating-point constant as a bit-vector term
    * Create with:
-   *   mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3)
+   *   mkFloatingPoint(uint32_t sig, uint32_t exp, Term val)
    */
   CONST_FLOATINGPOINT,
   /**
    * Floating-point rounding mode term.
    * Create with:
-   *   mkConst(RoundingMode rm)
+   *   mkRoundingMode(RoundingMode rm)
    */
   CONST_ROUNDINGMODE,
   /**
@@ -1830,7 +1812,6 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[1]: Sort of the set elements
    * Create with:
    *   mkEmptySet(Sort sort)
-   *   mkConst(Sort sort)
    */
   EMPTYSET,
   /**
@@ -1919,7 +1900,6 @@ enum CVC4_PUBLIC Kind : int32_t
    * All set variables must be interpreted as subsets of it.
    * Create with:
    *   mkUniverseSet(Sort sort)
-   *   mkConst(Kind kind, Sort sort)
    */
   UNIVERSE_SET,
   /**
@@ -2122,8 +2102,6 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkString(const std::string& s)
    *   mkString(const unsigned char c)
    *   mkString(const std::vector<unsigned>& s)
-   *   mkConst(Kind kind, const char* s)
-   *   mkConst(Kind kind, const std::string& s)
    */
   CONST_STRING,
   /**