New C++ API: Add tests for mk-functions in solver object. (#2764)

3 files changed, 604 insertions, 319 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index cd604a25c..8a583a671 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -32,6 +32,7 @@
 #include "util/result.h"
 #include "util/utility.h"
 
+#include <cstring>
 #include <sstream>
 
 namespace CVC4 {
@@ -639,6 +640,10 @@ class CVC4ApiExceptionStream
   CVC4_API_CHECK(!isNull()) << "Invalid call to '" << __PRETTY_FUNCTION__ \
                             << "', expected non-null object";
 
+#define CVC4_API_ARG_CHECK_NOT_NULL(arg) \
+  CVC4_API_CHECK(arg != nullptr)         \
+      << "Invalid null argument for '" << #arg << "'";
+
 #define CVC4_API_KIND_CHECK(kind)     \
   CVC4_API_CHECK(isDefinedKind(kind)) \
       << "Invalid kind '" << kindToString(kind) << "'";
@@ -665,12 +670,12 @@ class CVC4ApiExceptionStream
           & CVC4ApiExceptionStream().ostream()      \
                 << "Invalid size of argument '" << #arg << "', expected "
 
-#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx)         \
-  CVC4_PREDICT_FALSE(cond)                                                 \
-  ? (void)0                                                                \
-  : OstreamVoider()                                                        \
-          & CVC4ApiExceptionStream().ostream()                             \
-                << "Invalid " << what << "'" << arg << "' at index" << idx \
+#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx)          \
+  CVC4_PREDICT_FALSE(cond)                                                  \
+  ? (void)0                                                                 \
+  : OstreamVoider()                                                         \
+          & CVC4ApiExceptionStream().ostream()                              \
+                << "Invalid " << what << " '" << arg << "' at index" << idx \
                 << ", expected "
 }  // namespace
 
@@ -751,12 +756,16 @@ std::ostream& operator<<(std::ostream& out, const Result& r)
 
 Sort::Sort(const CVC4::Type& t) : d_type(new CVC4::Type(t)) {}
 
+Sort::Sort() : d_type(new CVC4::Type()) {}
+
 Sort::~Sort() {}
 
 bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; }
 
 bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; }
 
+bool Sort::isNull() const { return d_type->isNull(); }
+
 bool Sort::isBoolean() const { return d_type->isBoolean(); }
 
 bool Sort::isInteger() const { return d_type->isInteger(); }
@@ -1744,6 +1753,10 @@ Sort Solver::getRoundingmodeSort(void) const
 
 Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const
 {
+  CVC4_API_ARG_CHECK_EXPECTED(!indexSort.isNull(), indexSort)
+      << "non-null index sort";
+  CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
+      << "non-null element sort";
   return d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type);
 }
 
@@ -1769,6 +1782,8 @@ Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const
 
 Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const
 {
+  CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
+      << "non-null codomain sort";
   CVC4_API_ARG_CHECK_EXPECTED(domain.isFirstClass(), domain)
       << "first-class sort as domain sort for function sort";
   CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain)
@@ -1784,9 +1799,14 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const
   for (size_t i = 0, size = sorts.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        !sorts[i].isNull(), "parameter sort", sorts[i], i)
+        << "non-null sort";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
         << "first-class sort as parameter sort for function sort";
   }
+  CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
+      << "non-null codomain sort";
   CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain)
       << "first-class sort as codomain sort for function sort";
   Assert(!codomain.isFunction()); /* A function sort is not first-class. */
@@ -1806,6 +1826,9 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
   for (size_t i = 0, size = sorts.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        !sorts[i].isNull(), "parameter sort", sorts[i], i)
+        << "non-null sort";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
         << "first-class sort as parameter sort for predicate sort";
   }
@@ -1817,8 +1840,13 @@ Sort Solver::mkRecordSort(
     const std::vector<std::pair<std::string, Sort>>& fields) const
 {
   std::vector<std::pair<std::string, Type>> f;
+  size_t i = 0;
   for (const auto& p : fields)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        !p.second.isNull(), "parameter sort", p.second, i)
+        << "non-null sort";
+    i += 1;
     f.emplace_back(p.first, *p.second.d_type);
   }
   return d_exprMgr->mkRecordType(Record(f));
@@ -1826,6 +1854,8 @@ Sort Solver::mkRecordSort(
 
 Sort Solver::mkSetSort(Sort elemSort) const
 {
+  CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
+      << "non-null element sort";
   return d_exprMgr->mkSetType(*elemSort.d_type);
 }
 
@@ -1846,6 +1876,9 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
   for (size_t i = 0, size = sorts.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        !sorts[i].isNull(), "parameter sort", sorts[i], i)
+        << "non-null sort";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i)
         << "non-function-like sort as parameter sort for tuple sort";
   }
@@ -1873,327 +1906,437 @@ Term Solver::mkFalse(void) const { return d_exprMgr->mkConst<bool>(false); }
 
 Term Solver::mkBoolean(bool val) const { return d_exprMgr->mkConst<bool>(val); }
 
-Term Solver::mkInteger(const char* s, uint32_t base) const
-{
-  return d_exprMgr->mkConst(Rational(s, base));
-}
-
-Term Solver::mkInteger(const std::string& s, uint32_t base) const
-{
-  return d_exprMgr->mkConst(Rational(s, base));
-}
-
-Term Solver::mkInteger(int32_t val) const
-{
-  return d_exprMgr->mkConst(Rational(val));
-}
-
-Term Solver::mkInteger(uint32_t val) const
-{
-  return d_exprMgr->mkConst(Rational(val));
-}
-
-Term Solver::mkInteger(int64_t val) const
+Term Solver::mkPi() const
 {
-  return d_exprMgr->mkConst(Rational(val));
+  return d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
 }
 
-Term Solver::mkInteger(uint64_t val) const
+template <typename T>
+Term Solver::mkConstHelper(T t) const
 {
-  return d_exprMgr->mkConst(Rational(val));
+  try
+  {
+    Term res = d_exprMgr->mkConst(t);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (CVC4::TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
-Term Solver::mkPi() const
+/* Split out to avoid nested API calls (problematic with API tracing). */
+Term Solver::mkRealFromStrHelper(std::string s) const
 {
-  return d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+  try
+  {
+    /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
+     * throws an std::invalid_argument exception. For consistency, we treat it
+     * as invalid. */
+    CVC4_API_ARG_CHECK_EXPECTED(s != ".", s)
+        << "a string representing an integer, real or rational value.";
+    CVC4::Rational r = s.find('/') != std::string::npos
+                           ? CVC4::Rational(s)
+                           : CVC4::Rational::fromDecimal(s);
+    return mkConstHelper<CVC4::Rational>(r);
+  }
+  catch (std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
-Term Solver::mkReal(const char* s, uint32_t base) const
+Term Solver::mkReal(const char* s) const
 {
-  return d_exprMgr->mkConst(Rational(s, base));
+  CVC4_API_ARG_CHECK_NOT_NULL(s);
+  return mkRealFromStrHelper(std::string(s));
 }
 
-Term Solver::mkReal(const std::string& s, uint32_t base) const
+Term Solver::mkReal(const std::string& s) const
 {
-  return d_exprMgr->mkConst(Rational(s, base));
+  return mkRealFromStrHelper(s);
 }
 
 Term Solver::mkReal(int32_t val) const
 {
-  return d_exprMgr->mkConst(Rational(val));
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
 }
 
 Term Solver::mkReal(int64_t val) const
 {
-  return d_exprMgr->mkConst(Rational(val));
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
 }
 
 Term Solver::mkReal(uint32_t val) const
 {
-  return d_exprMgr->mkConst(Rational(val));
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
 }
 
 Term Solver::mkReal(uint64_t val) const
 {
-  return d_exprMgr->mkConst(Rational(val));
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
 }
 
 Term Solver::mkReal(int32_t num, int32_t den) const
 {
-  return d_exprMgr->mkConst(Rational(num, den));
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
 }
 
 Term Solver::mkReal(int64_t num, int64_t den) const
 {
-  return d_exprMgr->mkConst(Rational(num, den));
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
 }
 
 Term Solver::mkReal(uint32_t num, uint32_t den) const
 {
-  return d_exprMgr->mkConst(Rational(num, den));
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
 }
 
 Term Solver::mkReal(uint64_t num, uint64_t den) const
 {
-  return d_exprMgr->mkConst(Rational(num, den));
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
 }
 
 Term Solver::mkRegexpEmpty() const
 {
-  return d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<Expr>());
+  try
+  {
+    Term res =
+        d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Expr>());
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::mkRegexpSigma() const
 {
-  return d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<Expr>());
+  try
+  {
+    Term res =
+        d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Expr>());
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::mkEmptySet(Sort s) const
 {
-  return d_exprMgr->mkConst(EmptySet(*s.d_type));
+  CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s)
+      << "null sort or set sort";
+  return mkConstHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
 }
 
 Term Solver::mkSepNil(Sort sort) const
 {
-  return d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+    Term res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::mkString(const char* s) const
 {
-  return d_exprMgr->mkConst(String(s));
+  return mkConstHelper<CVC4::String>(CVC4::String(s));
 }
 
 Term Solver::mkString(const std::string& s) const
 {
-  return d_exprMgr->mkConst(String(s));
+  return mkConstHelper<CVC4::String>(CVC4::String(s));
 }
 
 Term Solver::mkString(const unsigned char c) const
 {
-  return d_exprMgr->mkConst(String(std::string(1, c)));
+  return mkConstHelper<CVC4::String>(CVC4::String(std::string(1, c)));
 }
 
 Term Solver::mkString(const std::vector<unsigned>& s) const
 {
-  return d_exprMgr->mkConst(String(s));
+  return mkConstHelper<CVC4::String>(CVC4::String(s));
 }
 
 Term Solver::mkUniverseSet(Sort sort) const
 {
-  return d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+    Term res =
+        d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
-Term Solver::mkBitVector(uint32_t size) const
+/* Split out to avoid nested API calls (problematic with API tracing). */
+Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
 {
-  return d_exprMgr->mkConst(BitVector(size));
+  CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
+  return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
 }
 
-Term Solver::mkBitVector(uint32_t size, uint32_t val) const
+Term Solver::mkBitVector(uint32_t size, uint64_t val) const
 {
-  return d_exprMgr->mkConst(BitVector(size, val));
+  return mkBVFromIntHelper(size, val);
 }
 
-Term Solver::mkBitVector(uint32_t size, uint64_t val) const
+/* Split out to avoid nested API calls (problematic with API tracing). */
+Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
 {
-  return d_exprMgr->mkConst(BitVector(size, val));
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
+    CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 16, s) << "base 2 or 16";
+    return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
+  }
+  catch (std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkBitVector(const char* s, uint32_t base) const
 {
-  return d_exprMgr->mkConst(BitVector(s, base));
+  CVC4_API_ARG_CHECK_NOT_NULL(s);
+  return mkBVFromStrHelper(std::string(s), base);
 }
 
-Term Solver::mkBitVector(std::string& s, uint32_t base) const
+Term Solver::mkBitVector(const std::string& s, uint32_t base) const
 {
-  return d_exprMgr->mkConst(BitVector(s, base));
+  return mkBVFromStrHelper(s, base);
 }
 
 Term Solver::mkConst(RoundingMode rm) const
 {
-  return d_exprMgr->mkConst(s_rmodes.at(rm));
+  try
+  {
+    return mkConstHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
+  }
+  catch (std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
 }
 
 Term Solver::mkConst(Kind kind, Sort arg) const
 {
-  CVC4_API_KIND_CHECK_EXPECTED(kind == EMPTYSET, kind) << "EMPTY_SET";
-  return d_exprMgr->mkConst(CVC4::EmptySet(*arg.d_type));
+  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 (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";
-  return d_exprMgr->mkConst(CVC4::UninterpretedConstant(*arg1.d_type, arg2));
+  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 d_exprMgr->mkConst<bool>(arg);
+  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 (std::invalid_argument& e)
+    {
+      throw CVC4ApiException(e.what());
+    }
+    catch (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_KIND_CHECK_EXPECTED(kind == CONST_STRING, kind) << "CONST_STRING";
-  return d_exprMgr->mkConst(CVC4::String(arg));
+  CVC4_API_ARG_CHECK_NOT_NULL(arg);
+  return mkConstFromStrHelper(kind, std::string(arg));
 }
 
 Term Solver::mkConst(Kind kind, const std::string& arg) const
 {
-  CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_STRING, kind) << "CONST_STRING";
-  return d_exprMgr->mkConst(CVC4::String(arg));
+  return mkConstFromStrHelper(kind, arg);
+}
+
+/* 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_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL
-                                   || kind == CONST_BITVECTOR,
-                               kind)
-      << "ABSTRACT_VALUE or CONST_RATIONAL or CONST_BITVECTOR";
-  if (kind == ABSTRACT_VALUE)
-  {
-    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg1, arg2)));
-  }
-  if (kind == CONST_RATIONAL)
-  {
-    return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
-  }
-  return d_exprMgr->mkConst(CVC4::BitVector(arg1, arg2));
+  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
 {
-  CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL
-                                   || kind == CONST_BITVECTOR,
-                               kind)
-      << "ABSTRACT_VALUE or CONST_RATIONAL or CONST_BITVECTOR";
-  if (kind == ABSTRACT_VALUE)
-  {
-    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg1, arg2)));
-  }
-  if (kind == CONST_RATIONAL)
-  {
-    return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
-  }
-  return d_exprMgr->mkConst(CVC4::BitVector(arg1, arg2));
+  return mkConstFromStrHelper(kind, arg1, arg2);
 }
 
-Term Solver::mkConst(Kind kind, uint32_t arg) const
+/* 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 == CONST_BITVECTOR,
+  CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL,
                                kind)
-      << "ABSTRACT_VALUE or CONST_RATIONAL or CONST_BITVECTOR";
+      << "ABSTRACT_VALUE or CONST_RATIONAL";
   if (kind == ABSTRACT_VALUE)
   {
-    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
-  }
-  if (kind == CONST_RATIONAL)
-  {
-    return d_exprMgr->mkConst(CVC4::Rational(arg));
+    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 (TypeCheckingException& e)
+    {
+      throw CVC4ApiException(e.getMessage());
+    }
   }
-  return d_exprMgr->mkConst(CVC4::BitVector(arg));
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(a));
 }
 
 Term Solver::mkConst(Kind kind, int32_t arg) const
 {
-  CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL,
-                               kind)
-      << "ABSTRACT_VALUE or CONST_RATIONAL";
-  if (kind == ABSTRACT_VALUE)
-  {
-    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
-  }
-  return d_exprMgr->mkConst(CVC4::Rational(arg));
+  return mkConstFromIntHelper<int64_t>(kind, static_cast<int64_t>(arg));
 }
 
 Term Solver::mkConst(Kind kind, int64_t arg) const
 {
-  CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL,
-                               kind)
-      << "ABSTRACT_VALUE or CONST_RATIONAL";
-  if (kind == ABSTRACT_VALUE)
-  {
-    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
-  }
-  return d_exprMgr->mkConst(CVC4::Rational(arg));
+  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
 {
-  CVC4_API_KIND_CHECK_EXPECTED(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL,
-                               kind)
-      << "ABSTRACT_VALUE or CONST_RATIONAL";
-  if (kind == ABSTRACT_VALUE)
-  {
-    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
-  }
-  return d_exprMgr->mkConst(CVC4::Rational(arg));
+  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_RATIONAL, kind)
-      << "CONST_RATIONAL";
-  return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+  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);
+  }
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
 }
 
 Term Solver::mkConst(Kind kind, int32_t arg1, int32_t arg2) const
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind)
       << "CONST_RATIONAL";
-  return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
 }
 
 Term Solver::mkConst(Kind kind, int64_t arg1, int64_t arg2) const
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind)
       << "CONST_RATIONAL";
-  return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
 }
 
 Term Solver::mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind)
       << "CONST_RATIONAL";
-  return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+  return mkConstHelper<CVC4::Rational>(CVC4::Rational(arg1, arg2));
 }
 
 Term Solver::mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_BITVECTOR, kind)
       << "CONST_BITVECTOR";
-  return d_exprMgr->mkConst(CVC4::BitVector(arg1, arg2));
+  return mkBVFromIntHelper(arg1, arg2);
 }
 
 Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const
 {
   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)
+      << "a bit-vector constant with bit-width '" << bw << "'";
+  CVC4_API_ARG_CHECK_EXPECTED(!arg3.isNull(), arg3) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(
       arg3.getSort().isBitVector() && arg3.d_expr->isConst(), arg3)
       << "bit-vector constant";
-  return d_exprMgr->mkConst(
+  return mkConstHelper<CVC4::FloatingPoint>(
       CVC4::FloatingPoint(arg1, arg2, arg3.d_expr->getConst<BitVector>()));
 }
 
@@ -2202,19 +2345,62 @@ Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const
 
 Term Solver::mkVar(const std::string& symbol, Sort sort) const
 {
-  return d_exprMgr->mkVar(symbol, *sort.d_type);
+  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 (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
-Term Solver::mkVar(Sort sort) const { return d_exprMgr->mkVar(*sort.d_type); }
+Term Solver::mkVar(Sort sort) const
+{
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+    Term res = d_exprMgr->mkVar(*sort.d_type);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
+}
 
 Term Solver::mkBoundVar(const std::string& symbol, Sort sort) const
 {
-  return d_exprMgr->mkBoundVar(symbol, *sort.d_type);
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+    Term res = d_exprMgr->mkBoundVar(symbol, *sort.d_type);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::mkBoundVar(Sort sort) const
 {
-  return d_exprMgr->mkBoundVar(*sort.d_type);
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+    Term res = d_exprMgr->mkBoundVar(*sort.d_type);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 /* Create terms                                                               */
@@ -2269,88 +2455,201 @@ void Solver::checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const
 
 Term Solver::mkTerm(Kind kind) const
 {
-  CVC4_API_KIND_CHECK_EXPECTED(
-      kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
-      << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
-  if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
+  try
   {
-    CVC4::Kind k = extToIntKind(kind);
-    Assert(isDefinedIntKind(k));
-    return d_exprMgr->mkExpr(k, std::vector<Expr>());
+    CVC4_API_KIND_CHECK_EXPECTED(
+        kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
+        << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
+    Term res;
+    if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
+    {
+      CVC4::Kind k = extToIntKind(kind);
+      Assert(isDefinedIntKind(k));
+      res = d_exprMgr->mkExpr(k, std::vector<Expr>());
+    }
+    else
+    {
+      Assert(kind == PI);
+      res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+    }
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
   }
-  Assert(kind == PI);
-  return d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
 }
 
 Term Solver::mkTerm(Kind kind, Sort sort) const
 {
-  CVC4_API_KIND_CHECK_EXPECTED(kind == SEP_NIL || kind == UNIVERSE_SET, kind)
-      << "SEP_NIL or UNIVERSE_SET";
-  return d_exprMgr->mkNullaryOperator(*sort.d_type, extToIntKind(kind));
+  try
+  {
+    CVC4_API_KIND_CHECK_EXPECTED(kind == SEP_NIL, kind) << "SEP_NIL";
+    Term res = d_exprMgr->mkNullaryOperator(*sort.d_type, extToIntKind(kind));
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::mkTerm(Kind kind, Term child) const
 {
-  checkMkTerm(kind, 1);
-  return d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
+    checkMkTerm(kind, 1);
+    Term res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
 {
-  checkMkTerm(kind, 2);
-  return d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr);
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
+    CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+    checkMkTerm(kind, 2);
+    Term res =
+        d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const
 {
-  checkMkTerm(kind, 3);
-  std::vector<Expr> echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr};
-  CVC4::Kind k = extToIntKind(kind);
-  Assert(isDefinedIntKind(k));
-  return kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
-                                : d_exprMgr->mkExpr(k, echildren);
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
+    CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+    CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
+    checkMkTerm(kind, 3);
+    std::vector<Expr> echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr};
+    CVC4::Kind k = extToIntKind(kind);
+    Assert(isDefinedIntKind(k));
+    Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
+                                      : d_exprMgr->mkExpr(k, echildren);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
 {
-  checkMkTerm(kind, children.size());
-  std::vector<Expr> echildren = termVectorToExprs(children);
-  CVC4::Kind k = extToIntKind(kind);
-  Assert(isDefinedIntKind(k));
-  return kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
-                                : d_exprMgr->mkExpr(k, echildren);
-}
-
-Term Solver::mkTerm(OpTerm opTerm) const
-{
-  checkMkOpTerm(opTerm, 0);
-  return d_exprMgr->mkExpr(*opTerm.d_expr);
+  try
+  {
+    for (size_t i = 0, size = children.size(); i < size; ++i)
+    {
+      CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+          !children[i].isNull(), "parameter term", children[i], i)
+          << "non-null term";
+    }
+    checkMkTerm(kind, children.size());
+    std::vector<Expr> echildren = termVectorToExprs(children);
+    CVC4::Kind k = extToIntKind(kind);
+    Assert(isDefinedIntKind(k));
+    Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
+                                      : d_exprMgr->mkExpr(k, echildren);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::mkTerm(OpTerm opTerm, Term child) const
 {
-  checkMkOpTerm(opTerm, 1);
-  return d_exprMgr->mkExpr(*opTerm.d_expr, *child.d_expr);
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
+    checkMkOpTerm(opTerm, 1);
+    Term res = d_exprMgr->mkExpr(*opTerm.d_expr, *child.d_expr);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2) const
 {
-  checkMkOpTerm(opTerm, 2);
-  return d_exprMgr->mkExpr(*opTerm.d_expr, *child1.d_expr, *child2.d_expr);
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
+    CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+    checkMkOpTerm(opTerm, 2);
+    Term res =
+        d_exprMgr->mkExpr(*opTerm.d_expr, *child1.d_expr, *child2.d_expr);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const
 {
-  checkMkOpTerm(opTerm, 3);
-  return d_exprMgr->mkExpr(
-      *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
+    CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+    CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
+    checkMkOpTerm(opTerm, 3);
+    Term res = d_exprMgr->mkExpr(
+        *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 Term Solver::mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
 {
-  checkMkOpTerm(opTerm, children.size());
-  std::vector<Expr> echildren = termVectorToExprs(children);
-  return d_exprMgr->mkExpr(*opTerm.d_expr, echildren);
+  try
+  {
+    for (size_t i = 0, size = children.size(); i < size; ++i)
+    {
+      CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+          !children[i].isNull(), "parameter term", children[i], i)
+          << "non-null term";
+    }
+    checkMkOpTerm(opTerm, children.size());
+    std::vector<Expr> echildren = termVectorToExprs(children);
+    Term res = d_exprMgr->mkExpr(*opTerm.d_expr, echildren);
+    (void)res.d_expr->getType(true); /* kick off type checking */
+    return res;
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 std::vector<Expr> Solver::termVectorToExprs(
@@ -2370,14 +2669,15 @@ std::vector<Expr> Solver::termVectorToExprs(
 OpTerm Solver::mkOpTerm(Kind kind, Kind k)
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP";
-  return d_exprMgr->mkConst(CVC4::Chain(extToIntKind(k)));
+  return *mkConstHelper<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 d_exprMgr->mkConst(CVC4::RecordUpdate(arg));
+  return *mkConstHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg))
+              .d_expr.get();
 }
 
 OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
@@ -2386,39 +2686,60 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
   OpTerm res;
   switch (kind)
   {
-    case DIVISIBLE_OP: res = d_exprMgr->mkConst(CVC4::Divisible(arg)); break;
+    case DIVISIBLE_OP:
+      res = *mkConstHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
+      break;
     case BITVECTOR_REPEAT_OP:
-      res = d_exprMgr->mkConst(CVC4::BitVectorRepeat(arg));
+      res = *mkConstHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
+                 .d_expr.get();
       break;
     case BITVECTOR_ZERO_EXTEND_OP:
-      res = d_exprMgr->mkConst(CVC4::BitVectorZeroExtend(arg));
+      res = *mkConstHelper<CVC4::BitVectorZeroExtend>(
+                 CVC4::BitVectorZeroExtend(arg))
+                 .d_expr.get();
       break;
     case BITVECTOR_SIGN_EXTEND_OP:
-      res = d_exprMgr->mkConst(CVC4::BitVectorSignExtend(arg));
+      res = *mkConstHelper<CVC4::BitVectorSignExtend>(
+                 CVC4::BitVectorSignExtend(arg))
+                 .d_expr.get();
       break;
     case BITVECTOR_ROTATE_LEFT_OP:
-      res = d_exprMgr->mkConst(CVC4::BitVectorRotateLeft(arg));
+      res = *mkConstHelper<CVC4::BitVectorRotateLeft>(
+                 CVC4::BitVectorRotateLeft(arg))
+                 .d_expr.get();
       break;
     case BITVECTOR_ROTATE_RIGHT_OP:
-      res = d_exprMgr->mkConst(CVC4::BitVectorRotateRight(arg));
+      res = *mkConstHelper<CVC4::BitVectorRotateRight>(
+                 CVC4::BitVectorRotateRight(arg))
+                 .d_expr.get();
       break;
     case INT_TO_BITVECTOR_OP:
-      res = d_exprMgr->mkConst(CVC4::IntToBitVector(arg));
+      res = *mkConstHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
+                 .d_expr.get();
       break;
     case FLOATINGPOINT_TO_UBV_OP:
-      res = d_exprMgr->mkConst(CVC4::FloatingPointToUBV(arg));
+      res = *mkConstHelper<CVC4::FloatingPointToUBV>(
+                 CVC4::FloatingPointToUBV(arg))
+                 .d_expr.get();
       break;
     case FLOATINGPOINT_TO_UBV_TOTAL_OP:
-      res = d_exprMgr->mkConst(CVC4::FloatingPointToUBVTotal(arg));
+      res = *mkConstHelper<CVC4::FloatingPointToUBVTotal>(
+                 CVC4::FloatingPointToUBVTotal(arg))
+                 .d_expr.get();
       break;
     case FLOATINGPOINT_TO_SBV_OP:
-      res = d_exprMgr->mkConst(CVC4::FloatingPointToSBV(arg));
+      res = *mkConstHelper<CVC4::FloatingPointToSBV>(
+                 CVC4::FloatingPointToSBV(arg))
+                 .d_expr.get();
       break;
     case FLOATINGPOINT_TO_SBV_TOTAL_OP:
-      res = d_exprMgr->mkConst(CVC4::FloatingPointToSBVTotal(arg));
+      res = *mkConstHelper<CVC4::FloatingPointToSBVTotal>(
+                 CVC4::FloatingPointToSBVTotal(arg))
+                 .d_expr.get();
       break;
     case TUPLE_UPDATE_OP:
-      res = d_exprMgr->mkConst(CVC4::TupleUpdate(arg));
+      res = *mkConstHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg))
+                 .d_expr.get();
       break;
     default:
       CVC4_API_KIND_CHECK_EXPECTED(false, kind)
@@ -2435,29 +2756,39 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2)
   switch (kind)
   {
     case BITVECTOR_EXTRACT_OP:
-      res = d_exprMgr->mkConst(CVC4::BitVectorExtract(arg1, arg2));
+      res = *mkConstHelper<CVC4::BitVectorExtract>(
+                 CVC4::BitVectorExtract(arg1, arg2))
+                 .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
-      res =
-          d_exprMgr->mkConst(CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2));
+      res = *mkConstHelper<CVC4::FloatingPointToFPIEEEBitVector>(
+                 CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
+                 .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
-      res =
-          d_exprMgr->mkConst(CVC4::FloatingPointToFPFloatingPoint(arg1, arg2));
+      res = *mkConstHelper<CVC4::FloatingPointToFPFloatingPoint>(
+                 CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
+                 .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_REAL_OP:
-      res = d_exprMgr->mkConst(CVC4::FloatingPointToFPReal(arg1, arg2));
+      res = *mkConstHelper<CVC4::FloatingPointToFPReal>(
+                 CVC4::FloatingPointToFPReal(arg1, arg2))
+                 .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
-      res = d_exprMgr->mkConst(
-          CVC4::FloatingPointToFPSignedBitVector(arg1, arg2));
+      res = *mkConstHelper<CVC4::FloatingPointToFPSignedBitVector>(
+                 CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
+                 .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
-      res = d_exprMgr->mkConst(
-          CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2));
+      res = *mkConstHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
+                 CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
+                 .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_GENERIC_OP:
-      res = d_exprMgr->mkConst(CVC4::FloatingPointToFPGeneric(arg1, arg2));
+      res = *mkConstHelper<CVC4::FloatingPointToFPGeneric>(
+                 CVC4::FloatingPointToFPGeneric(arg1, arg2))
+                 .d_expr.get();
       break;
     default:
       CVC4_API_KIND_CHECK_EXPECTED(false, kind)
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index d06955a05..e18e3ac6b 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -192,6 +192,11 @@ class CVC4_PUBLIC Sort
   Sort(const CVC4::Type& t);
 
   /**
+   * Constructor.
+   */
+  Sort();
+
+  /**
    * Destructor.
    */
   ~Sort();
@@ -211,6 +216,11 @@ class CVC4_PUBLIC Sort
   bool operator!=(const Sort& s) const;
 
   /**
+   * @return true if this Sort is a null sort.
+   */
+  bool isNull() const;
+
+  /**
    * Is this a Boolean sort?
    * @return true if the sort is a Boolean sort
    */
@@ -1691,14 +1701,6 @@ class CVC4_PUBLIC Solver
   Term mkTerm(Kind kind, const std::vector<Term>& children) const;
 
   /**
-   * Create term with no children from a given operator term.
-   * Create operator terms with mkOpTerm().
-   * @param the operator term
-   * @return the Term
-   */
-  Term mkTerm(OpTerm opTerm) const;
-
-  /**
    * Create unary term from a given operator term.
    * Create operator terms with mkOpTerm().
    * @param the operator term
@@ -1819,128 +1821,84 @@ class CVC4_PUBLIC Solver
   Term mkBoolean(bool val) const;
 
   /**
-   * Create an Integer constant.
-   * @param s the string represetntation of the constant
-   * @param base the base of the string representation
-   * @return the Integer constant
-   */
-  Term mkInteger(const char* s, uint32_t base = 10) const;
-
-  /**
-   * Create an Integer constant.
-   * @param s the string represetntation of the constant
-   * @param base the base of the string representation
-   * @return the Integer constant
-   */
-  Term mkInteger(const std::string& s, uint32_t base = 10) const;
-
-  /**
-   * Create an Integer constant.
-   * @param val the value of the constant
-   * @return the Integer constant
-   */
-  Term mkInteger(int32_t val) const;
-
-  /**
-   * Create an Integer constant.
-   * @param val the value of the constant
-   * @return the Integer constant
-   */
-  Term mkInteger(uint32_t val) const;
-
-  /**
-   * Create an Integer constant.
-   * @param val the value of the constant
-   * @return the Integer constant
-   */
-  Term mkInteger(int64_t val) const;
-
-  /**
-   * Create an Integer constant.
-   * @param val the value of the constant
-   * @return the Integer constant
-   */
-  Term mkInteger(uint64_t val) const;
-
-  /**
    * Create a constant representing the number Pi.
    * @return a constant representing Pi
    */
   Term mkPi() const;
 
   /**
-   * Create an Real constant.
-   * @param s the string represetntation of the constant
-   * @param base the base of the string representation
-   * @return the Real constant
+   * Create a real constant.
+   * @param s the string representation of the constant, may represent an
+   *          integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
+   * @return a constant of sort Real or Integer (if 's' represents an integer)
    */
-  Term mkReal(const char* s, uint32_t base = 10) const;
+  Term mkReal(const char* s) const;
 
   /**
-   * Create an Real constant.
-   * @param s the string represetntation of the constant
-   * @param base the base of the string representation
-   * @return the Real constant
+   * Create a real constant.
+   * @param s the string representation of the constant, may represent an
+   *          integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
+   * @return a constant of sort Real or Integer (if 's' represents an integer)
    */
-  Term mkReal(const std::string& s, uint32_t base = 10) const;
+  Term mkReal(const std::string& s) const;
 
   /**
-   * Create an Real constant.
+   * Create a real constant from an integer.
    * @param val the value of the constant
-   * @return the Real constant
+   * @return a constant of sort Integer
    */
   Term mkReal(int32_t val) const;
 
   /**
-   * Create an Real constant.
+   * Create a real constant from an integer.
    * @param val the value of the constant
-   * @return the Real constant
+   * @return a constant of sort Integer
    */
   Term mkReal(int64_t val) const;
 
   /**
-   * Create an Real constant.
+   * Create a real constant from an unsigned integer.
    * @param val the value of the constant
-   * @return the Real constant
+   * @return a constant of sort Integer
    */
   Term mkReal(uint32_t val) const;
 
   /**
-   * Create an Real constant.
+   * Create a real constant from an unsigned integer.
    * @param val the value of the constant
-   * @return the Real constant
+   * @return a constant of sort Integer
    */
   Term mkReal(uint64_t val) const;
 
   /**
-   * Create an Rational constant.
+   * Create a real constant from a rational.
    * @param num the value of the numerator
    * @param den the value of the denominator
-   * @return the Rational constant
+   * @return a constant of sort Real or Integer (if 'num' is divisible by 'den')
    */
   Term mkReal(int32_t num, int32_t den) const;
 
   /**
-   * Create an Rational constant.
+   * Create a real constant from a rational.
    * @param num the value of the numerator
    * @param den the value of the denominator
-   * @return the Rational constant
+   * @return a constant of sort Real or Integer (if 'num' is divisible by 'den')
    */
   Term mkReal(int64_t num, int64_t den) const;
 
   /**
-   * Create an Rational constant.
+   * Create a real constant from a rational.
    * @param num the value of the numerator
    * @param den the value of the denominator
-   * @return the Rational constant
+   * @return a constant of sort Real or Integer (if 'num' is divisible by 'den')
    */
   Term mkReal(uint32_t num, uint32_t den) const;
 
   /**
-   * Create an Rational constant.
+   * Create a real constant from a rational.
    * @param num the value of the numerator
    * @param den the value of the denominator
-   * @return the Rational constant
+   * @return a constant of sort Real or Integer (if 'num' is divisible by 'den')
    */
   Term mkReal(uint64_t num, uint64_t den) const;
 
@@ -2006,21 +1964,6 @@ class CVC4_PUBLIC Solver
   Term mkUniverseSet(Sort sort) const;
 
   /**
-   * Create a bit-vector constant of given size with value 0.
-   * @param size the bit-width of the bit-vector sort
-   * @return the bit-vector constant
-   */
-  Term mkBitVector(uint32_t size) const;
-
-  /**
-   * Create a bit-vector constant of given size and value.
-   * @param size the bit-width of the bit-vector sort
-   * @param val the value of the constant
-   * @return the bit-vector constant
-   */
-  Term mkBitVector(uint32_t size, uint32_t val) const;
-
-  /**
    * Create a bit-vector constant of given size and value.
    * @param size the bit-width of the bit-vector sort
    * @param val the value of the constant
@@ -2042,7 +1985,7 @@ class CVC4_PUBLIC Solver
    * @param base the base of the string representation
    * @return the bit-vector constant
    */
-  Term mkBitVector(std::string& s, uint32_t base = 2) const;
+  Term mkBitVector(const std::string& s, uint32_t base = 2) const;
 
   /**
    * Create constant of kind:
@@ -2081,6 +2024,8 @@ class CVC4_PUBLIC Solver
 
   /**
    * 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
@@ -2090,6 +2035,8 @@ class CVC4_PUBLIC Solver
 
   /**
    * 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
@@ -2099,33 +2046,28 @@ class CVC4_PUBLIC Solver
 
   /**
    * Create constant of kind:
-   *   - ABSTRACT_VALUE
-   *   - CONST_RATIONAL (for integers, reals)
    *   - 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 = 10) const;
+  Term mkConst(Kind kind, const char* arg1, uint32_t arg2) const;
 
   /**
    * Create constant of kind:
-   *   - ABSTRACT_VALUE
-   *   - CONST_RATIONAL (for integers, reals)
    *   - 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 std::string& arg1, uint32_t arg2 = 10) const;
+  Term mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const;
 
   /**
    * Create constant of kind:
    *   - ABSTRACT_VALUE
    *   - CONST_RATIONAL (for integers, reals)
-   *   - CONST_BITVECTOR
    * See enum Kind for a description of the parameters.
    * @param kind the kind of the constant
    * @param arg the argument to this kind
@@ -2185,6 +2127,7 @@ class CVC4_PUBLIC Solver
   /**
    * 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
@@ -2581,6 +2524,20 @@ class CVC4_PUBLIC Solver
   void checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const;
   /* Helper to check for API misuse in mkOpTerm functions. */
   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;
+  /* 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. */
+  Term mkBVFromStrHelper(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;
 
   /* The expression manager of this solver. */
   std::unique_ptr<ExprManager> d_exprMgr;
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index f91f934f9..a940dbefa 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -70,8 +70,8 @@ enum CVC4_PUBLIC Kind : int32_t
    * Parameters: 1
    *   -[1]: Index of the abstract value
    * Create with:
-   *   mkConst(Kind kind, const char* s, uint32_t base = 10)
-   *   mkConst(Kind kind, const std::string& s, uint32_t base = 10)
+   *   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)
@@ -658,14 +658,11 @@ enum CVC4_PUBLIC Kind : int32_t
    * Parameters:
    *   See mkBitVector().
    * Create with:
-   *   mkBitVector(uint32_t size)
-   *   mkBitVector(uint32_t size, uint32_t val)
    *   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 arg)
    *   mkConst(Kind kind, uint32_t arg1, uint64_t arg2)
    */
   CONST_BITVECTOR,
@@ -1922,7 +1919,7 @@ enum CVC4_PUBLIC Kind : int32_t
    * All set variables must be interpreted as subsets of it.
    * Create with:
    *   mkUniverseSet(Sort sort)
-   *   mkTerm(Kind kind, Sort sort)
+   *   mkConst(Kind kind, Sort sort)
    */
   UNIVERSE_SET,
   /**