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

5 files changed, 155 insertions, 535 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,
   /**
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e33ab7a70..c72a4f99b 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2330,16 +2330,16 @@ termAtomic[CVC4::api::Term& atomTerm]
     }
 
   // Floating-point rounding mode constants
-  | FP_RNE_TOK      { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_EVEN); }
-  | FP_RNA_TOK      { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_AWAY); }
-  | FP_RTP_TOK      { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_POSITIVE); }
-  | FP_RTN_TOK      { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_NEGATIVE); }
-  | FP_RTZ_TOK      { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_ZERO); }
-  | FP_RNE_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_EVEN); }
-  | FP_RNA_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_AWAY); }
-  | FP_RTP_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_POSITIVE); }
-  | FP_RTN_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_NEGATIVE); }
-  | FP_RTZ_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_ZERO); }
+  | FP_RNE_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN); }
+  | FP_RNA_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY); }
+  | FP_RTP_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_POSITIVE); }
+  | FP_RTN_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE); }
+  | FP_RTZ_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_ZERO); }
+  | FP_RNE_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN); }
+  | FP_RNA_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY); }
+  | FP_RTP_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_POSITIVE); }
+  | FP_RTN_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE); }
+  | FP_RTZ_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_ZERO); }
 
   // String constant
   | str[s,false] { atomTerm = SOLVER->mkString(s, true); }
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 5c2c7a8f5..3bfb51200 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -49,22 +49,29 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkTupleSort();
   void testMkUninterpretedSort();
 
+  void testMkAbstractValue();
   void testMkBitVector();
   void testMkBoolean();
   void testMkBoundVar();
-  void testMkConst();
   void testMkEmptySet();
   void testMkFalse();
   void testMkFloatingPoint();
+  void testMkNaN();
+  void testMkNegInf();
+  void testMkNegZero();
   void testMkPi();
+  void testMkPosInf();
+  void testMkPosZero();
   void testMkReal();
   void testMkRegexpEmpty();
   void testMkRegexpSigma();
+  void testMkRoundingMode();
   void testMkSepNil();
   void testMkString();
   void testMkTerm();
   void testMkTrue();
   void testMkTuple();
+  void testMkUninterpretedConst();
   void testMkUniverseSet();
   void testMkVar();
 
@@ -281,132 +288,58 @@ void SolverBlack::testMkBoolean()
   TS_ASSERT_THROWS_NOTHING(d_solver.mkBoolean(false));
 }
 
-void SolverBlack::testMkConst()
+void SolverBlack::testMkRoundingMode()
 {
-  // mkConst(RoundingMode rm) const
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(RoundingMode::ROUND_TOWARD_ZERO));
-
-  // mkConst(Kind kind, Sort arg) const
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(EMPTYSET, Sort()));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(
-      UNIVERSE_SET, d_solver.mkSetSort(d_solver.getBooleanSort())));
-  TS_ASSERT_THROWS(d_solver.mkConst(EMPTYSET, d_solver.getBooleanSort()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkTerm(UNIVERSE_SET, Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(APPLY, d_solver.getBooleanSort()),
-                   CVC4ApiException&);
-
-  // mkConst(Kind kind, Sort arg1, int32_t arg2) const
   TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkConst(UNINTERPRETED_CONSTANT, d_solver.getBooleanSort(), 1));
-  TS_ASSERT_THROWS(d_solver.mkConst(UNINTERPRETED_CONSTANT, Sort(), 1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(EMPTYSET, d_solver.getBooleanSort(), 1),
-                   CVC4ApiException&);
-
-  // mkConst(Kind kind, bool arg) const
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_BOOLEAN, true));
-  TS_ASSERT_THROWS(d_solver.mkConst(UNINTERPRETED_CONSTANT, true),
-                   CVC4ApiException&);
+      d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
+}
 
-  // mkConst(Kind kind, const char* arg) const
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(ABSTRACT_VALUE, std::string("1")));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_STRING, "asdf"));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, "1"));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, "1/2"));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, "1.2"));
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_STRING, nullptr), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_STRING, ""), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(ABSTRACT_VALUE, std::string("1.2")),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(ABSTRACT_VALUE, "1/2"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(ABSTRACT_VALUE, "asdf"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_RATIONAL, "1..2"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_RATIONAL, "asdf"), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(BITVECTOR_ULT, "asdf"), CVC4ApiException&);
-
-  // mkConst(Kind kind, const std::string& arg) const
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_STRING, std::string("asdf")));
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkConst(CONST_RATIONAL, std::string("1/2")));
+void SolverBlack::testMkUninterpretedConst()
+{
   TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkConst(CONST_RATIONAL, std::string("1.2")));
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_STRING, nullptr), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_STRING, std::string("")),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_RATIONAL, std::string("asdf")),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(BITVECTOR_ULT, std::string("asdf")),
-                   CVC4ApiException&);
+      d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
+  TS_ASSERT_THROWS(d_solver.mkUninterpretedConst(Sort(), 1), CVC4ApiException&);
+}
 
-  // mkConst(Kind kind, const char* arg1, uint32_t arg2) const
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkConst(CONST_BITVECTOR, std::string("101"), 2));
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkConst(CONST_BITVECTOR, std::string("10a"), 16));
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, nullptr, 1),
+void SolverBlack::testMkAbstractValue()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue(std::string("1")));
+  TS_ASSERT_THROWS(d_solver.mkAbstractValue(std::string("0")),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, std::string("")),
+  TS_ASSERT_THROWS(d_solver.mkAbstractValue(std::string("-1")),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, std::string("101"), 6),
+  TS_ASSERT_THROWS(d_solver.mkAbstractValue(std::string("1.2")),
                    CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkAbstractValue("1/2"), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkAbstractValue("asdf"), CVC4ApiException&);
 
-  // mkConst(Kind kind, int32_t arg) const
-  // mkConst(Kind kind, uint32_t arg) const
-  // mkConst(Kind kind, int64_t arg) const
-  // mkConst(Kind kind, uint64_t arg) const
-  int32_t val1 = 2;
-  uint32_t val2 = 2;
-  int64_t val3 = 2;
-  uint64_t val4 = 2;
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(ABSTRACT_VALUE, val1));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(ABSTRACT_VALUE, val2));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(ABSTRACT_VALUE, val3));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(ABSTRACT_VALUE, val4));
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, val1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, val2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, val3), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, val4), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val1));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val2));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val3));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val4));
-
-  // mkConst(Kind kind, int32_t arg1, int32_t arg2) const
-  // mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const
-  // mkConst(Kind kind, int64_t arg1, int64_t arg2) const
-  // mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val1, val1));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val2, val2));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val3, val3));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_RATIONAL, val4, val4));
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_BITVECTOR, val2, val2));
-
-  // mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((uint32_t)1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((int32_t)1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((uint64_t)1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((int64_t)1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((int32_t)-1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkAbstractValue((int64_t)-1));
+  TS_ASSERT_THROWS(d_solver.mkAbstractValue(0), CVC4ApiException&);
+}
+
+void SolverBlack::testMkFloatingPoint()
+{
   Term t1 = d_solver.mkBitVector(8);
   Term t2 = d_solver.mkBitVector(4);
   Term t3 = d_solver.mkReal(2);
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
-    TS_ASSERT_THROWS_NOTHING(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 5, t1));
+    TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPoint(3, 5, t1));
   }
   else
   {
-    TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 5, t1),
-                     CVC4ApiException&);
+    TS_ASSERT_THROWS(d_solver.mkFloatingPoint(3, 5, t1), CVC4ApiException&);
   }
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 0, 5, Term()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 0, 5, t1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 0, t1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 5, t2),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_FLOATINGPOINT, 3, 5, t2),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkConst(CONST_BITVECTOR, 3, 5, t1),
-                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkFloatingPoint(0, 5, Term()), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkFloatingPoint(0, 5, t1), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkFloatingPoint(3, 0, t1), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException&);
 }
 
 void SolverBlack::testMkEmptySet()
@@ -422,23 +355,63 @@ void SolverBlack::testMkFalse()
   TS_ASSERT_THROWS_NOTHING(d_solver.mkFalse());
 }
 
-void SolverBlack::testMkFloatingPoint()
+void SolverBlack::testMkNaN()
 {
   if (CVC4::Configuration::isBuiltWithSymFPU())
   {
-    TS_ASSERT_THROWS_NOTHING(d_solver.mkPosInf(3, 5));
-    TS_ASSERT_THROWS_NOTHING(d_solver.mkNegInf(3, 5));
     TS_ASSERT_THROWS_NOTHING(d_solver.mkNaN(3, 5));
-    TS_ASSERT_THROWS_NOTHING(d_solver.mkPosInf(3, 5));
+  }
+  else
+  {
+    TS_ASSERT_THROWS(d_solver.mkNaN(3, 5), CVC4ApiException&);
+  }
+}
+
+void SolverBlack::testMkNegZero()
+{
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
     TS_ASSERT_THROWS_NOTHING(d_solver.mkNegZero(3, 5));
   }
   else
   {
-    TS_ASSERT_THROWS(d_solver.mkPosInf(3, 5), CVC4ApiException&);
+    TS_ASSERT_THROWS(d_solver.mkNegZero(3, 5), CVC4ApiException&);
+  }
+}
+
+void SolverBlack::testMkNegInf()
+{
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    TS_ASSERT_THROWS_NOTHING(d_solver.mkNegInf(3, 5));
+  }
+  else
+  {
     TS_ASSERT_THROWS(d_solver.mkNegInf(3, 5), CVC4ApiException&);
-    TS_ASSERT_THROWS(d_solver.mkNaN(3, 5), CVC4ApiException&);
+  }
+}
+
+void SolverBlack::testMkPosInf()
+{
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    TS_ASSERT_THROWS_NOTHING(d_solver.mkPosInf(3, 5));
+  }
+  else
+  {
     TS_ASSERT_THROWS(d_solver.mkPosInf(3, 5), CVC4ApiException&);
-    TS_ASSERT_THROWS(d_solver.mkNegZero(3, 5), CVC4ApiException&);
+  }
+}
+
+void SolverBlack::testMkPosZero()
+{
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    TS_ASSERT_THROWS_NOTHING(d_solver.mkPosZero(3, 5));
+  }
+  else
+  {
+    TS_ASSERT_THROWS(d_solver.mkPosZero(3, 5), CVC4ApiException&);
   }
 }