From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 9 Mar 2021 00:59:35 +0000 (-0800)
Subject: New C++ API: Migrate to Node layer. (#6070)
X-Git-Tag: cvc5-1.0.0~2133
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=86ce1c18f8ea7a397a8b12405a196b126e82b648;p=cvc5.git

New C++ API: Migrate to Node layer. (#6070)

The following items will be added / adressed in subsequent PRs:

* migrate statistics tracking for variables and bound variables

* migrate adding of listeners when variables and bound variables
  are created

* consistent and clean NodeManagerScope handling
  (out of scope for this PR)

* clean up all interfaces to use const references when possible
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 974567380..bca1d147c 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -41,9 +41,6 @@
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/dtype_selector.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "expr/expr_manager_scope.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node.h"
@@ -687,7 +684,7 @@ uint32_t minArity(Kind k)
 {
   Assert(isDefinedKind(k));
   Assert(isDefinedIntKind(extToIntKind(k)));
-  uint32_t min = CVC4::ExprManager::minArity(extToIntKind(k));
+  uint32_t min = CVC4::kind::metakind::getLowerBoundForKind(extToIntKind(k));
 
   // At the API level, we treat functions/constructors/selectors/testers as
   // normal terms instead of making them part of the operator
@@ -702,7 +699,7 @@ uint32_t maxArity(Kind k)
 {
   Assert(isDefinedKind(k));
   Assert(isDefinedIntKind(extToIntKind(k)));
-  uint32_t max = CVC4::ExprManager::maxArity(extToIntKind(k));
+  uint32_t max = CVC4::kind::metakind::getUpperBoundForKind(extToIntKind(k));
 
   // At the API level, we treat functions/constructors/selectors/testers as
   // normal terms instead of making them part of the operator
@@ -1401,11 +1398,6 @@ Op::Op(const Solver* slv, const Kind k)
 {
 }
 
-Op::Op(const Solver* slv, const Kind k, const CVC4::Expr& e)
-    : d_solver(slv), d_kind(k), d_node(new CVC4::Node(Node::fromExpr(e)))
-{
-}
-
 Op::Op(const Solver* slv, const Kind k, const CVC4::Node& n)
     : d_solver(slv), d_kind(k), d_node(new CVC4::Node(n))
 {
@@ -1636,7 +1628,7 @@ size_t OpHashFunction::operator()(const Op& t) const
 {
   if (t.isIndexedHelper())
   {
-    return ExprHashFunction()(t.d_node->toExpr());
+    return NodeHashFunction()(*t.d_node);
   }
   else
   {
@@ -1650,13 +1642,6 @@ size_t OpHashFunction::operator()(const Op& t) const
 
 Term::Term() : d_solver(nullptr), d_node(new CVC4::Node()) {}
 
-Term::Term(const Solver* slv, const CVC4::Expr& e) : d_solver(slv)
-{
-  // Ensure that we create the node in the correct node manager.
-  NodeManagerScope scope(d_solver->getNodeManager());
-  d_node.reset(new CVC4::Node(e));
-}
-
 Term::Term(const Solver* slv, const CVC4::Node& n) : d_solver(slv)
 {
   // Ensure that we create the node in the correct node manager.
@@ -1768,12 +1753,12 @@ Term Term::operator[](size_t index) const
     if (index == 0)
     {
       // return the operator
-      return Term(d_solver, d_node->getOperator().toExpr());
+      return Term(d_solver, d_node->getOperator());
     }
     // otherwise we are looking up child at (index-1)
     index--;
   }
-  return Term(d_solver, (*d_node)[index].toExpr());
+  return Term(d_solver, (*d_node)[index]);
 }
 
 uint64_t Term::getId() const
@@ -1870,7 +1855,7 @@ bool Term::isNull() const { return isNullHelper(); }
 
 Term Term::getConstArrayBase() const
 {
-  CVC4::ExprManagerScope exmgrs(*(d_solver->getExprManager()));
+  NodeManagerScope scope(d_solver->getNodeManager());
   CVC4_API_CHECK_NOT_NULL;
   // CONST_ARRAY kind maps to STORE_ALL internal kind
   CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::STORE_ALL)
@@ -2122,18 +2107,6 @@ Term::const_iterator Term::end() const
   return Term::const_iterator(d_solver, d_node, endpos);
 }
 
-//// !!! This is only temporarily available until the parser is fully migrated
-//// to the new API. !!!
-CVC4::Expr Term::getExpr(void) const
-{
-  if (d_node->isNull())
-  {
-    return Expr();
-  }
-  NodeManagerScope scope(d_solver->getNodeManager());
-  return d_node->toExpr();
-}
-
 const CVC4::Node& Term::getNode(void) const { return *d_node; }
 
 namespace detail {
@@ -3045,9 +3018,10 @@ Sort Grammar::resolve()
 
   if (!d_sygusVars.empty())
   {
-    bvl = Term(d_solver,
-               d_solver->getExprManager()->mkExpr(
-                   CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(d_sygusVars)));
+    bvl = Term(
+        d_solver,
+        d_solver->getNodeManager()->mkNode(
+            CVC4::kind::BOUND_VAR_LIST, Term::termVectorToNodes(d_sygusVars)));
   }
 
   std::unordered_map<Term, Sort, TermHashFunction> ntsToUnres(d_ntSyms.size());
@@ -3124,14 +3098,14 @@ void Grammar::addSygusConstructorTerm(
   ssCName << op.getKind();
   if (!args.empty())
   {
-    Term lbvl = Term(d_solver,
-                     d_solver->getExprManager()->mkExpr(
-                         CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(args)));
+    Term lbvl =
+        Term(d_solver,
+             d_solver->getNodeManager()->mkNode(CVC4::kind::BOUND_VAR_LIST,
+                                                Term::termVectorToNodes(args)));
     // its operator is a lambda
-    op = Term(
-        d_solver,
-        d_solver->getExprManager()->mkExpr(
-            CVC4::kind::LAMBDA, {lbvl.d_node->toExpr(), op.d_node->toExpr()}));
+    op = Term(d_solver,
+              d_solver->getNodeManager()->mkNode(
+                  CVC4::kind::LAMBDA, *lbvl.d_node, *op.d_node));
   }
   std::vector<TypeNode> cargst = Sort::sortVectorToTypeNodes(cargs);
   dt.d_dtype->addSygusConstructor(*op.d_node, ssCName.str(), cargst);
@@ -3161,8 +3135,7 @@ Term Grammar::purifySygusGTerm(
     Term ptermc = purifySygusGTerm(
         Term(d_solver, (*term.d_node)[i]), args, cargs, ntsToUnres);
     pchildren.push_back(ptermc);
-    childChanged =
-        childChanged || ptermc.d_node->toExpr() != (term.d_node->toExpr())[i];
+    childChanged = childChanged || *ptermc.d_node != (*term.d_node)[i];
   }
   if (!childChanged)
   {
@@ -3250,8 +3223,8 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
 
 Solver::Solver(Options* opts)
 {
-  d_exprMgr.reset(new ExprManager);
-  d_smtEngine.reset(new SmtEngine(d_exprMgr->getNodeManager(), opts));
+  d_nodeMgr.reset(new NodeManager(nullptr));
+  d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), opts));
   d_smtEngine->setSolver(this);
   Options& o = d_smtEngine->getOptions();
   d_rng.reset(new Random(o[options::seed]));
@@ -3366,22 +3339,23 @@ Term Solver::getValueHelper(Term term) const
 
 Term Solver::mkTermFromKind(Kind kind) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_KIND_CHECK_EXPECTED(
       kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
       << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
 
-  Expr res;
+  Node res;
   if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
   {
     CVC4::Kind k = extToIntKind(kind);
     Assert(isDefinedIntKind(k));
-    res = d_exprMgr->mkExpr(k, std::vector<Expr>());
+    res = d_nodeMgr->mkNode(k, std::vector<Node>());
   }
   else
   {
     Assert(kind == PI);
-    res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+    res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), CVC4::kind::PI);
   }
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
@@ -3403,48 +3377,48 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
         << "a child term associated to this solver object";
   }
 
-  std::vector<Expr> echildren = termVectorToExprs(children);
+  std::vector<Node> echildren = Term::termVectorToNodes(children);
   CVC4::Kind k = extToIntKind(kind);
   Assert(isDefinedIntKind(k))
       << "Not a defined internal kind : " << k << " " << kind;
 
-  Expr res;
+  Node res;
   if (echildren.size() > 2)
   {
     if (kind == INTS_DIVISION || kind == XOR || kind == MINUS
         || kind == DIVISION || kind == HO_APPLY || kind == REGEXP_DIFF)
     {
       // left-associative, but CVC4 internally only supports 2 args
-      res = d_exprMgr->mkLeftAssociative(k, echildren);
+      res = d_nodeMgr->mkLeftAssociative(k, echildren);
     }
     else if (kind == IMPLIES)
     {
       // right-associative, but CVC4 internally only supports 2 args
-      res = d_exprMgr->mkRightAssociative(k, echildren);
+      res = d_nodeMgr->mkRightAssociative(k, echildren);
     }
     else if (kind == EQUAL || kind == LT || kind == GT || kind == LEQ
              || kind == GEQ)
     {
       // "chainable", but CVC4 internally only supports 2 args
-      res = d_exprMgr->mkChain(k, echildren);
+      res = d_nodeMgr->mkChain(k, echildren);
     }
     else if (kind::isAssociative(k))
     {
       // mkAssociative has special treatment for associative operators with lots
       // of children
-      res = d_exprMgr->mkAssociative(k, echildren);
+      res = d_nodeMgr->mkAssociative(k, echildren);
     }
     else
     {
       // default case, must check kind
       checkMkTerm(kind, children.size());
-      res = d_exprMgr->mkExpr(k, echildren);
+      res = d_nodeMgr->mkNode(k, echildren);
     }
   }
   else if (kind::isAssociative(k))
   {
     // associative case, same as above
-    res = d_exprMgr->mkAssociative(k, echildren);
+    res = d_nodeMgr->mkAssociative(k, echildren);
   }
   else
   {
@@ -3460,8 +3434,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
       // integers and reals (both are Rationals).
       // At the API, mkReal and mkInteger are different and therefore the
       // element type can be used safely here.
-      Node singleton = getNodeManager()->mkSingleton(type, *children[0].d_node);
-      res = Term(this, singleton).getExpr();
+      res = getNodeManager()->mkSingleton(type, *children[0].d_node);
     }
     else if (kind == api::MK_BAG)
     {
@@ -3473,13 +3446,12 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
       // integers and reals (both are Rationals).
       // At the API, mkReal and mkInteger are different and therefore the
       // element type can be used safely here.
-      Node bag = getNodeManager()->mkBag(
+      res = getNodeManager()->mkBag(
           type, *children[0].d_node, *children[1].d_node);
-      res = Term(this, bag).getExpr();
     }
     else
     {
-      res = d_exprMgr->mkExpr(k, echildren);
+      res = d_nodeMgr->mkNode(k, echildren);
     }
   }
 
@@ -3524,21 +3496,6 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-/* Helpers for converting vectors.                                            */
-/* .......................................................................... */
-
-std::vector<Expr> Solver::termVectorToExprs(
-    const std::vector<Term>& terms) const
-{
-  std::vector<Expr> res;
-  for (const Term& t : terms)
-  {
-    CVC4_API_SOLVER_CHECK_TERM(t);
-    res.push_back(t.d_node->toExpr());
-  }
-  return res;
-}
-
 /* Helpers for mkTerm checks.                                                 */
 /* .......................................................................... */
 
@@ -3903,21 +3860,21 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
 Term Solver::mkTrue(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return Term(this, d_exprMgr->mkConst<bool>(true));
+  return Term(this, d_nodeMgr->mkConst<bool>(true));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::mkFalse(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return Term(this, d_exprMgr->mkConst<bool>(false));
+  return Term(this, d_nodeMgr->mkConst<bool>(false));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::mkBoolean(bool val) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  return Term(this, d_exprMgr->mkConst<bool>(val));
+  return Term(this, d_nodeMgr->mkConst<bool>(val));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -3925,8 +3882,8 @@ Term Solver::mkPi() const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
 
-  Expr res =
-      d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+  Node res =
+      d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), CVC4::kind::PI);
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
 
@@ -4037,8 +3994,8 @@ Term Solver::mkRegexpEmpty() const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
 
-  Expr res =
-      d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Expr>());
+  Node res =
+      d_nodeMgr->mkNode(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Node>());
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
 
@@ -4049,8 +4006,8 @@ Term Solver::mkRegexpSigma() const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
 
-  Expr res =
-      d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Expr>());
+  Node res =
+      d_nodeMgr->mkNode(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Node>());
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
 
@@ -4133,7 +4090,7 @@ Term Solver::mkEmptySequence(Sort sort) const
   CVC4_API_SOLVER_CHECK_SORT(sort);
 
   std::vector<Node> seq;
-  Expr res = d_exprMgr->mkConst(Sequence(*sort.d_type, seq));
+  Node res = d_nodeMgr->mkConst(Sequence(*sort.d_type, seq));
   return Term(this, res);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -4180,7 +4137,7 @@ Term Solver::mkBitVector(uint32_t size,
 Term Solver::mkConstArray(Sort sort, Term val) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_ARG_CHECK_NOT_NULL(sort);
   CVC4_API_ARG_CHECK_NOT_NULL(val);
   CVC4_API_SOLVER_CHECK_SORT(sort);
@@ -4340,7 +4297,7 @@ Term Solver::mkConst(Sort sort, const std::string& symbol) const
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
   CVC4_API_SOLVER_CHECK_SORT(sort);
 
-  Expr res = d_exprMgr->mkVar(symbol, sort.d_type->toType());
+  Node res = d_nodeMgr->mkVar(symbol, *sort.d_type);
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
 
@@ -4354,7 +4311,7 @@ Term Solver::mkConst(Sort sort) const
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
   CVC4_API_SOLVER_CHECK_SORT(sort);
 
-  Expr res = d_exprMgr->mkVar(sort.d_type->toType());
+  Node res = d_nodeMgr->mkVar(*sort.d_type);
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
 
@@ -4366,13 +4323,13 @@ Term Solver::mkConst(Sort sort) const
 
 Term Solver::mkVar(Sort sort, const std::string& symbol) const
 {
+  NodeManagerScope scope(getNodeManager());
   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->toType())
-                 : d_exprMgr->mkBoundVar(symbol, sort.d_type->toType());
+  Node res = symbol.empty() ? d_nodeMgr->mkBoundVar(*sort.d_type)
+                            : d_nodeMgr->mkBoundVar(symbol, *sort.d_type);
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
 
@@ -4610,8 +4567,8 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const
     case BITVECTOR_REPEAT:
       res = Op(this,
                kind,
-               mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
-                   .d_node->toExpr());
+               *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
+                    .d_node);
       break;
     case BITVECTOR_ZERO_EXTEND:
       res = Op(this,
@@ -4794,11 +4751,11 @@ Op Solver::mkOp(Kind kind, const std::vector<uint32_t>& args) const
 Term Solver::simplify(const Term& term)
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_ARG_CHECK_NOT_NULL(term);
   CVC4_API_SOLVER_CHECK_TERM(term);
 
-  return Term(this, d_smtEngine->simplify(term.d_node->toExpr()));
+  return Term(this, d_smtEngine->simplify(*term.d_node));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4806,7 +4763,7 @@ Term Solver::simplify(const Term& term)
 Result Solver::checkEntailed(Term term) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_CHECK(!d_smtEngine->isQueryMade()
                  || d_smtEngine->getOptions()[options::incrementalSolving])
       << "Cannot make multiple queries unless incremental solving is enabled "
@@ -4823,7 +4780,7 @@ Result Solver::checkEntailed(Term term) const
 Result Solver::checkEntailed(const std::vector<Term>& terms) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_CHECK(!d_smtEngine->isQueryMade()
                  || d_smtEngine->getOptions()[options::incrementalSolving])
       << "Cannot make multiple queries unless incremental solving is enabled "
@@ -4862,7 +4819,7 @@ void Solver::assertFormula(Term term) const
 Result Solver::checkSat(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_CHECK(!d_smtEngine->isQueryMade()
                  || d_smtEngine->getOptions()[options::incrementalSolving])
       << "Cannot make multiple queries unless incremental solving is enabled "
@@ -4878,7 +4835,7 @@ Result Solver::checkSat(void) const
 Result Solver::checkSatAssuming(Term assumption) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_CHECK(!d_smtEngine->isQueryMade()
                  || d_smtEngine->getOptions()[options::incrementalSolving])
       << "Cannot make multiple queries unless incremental solving is enabled "
@@ -4895,7 +4852,7 @@ Result Solver::checkSatAssuming(Term assumption) const
 Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0
                  || d_smtEngine->getOptions()[options::incrementalSolving])
       << "Cannot make multiple queries unless incremental solving is enabled "
@@ -4962,7 +4919,7 @@ Term Solver::declareFun(const std::string& symbol,
     std::vector<TypeNode> types = Sort::sortVectorToTypeNodes(sorts);
     type = getNodeManager()->mkFunctionType(types, type);
   }
-  return Term(this, d_exprMgr->mkVar(symbol, type.toType()));
+  return Term(this, d_nodeMgr->mkVar(symbol, type));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -5020,7 +4977,7 @@ Term Solver::defineFun(const std::string& symbol,
   {
     type = nm->mkFunctionType(domain_types, type);
   }
-  Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType()));
+  Node fun = d_nodeMgr->mkVar(symbol, type);
   std::vector<Node> ebound_vars = Term::termVectorToNodes(bound_vars);
   d_smtEngine->defineFunction(fun, ebound_vars, *term.d_node, global);
   return Term(this, fun);
@@ -5128,10 +5085,9 @@ Term Solver::defineFunRec(const std::string& symbol,
   {
     type = nm->mkFunctionType(domain_types, type);
   }
-  Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType()));
+  Node fun = d_nodeMgr->mkVar(symbol, type);
   std::vector<Node> ebound_vars = Term::termVectorToNodes(bound_vars);
-  d_smtEngine->defineFunctionRec(
-      fun, ebound_vars, term.d_node->toExpr(), global);
+  d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_node, global);
   return Term(this, fun);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -5333,7 +5289,7 @@ std::string Solver::getOption(const std::string& option) const
 std::vector<Term> Solver::getUnsatAssumptions(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
       << "Cannot get unsat assumptions unless incremental solving is enabled "
          "(try --incremental)";
@@ -5348,9 +5304,9 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
    *   return std::vector<Term>(uassumptions.begin(), uassumptions.end());
    * here since constructor is private */
   std::vector<Term> res;
-  for (const Node& e : uassumptions)
+  for (const Node& n : uassumptions)
   {
-    res.push_back(Term(this, e.toExpr()));
+    res.push_back(Term(this, n));
   }
   return res;
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -5362,7 +5318,7 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
 std::vector<Term> Solver::getUnsatCore(void) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatCores])
       << "Cannot get unsat core unless explicitly enabled "
          "(try --produce-unsat-cores)";
@@ -5398,7 +5354,7 @@ Term Solver::getValue(Term term) const
 std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_RECOVERABLE_CHECK(d_smtEngine->getOptions()[options::produceModels])
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
@@ -5422,7 +5378,7 @@ Term Solver::getQuantifierElimination(api::Term q) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(q);
   CVC4_API_SOLVER_CHECK_TERM(q);
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   return Term(this,
               d_smtEngine->getQuantifierElimination(q.getNode(), true, true));
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -5433,7 +5389,7 @@ Term Solver::getQuantifierEliminationDisjunct(api::Term q) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(q);
   CVC4_API_SOLVER_CHECK_TERM(q);
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   return Term(
       this, d_smtEngine->getQuantifierElimination(q.getNode(), false, true));
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -5457,7 +5413,7 @@ Term Solver::getSeparationHeap() const
       d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
       << "Cannot obtain separation logic expressions if not using the "
          "separation logic theory.";
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
       << "Cannot get separation heap term unless model generation is enabled "
          "(try --produce-models)";
@@ -5474,7 +5430,7 @@ Term Solver::getSeparationNilTerm() const
       d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
       << "Cannot obtain separation logic expressions if not using the "
          "separation logic theory.";
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
       << "Cannot get separation nil term unless model generation is enabled "
          "(try --produce-models)";
@@ -5490,7 +5446,7 @@ Term Solver::getSeparationNilTerm() const
 void Solver::pop(uint32_t nscopes) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
       << "Cannot pop when not solving incrementally (use --incremental)";
   CVC4_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels())
@@ -5507,7 +5463,7 @@ void Solver::pop(uint32_t nscopes) const
 bool Solver::getInterpolant(Term conj, Term& output) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   Node result;
   bool success = d_smtEngine->getInterpol(*conj.d_node, result);
   if (success)
@@ -5521,7 +5477,7 @@ bool Solver::getInterpolant(Term conj, Term& output) const
 bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   Node result;
   bool success =
       d_smtEngine->getInterpol(*conj.d_node, *g.resolve().d_type, result);
@@ -5536,7 +5492,7 @@ bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const
 bool Solver::getAbduct(Term conj, Term& output) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   Node result;
   bool success = d_smtEngine->getAbduct(*conj.d_node, result);
   if (success)
@@ -5550,7 +5506,7 @@ bool Solver::getAbduct(Term conj, Term& output) const
 bool Solver::getAbduct(Term conj, Grammar& g, Term& output) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   Node result;
   bool success =
       d_smtEngine->getAbduct(*conj.d_node, *g.resolve().d_type, result);
@@ -5565,7 +5521,7 @@ bool Solver::getAbduct(Term conj, Grammar& g, Term& output) const
 void Solver::blockModel() const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
@@ -5594,7 +5550,7 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
         this == terms[i].d_solver, "term", terms[i], i)
         << "a term associated to this solver object";
   }
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   d_smtEngine->blockModelValues(Term::termVectorToNodes(terms));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -5602,7 +5558,7 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
 void Solver::printInstantiations(std::ostream& out) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   d_smtEngine->printInstantiations(out);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -5613,7 +5569,7 @@ void Solver::printInstantiations(std::ostream& out) const
 void Solver::push(uint32_t nscopes) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
       << "Cannot push when not solving incrementally (use --incremental)";
 
@@ -5711,9 +5667,9 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
     // advantage wrt using TO_REAL since (constant) division is always included
     // in the theory.
     res = Term(this,
-               d_exprMgr->mkExpr(extToIntKind(DIVISION),
-                                 res.d_node->toExpr(),
-                                 d_exprMgr->mkConst(CVC4::Rational(1))));
+               d_nodeMgr->mkNode(extToIntKind(DIVISION),
+                                 *res.d_node,
+                                 d_nodeMgr->mkConst(CVC4::Rational(1))));
   }
   Assert(res.getSort() == sort);
   return res;
@@ -6001,16 +5957,7 @@ void Solver::printSynthSolution(std::ostream& out) const
  * !!! This is only temporarily available until the parser is fully migrated to
  * the new API. !!!
  */
-ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); }
-
-/**
- * !!! This is only temporarily available until the parser is fully migrated to
- * the new API. !!!
- */
-NodeManager* Solver::getNodeManager(void) const
-{
-  return d_exprMgr->getNodeManager();
-}
+NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr.get(); }
 
 /**
  * !!! This is only temporarily available until the parser is fully migrated to
@@ -6024,20 +5971,6 @@ SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
  */
 Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); }
 
-/* -------------------------------------------------------------------------- */
-/* Conversions                                                                */
-/* -------------------------------------------------------------------------- */
-
-std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms)
-{
-  std::vector<Expr> exprs;
-  for (size_t i = 0, tsize = terms.size(); i < tsize; i++)
-  {
-    exprs.push_back(terms[i].getExpr());
-  }
-  return exprs;
-}
-
 }  // namespace api
 
 /* -------------------------------------------------------------------------- */
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 962fa55ab..84e6cd496 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -44,7 +44,6 @@ class AssertCommand;
 class BlockModelValuesCommand;
 class CheckSatCommand;
 class CheckSatAssumingCommand;
-class Expr;
 class DatatypeDeclarationCommand;
 class DeclareFunctionCommand;
 class DeclareHeapCommand;
@@ -56,7 +55,6 @@ class DefineSortCommand;
 class DType;
 class DTypeConstructor;
 class DTypeSelector;
-class ExprManager;
 class GetAbductCommand;
 class GetInterpolCommand;
 class GetModelCommand;
@@ -211,8 +209,8 @@ class CVC4_PUBLIC Result
 
   /**
    * The interal result wrapped by this result.
-   * This is a shared_ptr rather than a unique_ptr since CVC4::Result is
-   * not ref counted.
+   * Note: This is a shared_ptr rather than a unique_ptr since CVC4::Result is
+   *       not ref counted.
    */
   std::shared_ptr<CVC4::Result> d_result;
 };
@@ -710,7 +708,7 @@ class CVC4_PUBLIC Sort
 
   /** Helper to convert a set of Sorts to internal TypeNodes. */
   std::set<TypeNode> static sortSetToTypeNodes(const std::set<Sort>& sorts);
-  /* Helper to convert a vector of Sorts to internal TypeNodes. */
+  /** Helper to convert a vector of Sorts to internal TypeNodes. */
   std::vector<TypeNode> static sortVectorToTypeNodes(
       const std::vector<Sort>& sorts);
   /** Helper to convert a vector of internal TypeNodes to Sorts. */
@@ -739,9 +737,9 @@ class CVC4_PUBLIC Sort
 
   /**
    * The interal type wrapped by this sort.
-   * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
-   * memory allocation (CVC4::Type is already ref counted, so this could be
-   * a unique_ptr instead).
+   * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
+   *       to memory allocation (CVC4::Type is already ref counted, so this
+   *       could be a unique_ptr instead).
    */
   std::shared_ptr<CVC4::TypeNode> d_type;
 };
@@ -847,15 +845,6 @@ class CVC4_PUBLIC Op
    */
   Op(const Solver* slv, const Kind k);
 
-  /**
-   * 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 Solver* slv, const Kind k, const CVC4::Expr& e);
-
   /**
    * Constructor.
    * @param slv the associated solver object
@@ -872,7 +861,7 @@ class CVC4_PUBLIC Op
   bool isNullHelper() const;
 
   /**
-   * Note: An indexed operator has a non-null internal expr, d_expr
+   * Note: An indexed operator has a non-null internal node, d_node
    * Note 2: We use a helper method to avoid having API functions call
    *         other API functions (we need to call this internally)
    * @return true iff this Op is indexed
@@ -884,14 +873,14 @@ class CVC4_PUBLIC Op
    */
   const Solver* d_solver;
 
-  /* The kind of this operator. */
+  /** The kind of this operator. */
   Kind d_kind;
 
   /**
-   * The internal expression wrapped by this operator.
-   * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
-   * memory allocation (CVC4::Expr is already ref counted, so this could be
-   * a unique_ptr instead).
+   * The internal node wrapped by this operator.
+   * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
+   *       to memory allocation (CVC4::Node is already ref counted, so this
+   *       could be a unique_ptr instead).
    */
   std::shared_ptr<CVC4::Node> d_node;
 };
@@ -1128,7 +1117,7 @@ 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 e a shared pointer to the node that we're iterating over
      * @param p the position of the iterator (e.g. which child it's on)
      */
     const_iterator(const Solver* slv,
@@ -1184,9 +1173,9 @@ class CVC4_PUBLIC Term
      * The associated solver object.
      */
     const Solver* d_solver;
-    /* The original node to be iterated over */
+    /** The original node to be iterated over. */
     std::shared_ptr<CVC4::Node> d_origNode;
-    /* Keeps track of the iteration position */
+    /** Keeps track of the iteration position. */
     uint32_t d_pos;
   };
 
@@ -1200,10 +1189,6 @@ class CVC4_PUBLIC Term
    */
   const_iterator end() const;
 
-  // !!! This is only temporarily available until the parser is fully migrated
-  // to the new API. !!!
-  CVC4::Expr getExpr(void) const;
-
   /**
    * @return true if the term is an integer that fits within std::int32_t.
    */
@@ -1270,17 +1255,9 @@ class CVC4_PUBLIC Term
   const Solver* d_solver;
 
  private:
-  /* Helper to convert a vector of Terms to internal Nodes. */
+  /** Helper to convert a vector of Terms to internal Nodes. */
   std::vector<Node> static termVectorToNodes(const std::vector<Term>& terms);
 
-  /**
-   * 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 Solver* slv, const CVC4::Expr& e);
-
   /**
    * Constructor.
    * @param slv the associated solver object
@@ -1311,10 +1288,10 @@ class CVC4_PUBLIC Term
    */
   bool isCastedReal() const;
   /**
-   * The internal expression wrapped by this term.
-   * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
-   * memory allocation (CVC4::Expr is already ref counted, so this could be
-   * a unique_ptr instead).
+   * The internal node wrapped by this term.
+   * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
+   *       to memory allocation (CVC4::Node is already ref counted, so this
+   *       could be a unique_ptr instead).
    */
   std::shared_ptr<CVC4::Node> d_node;
 };
@@ -1461,8 +1438,8 @@ class CVC4_PUBLIC DatatypeConstructorDecl
   /**
    * The internal (intermediate) datatype constructor wrapped by this
    * datatype constructor declaration.
-   * This is a shared_ptr rather than a unique_ptr since
-   * CVC4::DTypeConstructor is not ref counted.
+   * Note: This is a shared_ptr rather than a unique_ptr since
+   *       CVC4::DTypeConstructor is not ref counted.
    */
   std::shared_ptr<CVC4::DTypeConstructor> d_ctor;
 };
@@ -1564,10 +1541,11 @@ class CVC4_PUBLIC DatatypeDecl
    */
   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::DType is
-   * not ref counted.
+  /**
+   * The internal (intermediate) datatype wrapped by this datatype
+   * declaration.
+   * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
+   *       not ref counted.
    */
   std::shared_ptr<CVC4::DType> d_dtype;
 };
@@ -1624,8 +1602,8 @@ class CVC4_PUBLIC DatatypeSelector
 
   /**
    * The internal datatype selector wrapped by this datatype selector.
-   * This is a shared_ptr rather than a unique_ptr since CVC4::DType is
-   * not ref counted.
+   * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
+   *       not ref counted.
    */
   std::shared_ptr<CVC4::DTypeSelector> d_stor;
 };
@@ -1793,15 +1771,17 @@ class CVC4_PUBLIC DatatypeConstructor
      */
     const Solver* d_solver;
 
-    /* A pointer to the list of selectors of the internal datatype
+    /**
+     * A pointer to the list of selectors of the internal datatype
      * constructor to iterate over.
-     * This pointer is maintained for operators == and != only. */
+     * This pointer is maintained for operators == and != only.
+     */
     const void* d_int_stors;
 
-    /* The list of datatype selector (wrappers) to iterate over. */
+    /** The list of datatype selector (wrappers) to iterate over. */
     std::vector<DatatypeSelector> d_stors;
 
-    /* The current index of the iterator. */
+    /** The current index of the iterator. */
     size_t d_idx;
   };
 
@@ -1837,8 +1817,8 @@ class CVC4_PUBLIC DatatypeConstructor
 
   /**
    * The internal datatype constructor wrapped by this datatype constructor.
-   * This is a shared_ptr rather than a unique_ptr since CVC4::DType is
-   * not ref counted.
+   * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
+   *       not ref counted.
    */
   std::shared_ptr<CVC4::DTypeConstructor> d_ctor;
 };
@@ -2001,15 +1981,17 @@ class CVC4_PUBLIC Datatype
      */
     const Solver* d_solver;
 
-    /* A pointer to the list of constructors of the internal datatype
+    /**
+     * A pointer to the list of constructors of the internal datatype
      * to iterate over.
-     * This pointer is maintained for operators == and != only. */
+     * This pointer is maintained for operators == and != only.
+     */
     const void* d_int_ctors;
 
-    /* The list of datatype constructor (wrappers) to iterate over. */
+    /** The list of datatype constructor (wrappers) to iterate over. */
     std::vector<DatatypeConstructor> d_ctors;
 
-    /* The current index of the iterator. */
+    /** The current index of the iterator. */
     size_t d_idx;
   };
 
@@ -2045,8 +2027,8 @@ class CVC4_PUBLIC Datatype
 
   /**
    * The internal datatype wrapped by this datatype.
-   * This is a shared_ptr rather than a unique_ptr since CVC4::DType is
-   * not ref counted.
+   * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
+   *       not ref counted.
    */
   std::shared_ptr<CVC4::DType> d_dtype;
 };
@@ -2286,6 +2268,16 @@ struct CVC4_PUBLIC RoundingModeHashFunction
  */
 class CVC4_PUBLIC Solver
 {
+  friend class Datatype;
+  friend class DatatypeDecl;
+  friend class DatatypeConstructor;
+  friend class DatatypeConstructorDecl;
+  friend class DatatypeSelector;
+  friend class Grammar;
+  friend class Op;
+  friend class Sort;
+  friend class Term;
+
  public:
   /* .................................................................... */
   /* Constructors/Destructors                                             */
@@ -3545,13 +3537,6 @@ class CVC4_PUBLIC Solver
    */
   void printSynthSolution(std::ostream& out) const;
 
-  // !!! This is only temporarily available until the parser is fully migrated
-  // to the new API. !!!
-  ExprManager* getExprManager(void) const;
-
-  // !!! This is only temporarily available until the parser is fully migrated
-  // to the new API. !!!
-  NodeManager* getNodeManager(void) const;
 
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
@@ -3562,29 +3547,31 @@ class CVC4_PUBLIC Solver
   Options& getOptions(void);
 
  private:
-  /* Helper to convert a vector of Terms to internal Exprs. */
-  std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const;
-  /* Helper to check for API misuse in mkOp functions. */
+  /** @return the node manager of this solver */
+  NodeManager* getNodeManager(void) const;
+  /** Helper to check for API misuse in mkOp functions. */
   void checkMkTerm(Kind kind, uint32_t nchildren) const;
-  /* Helper for mk-functions that call d_exprMgr->mkConst(). */
+  /** Helper for mk-functions that call d_nodeMgr->mkConst(). */
   template <typename T>
   Term mkValHelper(T t) const;
-  /* Helper for mkReal functions that take a string as argument. */
+  /** Helper for mkReal functions that take a string as argument. */
   Term mkRealFromStrHelper(const std::string& s) const;
-  /* Helper for mkBitVector functions that take a string as argument. */
+  /** Helper for mkBitVector functions that take a string as argument. */
   Term mkBVFromStrHelper(const std::string& s, uint32_t base) const;
-  /* Helper for mkBitVector functions that take a string and a size as
-   * arguments. */
+  /**
+   * Helper for mkBitVector functions that take a string and a size as
+   * arguments.
+   */
   Term mkBVFromStrHelper(uint32_t size,
                          const std::string& s,
                          uint32_t base) const;
-  /* Helper for mkBitVector functions that take an integer as argument. */
+  /** Helper for mkBitVector functions that take an integer as argument. */
   Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
-  /* Helper for setLogic. */
+  /** Helper for setLogic. */
   void setLogicHelper(const std::string& logic) const;
-  /* Helper for mkTerm functions that create Term from a Kind */
+  /** Helper for mkTerm functions that create Term from a Kind */
   Term mkTermFromKind(Kind kind) const;
-  /* Helper for mkChar functions that take a string as argument. */
+  /** Helper for mkChar functions that take a string as argument. */
   Term mkCharFromStrHelper(const std::string& s) const;
   /** Get value helper, which accounts for subtyping */
   Term getValueHelper(Term term) const;
@@ -3644,18 +3631,14 @@ class CVC4_PUBLIC Solver
   /** check whether string s is a valid decimal integer */
   bool isValidInteger(const std::string& s) const;
 
-  /* The expression manager of this solver. */
-  std::unique_ptr<ExprManager> d_exprMgr;
-  /* The SMT engine of this solver. */
+  /** The node manager of this solver. */
+  std::unique_ptr<NodeManager> d_nodeMgr;
+  /** The SMT engine of this solver. */
   std::unique_ptr<SmtEngine> d_smtEngine;
-  /* The random number generator of this solver. */
+  /** The random number generator of this solver. */
   std::unique_ptr<Random> d_rng;
 };
 
-// !!! Only temporarily public until the parser is fully migrated to the
-// new API. !!!
-std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms);
-
 }  // namespace api
 
 // !!! Only temporarily public until the parser is fully migrated to the
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 43161fe04..5dd7a4dfd 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -695,7 +695,8 @@ Expr ExprManager::mkVar(Type type)
   return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
 }
 
-Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
+Expr ExprManager::mkBoundVar(const std::string& name, Type type)
+{
   NodeManagerScope nms(d_nodeManager);
   Node* n = d_nodeManager->mkBoundVarPtr(name, *type.d_typeNode);
   Debug("nm") << "set " << name << " on " << *n << std::endl;
@@ -703,7 +704,8 @@ Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
   return Expr(this, n);
 }
 
-Expr ExprManager::mkBoundVar(Type type) {
+Expr ExprManager::mkBoundVar(Type type)
+{
   NodeManagerScope nms(d_nodeManager);
   INC_STAT_VAR(type, true);
   return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 076b6d164..319ab4461 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -40,6 +40,10 @@
 
 namespace CVC4 {
 
+namespace api {
+class Solver;
+}
+
 class StatisticsRegistry;
 class ResourceManager;
 class SkolemManager;
@@ -82,16 +86,19 @@ class NodeManagerListener {
   virtual void nmNotifyDeleteNode(TNode n) {}
 }; /* class NodeManagerListener */
 
-class NodeManager {
-  template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
-  friend class NodeManagerScope;
+class NodeManager
+{
+  friend class api::Solver;
   friend class expr::NodeValue;
   friend class expr::TypeChecker;
-
   // friends so they can access mkVar() here, which is private
   friend Expr ExprManager::mkVar(const std::string&, Type);
   friend Expr ExprManager::mkVar(Type);
 
+  template <unsigned nchild_thresh>
+  friend class NodeBuilder;
+  friend class NodeManagerScope;
+
   /** Predicate for use with STL algorithms */
   struct NodeValueReferenceCountNonZero {
     bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
@@ -1147,7 +1154,7 @@ class NodeManager {
    * any published code!
    */
   void debugHook(int debugFlag);
-};/* class NodeManager */
+}; /* class NodeManager */
 
 /**
  * This class changes the "current" thread-global
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index f5a729b36..3436cc138 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -44,7 +44,7 @@ ${typerules}
 
   default:
     Debug("getType") << "FAILURE" << std::endl;
-    Unhandled() << n.getKind();
+    Unhandled() << " " << n.getKind();
   }
 
   nodeManager->setAttribute(n, TypeAttr(), typeNode);