New C++ Api: First batch of API guards. (#4557)

This is the first batch of API guards, mainly extending existing guards
in the Solver object with checks that Ops, Terms, Sorts, and datatype objects
are associated to this solver object.

This further changes how DatatypeConstructorDecl objects are created. Previously,
they were not created via the Solver object (while DatatypeDecl was). Now, they are
created via Solver::mkDatatypeConstructorDecl, consistent with how DatatypeDecl
objects are created.

4 files changed, 226 insertions, 50 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 0bfb9a325..f225da333 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -702,8 +702,6 @@ class CVC4ApiExceptionStream
   CVC4_API_CHECK(isDefinedKind(kind)) \
       << "Invalid kind '" << kindToString(kind) << "'";
 
-#define CVC4_API_SORT_CHECK_SOLVER(sort)
-
 #define CVC4_API_KIND_CHECK_EXPECTED(cond, kind) \
   CVC4_PREDICT_TRUE(cond)                        \
   ? (void)0                                      \
@@ -726,12 +724,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_TRUE(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_TRUE(cond)                                                    \
+  ? (void)0                                                                  \
+  : OstreamVoider()                                                          \
+          & CVC4ApiExceptionStream().ostream()                               \
+                << "Invalid " << what << " '" << arg << "' at index " << idx \
                 << ", expected "
 
 #define CVC4_API_SOLVER_TRY_CATCH_BEGIN \
@@ -741,6 +739,19 @@ class CVC4ApiExceptionStream
   }                                                                            \
   catch (const CVC4::Exception& e) { throw CVC4ApiException(e.getMessage()); } \
   catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); }
+
+#define CVC4_API_SOLVER_CHECK_SORT(sort) \
+  CVC4_API_CHECK(this == sort.d_solver)  \
+      << "Given sort is not associated with this solver";
+
+#define CVC4_API_SOLVER_CHECK_TERM(term) \
+  CVC4_API_CHECK(this == term.d_solver)  \
+      << "Given term is not associated with this solver";
+
+#define CVC4_API_SOLVER_CHECK_OP(op)  \
+  CVC4_API_CHECK(this == op.d_solver) \
+      << "Given operator is not associated with this solver";
+
 }  // namespace
 
 /* -------------------------------------------------------------------------- */
@@ -1612,6 +1623,7 @@ Term::const_iterator::const_iterator(const const_iterator& it)
 {
   if (it.d_orig_expr != nullptr)
   {
+    d_solver = it.d_solver;
     d_orig_expr = it.d_orig_expr;
     d_pos = it.d_pos;
   }
@@ -1619,6 +1631,7 @@ Term::const_iterator::const_iterator(const const_iterator& it)
 
 Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it)
 {
+  d_solver = it.d_solver;
   d_orig_expr = it.d_orig_expr;
   d_pos = it.d_pos;
   return *this;
@@ -1630,7 +1643,8 @@ bool Term::const_iterator::operator==(const const_iterator& it) const
   {
     return false;
   }
-  return (*d_orig_expr == *it.d_orig_expr) && (d_pos == it.d_pos);
+  return (d_solver == it.d_solver && *d_orig_expr == *it.d_orig_expr)
+         && (d_pos == it.d_pos);
 }
 
 bool Term::const_iterator::operator!=(const const_iterator& it) const
@@ -1756,8 +1770,14 @@ size_t TermHashFunction::operator()(const Term& t) const
 
 /* DatatypeConstructorDecl -------------------------------------------------- */
 
-DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name)
-    : d_ctor(new CVC4::DatatypeConstructor(name))
+DatatypeConstructorDecl::DatatypeConstructorDecl()
+    : d_solver(nullptr), d_ctor(nullptr)
+{
+}
+
+DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver* slv,
+                                                 const std::string& name)
+    : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(name))
 {
 }
 
@@ -1804,10 +1824,13 @@ std::ostream& operator<<(std::ostream& out,
 
 /* DatatypeDecl ------------------------------------------------------------- */
 
+DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
+
 DatatypeDecl::DatatypeDecl(const Solver* slv,
                            const std::string& name,
                            bool isCoDatatype)
-    : d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype))
+    : d_solver(slv),
+      d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype))
 {
 }
 
@@ -1815,7 +1838,8 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
                            const std::string& name,
                            Sort param,
                            bool isCoDatatype)
-    : d_dtype(new CVC4::Datatype(slv->getExprManager(),
+    : d_solver(slv),
+      d_dtype(new CVC4::Datatype(slv->getExprManager(),
                                  name,
                                  std::vector<Type>{*param.d_type},
                                  isCoDatatype))
@@ -1826,6 +1850,7 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
                            const std::string& name,
                            const std::vector<Sort>& params,
                            bool isCoDatatype)
+    : d_solver(slv)
 {
   std::vector<Type> tparams;
   for (const Sort& p : params)
@@ -1838,8 +1863,6 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
 
 bool DatatypeDecl::isNullHelper() const { return !d_dtype; }
 
-DatatypeDecl::DatatypeDecl() {}
-
 DatatypeDecl::~DatatypeDecl() {}
 
 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor)
@@ -2683,8 +2706,11 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
   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)
+        !children[i].isNull(), "child term", children[i], i)
         << "non-null term";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == children[i].d_solver, "child term", children[i], i)
+        << "a child term associated to this solver object";
   }
 
   std::vector<Expr> echildren = termVectorToExprs(children);
@@ -2749,13 +2775,24 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
 
   std::vector<CVC4::Datatype> datatypes;
-  for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; i++)
-  {
-    CVC4_API_ARG_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0,
-                                dtypedecls[i])
+  for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i)
+  {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == dtypedecls[i].d_solver,
+                                         "datatype declaration",
+                                         dtypedecls[i],
+                                         i)
+        << "a datatype declaration associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0,
+                                         "datatype declaration",
+                                         dtypedecls[i],
+                                         i)
         << "a datatype declaration with at least one constructor";
     datatypes.push_back(dtypedecls[i].getDatatype());
   }
+  for (auto& sort : unresolvedSorts)
+  {
+    CVC4_API_SOLVER_CHECK_SORT(sort);
+  }
   std::set<Type> utypes = sortSetToTypes(unresolvedSorts);
   std::vector<CVC4::DatatypeType> dtypes =
       d_exprMgr->mkMutualDatatypeTypes(datatypes, utypes);
@@ -2778,6 +2815,7 @@ std::vector<Type> Solver::sortVectorToTypes(
   std::vector<Type> res;
   for (const Sort& s : sorts)
   {
+    CVC4_API_SOLVER_CHECK_SORT(s);
     res.push_back(*s.d_type);
   }
   return res;
@@ -2789,6 +2827,7 @@ std::vector<Expr> Solver::termVectorToExprs(
   std::vector<Expr> res;
   for (const Term& t : terms)
   {
+    CVC4_API_SOLVER_CHECK_TERM(t);
     res.push_back(*t.d_expr);
   }
   return res;
@@ -2877,6 +2916,8 @@ Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const
       << "non-null index sort";
   CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
       << "non-null element sort";
+  CVC4_API_SOLVER_CHECK_SORT(indexSort);
+  CVC4_API_SOLVER_CHECK_SORT(elemSort);
 
   return Sort(this,
               d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type));
@@ -2908,6 +2949,8 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
 Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(this == dtypedecl.d_solver)
+      << "Given datatype declaration is not associated with this solver";
   CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl)
       << "a datatype declaration with at least one constructor";
 
@@ -2934,6 +2977,8 @@ Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
       << "non-null codomain sort";
+  CVC4_API_SOLVER_CHECK_SORT(domain);
+  CVC4_API_SOLVER_CHECK_SORT(codomain);
   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)
@@ -2957,11 +3002,15 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const
         !sorts[i].isNull(), "parameter sort", sorts[i], i)
         << "non-null sort";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+        << "sort associated to this solver object";
+    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_SOLVER_CHECK_SORT(codomain);
   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. */
@@ -2991,6 +3040,9 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
         !sorts[i].isNull(), "parameter sort", sorts[i], i)
         << "non-null sort";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+        << "sort associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
         << "first-class sort as parameter sort for predicate sort";
   }
@@ -3012,6 +3064,9 @@ Sort Solver::mkRecordSort(
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !p.second.isNull(), "parameter sort", p.second, i)
         << "non-null sort";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == p.second.d_solver, "parameter sort", p.second, i)
+        << "sort associated to this solver object";
     i += 1;
     f.emplace_back(p.first, *p.second.d_type);
   }
@@ -3026,6 +3081,7 @@ Sort Solver::mkSetSort(Sort elemSort) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
       << "non-null element sort";
+  CVC4_API_SOLVER_CHECK_SORT(elemSort);
 
   return Sort(this, d_exprMgr->mkSetType(*elemSort.d_type));
 
@@ -3059,6 +3115,9 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
         !sorts[i].isNull(), "parameter sort", sorts[i], i)
         << "non-null sort";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+        << "sort associated to this solver object";
+    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";
   }
@@ -3207,6 +3266,8 @@ Term Solver::mkEmptySet(Sort s) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s)
       << "null sort or set sort";
+  CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || this == s.d_solver, s)
+      << "set sort associated to this solver object";
 
   return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
 
@@ -3217,6 +3278,7 @@ Term Solver::mkSepNil(Sort sort) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   Expr res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
   (void)res.getType(true); /* kick off type checking */
@@ -3272,6 +3334,7 @@ Term Solver::mkUniverseSet(Sort sort) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   Expr res =
       d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
@@ -3324,7 +3387,10 @@ Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const
 Term Solver::mkConstArray(Sort sort, Term val) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_NOT_NULL(sort);
   CVC4_API_ARG_CHECK_NOT_NULL(val);
+  CVC4_API_SOLVER_CHECK_SORT(sort);
+  CVC4_API_SOLVER_CHECK_TERM(val);
   CVC4_API_CHECK(sort.isArray()) << "Not an array sort.";
   CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort()))
       << "Value does not match element sort.";
@@ -3405,6 +3471,7 @@ Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   return mkValHelper<CVC4::UninterpretedConstant>(
       CVC4::UninterpretedConstant(*sort.d_type, index));
@@ -3448,6 +3515,7 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
   CVC4_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val)
       << "a bit-vector constant with bit-width '" << bw << "'";
   CVC4_API_ARG_CHECK_EXPECTED(!val.isNull(), val) << "non-null term";
+  CVC4_API_SOLVER_CHECK_TERM(val);
   CVC4_API_ARG_CHECK_EXPECTED(
       val.getSort().isBitVector() && val.d_expr->isConst(), val)
       << "bit-vector constant";
@@ -3465,6 +3533,7 @@ Term Solver::mkConst(Sort sort, const std::string& symbol) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   Expr res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type)
                             : d_exprMgr->mkVar(symbol, *sort.d_type);
@@ -3481,6 +3550,7 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   Expr res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type)
                             : d_exprMgr->mkBoundVar(symbol, *sort.d_type);
@@ -3490,6 +3560,15 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+/* Create datatype constructor declarations                                   */
+/* -------------------------------------------------------------------------- */
+
+DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl(
+    const std::string& name)
+{
+  return DatatypeConstructorDecl(this, name);
+}
+
 /* Create datatype declarations                                               */
 /* -------------------------------------------------------------------------- */
 
@@ -3526,6 +3605,7 @@ 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";
+  CVC4_API_SOLVER_CHECK_TERM(child);
   checkMkTerm(kind, 1);
 
   Expr res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
@@ -3540,6 +3620,8 @@ 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";
+  CVC4_API_SOLVER_CHECK_TERM(child1);
+  CVC4_API_SOLVER_CHECK_TERM(child2);
   checkMkTerm(kind, 2);
 
   Expr res =
@@ -3564,6 +3646,7 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
 Term Solver::mkTerm(Op op) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_OP(op);
 
   Term res;
   if (op.isIndexedHelper())
@@ -3585,7 +3668,9 @@ Term Solver::mkTerm(Op op) const
 Term Solver::mkTerm(Op op, Term child) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_OP(op);
   CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
+  CVC4_API_SOLVER_CHECK_TERM(child);
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
   Expr res;
@@ -3607,8 +3692,11 @@ Term Solver::mkTerm(Op op, Term child) const
 Term Solver::mkTerm(Op op, Term child1, Term child2) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_OP(op);
   CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+  CVC4_API_SOLVER_CHECK_TERM(child1);
+  CVC4_API_SOLVER_CHECK_TERM(child2);
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
   Expr res;
@@ -3630,9 +3718,13 @@ Term Solver::mkTerm(Op op, Term child1, Term child2) const
 Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_OP(op);
   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";
+  CVC4_API_SOLVER_CHECK_TERM(child1);
+  CVC4_API_SOLVER_CHECK_TERM(child2);
+  CVC4_API_SOLVER_CHECK_TERM(child3);
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
   Expr res;
@@ -3656,11 +3748,15 @@ Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
 Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_OP(op);
   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)
+        !children[i].isNull(), "child term", children[i], i)
         << "non-null term";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == children[i].d_solver, "child term", children[i], i)
+        << "child term associated to this solver object";
   }
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
@@ -3690,6 +3786,12 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
   std::vector<CVC4::Expr> args;
   for (size_t i = 0, size = sorts.size(); i < size; i++)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == terms[i].d_solver, "child term", terms[i], i)
+        << "child term associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == sorts[i].d_solver, "child sort", sorts[i], i)
+        << "child sort associated to this solver object";
     args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr);
   }
 
@@ -3913,12 +4015,13 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
 /* Non-SMT-LIB commands                                                       */
 /* -------------------------------------------------------------------------- */
 
-Term Solver::simplify(const Term& t)
+Term Solver::simplify(const Term& term)
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_ARG_CHECK_NOT_NULL(t);
+  CVC4_API_ARG_CHECK_NOT_NULL(term);
+  CVC4_API_SOLVER_CHECK_TERM(term);
 
-  return Term(this, d_smtEngine->simplify(*t.d_expr));
+  return Term(this, d_smtEngine->simplify(*term.d_expr));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3932,6 +4035,7 @@ Result Solver::checkEntailed(Term term) const
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC4_API_ARG_CHECK_NOT_NULL(term);
+  CVC4_API_SOLVER_CHECK_TERM(term);
 
   CVC4::Result r = d_smtEngine->checkEntailed(*term.d_expr);
   return Result(r);
@@ -3949,6 +4053,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const
          "(try --incremental)";
   for (const Term& term : terms)
   {
+    CVC4_API_SOLVER_CHECK_TERM(term);
     CVC4_API_ARG_CHECK_NOT_NULL(term);
   }
 
@@ -3967,10 +4072,11 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const
  */
 void Solver::assertFormula(Term term) const
 {
-  // CHECK:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_TERM(term);
+  CVC4_API_ARG_CHECK_NOT_NULL(term);
   d_smtEngine->assertFormula(*term.d_expr);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -3978,10 +4084,15 @@ void Solver::assertFormula(Term term) const
  */
 Result Solver::checkSat(void) const
 {
-  // CHECK:
-  // if d_queryMade -> incremental enabled
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(!d_smtEngine->isQueryMade()
+                 || CVC4::options::incrementalSolving())
+      << "Cannot make multiple queries unless incremental solving is enabled "
+         "(try --incremental)";
   CVC4::Result r = d_smtEngine->checkSat();
   return Result(r);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -3989,10 +4100,16 @@ Result Solver::checkSat(void) const
  */
 Result Solver::checkSatAssuming(Term assumption) const
 {
-  // CHECK:
-  // if assumptions.size() > 0:  incremental enabled?
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(!d_smtEngine->isQueryMade()
+                 || CVC4::options::incrementalSolving())
+      << "Cannot make multiple queries unless incremental solving is enabled "
+         "(try --incremental)";
+  CVC4_API_SOLVER_CHECK_TERM(assumption);
   CVC4::Result r = d_smtEngine->checkSat(*assumption.d_expr);
   return Result(r);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4000,11 +4117,21 @@ Result Solver::checkSatAssuming(Term assumption) const
  */
 Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
 {
-  // CHECK:
-  // if assumptions.size() > 0:  incremental enabled?
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0
+                 || CVC4::options::incrementalSolving())
+      << "Cannot make multiple queries unless incremental solving is enabled "
+         "(try --incremental)";
+  for (const Term& term : assumptions)
+  {
+    CVC4_API_SOLVER_CHECK_TERM(term);
+    CVC4_API_ARG_CHECK_NOT_NULL(term);
+  }
   std::vector<Expr> eassumptions = termVectorToExprs(assumptions);
   CVC4::Result r = d_smtEngine->checkSat(eassumptions);
   return Result(r);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4014,14 +4141,21 @@ Sort Solver::declareDatatype(
     const std::string& symbol,
     const std::vector<DatatypeConstructorDecl>& ctors) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(ctors.size() > 0, ctors)
       << "a datatype declaration with at least one constructor";
   DatatypeDecl dtdecl(this, symbol);
-  for (const DatatypeConstructorDecl& ctor : ctors)
+  for (size_t i = 0, size = ctors.size(); i < size; i++)
   {
-    dtdecl.addConstructor(ctor);
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == ctors[i].d_solver,
+                                         "datatype constructor declaration",
+                                         ctors[i],
+                                         i)
+        << "datatype constructor declaration associated to this solver object";
+    dtdecl.addConstructor(ctors[i]);
   }
   return Sort(this, d_exprMgr->mkDatatypeType(*dtdecl.d_dtype));
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4031,14 +4165,19 @@ Term Solver::declareFun(const std::string& symbol,
                         const std::vector<Sort>& sorts,
                         Sort sort) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   for (size_t i = 0, size = sorts.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+        << "parameter sort associated to this solver object";
+    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(sort.isFirstClass(), sort)
       << "first-class sort as function codomain sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
   Assert(!sort.isFunction()); /* A function sort is not first-class. */
   Type type = *sort.d_type;
   if (!sorts.empty())
@@ -4047,6 +4186,7 @@ Term Solver::declareFun(const std::string& symbol,
     type = d_exprMgr->mkFunctionType(types, type);
   }
   return Term(this, d_exprMgr->mkVar(symbol, type));
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 87be7b74c..855ba4400 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1167,14 +1167,13 @@ class DatatypeIterator;
 class CVC4_PUBLIC DatatypeConstructorDecl
 {
   friend class DatatypeDecl;
+  friend class Solver;
 
  public:
   /**
-   * Constructor.
-   * @param name the name of the datatype constructor
-   * @return the DatatypeConstructorDecl
+   * Nullary constructor for Cython.
    */
-  DatatypeConstructorDecl(const std::string& name);
+  DatatypeConstructorDecl();
 
   /**
    * Add datatype selector declaration.
@@ -1199,6 +1198,19 @@ class CVC4_PUBLIC DatatypeConstructorDecl
 
  private:
   /**
+   * Constructor.
+   * @param slv the associated solver object
+   * @param name the name of the datatype constructor
+   * @return the DatatypeConstructorDecl
+   */
+  DatatypeConstructorDecl(const Solver* slv, const std::string& name);
+
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
+  /**
    * The internal (intermediate) datatype constructor wrapped by this
    * datatype constructor declaration.
    * This is a shared_ptr rather than a unique_ptr since
@@ -1219,7 +1231,7 @@ class CVC4_PUBLIC DatatypeDecl
 
  public:
   /**
-   * Nullary constructor for Cython
+   * Nullary constructor for Cython.
    */
   DatatypeDecl();
 
@@ -1240,6 +1252,9 @@ class CVC4_PUBLIC DatatypeDecl
   /** Is this Datatype declaration parametric? */
   bool isParametric() const;
 
+  /**
+   * @return true if this DatatypeDecl is a null object
+   */
   bool isNull() const;
 
   /**
@@ -1257,7 +1272,7 @@ class CVC4_PUBLIC DatatypeDecl
  private:
   /**
    * Constructor.
-   * @param slv the solver that created this datatype declaration
+   * @param slv the associated solver object
    * @param name the name of the datatype
    * @param isCoDatatype true if a codatatype is to be constructed
    * @return the DatatypeDecl
@@ -1269,7 +1284,7 @@ class CVC4_PUBLIC DatatypeDecl
   /**
    * Constructor for parameterized datatype declaration.
    * Create sorts parameter with Solver::mkParamSort().
-   * @param slv the solver that created this datatype declaration
+   * @param slv the associated solver object
    * @param name the name of the datatype
    * @param param the sort parameter
    * @param isCoDatatype true if a codatatype is to be constructed
@@ -1282,7 +1297,7 @@ class CVC4_PUBLIC DatatypeDecl
   /**
    * Constructor for parameterized datatype declaration.
    * Create sorts parameter with Solver::mkParamSort().
-   * @param slv the solver that created this datatype declaration
+   * @param slv the associated solver object
    * @param name the name of the datatype
    * @param params a list of sort parameters
    * @param isCoDatatype true if a codatatype is to be constructed
@@ -1292,9 +1307,17 @@ class CVC4_PUBLIC DatatypeDecl
                const std::vector<Sort>& params,
                bool isCoDatatype = false);
 
-  // helper for isNull() to avoid calling API functions from other API functions
+  /**
+   * Helper for isNull checks. This prevents calling an API function with
+   * CVC4_API_CHECK_NOT_NULL
+   */
   bool isNullHelper() const;
 
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
   /* The internal (intermediate) datatype wrapped by this datatype
    * declaration
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -2680,6 +2703,12 @@ class CVC4_PUBLIC Solver
   Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
 
   /* .................................................................... */
+  /* Create datatype constructor declarations                             */
+  /* .................................................................... */
+
+  DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name);
+
+  /* .................................................................... */
   /* Create datatype declarations                                         */
   /* .................................................................... */
 
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 1c7071958..2ca4b3645 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -54,7 +54,6 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
 
 
     cdef cppclass DatatypeConstructorDecl:
-        DatatypeConstructorDecl(const string& name) except +
         void addSelector(const string& name, Sort sort) except +
         void addSelectorSelf(const string& name) except +
         string toString() except +
@@ -160,6 +159,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         # default value for symbol defined in cvc4cpp.h
         Term mkConst(Sort sort) except +
         Term mkVar(Sort sort, const string& symbol) except +
+        DatatypeConstructorDecl mkDatatypeConstructorDecl(const string& name) except +
         DatatypeDecl mkDatatypeDecl(const string& name) except +
         DatatypeDecl mkDatatypeDecl(const string& name, bint isCoDatatype) except +
         DatatypeDecl mkDatatypeDecl(const string& name, Sort param) except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index fa5313f0e..e742e0061 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -134,12 +134,14 @@ cdef class DatatypeConstructor:
 
 
 cdef class DatatypeConstructorDecl:
-    cdef c_DatatypeConstructorDecl* cddc
-    def __cinit__(self, str name):
-        self.cddc = new c_DatatypeConstructorDecl(name.encode())
+    cdef c_DatatypeConstructorDecl cddc
+
+    def __cinit__(self):
+      pass
 
     def addSelector(self, str name, Sort sort):
         self.cddc.addSelector(name.encode(), sort.csort)
+
     def addSelectorSelf(self, str name):
         self.cddc.addSelectorSelf(name.encode())
 
@@ -156,7 +158,7 @@ cdef class DatatypeDecl:
         pass
 
     def addConstructor(self, DatatypeConstructorDecl ctor):
-        self.cdd.addConstructor(ctor.cddc[0])
+        self.cdd.addConstructor(ctor.cddc)
 
     def isParametric(self):
         return self.cdd.isParametric()
@@ -675,6 +677,11 @@ cdef class Solver:
                                             (<str?> symbol).encode())
         return term
 
+    def mkDatatypeConstructorDecl(self, str name):
+        cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl()
+        ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
+        return ddc
+
     def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
         cdef DatatypeDecl dd = DatatypeDecl()
         cdef vector[c_Sort] v
@@ -790,7 +797,7 @@ cdef class Solver:
         cdef vector[c_DatatypeConstructorDecl] v
 
         for c in ctors:
-            v.push_back((<DatatypeConstructorDecl?> c).cddc[0])
+            v.push_back((<DatatypeConstructorDecl?> c).cddc)
         sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
         return sort