New C++ API: Reorganize Solver code (move only). (#3170)

1 files changed, 193 insertions, 143 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 1538d3558..ad49efce6 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1936,6 +1936,146 @@ Solver::Solver(Options* opts)
 
 Solver::~Solver() {}
 
+/* Helpers                                                                    */
+/* -------------------------------------------------------------------------- */
+
+/* Split out to avoid nested API calls (problematic with API tracing).        */
+/* .......................................................................... */
+
+template <typename T>
+Term Solver::mkValHelper(T t) const
+{
+  Term res = d_exprMgr->mkConst(t);
+  (void)res.d_expr->getType(true); /* kick off type checking */
+  return res;
+}
+
+Term Solver::mkRealFromStrHelper(std::string s) const
+{
+  /* 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 mkValHelper<CVC4::Rational>(r);
+}
+
+Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
+
+  return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
+{
+  CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
+  CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
+      << "base 2, 10, or 16";
+
+  return mkValHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
+}
+
+Term Solver::mkBVFromStrHelper(uint32_t size,
+                               std::string s,
+                               uint32_t base) const
+{
+  CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
+  CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
+      << "base 2, 10, or 16";
+
+  Integer val(s, base);
+  CVC4_API_CHECK(val.modByPow2(size) == val)
+      << "Overflow in bitvector construction (specified bitvector size " << size
+      << " too small to hold value " << s << ")";
+
+  return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+}
+
+/* Helpers for converting vectors.                                            */
+/* .......................................................................... */
+
+std::vector<Type> Solver::sortVectorToTypes(
+    const std::vector<Sort>& sorts) const
+{
+  std::vector<Type> res;
+  for (const Sort& s : sorts)
+  {
+    res.push_back(*s.d_type);
+  }
+  return res;
+}
+
+std::vector<Expr> Solver::termVectorToExprs(
+    const std::vector<Term>& terms) const
+{
+  std::vector<Expr> res;
+  for (const Term& t : terms)
+  {
+    res.push_back(*t.d_expr);
+  }
+  return res;
+}
+
+/* Helpers for mkTerm checks.                                                  */
+/* .......................................................................... */
+
+void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
+{
+  CVC4_API_KIND_CHECK(kind);
+  Assert(isDefinedIntKind(extToIntKind(kind)));
+  const CVC4::kind::MetaKind mk = kind::metaKindOf(extToIntKind(kind));
+  CVC4_API_KIND_CHECK_EXPECTED(
+      mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
+      kind)
+      << "Only operator-style terms are created with mkTerm(), "
+         "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 "
+      << minArity(kind) << " children and at most " << maxArity(kind)
+      << " children (the one under construction has " << nchildren << ")";
+}
+
+void Solver::checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const
+{
+  Assert(isDefinedIntKind(extToIntKind(kind)));
+  const CVC4::Kind int_kind = extToIntKind(kind);
+  const CVC4::Kind int_op_kind = opTerm.d_expr->getKind();
+  const CVC4::Kind int_op_to_kind =
+      NodeManager::operatorToKind(opTerm.d_expr->getNode());
+  CVC4_API_ARG_CHECK_EXPECTED(
+      int_kind == int_op_to_kind
+          || (kind == APPLY_CONSTRUCTOR
+              && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
+          || (kind == APPLY_SELECTOR
+              && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
+          || (kind == APPLY_UF && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND),
+      kind)
+      << "kind that matches kind associated with given operator term";
+  CVC4_API_ARG_CHECK_EXPECTED(
+      int_op_kind == CVC4::kind::BUILTIN
+          || CVC4::kind::metaKindOf(int_kind) == kind::metakind::PARAMETERIZED,
+      opTerm)
+      << "This term constructor is for parameterized kinds only";
+  uint32_t min_arity = ExprManager::minArity(int_kind);
+  uint32_t max_arity = ExprManager::maxArity(int_kind);
+  CVC4_API_KIND_CHECK_EXPECTED(nchildren >= min_arity && nchildren <= max_arity,
+                               kind)
+      << "Terms with kind " << kindToString(kind) << " must have at least "
+      << min_arity << " children and at most " << max_arity
+      << " children (the one under construction has " << nchildren << ")";
+}
+
 /* Sorts Handling                                                             */
 /* -------------------------------------------------------------------------- */
 
@@ -1999,6 +2139,7 @@ Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const
       << "non-null element sort";
 
   return d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type);
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2008,6 +2149,7 @@ Sort Solver::mkBitVectorSort(uint32_t size) const
   CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0";
 
   return d_exprMgr->mkBitVectorType(size);
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2018,6 +2160,7 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
   CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0";
 
   return d_exprMgr->mkFloatingPointType(exp, sig);
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2028,6 +2171,7 @@ Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const
       << "a datatype declaration with at least one constructor";
 
   return d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype);
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2043,6 +2187,7 @@ Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const
   Assert(!codomain.isFunction()); /* A function sort is not first-class. */
 
   return d_exprMgr->mkFunctionType(*domain.d_type, *codomain.d_type);
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2068,6 +2213,7 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const
 
   std::vector<Type> argTypes = sortVectorToTypes(sorts);
   return d_exprMgr->mkFunctionType(argTypes, *codomain.d_type);
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2095,6 +2241,7 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
   std::vector<Type> types = sortVectorToTypes(sorts);
 
   return d_exprMgr->mkPredicateType(types);
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2114,6 +2261,7 @@ Sort Solver::mkRecordSort(
   }
 
   return d_exprMgr->mkRecordType(Record(f));
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2124,6 +2272,7 @@ Sort Solver::mkSetSort(Sort elemSort) const
       << "non-null element sort";
 
   return d_exprMgr->mkSetType(*elemSort.d_type);
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2141,6 +2290,7 @@ Sort Solver::mkSortConstructorSort(const std::string& symbol,
   CVC4_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0";
 
   return d_exprMgr->mkSortConstructor(symbol, arity);
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2159,18 +2309,8 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
   std::vector<Type> types = sortVectorToTypes(sorts);
 
   return d_exprMgr->mkTupleType(types);
-  CVC4_API_SOLVER_TRY_CATCH_END;
-}
 
-std::vector<Type> Solver::sortVectorToTypes(
-    const std::vector<Sort>& sorts) const
-{
-  std::vector<Type> res;
-  for (const Sort& s : sorts)
-  {
-    res.push_back(*s.d_type);
-  }
-  return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /* Create consts                                                              */
@@ -2200,35 +2340,12 @@ Term Solver::mkBoolean(bool val) const
 Term Solver::mkPi() const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+
   Term res =
       d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
-  CVC4_API_SOLVER_TRY_CATCH_END;
-}
-
-template <typename T>
-Term Solver::mkValHelper(T t) const
-{
-  Term res = d_exprMgr->mkConst(t);
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
-}
 
-/* Split out to avoid nested API calls (problematic with API tracing). */
-Term Solver::mkRealFromStrHelper(std::string s) const
-{
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  /* 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 mkValHelper<CVC4::Rational>(r);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2238,6 +2355,7 @@ Term Solver::mkReal(const char* s) const
   CVC4_API_ARG_CHECK_NOT_NULL(s);
 
   return mkRealFromStrHelper(std::string(s));
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2312,16 +2430,19 @@ Term Solver::mkRegexpEmpty() const
       d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Expr>());
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::mkRegexpSigma() const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+
   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;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2332,6 +2453,7 @@ Term Solver::mkEmptySet(Sort s) const
       << "null sort or set sort";
 
   return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2343,6 +2465,7 @@ Term Solver::mkSepNil(Sort sort) const
   Term res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2384,16 +2507,7 @@ Term Solver::mkUniverseSet(Sort sort) const
   // TODO(#2771): Reenable?
   // (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
-  CVC4_API_SOLVER_TRY_CATCH_END;
-}
-
-/* Split out to avoid nested API calls (problematic with API tracing). */
-Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
-{
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
 
-  return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2404,41 +2518,13 @@ Term Solver::mkBitVector(uint32_t size, uint64_t val) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-/* Split out to avoid nested API calls (problematic with API tracing). */
-Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
-{
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
-  CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
-      << "base 2, 10, or 16";
-
-  return mkValHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
-  CVC4_API_SOLVER_TRY_CATCH_END;
-}
-
-Term Solver::mkBVFromStrHelper(uint32_t size,
-                               std::string s,
-                               uint32_t base) const
-{
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
-  CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
-      << "base 2, 10, or 16";
-
-  Integer val(s, base);
-  CVC4_API_CHECK(val.modByPow2(size) == val)
-      << "Overflow in bitvector construction (specified bitvector size " << size
-      << " too small to hold value " << s << ")";
-  return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
-  CVC4_API_SOLVER_TRY_CATCH_END;
-}
-
 Term Solver::mkBitVector(const char* s, uint32_t base) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(s);
 
   return mkBVFromStrHelper(std::string(s), base);
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2453,7 +2539,6 @@ Term Solver::mkBitVector(uint32_t size, const char* s, uint32_t base) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(s);
-
   return mkBVFromStrHelper(size, s, base);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -2473,6 +2558,7 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
 
   return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), false));
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2484,6 +2570,7 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
 
   return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2495,6 +2582,7 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
 
   return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2506,6 +2594,7 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
 
   return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), false));
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2517,6 +2606,7 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
 
   return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2534,6 +2624,7 @@ Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const
 
   return mkValHelper<CVC4::UninterpretedConstant>(
       CVC4::UninterpretedConstant(*sort.d_type, index));
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2579,6 +2670,7 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
 
   return mkValHelper<CVC4::FloatingPoint>(
       CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>()));
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2594,6 +2686,7 @@ Term Solver::mkConst(Sort sort, const std::string& symbol) const
                             : d_exprMgr->mkVar(symbol, *sort.d_type);
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2609,61 +2702,13 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
                             : d_exprMgr->mkBoundVar(symbol, *sort.d_type);
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /* Create terms                                                               */
 /* -------------------------------------------------------------------------- */
 
-void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
-{
-  CVC4_API_KIND_CHECK(kind);
-  Assert(isDefinedIntKind(extToIntKind(kind)));
-  const CVC4::kind::MetaKind mk = kind::metaKindOf(extToIntKind(kind));
-  CVC4_API_KIND_CHECK_EXPECTED(
-      mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
-      kind)
-      << "Only operator-style terms are created with mkTerm(), "
-         "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 "
-      << minArity(kind) << " children and at most " << maxArity(kind)
-      << " children (the one under construction has " << nchildren << ")";
-}
-
-void Solver::checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const
-{
-  Assert(isDefinedIntKind(extToIntKind(kind)));
-  const CVC4::Kind int_kind = extToIntKind(kind);
-  const CVC4::Kind int_op_kind = opTerm.d_expr->getKind();
-  const CVC4::Kind int_op_to_kind =
-      NodeManager::operatorToKind(opTerm.d_expr->getNode());
-  CVC4_API_ARG_CHECK_EXPECTED(
-      int_kind == int_op_to_kind
-          || (kind == APPLY_CONSTRUCTOR
-              && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
-          || (kind == APPLY_SELECTOR
-              && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
-          || (kind == APPLY_UF && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND),
-      kind)
-      << "kind that matches kind associated with given operator term";
-  CVC4_API_ARG_CHECK_EXPECTED(
-      int_op_kind == CVC4::kind::BUILTIN
-          || CVC4::kind::metaKindOf(int_kind) == kind::metakind::PARAMETERIZED,
-      opTerm)
-      << "This term constructor is for parameterized kinds only";
-  uint32_t min_arity = ExprManager::minArity(int_kind);
-  uint32_t max_arity = ExprManager::maxArity(int_kind);
-  CVC4_API_KIND_CHECK_EXPECTED(nchildren >= min_arity && nchildren <= max_arity,
-                               kind)
-      << "Terms with kind " << kindToString(kind) << " must have at least "
-      << min_arity << " children and at most " << max_arity
-      << " children (the one under construction has " << nchildren << ")";
-}
-
 Term Solver::mkTerm(Kind kind) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
@@ -2685,6 +2730,7 @@ Term Solver::mkTerm(Kind kind) const
   }
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2692,11 +2738,12 @@ Term Solver::mkTerm(Kind kind, Term child) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   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;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2705,12 +2752,13 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   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;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2720,8 +2768,8 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const
   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));
@@ -2729,6 +2777,7 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const
                                     : d_exprMgr->mkExpr(k, echildren);
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2741,8 +2790,8 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
         !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));
@@ -2750,6 +2799,7 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
                                     : d_exprMgr->mkExpr(k, echildren);
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2757,10 +2807,12 @@ Term Solver::mkTerm(Kind kind, OpTerm opTerm) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   checkMkOpTerm(kind, opTerm, 0);
+
   const CVC4::Kind int_kind = extToIntKind(kind);
   Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr);
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2768,12 +2820,13 @@ Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
-
   checkMkOpTerm(kind, opTerm, 1);
+
   const CVC4::Kind int_kind = extToIntKind(kind);
   Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, *child.d_expr);
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2782,8 +2835,8 @@ Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
-
   checkMkOpTerm(kind, opTerm, 2);
+
   const CVC4::Kind int_kind = extToIntKind(kind);
   Term res = d_exprMgr->mkExpr(
       int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr);
@@ -2799,13 +2852,14 @@ Term Solver::mkTerm(
   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(kind, opTerm, 3);
+
   const CVC4::Kind int_kind = extToIntKind(kind);
   Term res = d_exprMgr->mkExpr(
       int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr);
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2820,13 +2874,14 @@ Term Solver::mkTerm(Kind kind,
         !children[i].isNull(), "parameter term", children[i], i)
         << "non-null term";
   }
-
   checkMkOpTerm(kind, opTerm, children.size());
+
   const CVC4::Kind int_kind = extToIntKind(kind);
   std::vector<Expr> echildren = termVectorToExprs(children);
   Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, echildren);
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2836,7 +2891,6 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_CHECK(sorts.size() == terms.size())
       << "Expected the same number of sorts and elements";
-
   std::vector<CVC4::Expr> args;
   for (size_t i = 0, size = sorts.size(); i < size; i++)
   {
@@ -2850,18 +2904,8 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
                                args);
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
-  CVC4_API_SOLVER_TRY_CATCH_END;
-}
 
-std::vector<Expr> Solver::termVectorToExprs(
-    const std::vector<Term>& terms) const
-{
-  std::vector<Expr> res;
-  for (const Term& t : terms)
-  {
-    res.push_back(*t.d_expr);
-  }
-  return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /* Create operator terms                                                      */
@@ -2873,6 +2917,7 @@ OpTerm Solver::mkOpTerm(Kind kind, Kind k) const
   CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP";
 
   return *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2899,6 +2944,7 @@ OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) const
                .d_expr.get();
   }
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2971,6 +3017,7 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) const
   }
   Assert(!res.isNull());
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -3023,6 +3070,7 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) const
   }
   Assert(!res.isNull());
   return res;
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -3511,6 +3559,7 @@ void Solver::pop(uint32_t nscopes) const
   {
     d_smtEngine->pop();
   }
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -3533,6 +3582,7 @@ void Solver::push(uint32_t nscopes) const
   {
     d_smtEngine->push();
   }
+
   CVC4_API_SOLVER_TRY_CATCH_END;
 }