From 50edf184492d20f4acb7b8d82f3843f3146f77d5 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 2 Jun 2020 09:09:15 -0700
Subject: New C++ API: Keep reference to solver object in non-solver objects.
 (#4549)

This is in preparation for adding guards to ensure that sort and term
arguments belong to the same solver.
---
 src/api/cvc4cpp.cpp | 545 +++++++++++++++++++++++++++++-----------------------
 src/api/cvc4cpp.h   | 111 +++++++++--
 2 files changed, 395 insertions(+), 261 deletions(-)

(limited to 'src/api')

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 1ea421c4b..0bfb9a325 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -702,6 +702,8 @@ 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                                      \
@@ -823,9 +825,12 @@ std::ostream& operator<<(std::ostream& out, const Result& r)
 /* Sort                                                                       */
 /* -------------------------------------------------------------------------- */
 
-Sort::Sort(const CVC4::Type& t) : d_type(new CVC4::Type(t)) {}
+Sort::Sort(const Solver* slv, const CVC4::Type& t)
+    : d_solver(slv), d_type(new CVC4::Type(t))
+{
+}
 
-Sort::Sort() : d_type(new CVC4::Type()) {}
+Sort::Sort() : d_solver(nullptr), d_type(new CVC4::Type()) {}
 
 Sort::~Sort() {}
 
@@ -909,7 +914,7 @@ bool Sort::isComparableTo(Sort s) const
 Datatype Sort::getDatatype() const
 {
   CVC4_API_CHECK(isDatatype()) << "Expected datatype sort.";
-  return DatatypeType(*d_type).getDatatype();
+  return Datatype(d_solver, DatatypeType(*d_type).getDatatype());
 }
 
 Sort Sort::instantiate(const std::vector<Sort>& params) const
@@ -923,10 +928,10 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   }
   if (d_type->isDatatype())
   {
-    return DatatypeType(*d_type).instantiate(tparams);
+    return Sort(d_solver, DatatypeType(*d_type).instantiate(tparams));
   }
   Assert(d_type->isSortConstructor());
-  return SortConstructorType(*d_type).instantiate(tparams);
+  return Sort(d_solver, SortConstructorType(*d_type).instantiate(tparams));
 }
 
 std::string Sort::toString() const { return d_type->toString(); }
@@ -947,13 +952,13 @@ std::vector<Sort> Sort::getConstructorDomainSorts() const
 {
   CVC4_API_CHECK(isConstructor()) << "Not a function sort.";
   std::vector<CVC4::Type> types = ConstructorType(*d_type).getArgTypes();
-  return typeVectorToSorts(types);
+  return typeVectorToSorts(d_solver, types);
 }
 
 Sort Sort::getConstructorCodomainSort() const
 {
   CVC4_API_CHECK(isConstructor()) << "Not a function sort.";
-  return ConstructorType(*d_type).getRangeType();
+  return Sort(d_solver, ConstructorType(*d_type).getRangeType());
 }
 
 /* Function sort ------------------------------------------------------- */
@@ -968,13 +973,13 @@ std::vector<Sort> Sort::getFunctionDomainSorts() const
 {
   CVC4_API_CHECK(isFunction()) << "Not a function sort.";
   std::vector<CVC4::Type> types = FunctionType(*d_type).getArgTypes();
-  return typeVectorToSorts(types);
+  return typeVectorToSorts(d_solver, types);
 }
 
 Sort Sort::getFunctionCodomainSort() const
 {
   CVC4_API_CHECK(isFunction()) << "Not a function sort.";
-  return FunctionType(*d_type).getRangeType();
+  return Sort(d_solver, FunctionType(*d_type).getRangeType());
 }
 
 /* Array sort ---------------------------------------------------------- */
@@ -982,13 +987,13 @@ Sort Sort::getFunctionCodomainSort() const
 Sort Sort::getArrayIndexSort() const
 {
   CVC4_API_CHECK(isArray()) << "Not an array sort.";
-  return ArrayType(*d_type).getIndexType();
+  return Sort(d_solver, ArrayType(*d_type).getIndexType());
 }
 
 Sort Sort::getArrayElementSort() const
 {
   CVC4_API_CHECK(isArray()) << "Not an array sort.";
-  return ArrayType(*d_type).getConstituentType();
+  return Sort(d_solver, ArrayType(*d_type).getConstituentType());
 }
 
 /* Set sort ------------------------------------------------------------ */
@@ -996,7 +1001,7 @@ Sort Sort::getArrayElementSort() const
 Sort Sort::getSetElementSort() const
 {
   CVC4_API_CHECK(isSet()) << "Not a set sort.";
-  return SetType(*d_type).getElementType();
+  return Sort(d_solver, SetType(*d_type).getElementType());
 }
 
 /* Uninterpreted sort -------------------------------------------------- */
@@ -1017,7 +1022,7 @@ std::vector<Sort> Sort::getUninterpretedSortParamSorts() const
 {
   CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
   std::vector<CVC4::Type> types = SortType(*d_type).getParamTypes();
-  return typeVectorToSorts(types);
+  return typeVectorToSorts(d_solver, types);
 }
 
 /* Sort constructor sort ----------------------------------------------- */
@@ -1062,7 +1067,7 @@ std::vector<Sort> Sort::getDatatypeParamSorts() const
 {
   CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
   std::vector<CVC4::Type> types = DatatypeType(*d_type).getParamTypes();
-  return typeVectorToSorts(types);
+  return typeVectorToSorts(d_solver, types);
 }
 
 size_t Sort::getDatatypeArity() const
@@ -1083,7 +1088,7 @@ std::vector<Sort> Sort::getTupleSorts() const
 {
   CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
   std::vector<CVC4::Type> types = DatatypeType(*d_type).getTupleTypes();
-  return typeVectorToSorts(types);
+  return typeVectorToSorts(d_solver, types);
 }
 
 /* --------------------------------------------------------------------- */
@@ -1105,9 +1110,13 @@ size_t SortHashFunction::operator()(const Sort& s) const
 
 Op::Op() : d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {}
 
-Op::Op(const Kind k) : d_kind(k), d_expr(new CVC4::Expr()) {}
+Op::Op(const Solver* slv, const Kind k)
+    : d_solver(slv), d_kind(k), d_expr(new CVC4::Expr())
+{
+}
 
-Op::Op(const Kind k, const CVC4::Expr& e) : d_kind(k), d_expr(new CVC4::Expr(e))
+Op::Op(const Solver* slv, const Kind k, const CVC4::Expr& e)
+    : d_solver(slv), d_kind(k), d_expr(new CVC4::Expr(e))
 {
 }
 
@@ -1323,19 +1332,20 @@ size_t OpHashFunction::operator()(const Op& t) const
 /* Term                                                                       */
 /* -------------------------------------------------------------------------- */
 
-Term::Term() : d_expr(new CVC4::Expr()) {}
+Term::Term() : d_solver(nullptr), d_expr(new CVC4::Expr()) {}
 
-Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
+Term::Term(const Solver* slv, const CVC4::Expr& e)
+    : d_solver(slv), d_expr(new CVC4::Expr(e))
+{
+}
 
 Term::~Term() {}
 
-/* Helpers                                                                    */
-/* -------------------------------------------------------------------------- */
-
-/* Split out to avoid nested API calls (problematic with API tracing).        */
-/* .......................................................................... */
-
-bool Term::isNullHelper() const { return d_expr->isNull(); }
+bool Term::isNullHelper() const
+{
+  /* Split out to avoid nested API calls (problematic with API tracing). */
+  return d_expr->isNull();
+}
 
 bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
 
@@ -1371,12 +1381,12 @@ Term Term::operator[](size_t index) const
     if (index == 0)
     {
       // return the operator
-      return api::Term(d_expr->getOperator());
+      return Term(d_solver, d_expr->getOperator());
     }
     // otherwise we are looking up child at (index-1)
     index--;
   }
-  return api::Term((*d_expr)[index]);
+  return Term(d_solver, (*d_expr)[index]);
 }
 
 uint64_t Term::getId() const
@@ -1394,7 +1404,7 @@ Kind Term::getKind() const
 Sort Term::getSort() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  return Sort(d_expr->getType());
+  return Sort(d_solver, d_expr->getType());
 }
 
 Term Term::substitute(Term e, Term replacement) const
@@ -1406,7 +1416,7 @@ Term Term::substitute(Term e, Term replacement) const
       << "Expected non-null term as replacement in substitute";
   CVC4_API_CHECK(e.getSort().isComparableTo(replacement.getSort()))
       << "Expecting terms of comparable sort in substitute";
-  return api::Term(d_expr->substitute(e.getExpr(), replacement.getExpr()));
+  return Term(d_solver, d_expr->substitute(e.getExpr(), replacement.getExpr()));
 }
 
 Term Term::substitute(const std::vector<Term> es,
@@ -1424,8 +1434,9 @@ Term Term::substitute(const std::vector<Term> es,
     CVC4_API_CHECK(es[i].getSort().isComparableTo(replacements[i].getSort()))
         << "Expecting terms of comparable sort in substitute";
   }
-  return api::Term(d_expr->substitute(termVectorToExprs(es),
-                                      termVectorToExprs(replacements)));
+  return Term(d_solver,
+              d_expr->substitute(termVectorToExprs(es),
+                                 termVectorToExprs(replacements)));
 }
 
 bool Term::hasOp() const
@@ -1447,18 +1458,18 @@ Op Term::getOp() const
   // is one of the APPLY_* kinds
   if (isApplyKind(d_expr->getKind()))
   {
-    return Op(intToExtKind(d_expr->getKind()));
+    return Op(d_solver, intToExtKind(d_expr->getKind()));
   }
   else if (d_expr->isParameterized())
   {
     // it's an indexed operator
     // so we should return the indexed op
     CVC4::Expr op = d_expr->getOperator();
-    return Op(intToExtKind(d_expr->getKind()), op);
+    return Op(d_solver, intToExtKind(d_expr->getKind()), op);
   }
   else
   {
-    return Op(intToExtKind(d_expr->getKind()));
+    return Op(d_solver, intToExtKind(d_expr->getKind()));
   }
 }
 
@@ -1475,9 +1486,9 @@ Term Term::notTerm() const
   CVC4_API_CHECK_NOT_NULL;
   try
   {
-    Term res = d_expr->notExpr();
-    (void)res.d_expr->getType(true); /* kick off type checking */
-    return res;
+    Expr res = d_expr->notExpr();
+    (void)res.getType(true); /* kick off type checking */
+    return Term(d_solver, res);
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1491,9 +1502,9 @@ Term Term::andTerm(const Term& t) const
   CVC4_API_ARG_CHECK_NOT_NULL(t);
   try
   {
-    Term res = d_expr->andExpr(*t.d_expr);
-    (void)res.d_expr->getType(true); /* kick off type checking */
-    return res;
+    Expr res = d_expr->andExpr(*t.d_expr);
+    (void)res.getType(true); /* kick off type checking */
+    return Term(d_solver, res);
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1507,9 +1518,9 @@ Term Term::orTerm(const Term& t) const
   CVC4_API_ARG_CHECK_NOT_NULL(t);
   try
   {
-    Term res = d_expr->orExpr(*t.d_expr);
-    (void)res.d_expr->getType(true); /* kick off type checking */
-    return res;
+    Expr res = d_expr->orExpr(*t.d_expr);
+    (void)res.getType(true); /* kick off type checking */
+    return Term(d_solver, res);
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1523,9 +1534,9 @@ Term Term::xorTerm(const Term& t) const
   CVC4_API_ARG_CHECK_NOT_NULL(t);
   try
   {
-    Term res = d_expr->xorExpr(*t.d_expr);
-    (void)res.d_expr->getType(true); /* kick off type checking */
-    return res;
+    Expr res = d_expr->xorExpr(*t.d_expr);
+    (void)res.getType(true); /* kick off type checking */
+    return Term(d_solver, res);
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1539,9 +1550,9 @@ Term Term::eqTerm(const Term& t) const
   CVC4_API_ARG_CHECK_NOT_NULL(t);
   try
   {
-    Term res = d_expr->eqExpr(*t.d_expr);
-    (void)res.d_expr->getType(true); /* kick off type checking */
-    return res;
+    Expr res = d_expr->eqExpr(*t.d_expr);
+    (void)res.getType(true); /* kick off type checking */
+    return Term(d_solver, res);
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1555,9 +1566,9 @@ Term Term::impTerm(const Term& t) const
   CVC4_API_ARG_CHECK_NOT_NULL(t);
   try
   {
-    Term res = d_expr->impExpr(*t.d_expr);
-    (void)res.d_expr->getType(true); /* kick off type checking */
-    return res;
+    Expr res = d_expr->impExpr(*t.d_expr);
+    (void)res.getType(true); /* kick off type checking */
+    return Term(d_solver, res);
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1572,9 +1583,9 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const
   CVC4_API_ARG_CHECK_NOT_NULL(else_t);
   try
   {
-    Term res = d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
-    (void)res.d_expr->getType(true); /* kick off type checking */
-    return res;
+    Expr res = d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
+    (void)res.getType(true); /* kick off type checking */
+    return Term(d_solver, res);
   }
   catch (const CVC4::TypeCheckingException& e)
   {
@@ -1584,11 +1595,15 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const
 
 std::string Term::toString() const { return d_expr->toString(); }
 
-Term::const_iterator::const_iterator() : d_orig_expr(nullptr), d_pos(0) {}
+Term::const_iterator::const_iterator()
+    : d_solver(nullptr), d_orig_expr(nullptr), d_pos(0)
+{
+}
 
-Term::const_iterator::const_iterator(const std::shared_ptr<CVC4::Expr>& e,
+Term::const_iterator::const_iterator(const Solver* slv,
+                                     const std::shared_ptr<CVC4::Expr>& e,
                                      uint32_t p)
-    : d_orig_expr(e), d_pos(p)
+    : d_solver(slv), d_orig_expr(e), d_pos(p)
 {
 }
 
@@ -1647,7 +1662,7 @@ Term Term::const_iterator::operator*() const
 
   if (!d_pos && extra_child)
   {
-    return Term(d_orig_expr->getOperator());
+    return Term(d_solver, d_orig_expr->getOperator());
   }
   else
   {
@@ -1658,13 +1673,13 @@ Term Term::const_iterator::operator*() const
       --idx;
     }
     Assert(idx >= 0);
-    return Term((*d_orig_expr)[idx]);
+    return Term(d_solver, (*d_orig_expr)[idx]);
   }
 }
 
 Term::const_iterator Term::begin() const
 {
-  return Term::const_iterator(d_expr, 0);
+  return Term::const_iterator(d_solver, d_expr, 0);
 }
 
 Term::const_iterator Term::end() const
@@ -1681,7 +1696,7 @@ Term::const_iterator Term::end() const
     // one more child if this is a UF application (count the UF as a child)
     ++endpos;
   }
-  return Term::const_iterator(d_expr, endpos);
+  return Term::const_iterator(d_solver, d_expr, endpos);
 }
 
 // !!! This is only temporarily available until the parser is fully migrated
@@ -1789,25 +1804,25 @@ std::ostream& operator<<(std::ostream& out,
 
 /* DatatypeDecl ------------------------------------------------------------- */
 
-DatatypeDecl::DatatypeDecl(const Solver* s,
+DatatypeDecl::DatatypeDecl(const Solver* slv,
                            const std::string& name,
                            bool isCoDatatype)
-    : d_dtype(new CVC4::Datatype(s->getExprManager(), name, isCoDatatype))
+    : d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype))
 {
 }
 
-DatatypeDecl::DatatypeDecl(const Solver* s,
+DatatypeDecl::DatatypeDecl(const Solver* slv,
                            const std::string& name,
                            Sort param,
                            bool isCoDatatype)
-    : d_dtype(new CVC4::Datatype(s->getExprManager(),
+    : d_dtype(new CVC4::Datatype(slv->getExprManager(),
                                  name,
                                  std::vector<Type>{*param.d_type},
                                  isCoDatatype))
 {
 }
 
-DatatypeDecl::DatatypeDecl(const Solver* s,
+DatatypeDecl::DatatypeDecl(const Solver* slv,
                            const std::string& name,
                            const std::vector<Sort>& params,
                            bool isCoDatatype)
@@ -1818,7 +1833,7 @@ DatatypeDecl::DatatypeDecl(const Solver* s,
     tparams.push_back(*p.d_type);
   }
   d_dtype = std::shared_ptr<CVC4::Datatype>(
-      new CVC4::Datatype(s->getExprManager(), name, tparams, isCoDatatype));
+      new CVC4::Datatype(slv->getExprManager(), name, tparams, isCoDatatype));
 }
 
 bool DatatypeDecl::isNullHelper() const { return !d_dtype; }
@@ -1875,8 +1890,9 @@ std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl)
 
 DatatypeSelector::DatatypeSelector() { d_stor = nullptr; }
 
-DatatypeSelector::DatatypeSelector(const CVC4::DatatypeConstructorArg& stor)
-    : d_stor(new CVC4::DatatypeConstructorArg(stor))
+DatatypeSelector::DatatypeSelector(const Solver* slv,
+                                   const CVC4::DatatypeConstructorArg& stor)
+    : d_solver(slv), d_stor(new CVC4::DatatypeConstructorArg(stor))
 {
   CVC4_API_CHECK(d_stor->isResolved()) << "Expected resolved datatype selector";
 }
@@ -1887,13 +1903,13 @@ std::string DatatypeSelector::getName() const { return d_stor->getName(); }
 
 Term DatatypeSelector::getSelectorTerm() const
 {
-  Term sel = d_stor->getSelector();
+  Term sel = Term(d_solver, d_stor->getSelector());
   return sel;
 }
 
 Sort DatatypeSelector::getRangeSort() const
 {
-  return Sort(d_stor->getRangeType());
+  return Sort(d_solver, d_stor->getRangeType());
 }
 
 std::string DatatypeSelector::toString() const
@@ -1919,10 +1935,13 @@ std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor)
 
 /* DatatypeConstructor ------------------------------------------------------ */
 
-DatatypeConstructor::DatatypeConstructor() { d_ctor = nullptr; }
+DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
+{
+}
 
-DatatypeConstructor::DatatypeConstructor(const CVC4::DatatypeConstructor& ctor)
-    : d_ctor(new CVC4::DatatypeConstructor(ctor))
+DatatypeConstructor::DatatypeConstructor(const Solver* slv,
+                                         const CVC4::DatatypeConstructor& ctor)
+    : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(ctor))
 {
   CVC4_API_CHECK(d_ctor->isResolved())
       << "Expected resolved datatype constructor";
@@ -1934,13 +1953,13 @@ std::string DatatypeConstructor::getName() const { return d_ctor->getName(); }
 
 Term DatatypeConstructor::getConstructorTerm() const
 {
-  Term ctor = d_ctor->getConstructor();
+  Term ctor = Term(d_solver, d_ctor->getConstructor());
   return ctor;
 }
 
 Term DatatypeConstructor::getTesterTerm() const
 {
-  Term tst = d_ctor->getTester();
+  Term tst = Term(d_solver, d_ctor->getTester());
   return tst;
 }
 
@@ -1951,7 +1970,7 @@ size_t DatatypeConstructor::getNumSelectors() const
 
 DatatypeSelector DatatypeConstructor::operator[](size_t index) const
 {
-  return (*d_ctor)[index];
+  return DatatypeSelector(d_solver, (*d_ctor)[index]);
 }
 
 DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
@@ -1972,36 +1991,41 @@ Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
 
 DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
 {
-  return DatatypeConstructor::const_iterator(*d_ctor, true);
+  return DatatypeConstructor::const_iterator(d_solver, *d_ctor, true);
 }
 
 DatatypeConstructor::const_iterator DatatypeConstructor::end() const
 {
-  return DatatypeConstructor::const_iterator(*d_ctor, false);
+  return DatatypeConstructor::const_iterator(d_solver, *d_ctor, false);
 }
 
 DatatypeConstructor::const_iterator::const_iterator(
-    const CVC4::DatatypeConstructor& ctor, bool begin)
+    const Solver* slv, const CVC4::DatatypeConstructor& ctor, bool begin)
 {
+  d_solver = slv;
   d_int_stors = ctor.getArgs();
+
   const std::vector<CVC4::DatatypeConstructorArg>* sels =
       static_cast<const std::vector<CVC4::DatatypeConstructorArg>*>(
           d_int_stors);
   for (const auto& s : *sels)
   {
     /* Can not use emplace_back here since constructor is private. */
-    d_stors.push_back(DatatypeSelector(s));
+    d_stors.push_back(DatatypeSelector(d_solver, s));
   }
   d_idx = begin ? 0 : sels->size();
 }
 
-// Nullary constructor for Cython
-DatatypeConstructor::const_iterator::const_iterator() {}
+DatatypeConstructor::const_iterator::const_iterator()
+    : d_solver(nullptr), d_int_stors(nullptr), d_idx(0)
+{
+}
 
 DatatypeConstructor::const_iterator&
 DatatypeConstructor::const_iterator::operator=(
     const DatatypeConstructor::const_iterator& it)
 {
+  d_solver = it.d_solver;
   d_int_stors = it.d_int_stors;
   d_stors = it.d_stors;
   d_idx = it.d_idx;
@@ -2076,7 +2100,7 @@ DatatypeSelector DatatypeConstructor::getSelectorForName(
   }
   CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor "
                            << getName() << " exists";
-  return (*d_ctor)[index];
+  return DatatypeSelector(d_solver, (*d_ctor)[index]);
 }
 
 std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
@@ -2087,21 +2111,20 @@ std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
 
 /* Datatype ----------------------------------------------------------------- */
 
-Datatype::Datatype(const CVC4::Datatype& dtype)
-    : d_dtype(new CVC4::Datatype(dtype))
+Datatype::Datatype(const Solver* slv, const CVC4::Datatype& dtype)
+    : d_solver(slv), d_dtype(new CVC4::Datatype(dtype))
 {
   CVC4_API_CHECK(d_dtype->isResolved()) << "Expected resolved datatype";
 }
 
-// Nullary constructor for Cython
-Datatype::Datatype() {}
+Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {}
 
 Datatype::~Datatype() {}
 
 DatatypeConstructor Datatype::operator[](size_t idx) const
 {
   CVC4_API_CHECK(idx < getNumConstructors()) << "Index out of bounds.";
-  return (*d_dtype)[idx];
+  return DatatypeConstructor(d_solver, (*d_dtype)[idx]);
 }
 
 DatatypeConstructor Datatype::operator[](const std::string& name) const
@@ -2141,12 +2164,12 @@ std::string Datatype::toString() const { return d_dtype->getName(); }
 
 Datatype::const_iterator Datatype::begin() const
 {
-  return Datatype::const_iterator(*d_dtype, true);
+  return Datatype::const_iterator(d_solver, *d_dtype, true);
 }
 
 Datatype::const_iterator Datatype::end() const
 {
-  return Datatype::const_iterator(*d_dtype, false);
+  return Datatype::const_iterator(d_solver, *d_dtype, false);
 }
 
 // !!! This is only temporarily available until the parser is fully migrated
@@ -2169,28 +2192,33 @@ DatatypeConstructor Datatype::getConstructorForName(
   }
   CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype "
                             << getName() << " exists";
-  return (*d_dtype)[index];
+  return DatatypeConstructor(d_solver, (*d_dtype)[index]);
 }
 
-Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype,
+Datatype::const_iterator::const_iterator(const Solver* slv,
+                                         const CVC4::Datatype& dtype,
                                          bool begin)
+    : d_solver(slv), d_int_ctors(dtype.getConstructors())
 {
-  d_int_ctors = dtype.getConstructors();
   const std::vector<CVC4::DatatypeConstructor>* cons =
       static_cast<const std::vector<CVC4::DatatypeConstructor>*>(d_int_ctors);
   for (const auto& c : *cons)
   {
     /* Can not use emplace_back here since constructor is private. */
-    d_ctors.push_back(DatatypeConstructor(c));
+    d_ctors.push_back(DatatypeConstructor(d_solver, c));
   }
   d_idx = begin ? 0 : cons->size();
 }
 
-Datatype::const_iterator::const_iterator() {}
+Datatype::const_iterator::const_iterator()
+    : d_solver(nullptr), d_int_ctors(nullptr), d_idx(0)
+{
+}
 
 Datatype::const_iterator& Datatype::const_iterator::operator=(
     const Datatype::const_iterator& it)
 {
+  d_solver = it.d_solver;
   d_int_ctors = it.d_int_ctors;
   d_ctors = it.d_ctors;
   d_idx = it.d_idx;
@@ -2235,10 +2263,10 @@ bool Datatype::const_iterator::operator!=(
 /* -------------------------------------------------------------------------- */
 /* Grammar                                                                    */
 /* -------------------------------------------------------------------------- */
-Grammar::Grammar(const Solver* s,
+Grammar::Grammar(const Solver* slv,
                  const std::vector<Term>& sygusVars,
                  const std::vector<Term>& ntSymbols)
-    : d_s(s),
+    : d_solver(slv),
       d_sygusVars(sygusVars),
       d_ntSyms(ntSymbols),
       d_ntsToTerms(ntSymbols.size()),
@@ -2326,8 +2354,9 @@ Sort Grammar::resolve()
 
   if (!d_sygusVars.empty())
   {
-    bvl = d_s->getExprManager()->mkExpr(CVC4::kind::BOUND_VAR_LIST,
-                                        termVectorToExprs(d_sygusVars));
+    bvl = Term(d_solver,
+               d_solver->getExprManager()->mkExpr(
+                   CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(d_sygusVars)));
   }
 
   std::unordered_map<Term, Sort, TermHashFunction> ntsToUnres(d_ntSyms.size());
@@ -2336,7 +2365,8 @@ Sort Grammar::resolve()
   {
     // make the unresolved type, used for referencing the final version of
     // the ntsymbol's datatype
-    ntsToUnres[ntsymbol] = d_s->getExprManager()->mkSort(ntsymbol.toString());
+    ntsToUnres[ntsymbol] =
+        Sort(d_solver, d_solver->getExprManager()->mkSort(ntsymbol.toString()));
   }
 
   std::vector<CVC4::Datatype> datatypes;
@@ -2347,7 +2377,7 @@ Sort Grammar::resolve()
   for (const Term& ntSym : d_ntSyms)
   {
     // make the datatype, which encodes terms generated by this non-terminal
-    DatatypeDecl dtDecl(d_s, ntSym.toString());
+    DatatypeDecl dtDecl(d_solver, ntSym.toString());
 
     for (const Term& consTerm : d_ntsToTerms[ntSym])
     {
@@ -2356,7 +2386,8 @@ Sort Grammar::resolve()
 
     if (d_allowVars.find(ntSym) != d_allowVars.cend())
     {
-      addSygusConstructorVariables(dtDecl, ntSym.d_expr->getType());
+      addSygusConstructorVariables(dtDecl,
+                                   Sort(d_solver, ntSym.d_expr->getType()));
     }
 
     bool aci = d_allowConst.find(ntSym) != d_allowConst.end();
@@ -2375,11 +2406,11 @@ Sort Grammar::resolve()
   }
 
   std::vector<DatatypeType> datatypeTypes =
-      d_s->getExprManager()->mkMutualDatatypeTypes(
+      d_solver->getExprManager()->mkMutualDatatypeTypes(
           datatypes, unresTypes, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
 
   // return is the first datatype
-  return datatypeTypes[0];
+  return Sort(d_solver, datatypeTypes[0]);
 }
 
 void Grammar::addSygusConstructorTerm(
@@ -2406,11 +2437,13 @@ void Grammar::addSygusConstructorTerm(
       *op.d_expr, termVectorToExprs(args));
   if (!args.empty())
   {
-    Term lbvl = d_s->getExprManager()->mkExpr(CVC4::kind::BOUND_VAR_LIST,
-                                              termVectorToExprs(args));
+    Term lbvl = Term(d_solver,
+                     d_solver->getExprManager()->mkExpr(
+                         CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(args)));
     // its operator is a lambda
-    op = d_s->getExprManager()->mkExpr(CVC4::kind::LAMBDA,
-                                       {*lbvl.d_expr, *op.d_expr});
+    op = Term(d_solver,
+              d_solver->getExprManager()->mkExpr(CVC4::kind::LAMBDA,
+                                                 {*lbvl.d_expr, *op.d_expr}));
   }
   dt.d_dtype->addSygusConstructor(
       *op.d_expr, ssCName.str(), sortVectorToTypes(cargs), spc);
@@ -2426,7 +2459,9 @@ Term Grammar::purifySygusGTerm(
       ntsToUnres.find(term);
   if (itn != ntsToUnres.cend())
   {
-    Term ret = d_s->getExprManager()->mkBoundVar(term.d_expr->getType());
+    Term ret =
+        Term(d_solver,
+             d_solver->getExprManager()->mkBoundVar(term.d_expr->getType()));
     args.push_back(ret);
     cargs.push_back(itn->second);
     return ret;
@@ -2435,7 +2470,8 @@ Term Grammar::purifySygusGTerm(
   bool childChanged = false;
   for (unsigned i = 0, nchild = term.d_expr->getNumChildren(); i < nchild; i++)
   {
-    Term ptermc = purifySygusGTerm((*term.d_expr)[i], args, cargs, ntsToUnres);
+    Term ptermc = purifySygusGTerm(
+        Term(d_solver, (*term.d_expr)[i]), args, cargs, ntsToUnres);
     pchildren.push_back(ptermc);
     childChanged = childChanged || *ptermc.d_expr != (*term.d_expr)[i];
   }
@@ -2444,22 +2480,22 @@ Term Grammar::purifySygusGTerm(
     return term;
   }
 
-  Term nret;
+  Expr nret;
 
   if (term.d_expr->isParameterized())
   {
     // it's an indexed operator so we should provide the op
-    nret = d_s->getExprManager()->mkExpr(term.d_expr->getKind(),
-                                         term.d_expr->getOperator(),
-                                         termVectorToExprs(pchildren));
+    nret = d_solver->getExprManager()->mkExpr(term.d_expr->getKind(),
+                                              term.d_expr->getOperator(),
+                                              termVectorToExprs(pchildren));
   }
   else
   {
-    nret = d_s->getExprManager()->mkExpr(term.d_expr->getKind(),
-                                         termVectorToExprs(pchildren));
+    nret = d_solver->getExprManager()->mkExpr(term.d_expr->getKind(),
+                                              termVectorToExprs(pchildren));
   }
 
-  return nret;
+  return Term(d_solver, nret);
 }
 
 void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const
@@ -2538,9 +2574,9 @@ Solver::~Solver() {}
 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;
+  Expr res = d_exprMgr->mkConst(t);
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 }
 
 Term Solver::mkRealFromStrHelper(const std::string& s) const
@@ -2623,7 +2659,7 @@ Term Solver::mkTermFromKind(Kind kind) const
       kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
       << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
 
-  Term res;
+  Expr res;
   if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
   {
     CVC4::Kind k = extToIntKind(kind);
@@ -2635,8 +2671,8 @@ Term Solver::mkTermFromKind(Kind kind) const
     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;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -2656,7 +2692,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
   Assert(isDefinedIntKind(k))
       << "Not a defined internal kind : " << k << " " << kind;
 
-  Term res;
+  Expr res;
   if (echildren.size() > 2)
   {
     if (kind == INTS_DIVISION || kind == XOR || kind == MINUS
@@ -2701,8 +2737,8 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
     res = d_exprMgr->mkExpr(k, echildren);
   }
 
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2726,7 +2762,7 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
   std::vector<Sort> retTypes;
   for (CVC4::DatatypeType t : dtypes)
   {
-    retTypes.push_back(Sort(t));
+    retTypes.push_back(Sort(this, t));
   }
   return retTypes;
 
@@ -2786,49 +2822,49 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
 Sort Solver::getNullSort(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return Type();
+  return Sort(this, Type());
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Sort Solver::getBooleanSort(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return d_exprMgr->booleanType();
+  return Sort(this, d_exprMgr->booleanType());
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Sort Solver::getIntegerSort(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return d_exprMgr->integerType();
+  return Sort(this, d_exprMgr->integerType());
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Sort Solver::getRealSort(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return d_exprMgr->realType();
+  return Sort(this, d_exprMgr->realType());
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Sort Solver::getRegExpSort(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return d_exprMgr->regExpType();
+  return Sort(this, d_exprMgr->regExpType());
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Sort Solver::getStringSort(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return d_exprMgr->stringType();
+  return Sort(this, d_exprMgr->stringType());
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Sort Solver::getRoundingmodeSort(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return d_exprMgr->roundingModeType();
+  return Sort(this, d_exprMgr->roundingModeType());
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2842,7 +2878,8 @@ Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const
   CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
       << "non-null element sort";
 
-  return d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type);
+  return Sort(this,
+              d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -2852,7 +2889,7 @@ Sort Solver::mkBitVectorSort(uint32_t size) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0";
 
-  return d_exprMgr->mkBitVectorType(size);
+  return Sort(this, d_exprMgr->mkBitVectorType(size));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -2863,7 +2900,7 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
   CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0";
   CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0";
 
-  return d_exprMgr->mkFloatingPointType(exp, sig);
+  return Sort(this, d_exprMgr->mkFloatingPointType(exp, sig));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -2874,7 +2911,7 @@ Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const
   CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl)
       << "a datatype declaration with at least one constructor";
 
-  return d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype);
+  return Sort(this, d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -2903,7 +2940,8 @@ Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const
       << "first-class sort as codomain sort for function sort";
   Assert(!codomain.isFunction()); /* A function sort is not first-class. */
 
-  return d_exprMgr->mkFunctionType(*domain.d_type, *codomain.d_type);
+  return Sort(this,
+              d_exprMgr->mkFunctionType(*domain.d_type, *codomain.d_type));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -2929,7 +2967,7 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const
   Assert(!codomain.isFunction()); /* A function sort is not first-class. */
 
   std::vector<Type> argTypes = sortVectorToTypes(sorts);
-  return d_exprMgr->mkFunctionType(argTypes, *codomain.d_type);
+  return Sort(this, d_exprMgr->mkFunctionType(argTypes, *codomain.d_type));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -2937,7 +2975,8 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const
 Sort Solver::mkParamSort(const std::string& symbol) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return d_exprMgr->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER);
+  return Sort(this,
+              d_exprMgr->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2957,7 +2996,7 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
   }
   std::vector<Type> types = sortVectorToTypes(sorts);
 
-  return d_exprMgr->mkPredicateType(types);
+  return Sort(this, d_exprMgr->mkPredicateType(types));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -2977,7 +3016,7 @@ Sort Solver::mkRecordSort(
     f.emplace_back(p.first, *p.second.d_type);
   }
 
-  return d_exprMgr->mkRecordType(Record(f));
+  return Sort(this, d_exprMgr->mkRecordType(Record(f)));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -2988,7 +3027,7 @@ 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);
+  return Sort(this, d_exprMgr->mkSetType(*elemSort.d_type));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -2996,7 +3035,7 @@ Sort Solver::mkSetSort(Sort elemSort) const
 Sort Solver::mkUninterpretedSort(const std::string& symbol) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return d_exprMgr->mkSort(symbol);
+  return Sort(this, d_exprMgr->mkSort(symbol));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -3006,7 +3045,7 @@ Sort Solver::mkSortConstructorSort(const std::string& symbol,
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0";
 
-  return d_exprMgr->mkSortConstructor(symbol, arity);
+  return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3025,7 +3064,7 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
   }
   std::vector<Type> types = sortVectorToTypes(sorts);
 
-  return d_exprMgr->mkTupleType(types);
+  return Sort(this, d_exprMgr->mkTupleType(types));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3036,21 +3075,21 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
 Term Solver::mkTrue(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return d_exprMgr->mkConst<bool>(true);
+  return Term(this, d_exprMgr->mkConst<bool>(true));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::mkFalse(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return d_exprMgr->mkConst<bool>(false);
+  return Term(this, d_exprMgr->mkConst<bool>(false));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::mkBoolean(bool val) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return d_exprMgr->mkConst<bool>(val);
+  return Term(this, d_exprMgr->mkConst<bool>(val));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -3058,10 +3097,10 @@ Term Solver::mkPi() const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
 
-  Term res =
+  Expr res =
       d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3143,10 +3182,10 @@ Term Solver::mkRegexpEmpty() const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
 
-  Term res =
+  Expr res =
       d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Expr>());
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3155,10 +3194,10 @@ Term Solver::mkRegexpSigma() const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
 
-  Term res =
+  Expr res =
       d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Expr>());
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3179,9 +3218,9 @@ Term Solver::mkSepNil(Sort sort) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   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;
+  Expr res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3234,11 +3273,11 @@ Term Solver::mkUniverseSet(Sort sort) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
 
-  Term res =
+  Expr res =
       d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
   // TODO(#2771): Reenable?
-  // (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  // (void)res->getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3381,7 +3420,7 @@ Term Solver::mkAbstractValue(const std::string& index) const
   CVC4::Integer idx(index, 10);
   CVC4_API_ARG_CHECK_EXPECTED(idx > 0, index)
       << "a string representing an integer > 0";
-  return d_exprMgr->mkConst(CVC4::AbstractValue(idx));
+  return Term(this, d_exprMgr->mkConst(CVC4::AbstractValue(idx)));
   // do not call getType(), for abstract values, type can not be computed
   // until it is substituted away
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -3392,7 +3431,7 @@ Term Solver::mkAbstractValue(uint64_t index) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0";
 
-  return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index)));
+  return Term(this, d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index))));
   // do not call getType(), for abstract values, type can not be computed
   // until it is substituted away
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -3427,10 +3466,10 @@ 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";
 
-  Term res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type)
+  Expr res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type)
                             : d_exprMgr->mkVar(symbol, *sort.d_type);
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3443,10 +3482,10 @@ 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";
 
-  Term res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type)
+  Expr res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type)
                             : d_exprMgr->mkBoundVar(symbol, *sort.d_type);
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3489,9 +3528,9 @@ Term Solver::mkTerm(Kind kind, Term child) const
   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;
+  Expr res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3503,10 +3542,10 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
   CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
   checkMkTerm(kind, 2);
 
-  Term res =
+  Expr res =
       d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr);
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3530,7 +3569,7 @@ Term Solver::mkTerm(Op op) const
   if (op.isIndexedHelper())
   {
     const CVC4::Kind int_kind = extToIntKind(op.d_kind);
-    res = d_exprMgr->mkExpr(int_kind, *op.d_expr);
+    res = Term(this, d_exprMgr->mkExpr(int_kind, *op.d_expr));
   }
   else
   {
@@ -3549,7 +3588,7 @@ Term Solver::mkTerm(Op op, Term child) const
   CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
-  Term res;
+  Expr res;
   if (op.isIndexedHelper())
   {
     res = d_exprMgr->mkExpr(int_kind, *op.d_expr, *child.d_expr);
@@ -3559,8 +3598,8 @@ Term Solver::mkTerm(Op op, Term child) const
     res = d_exprMgr->mkExpr(int_kind, *child.d_expr);
   }
 
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3572,7 +3611,7 @@ Term Solver::mkTerm(Op op, Term child1, Term child2) const
   CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
-  Term res;
+  Expr res;
   if (op.isIndexedHelper())
   {
     res =
@@ -3583,8 +3622,8 @@ Term Solver::mkTerm(Op op, Term child1, Term child2) const
     res = d_exprMgr->mkExpr(int_kind, *child1.d_expr, *child2.d_expr);
   }
 
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -3596,7 +3635,7 @@ Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
   CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
-  Term res;
+  Expr res;
   if (op.isIndexedHelper())
   {
     res = d_exprMgr->mkExpr(
@@ -3608,8 +3647,8 @@ Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
         int_kind, *child1.d_expr, *child2.d_expr, *child3.d_expr);
   }
 
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3626,7 +3665,7 @@ Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
   std::vector<Expr> echildren = termVectorToExprs(children);
-  Term res;
+  Expr res;
   if (op.isIndexedHelper())
   {
     res = d_exprMgr->mkExpr(int_kind, *op.d_expr, echildren);
@@ -3636,8 +3675,8 @@ Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
     res = d_exprMgr->mkExpr(int_kind, echildren);
   }
 
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3656,11 +3695,11 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
 
   Sort s = mkTupleSort(sorts);
   Datatype dt = s.getDatatype();
-  Term res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR),
+  Expr res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR),
                                *dt[0].getConstructorTerm().d_expr,
                                args);
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3673,7 +3712,7 @@ Op Solver::mkOp(Kind kind) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_CHECK(s_indexed_kinds.find(kind) == s_indexed_kinds.end())
       << "Expected a kind for a non-indexed operator.";
-  return Op(kind);
+  return Op(this, kind);
   CVC4_API_SOLVER_TRY_CATCH_END
 }
 
@@ -3687,6 +3726,7 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const
   if (kind == RECORD_UPDATE)
   {
     res = Op(
+        this,
         kind,
         *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get());
   }
@@ -3697,7 +3737,8 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const
      * as invalid. */
     CVC4_API_ARG_CHECK_EXPECTED(arg != ".", arg)
         << "a string representing an integer, real or rational value.";
-    res = Op(kind,
+    res = Op(this,
+             kind,
              *mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg)))
                   .d_expr.get());
   }
@@ -3716,62 +3757,73 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const
   {
     case DIVISIBLE:
       res =
-          Op(kind,
+          Op(this,
+             kind,
              *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get());
       break;
     case BITVECTOR_REPEAT:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
                     .d_expr.get());
       break;
     case BITVECTOR_ZERO_EXTEND:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::BitVectorZeroExtend>(
                     CVC4::BitVectorZeroExtend(arg))
                     .d_expr.get());
       break;
     case BITVECTOR_SIGN_EXTEND:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::BitVectorSignExtend>(
                     CVC4::BitVectorSignExtend(arg))
                     .d_expr.get());
       break;
     case BITVECTOR_ROTATE_LEFT:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::BitVectorRotateLeft>(
                     CVC4::BitVectorRotateLeft(arg))
                     .d_expr.get());
       break;
     case BITVECTOR_ROTATE_RIGHT:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::BitVectorRotateRight>(
                     CVC4::BitVectorRotateRight(arg))
                     .d_expr.get());
       break;
     case INT_TO_BITVECTOR:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
                     .d_expr.get());
       break;
     case FLOATINGPOINT_TO_UBV:
       res = Op(
+          this,
           kind,
           *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg))
                .d_expr.get());
       break;
     case FLOATINGPOINT_TO_SBV:
       res = Op(
+          this,
           kind,
           *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg))
                .d_expr.get());
       break;
     case TUPLE_UPDATE:
       res = Op(
+          this,
           kind,
           *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get());
       break;
     case REGEXP_REPEAT:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg))
                     .d_expr.get());
       break;
@@ -3794,49 +3846,57 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
   switch (kind)
   {
     case BITVECTOR_EXTRACT:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::BitVectorExtract>(
                     CVC4::BitVectorExtract(arg1, arg2))
                     .d_expr.get());
       break;
     case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
                     CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
                     .d_expr.get());
       break;
     case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
                     CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
                     .d_expr.get());
       break;
     case FLOATINGPOINT_TO_FP_REAL:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::FloatingPointToFPReal>(
                     CVC4::FloatingPointToFPReal(arg1, arg2))
                     .d_expr.get());
       break;
     case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
                     CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
                     .d_expr.get());
       break;
     case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
                     CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
                     .d_expr.get());
       break;
     case FLOATINGPOINT_TO_FP_GENERIC:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::FloatingPointToFPGeneric>(
                     CVC4::FloatingPointToFPGeneric(arg1, arg2))
                     .d_expr.get());
       break;
     case REGEXP_LOOP:
-      res = Op(kind,
+      res = Op(this,
+               kind,
                *mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2))
                     .d_expr.get());
       break;
@@ -3858,7 +3918,7 @@ Term Solver::simplify(const Term& t)
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(t);
 
-  return d_smtEngine->simplify(*t.d_expr);
+  return Term(this, d_smtEngine->simplify(*t.d_expr));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3961,7 +4021,7 @@ Sort Solver::declareDatatype(
   {
     dtdecl.addConstructor(ctor);
   }
-  return d_exprMgr->mkDatatypeType(*dtdecl.d_dtype);
+  return Sort(this, d_exprMgr->mkDatatypeType(*dtdecl.d_dtype));
 }
 
 /**
@@ -3986,7 +4046,7 @@ Term Solver::declareFun(const std::string& symbol,
     std::vector<Type> types = sortVectorToTypes(sorts);
     type = d_exprMgr->mkFunctionType(types, type);
   }
-  return d_exprMgr->mkVar(symbol, type);
+  return Term(this, d_exprMgr->mkVar(symbol, type));
 }
 
 /**
@@ -3994,8 +4054,8 @@ Term Solver::declareFun(const std::string& symbol,
  */
 Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const
 {
-  if (arity == 0) return d_exprMgr->mkSort(symbol);
-  return d_exprMgr->mkSortConstructor(symbol, arity);
+  if (arity == 0) return Sort(this, d_exprMgr->mkSort(symbol));
+  return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity));
 }
 
 /**
@@ -4037,7 +4097,7 @@ Term Solver::defineFun(const std::string& symbol,
   Expr fun = d_exprMgr->mkVar(symbol, type);
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
   d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr);
-  return fun;
+  return Term(this, fun);
 }
 
 Term Solver::defineFun(Term fun,
@@ -4115,7 +4175,7 @@ Term Solver::defineFunRec(const std::string& symbol,
   Expr fun = d_exprMgr->mkVar(symbol, type);
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
   d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr);
-  return fun;
+  return Term(this, fun);
 }
 
 Term Solver::defineFunRec(Term fun,
@@ -4229,7 +4289,7 @@ std::vector<Term> Solver::getAssertions(void) const
   std::vector<Term> res;
   for (const Expr& e : assertions)
   {
-    res.push_back(Term(e));
+    res.push_back(Term(this, e));
   }
   return res;
 }
@@ -4245,7 +4305,7 @@ std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const
   std::vector<std::pair<Term, Term>> res;
   for (const auto& p : assignment)
   {
-    res.emplace_back(Term(p.first), Term(p.second));
+    res.emplace_back(Term(this, p.first), Term(this, p.second));
   }
   return res;
 }
@@ -4284,7 +4344,7 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
   std::vector<Term> res;
   for (const Expr& e : uassumptions)
   {
-    res.push_back(Term(e));
+    res.push_back(Term(this, e));
   }
   return res;
 }
@@ -4302,7 +4362,7 @@ std::vector<Term> Solver::getUnsatCore(void) const
   std::vector<Term> res;
   for (const Expr& e : core)
   {
-    res.push_back(Term(e));
+    res.push_back(Term(this, e));
   }
   return res;
 }
@@ -4315,7 +4375,7 @@ Term Solver::getValue(Term term) const
   // CHECK:
   // NodeManager::fromExprManager(d_exprMgr)
   // == NodeManager::fromExprManager(expr.getExprManager())
-  return d_smtEngine->getValue(*term.d_expr);
+  return Term(this, d_smtEngine->getValue(*term.d_expr));
 }
 
 /**
@@ -4331,7 +4391,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
   for (const Term& t : terms)
   {
     /* Can not use emplace_back here since constructor is private. */
-    res.push_back(Term(d_smtEngine->getValue(*t.d_expr)));
+    res.push_back(Term(this, d_smtEngine->getValue(*t.d_expr)));
   }
   return res;
 }
@@ -4471,7 +4531,8 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
     // constructors. We do this cast using division with 1. This has the
     // advantage wrt using TO_REAL since (constant) division is always included
     // in the theory.
-    res = Term(d_exprMgr->mkExpr(extToIntKind(DIVISION),
+    res = Term(this,
+               d_exprMgr->mkExpr(extToIntKind(DIVISION),
                                  *res.d_expr,
                                  d_exprMgr->mkConst(CVC4::Rational(1))));
   }
@@ -4489,7 +4550,7 @@ Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const
 
   d_smtEngine->declareSygusVar(symbol, res, *sort.d_type);
 
-  return res;
+  return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4535,14 +4596,16 @@ Term Solver::synthFun(const std::string& symbol,
 Term Solver::synthInv(const std::string& symbol,
                       const std::vector<Term>& boundVars) const
 {
-  return synthFunHelper(symbol, boundVars, d_exprMgr->booleanType(), true);
+  return synthFunHelper(
+      symbol, boundVars, Sort(this, d_exprMgr->booleanType()), true);
 }
 
 Term Solver::synthInv(const std::string& symbol,
                       const std::vector<Term>& boundVars,
                       Grammar& g) const
 {
-  return synthFunHelper(symbol, boundVars, d_exprMgr->booleanType(), true, &g);
+  return synthFunHelper(
+      symbol, boundVars, Sort(this, d_exprMgr->booleanType()), true, &g);
 }
 
 Term Solver::synthFunHelper(const std::string& symbol,
@@ -4586,7 +4649,7 @@ Term Solver::synthFunHelper(const std::string& symbol,
                                isInv,
                                termVectorToExprs(boundVars));
 
-  return fun;
+  return Term(this, fun);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4661,7 +4724,7 @@ Term Solver::getSynthSolution(Term term) const
 
   CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term";
 
-  return it->second;
+  return Term(this, it->second);
 }
 
 std::vector<Term> Solver::getSynthSolutions(
@@ -4692,7 +4755,7 @@ std::vector<Term> Solver::getSynthSolutions(
     CVC4_API_CHECK(it != map.cend())
         << "Synth solution not found for term at index " << i;
 
-    synthSolution.push_back(it->second);
+    synthSolution.push_back(Term(this, it->second));
   }
 
   return synthSolution;
@@ -4749,22 +4812,24 @@ std::set<Type> sortSetToTypes(const std::set<Sort>& sorts)
   return types;
 }
 
-std::vector<Term> exprVectorToTerms(const std::vector<Expr>& exprs)
+std::vector<Term> exprVectorToTerms(const Solver* slv,
+                                    const std::vector<Expr>& exprs)
 {
   std::vector<Term> terms;
   for (size_t i = 0, esize = exprs.size(); i < esize; i++)
   {
-    terms.push_back(Term(exprs[i]));
+    terms.push_back(Term(slv, exprs[i]));
   }
   return terms;
 }
 
-std::vector<Sort> typeVectorToSorts(const std::vector<Type>& types)
+std::vector<Sort> typeVectorToSorts(const Solver* slv,
+                                    const std::vector<Type>& types)
 {
   std::vector<Sort> sorts;
   for (size_t i = 0, tsize = types.size(); i < tsize; i++)
   {
-    sorts.push_back(Sort(types[i]));
+    sorts.push_back(Sort(slv, types[i]));
   }
   return sorts;
 }
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 279453747..87be7b74c 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -49,6 +49,8 @@ class Result;
 
 namespace api {
 
+class Solver;
+
 /* -------------------------------------------------------------------------- */
 /* Exception                                                                  */
 /* -------------------------------------------------------------------------- */
@@ -199,10 +201,11 @@ class CVC4_PUBLIC Sort
   // migrated to the new API. !!!
   /**
    * Constructor.
+   * @param slv the associated solver object
    * @param t the internal type that is to be wrapped by this sort
    * @return the Sort
    */
-  Sort(const CVC4::Type& t);
+  Sort(const Solver* slv, const CVC4::Type& t);
 
   /**
    * Constructor.
@@ -588,6 +591,11 @@ class CVC4_PUBLIC Sort
    */
   bool isNullHelper() const;
 
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
   /**
    * The interal type wrapped by this sort.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
@@ -637,19 +645,21 @@ class CVC4_PUBLIC Op
   // migrated to the new API. !!!
   /**
    * Constructor for a single kind (non-indexed operator).
+   * @param slv the associated solver object
    * @param k the kind of this Op
    */
-  Op(const Kind k);
+  Op(const Solver* slv, const Kind k);
 
   // !!! This constructor is only temporarily public until the parser is fully
   // migrated to the new API. !!!
   /**
    * Constructor.
+   * @param slv the associated solver object
    * @param k the kind of this Op
    * @param e the internal expression that is to be wrapped by this term
    * @return the Term
    */
-  Op(const Kind k, const CVC4::Expr& e);
+  Op(const Solver* slv, const Kind k, const CVC4::Expr& e);
 
   /**
    * Destructor.
@@ -726,6 +736,11 @@ class CVC4_PUBLIC Op
    */
   bool isIndexedHelper() const;
 
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
   /* The kind of this operator. */
   Kind d_kind;
 
@@ -758,10 +773,11 @@ class CVC4_PUBLIC Term
   // migrated to the new API. !!!
   /**
    * Constructor.
+   * @param slv the associated solver object
    * @param e the internal expression that is to be wrapped by this term
    * @return the Term
    */
-  Term(const CVC4::Expr& e);
+  Term(const Solver* slv, const CVC4::Expr& e);
 
   /**
    * Constructor.
@@ -955,10 +971,13 @@ class CVC4_PUBLIC Term
 
     /**
      * Constructor
+     * @param slv the associated solver object
      * @param e a shared pointer to the expression that we're iterating over
      * @param p the position of the iterator (e.g. which child it's on)
      */
-    const_iterator(const std::shared_ptr<CVC4::Expr>& e, uint32_t p);
+    const_iterator(const Solver* slv,
+                   const std::shared_ptr<CVC4::Expr>& e,
+                   uint32_t p);
 
     /**
      * Copy constructor.
@@ -1005,6 +1024,10 @@ class CVC4_PUBLIC Term
     Term operator*() const;
 
    private:
+    /**
+     * The associated solver object.
+     */
+    const Solver* d_solver;
     /* The original expression to be iterated over */
     std::shared_ptr<CVC4::Expr> d_orig_expr;
     /* Keeps track of the iteration position */
@@ -1025,6 +1048,12 @@ class CVC4_PUBLIC Term
   // to the new API. !!!
   CVC4::Expr getExpr(void) const;
 
+ protected:
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
  private:
   /**
    * Helper for isNull checks. This prevents calling an API function with
@@ -1228,24 +1257,24 @@ class CVC4_PUBLIC DatatypeDecl
  private:
   /**
    * Constructor.
-   * @param s the solver that created this datatype declaration
+   * @param slv the solver that created this datatype declaration
    * @param name the name of the datatype
    * @param isCoDatatype true if a codatatype is to be constructed
    * @return the DatatypeDecl
    */
-  DatatypeDecl(const Solver* s,
+  DatatypeDecl(const Solver* slv,
                const std::string& name,
                bool isCoDatatype = false);
 
   /**
    * Constructor for parameterized datatype declaration.
    * Create sorts parameter with Solver::mkParamSort().
-   * @param s the solver that created this datatype declaration
+   * @param slv the solver that created this datatype declaration
    * @param name the name of the datatype
    * @param param the sort parameter
    * @param isCoDatatype true if a codatatype is to be constructed
    */
-  DatatypeDecl(const Solver* s,
+  DatatypeDecl(const Solver* slv,
                const std::string& name,
                Sort param,
                bool isCoDatatype = false);
@@ -1253,12 +1282,12 @@ class CVC4_PUBLIC DatatypeDecl
   /**
    * Constructor for parameterized datatype declaration.
    * Create sorts parameter with Solver::mkParamSort().
-   * @param s the solver that created this datatype declaration
+   * @param slv the solver that created this datatype declaration
    * @param name the name of the datatype
    * @param params a list of sort parameters
    * @param isCoDatatype true if a codatatype is to be constructed
    */
-  DatatypeDecl(const Solver* s,
+  DatatypeDecl(const Solver* slv,
                const std::string& name,
                const std::vector<Sort>& params,
                bool isCoDatatype = false);
@@ -1292,10 +1321,11 @@ class CVC4_PUBLIC DatatypeSelector
   // migrated to the new API. !!!
   /**
    * Constructor.
+   * @param slv the associated solver object
    * @param stor the internal datatype selector to be wrapped
    * @return the DatatypeSelector
    */
-  DatatypeSelector(const CVC4::DatatypeConstructorArg& stor);
+  DatatypeSelector(const Solver* slv, const CVC4::DatatypeConstructorArg& stor);
 
   /**
    * Destructor.
@@ -1324,6 +1354,11 @@ class CVC4_PUBLIC DatatypeSelector
   CVC4::DatatypeConstructorArg getDatatypeConstructorArg(void) const;
 
  private:
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
   /**
    * The internal datatype selector wrapped by this datatype selector.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -1353,7 +1388,7 @@ class CVC4_PUBLIC DatatypeConstructor
    * @param ctor the internal datatype constructor to be wrapped
    * @return the DatatypeConstructor
    */
-  DatatypeConstructor(const CVC4::DatatypeConstructor& ctor);
+  DatatypeConstructor(const Solver* slv, const CVC4::DatatypeConstructor& ctor);
 
   /**
    * Destructor.
@@ -1466,16 +1501,27 @@ class CVC4_PUBLIC DatatypeConstructor
    private:
     /**
      * Constructor.
+     * @param slv the associated Solver object
      * @param ctor the internal datatype constructor to iterate over
      * @param true if this is a begin() iterator
      */
-    const_iterator(const CVC4::DatatypeConstructor& ctor, bool begin);
+    const_iterator(const Solver* slv,
+                   const CVC4::DatatypeConstructor& ctor,
+                   bool begin);
+
+    /**
+     * The associated solver object.
+     */
+    const Solver* d_solver;
+
     /* A pointer to the list of selectors of the internal datatype
      * constructor to iterate over.
      * This pointer is maintained for operators == and != only. */
     const void* d_int_stors;
+
     /* The list of datatype selector (wrappers) to iterate over. */
     std::vector<DatatypeSelector> d_stors;
+
     /* The current index of the iterator. */
     size_t d_idx;
   };
@@ -1501,6 +1547,12 @@ class CVC4_PUBLIC DatatypeConstructor
    * @return the selector object for the name
    */
   DatatypeSelector getSelectorForName(const std::string& name) const;
+
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
   /**
    * The internal datatype constructor wrapped by this datatype constructor.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -1525,7 +1577,7 @@ class CVC4_PUBLIC Datatype
    * @param dtype the internal datatype to be wrapped
    * @return the Datatype
    */
-  Datatype(const CVC4::Datatype& dtype);
+  Datatype(const Solver* slv, const CVC4::Datatype& dtype);
 
   // Nullary constructor for Cython
   Datatype();
@@ -1654,16 +1706,25 @@ class CVC4_PUBLIC Datatype
    private:
     /**
      * Constructor.
+     * @param slv the associated Solver object
      * @param dtype the internal datatype to iterate over
      * @param true if this is a begin() iterator
      */
-    const_iterator(const CVC4::Datatype& dtype, bool begin);
+    const_iterator(const Solver* slv, const CVC4::Datatype& dtype, bool begin);
+
+    /**
+     * The associated solver object.
+     */
+    const Solver* d_solver;
+
     /* A pointer to the list of constructors of the internal datatype
      * to iterate over.
      * This pointer is maintained for operators == and != only. */
     const void* d_int_ctors;
+
     /* The list of datatype constructor (wrappers) to iterate over. */
     std::vector<DatatypeConstructor> d_ctors;
+
     /* The current index of the iterator. */
     size_t d_idx;
   };
@@ -1689,6 +1750,12 @@ class CVC4_PUBLIC Datatype
    * @return the constructor object for the name
    */
   DatatypeConstructor getConstructorForName(const std::string& name) const;
+
+  /**
+   * The associated solver object.
+   */
+  const Solver* d_solver;
+
   /**
    * The internal datatype wrapped by this datatype.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -1793,11 +1860,11 @@ class CVC4_PUBLIC Grammar
  private:
   /**
    * Constructor.
-   * @param s the solver that created this grammar
+   * @param slv the solver that created this grammar
    * @param sygusVars the input variables to synth-fun/synth-var
    * @param ntSymbols the non-terminals of this grammar
    */
-  Grammar(const Solver* s,
+  Grammar(const Solver* slv,
           const std::vector<Term>& sygusVars,
           const std::vector<Term>& ntSymbols);
 
@@ -1863,7 +1930,7 @@ class CVC4_PUBLIC Grammar
   void addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const;
 
   /** The solver that created this grammar. */
-  const Solver* d_s;
+  const Solver* d_solver;
   /** Input variables to the corresponding function/invariant to synthesize.*/
   std::vector<Term> d_sygusVars;
   /** The non-terminal symbols of this grammar. */
@@ -3142,9 +3209,11 @@ class CVC4_PUBLIC Solver
 // new API. !!!
 std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms);
 std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts);
-std::vector<Term> exprVectorToTerms(const std::vector<Expr>& terms);
-std::vector<Sort> typeVectorToSorts(const std::vector<Type>& sorts);
 std::set<Type> sortSetToTypes(const std::set<Sort>& sorts);
+std::vector<Term> exprVectorToTerms(const Solver* slv,
+                                    const std::vector<Expr>& terms);
+std::vector<Sort> typeVectorToSorts(const Solver* slv,
+                                    const std::vector<Type>& sorts);
 
 }  // namespace api
 
-- 
cgit v1.2.3