New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)

This cleans up naming of API functions to create first-order constants and variables.

mkVar -> mkConst
mkBoundVar -> mkVar
declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed.

Note that we want to avoid redundancy in order to reduce code duplication and maintenance
overhead (we do not allow nested API calls, since this is problematic when tracing API calls).

4 files changed, 91 insertions, 114 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 86072d601..4cd9f4923 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -56,8 +56,8 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {APPLY, CVC4::Kind::APPLY},
     {EQUAL, CVC4::Kind::EQUAL},
     {DISTINCT, CVC4::Kind::DISTINCT},
-    {VARIABLE, CVC4::Kind::VARIABLE},
-    {BOUND_VARIABLE, CVC4::Kind::BOUND_VARIABLE},
+    {CONSTANT, CVC4::Kind::VARIABLE},
+    {VARIABLE, CVC4::Kind::BOUND_VARIABLE},
     {LAMBDA, CVC4::Kind::LAMBDA},
     {CHOICE, CVC4::Kind::CHOICE},
     {CHAIN, CVC4::Kind::CHAIN},
@@ -304,8 +304,8 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::APPLY, APPLY},
         {CVC4::Kind::EQUAL, EQUAL},
         {CVC4::Kind::DISTINCT, DISTINCT},
-        {CVC4::Kind::VARIABLE, VARIABLE},
-        {CVC4::Kind::BOUND_VARIABLE, BOUND_VARIABLE},
+        {CVC4::Kind::VARIABLE, CONSTANT},
+        {CVC4::Kind::BOUND_VARIABLE, VARIABLE},
         {CVC4::Kind::LAMBDA, LAMBDA},
         {CVC4::Kind::CHOICE, CHOICE},
         {CVC4::Kind::CHAIN, CHAIN},
@@ -1970,7 +1970,7 @@ Term Solver::mkPi() const
 }
 
 template <typename T>
-Term Solver::mkConstHelper(T t) const
+Term Solver::mkValHelper(T t) const
 {
   try
   {
@@ -1997,7 +1997,7 @@ Term Solver::mkRealFromStrHelper(std::string s) const
     CVC4::Rational r = s.find('/') != std::string::npos
                            ? CVC4::Rational(s)
                            : CVC4::Rational::fromDecimal(s);
-    return mkConstHelper<CVC4::Rational>(r);
+    return mkValHelper<CVC4::Rational>(r);
   }
   catch (const std::invalid_argument& e)
   {
@@ -2020,7 +2020,7 @@ Term Solver::mkReal(int32_t val) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2032,7 +2032,7 @@ Term Solver::mkReal(int64_t val) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2044,7 +2044,7 @@ Term Solver::mkReal(uint32_t val) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2056,7 +2056,7 @@ Term Solver::mkReal(uint64_t val) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2068,7 +2068,7 @@ Term Solver::mkReal(int32_t num, int32_t den) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2080,7 +2080,7 @@ Term Solver::mkReal(int64_t num, int64_t den) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2092,7 +2092,7 @@ Term Solver::mkReal(uint32_t num, uint32_t den) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2104,7 +2104,7 @@ Term Solver::mkReal(uint64_t num, uint64_t den) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2146,7 +2146,7 @@ Term Solver::mkEmptySet(Sort s) const
 {
   CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s)
       << "null sort or set sort";
-  return mkConstHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
+  return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
 }
 
 Term Solver::mkSepNil(Sort sort) const
@@ -2166,22 +2166,22 @@ Term Solver::mkSepNil(Sort sort) const
 
 Term Solver::mkString(const char* s, bool useEscSequences) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences));
+  return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences));
 }
 
 Term Solver::mkString(const std::string& s, bool useEscSequences) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences));
+  return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences));
 }
 
 Term Solver::mkString(const unsigned char c) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(std::string(1, c)));
+  return mkValHelper<CVC4::String>(CVC4::String(std::string(1, c)));
 }
 
 Term Solver::mkString(const std::vector<unsigned>& s) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(s));
+  return mkValHelper<CVC4::String>(CVC4::String(s));
 }
 
 Term Solver::mkUniverseSet(Sort sort) const
@@ -2207,7 +2207,7 @@ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
   CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
   try
   {
-    return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+    return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2228,7 +2228,7 @@ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
       << "base 2, 10, or 16";
   try
   {
-    return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
+    return mkValHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2249,7 +2249,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
     CVC4_API_CHECK(val.modByPow2(size) == val)
         << "Overflow in bitvector construction (specified bitvector size "
         << size << " too small to hold value " << s << ")";
-    return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+    return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2283,7 +2283,7 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), false));
 }
 
@@ -2291,7 +2291,7 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
 }
 
@@ -2299,7 +2299,7 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
 }
 
@@ -2307,7 +2307,7 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), false));
 }
 
@@ -2315,19 +2315,19 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
 }
 
 Term Solver::mkRoundingMode(RoundingMode rm) const
 {
-  return mkConstHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
+  return mkValHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
 }
 
 Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const
 {
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
-  return mkConstHelper<CVC4::UninterpretedConstant>(
+  return mkValHelper<CVC4::UninterpretedConstant>(
       CVC4::UninterpretedConstant(*sort.d_type, index));
 }
 
@@ -2385,14 +2385,14 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
   CVC4_API_ARG_CHECK_EXPECTED(
       val.getSort().isBitVector() && val.d_expr->isConst(), val)
       << "bit-vector constant";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>()));
 }
 
-/* Create variables                                                           */
+/* Create constants                                                           */
 /* -------------------------------------------------------------------------- */
 
-Term Solver::mkVar(Sort sort, const std::string& symbol) const
+Term Solver::mkConst(Sort sort, const std::string& symbol) const
 {
   try
   {
@@ -2408,7 +2408,10 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
   }
 }
 
-Term Solver::mkBoundVar(Sort sort, const std::string& symbol) const
+/* Create variables                                                           */
+/* -------------------------------------------------------------------------- */
+
+Term Solver::mkVar(Sort sort, const std::string& symbol) const
 {
   try
   {
@@ -2436,8 +2439,9 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
       mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
       kind)
       << "Only operator-style terms are created with mkTerm(), "
-         "to create variables and constants see mkVar(), mkBoundVar(), "
-         "and mkConst().";
+         "to create variables, constants and values see mkVar(), mkConst() "
+         "and the respective theory-specific functions to create values, "
+         "e.g., mkBitVector().";
   CVC4_API_KIND_CHECK_EXPECTED(
       nchildren >= minArity(kind) && nchildren <= maxArity(kind), kind)
       << "Terms with kind " << kindToString(kind) << " must have at least "
@@ -2729,15 +2733,14 @@ std::vector<Expr> Solver::termVectorToExprs(
 OpTerm Solver::mkOpTerm(Kind kind, Kind k)
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP";
-  return *mkConstHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
+  return *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
 }
 
 OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg)
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == RECORD_UPDATE_OP, kind)
       << "RECORD_UPDATE_OP";
-  return *mkConstHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg))
-              .d_expr.get();
+  return *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get();
 }
 
 OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
@@ -2747,59 +2750,59 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
   switch (kind)
   {
     case DIVISIBLE_OP:
-      res = *mkConstHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
+      res = *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
       break;
     case BITVECTOR_REPEAT_OP:
-      res = *mkConstHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
+      res = *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
                  .d_expr.get();
       break;
     case BITVECTOR_ZERO_EXTEND_OP:
-      res = *mkConstHelper<CVC4::BitVectorZeroExtend>(
+      res = *mkValHelper<CVC4::BitVectorZeroExtend>(
                  CVC4::BitVectorZeroExtend(arg))
                  .d_expr.get();
       break;
     case BITVECTOR_SIGN_EXTEND_OP:
-      res = *mkConstHelper<CVC4::BitVectorSignExtend>(
+      res = *mkValHelper<CVC4::BitVectorSignExtend>(
                  CVC4::BitVectorSignExtend(arg))
                  .d_expr.get();
       break;
     case BITVECTOR_ROTATE_LEFT_OP:
-      res = *mkConstHelper<CVC4::BitVectorRotateLeft>(
+      res = *mkValHelper<CVC4::BitVectorRotateLeft>(
                  CVC4::BitVectorRotateLeft(arg))
                  .d_expr.get();
       break;
     case BITVECTOR_ROTATE_RIGHT_OP:
-      res = *mkConstHelper<CVC4::BitVectorRotateRight>(
+      res = *mkValHelper<CVC4::BitVectorRotateRight>(
                  CVC4::BitVectorRotateRight(arg))
                  .d_expr.get();
       break;
     case INT_TO_BITVECTOR_OP:
-      res = *mkConstHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
+      res = *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_UBV_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToUBV>(
-                 CVC4::FloatingPointToUBV(arg))
-                 .d_expr.get();
+      res =
+          *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg))
+               .d_expr.get();
       break;
     case FLOATINGPOINT_TO_UBV_TOTAL_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToUBVTotal>(
+      res = *mkValHelper<CVC4::FloatingPointToUBVTotal>(
                  CVC4::FloatingPointToUBVTotal(arg))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_SBV_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToSBV>(
-                 CVC4::FloatingPointToSBV(arg))
-                 .d_expr.get();
+      res =
+          *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg))
+               .d_expr.get();
       break;
     case FLOATINGPOINT_TO_SBV_TOTAL_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToSBVTotal>(
+      res = *mkValHelper<CVC4::FloatingPointToSBVTotal>(
                  CVC4::FloatingPointToSBVTotal(arg))
                  .d_expr.get();
       break;
     case TUPLE_UPDATE_OP:
-      res = *mkConstHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg))
-                 .d_expr.get();
+      res =
+          *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get();
       break;
     default:
       CVC4_API_KIND_CHECK_EXPECTED(false, kind)
@@ -2816,37 +2819,37 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2)
   switch (kind)
   {
     case BITVECTOR_EXTRACT_OP:
-      res = *mkConstHelper<CVC4::BitVectorExtract>(
+      res = *mkValHelper<CVC4::BitVectorExtract>(
                  CVC4::BitVectorExtract(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPIEEEBitVector>(
+      res = *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
                  CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPFloatingPoint>(
+      res = *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
                  CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_REAL_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPReal>(
+      res = *mkValHelper<CVC4::FloatingPointToFPReal>(
                  CVC4::FloatingPointToFPReal(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPSignedBitVector>(
+      res = *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
                  CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
+      res = *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
                  CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_GENERIC_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPGeneric>(
+      res = *mkValHelper<CVC4::FloatingPointToFPGeneric>(
                  CVC4::FloatingPointToFPGeneric(arg1, arg2))
                  .d_expr.get();
       break;
@@ -2940,24 +2943,6 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
 }
 
 /**
- *  ( declare-const <symbol> <sort> )
- */
-Term Solver::declareConst(const std::string& symbol, Sort sort) const
-{
-  try
-  {
-    CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
-    Term res = d_exprMgr->mkVar(symbol, *sort.d_type);
-    (void)res.d_expr->getType(true); /* kick off type checking */
-    return res;
-  }
-  catch (const CVC4::TypeCheckingException& e)
-  {
-    throw CVC4ApiException(e.getMessage());
-  }
-}
-
-/**
  *  ( declare-datatype <symbol> <datatype_decl> )
  */
 Sort Solver::declareDatatype(
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 203586066..c13c7919e 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2166,20 +2166,23 @@ class CVC4_PUBLIC Solver
   /* .................................................................... */
 
   /**
-   * Create variable.
-   * @param sort the sort of the variable
-   * @param symbol the name of the variable
-   * @return the variable
+   * Create (first-order) constant (0-arity function symbol).
+   * SMT-LIB: ( declare-const <symbol> <sort> )
+   * SMT-LIB: ( declare-fun <symbol> ( ) <sort> )
+   *
+   * @param sort the sort of the constant
+   * @param symbol the name of the constant
+   * @return the first-order constant
    */
-  Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
+  Term mkConst(Sort sort, const std::string& symbol = std::string()) const;
 
   /**
-   * Create bound variable.
+   * Create (bound) variable.
    * @param sort the sort of the variable
    * @param symbol the name of the variable
    * @return the variable
    */
-  Term mkBoundVar(Sort sort, const std::string& symbol = std::string()) const;
+  Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
 
   /* .................................................................... */
   /* Formula Handling                                                     */
@@ -2246,17 +2249,6 @@ class CVC4_PUBLIC Solver
   Result checkValidAssuming(const std::vector<Term>& assumptions) const;
 
   /**
-   * Declare first-order constant (0-arity function symbol).
-   * SMT-LIB: ( declare-const <symbol> <sort> )
-   * SMT-LIB: ( declare-fun <symbol> ( ) <sort> )
-   * This command corresponds to mkVar().
-   * @param symbol the name of the first-order constant
-   * @param sort the sort of the first-order constant
-   * @return the first-order constant
-   */
-  Term declareConst(const std::string& symbol, Sort sort) const;
-
-  /**
    * Create datatype sort.
    * SMT-LIB: ( declare-datatype <symbol> <datatype_decl> )
    * @param symbol the name of the datatype sort
@@ -2303,7 +2295,7 @@ class CVC4_PUBLIC Solver
   /**
    * Define n-ary function.
    * SMT-LIB: ( define-fun <function_def> )
-   * Create parameter 'fun' with mkVar().
+   * Create parameter 'fun' with mkConst().
    * @param fun the sorted function
    * @param bound_vars the parameters to this function
    * @param term the function body
@@ -2330,7 +2322,7 @@ class CVC4_PUBLIC Solver
   /**
    * Define recursive function.
    * SMT-LIB: ( define-fun-rec <function_def> )
-   * Create parameter 'fun' with mkVar().
+   * Create parameter 'fun' with mkConst().
    * @param fun the sorted function
    * @param bound_vars the parameters to this function
    * @param term the function body
@@ -2343,7 +2335,7 @@ class CVC4_PUBLIC Solver
   /**
    * Define recursive functions.
    * SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
-   * Create elements of parameter 'funs' with mkVar().
+   * Create elements of parameter 'funs' with mkConst().
    * @param funs the sorted functions
    * @param bound_vars the list of parameters to the functions
    * @param term the list of function bodies of the functions
@@ -2506,7 +2498,7 @@ class CVC4_PUBLIC Solver
   void checkMkTerm(Kind kind, uint32_t nchildren) const;
   /* Helper for mk-functions that call d_exprMgr->mkConst(). */
   template <typename T>
-  Term mkConstHelper(T t) const;
+  Term mkValHelper(T t) const;
   /* Helper for mkReal functions that take a string as argument. */
   Term mkRealFromStrHelper(std::string s) const;
   /* Helper for mkBitVector functions that take a string as argument. */
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 3aba6cebb..d4f6880f9 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -123,25 +123,25 @@ enum CVC4_PUBLIC Kind : int32_t
    */
   DISTINCT,
   /**
-   * Variable.
+   * First-order constant.
    * Not permitted in bindings (forall, exists, ...).
    * Parameters:
-   *   See mkVar().
+   *   See mkConst().
    * Create with:
-   *   mkVar(const std::string& symbol, Sort sort)
-   *   mkVar(Sort sort)
+   *   mkConst(const std::string& symbol, Sort sort)
+   *   mkConst(Sort sort)
    */
-  VARIABLE,
+  CONSTANT,
   /**
-   * Bound variable.
+   * (Bound) variable.
    * Permitted in bindings and in the lambda and quantifier bodies only.
    * Parameters:
-   *   See mkBoundVar().
+   *   See mkVar().
    * Create with:
-   *   mkBoundVar(const std::string& symbol, Sort sort)
-   *   mkBoundVar(Sort sort)
+   *   mkVar(const std::string& symbol, Sort sort)
+   *   mkVar(Sort sort)
    */
-  BOUND_VARIABLE,
+  VARIABLE,
 #if 0
   /* Skolem variable (internal only) */
   SKOLEM,
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 00f2e944d..75df38637 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2307,8 +2307,8 @@ termAtomic[CVC4::api::Term& atomTerm]
       sortSymbol[type,CHECK_DECLARED]
       sortSymbol[type2,CHECK_DECLARED]
       {
-        api::Term v1 = SOLVER->mkVar(api::Sort(type), "_emp1");
-        api::Term v2 = SOLVER->mkVar(api::Sort(type2), "_emp2");
+        api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1");
+        api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2");
         atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
       }