From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 28 Jul 2020 18:59:28 +0000 (-0700)
Subject: Replace Expr with Node in Term/Op (#4781)
X-Git-Tag: cvc5-1.0.0~3074
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e8bbee7afb039834955aee96d181b499550a28fe;p=cvc5.git

Replace Expr with Node in Term/Op (#4781)

This commit changes Term and Op to use Nodes internally instead of
Exprs. This is a step towards removing the Expr-layer. This commit also
adds some missing checks regarding the number of arguments for a given
kind that were previously missing, which caused issues in unit tests when
using Node instead of Expr.
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index c009f69e5..2da791da0 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -43,6 +43,7 @@
 #include "expr/expr_manager_scope.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
+#include "expr/node.h"
 #include "expr/node_manager.h"
 #include "expr/sequence.h"
 #include "expr/type.h"
@@ -644,7 +645,15 @@ uint32_t minArity(Kind k)
 {
   Assert(isDefinedKind(k));
   Assert(isDefinedIntKind(extToIntKind(k)));
-  return CVC4::ExprManager::minArity(extToIntKind(k));
+  uint32_t min = CVC4::ExprManager::minArity(extToIntKind(k));
+
+  // At the API level, we treat functions/constructors/selectors/testers as
+  // normal terms instead of making them part of the operator
+  if (isApplyKind(extToIntKind(k)))
+  {
+    min++;
+  }
+  return min;
 }
 
 uint32_t maxArity(Kind k)
@@ -653,9 +662,8 @@ uint32_t maxArity(Kind k)
   Assert(isDefinedIntKind(extToIntKind(k)));
   uint32_t max = CVC4::ExprManager::maxArity(extToIntKind(k));
 
-  // special cases for API level
-  // higher-order logic perspective at API
-  // functions/constructors/selectors/testers are terms
+  // At the API level, we treat functions/constructors/selectors/testers as
+  // normal terms instead of making them part of the operator
   if (isApplyKind(extToIntKind(k))
       && max != std::numeric_limits<uint32_t>::max())  // be careful not to
                                                        // overflow
@@ -1159,19 +1167,33 @@ size_t SortHashFunction::operator()(const Sort& s) const
 /* Op                                                                     */
 /* -------------------------------------------------------------------------- */
 
-Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {}
+Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_node(new CVC4::Node()) {}
 
 Op::Op(const Solver* slv, const Kind k)
-    : d_solver(slv), d_kind(k), d_expr(new CVC4::Expr())
+    : d_solver(slv), d_kind(k), d_node(new CVC4::Node())
 {
 }
 
 Op::Op(const Solver* slv, const Kind k, const CVC4::Expr& e)
-    : d_solver(slv), d_kind(k), d_expr(new 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))
 {
 }
 
-Op::~Op() {}
+Op::~Op()
+{
+  if (d_solver != nullptr)
+  {
+    // Ensure that the correct node manager is in scope when the node is
+    // destroyed.
+    NodeManagerScope scope(d_solver->getNodeManager());
+    d_node.reset();
+  }
+}
 
 /* Helpers                                                                    */
 /* -------------------------------------------------------------------------- */
@@ -1181,23 +1203,23 @@ Op::~Op() {}
 
 bool Op::isNullHelper() const
 {
-  return (d_expr->isNull() && (d_kind == NULL_EXPR));
+  return (d_node->isNull() && (d_kind == NULL_EXPR));
 }
 
-bool Op::isIndexedHelper() const { return !d_expr->isNull(); }
+bool Op::isIndexedHelper() const { return !d_node->isNull(); }
 
 /* Public methods                                                             */
 bool Op::operator==(const Op& t) const
 {
-  if (d_expr->isNull() && t.d_expr->isNull())
+  if (d_node->isNull() && t.d_node->isNull())
   {
     return (d_kind == t.d_kind);
   }
-  else if (d_expr->isNull() || t.d_expr->isNull())
+  else if (d_node->isNull() || t.d_node->isNull())
   {
     return false;
   }
-  return (d_kind == t.d_kind) && (*d_expr == *t.d_expr);
+  return (d_kind == t.d_kind) && (*d_node == *t.d_node);
 }
 
 bool Op::operator!=(const Op& t) const { return !(*this == t); }
@@ -1216,22 +1238,22 @@ template <>
 std::string Op::getIndices() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  CVC4_API_CHECK(!d_expr->isNull())
+  CVC4_API_CHECK(!d_node->isNull())
       << "Expecting a non-null internal expression. This Op is not indexed.";
 
   std::string i;
-  Kind k = intToExtKind(d_expr->getKind());
+  Kind k = intToExtKind(d_node->getKind());
 
   if (k == DIVISIBLE)
   {
     // DIVISIBLE returns a string index to support
     // arbitrary precision integers
-    CVC4::Integer _int = d_expr->getConst<Divisible>().k;
+    CVC4::Integer _int = d_node->getConst<Divisible>().k;
     i = _int.toString();
   }
   else if (k == RECORD_UPDATE)
   {
-    i = d_expr->getConst<RecordUpdate>().getField();
+    i = d_node->getConst<RecordUpdate>().getField();
   }
   else
   {
@@ -1246,37 +1268,37 @@ template <>
 uint32_t Op::getIndices() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  CVC4_API_CHECK(!d_expr->isNull())
+  CVC4_API_CHECK(!d_node->isNull())
       << "Expecting a non-null internal expression. This Op is not indexed.";
 
   uint32_t i = 0;
-  Kind k = intToExtKind(d_expr->getKind());
+  Kind k = intToExtKind(d_node->getKind());
   switch (k)
   {
     case BITVECTOR_REPEAT:
-      i = d_expr->getConst<BitVectorRepeat>().d_repeatAmount;
+      i = d_node->getConst<BitVectorRepeat>().d_repeatAmount;
       break;
     case BITVECTOR_ZERO_EXTEND:
-      i = d_expr->getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
+      i = d_node->getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
       break;
     case BITVECTOR_SIGN_EXTEND:
-      i = d_expr->getConst<BitVectorSignExtend>().d_signExtendAmount;
+      i = d_node->getConst<BitVectorSignExtend>().d_signExtendAmount;
       break;
     case BITVECTOR_ROTATE_LEFT:
-      i = d_expr->getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
+      i = d_node->getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
       break;
     case BITVECTOR_ROTATE_RIGHT:
-      i = d_expr->getConst<BitVectorRotateRight>().d_rotateRightAmount;
+      i = d_node->getConst<BitVectorRotateRight>().d_rotateRightAmount;
       break;
-    case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().d_size; break;
-    case IAND: i = d_expr->getConst<IntAnd>().d_size; break;
+    case INT_TO_BITVECTOR: i = d_node->getConst<IntToBitVector>().d_size; break;
+    case IAND: i = d_node->getConst<IntAnd>().d_size; break;
     case FLOATINGPOINT_TO_UBV:
-      i = d_expr->getConst<FloatingPointToUBV>().bvs.d_size;
+      i = d_node->getConst<FloatingPointToUBV>().bvs.d_size;
       break;
     case FLOATINGPOINT_TO_SBV:
-      i = d_expr->getConst<FloatingPointToSBV>().bvs.d_size;
+      i = d_node->getConst<FloatingPointToSBV>().bvs.d_size;
       break;
-    case TUPLE_UPDATE: i = d_expr->getConst<TupleUpdate>().getIndex(); break;
+    case TUPLE_UPDATE: i = d_node->getConst<TupleUpdate>().getIndex(); break;
     default:
       CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from"
                                          << " kind " << kindToString(k);
@@ -1288,51 +1310,51 @@ template <>
 std::pair<uint32_t, uint32_t> Op::getIndices() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  CVC4_API_CHECK(!d_expr->isNull())
+  CVC4_API_CHECK(!d_node->isNull())
       << "Expecting a non-null internal expression. This Op is not indexed.";
 
   std::pair<uint32_t, uint32_t> indices;
-  Kind k = intToExtKind(d_expr->getKind());
+  Kind k = intToExtKind(d_node->getKind());
 
   // using if/else instead of case statement because want local variables
   if (k == BITVECTOR_EXTRACT)
   {
-    CVC4::BitVectorExtract ext = d_expr->getConst<BitVectorExtract>();
+    CVC4::BitVectorExtract ext = d_node->getConst<BitVectorExtract>();
     indices = std::make_pair(ext.d_high, ext.d_low);
   }
   else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR)
   {
     CVC4::FloatingPointToFPIEEEBitVector ext =
-        d_expr->getConst<FloatingPointToFPIEEEBitVector>();
+        d_node->getConst<FloatingPointToFPIEEEBitVector>();
     indices = std::make_pair(ext.t.exponent(), ext.t.significand());
   }
   else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT)
   {
     CVC4::FloatingPointToFPFloatingPoint ext =
-        d_expr->getConst<FloatingPointToFPFloatingPoint>();
+        d_node->getConst<FloatingPointToFPFloatingPoint>();
     indices = std::make_pair(ext.t.exponent(), ext.t.significand());
   }
   else if (k == FLOATINGPOINT_TO_FP_REAL)
   {
-    CVC4::FloatingPointToFPReal ext = d_expr->getConst<FloatingPointToFPReal>();
+    CVC4::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>();
     indices = std::make_pair(ext.t.exponent(), ext.t.significand());
   }
   else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR)
   {
     CVC4::FloatingPointToFPSignedBitVector ext =
-        d_expr->getConst<FloatingPointToFPSignedBitVector>();
+        d_node->getConst<FloatingPointToFPSignedBitVector>();
     indices = std::make_pair(ext.t.exponent(), ext.t.significand());
   }
   else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR)
   {
     CVC4::FloatingPointToFPUnsignedBitVector ext =
-        d_expr->getConst<FloatingPointToFPUnsignedBitVector>();
+        d_node->getConst<FloatingPointToFPUnsignedBitVector>();
     indices = std::make_pair(ext.t.exponent(), ext.t.significand());
   }
   else if (k == FLOATINGPOINT_TO_FP_GENERIC)
   {
     CVC4::FloatingPointToFPGeneric ext =
-        d_expr->getConst<FloatingPointToFPGeneric>();
+        d_node->getConst<FloatingPointToFPGeneric>();
     indices = std::make_pair(ext.t.exponent(), ext.t.significand());
   }
   else
@@ -1346,21 +1368,26 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const
 std::string Op::toString() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  if (d_expr->isNull())
+  if (d_node->isNull())
   {
     return kindToString(d_kind);
   }
   else
   {
-    CVC4_API_CHECK(!d_expr->isNull())
+    CVC4_API_CHECK(!d_node->isNull())
         << "Expecting a non-null internal expression";
-    return d_expr->toString();
+    return d_node->toString();
   }
 }
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
-CVC4::Expr Op::getExpr(void) const { return *d_expr; }
+CVC4::Expr Op::getExpr(void) const
+{
+  if (d_node->isNull()) return Expr();
+  NodeManagerScope scope(d_solver->getNodeManager());
+  return d_node->toExpr();
+}
 
 std::ostream& operator<<(std::ostream& out, const Op& t)
 {
@@ -1372,7 +1399,7 @@ size_t OpHashFunction::operator()(const Op& t) const
 {
   if (t.isIndexedHelper())
   {
-    return ExprHashFunction()(*t.d_expr);
+    return ExprHashFunction()(t.d_node->toExpr());
   }
   else
   {
@@ -1384,19 +1411,33 @@ size_t OpHashFunction::operator()(const Op& t) const
 /* Term                                                                       */
 /* -------------------------------------------------------------------------- */
 
-Term::Term() : d_solver(nullptr), d_expr(new CVC4::Expr()) {}
+Term::Term() : d_solver(nullptr), d_node(new CVC4::Node()) {}
 
 Term::Term(const Solver* slv, const CVC4::Expr& e)
-    : d_solver(slv), d_expr(new CVC4::Expr(e))
+    : d_solver(slv), d_node(new CVC4::Node(e))
+{
+}
+
+Term::Term(const Solver* slv, const CVC4::Node& n)
+    : d_solver(slv), d_node(new CVC4::Node(n))
 {
 }
 
-Term::~Term() {}
+Term::~Term()
+{
+  if (d_solver != nullptr)
+  {
+    // Ensure that the correct node manager is in scope when the node is
+    // destroyed.
+    NodeManagerScope scope(d_solver->getNodeManager());
+    d_node.reset();
+  }
+}
 
 bool Term::isNullHelper() const
 {
   /* Split out to avoid nested API calls (problematic with API tracing). */
-  return d_expr->isNull();
+  return d_node->isNull();
 }
 
 Kind Term::getKindHelper() const
@@ -1407,7 +1448,7 @@ Kind Term::getKindHelper() const
   // we check here.
   if (getNumChildren() > 0 && (*this)[0].getSort().isSequence())
   {
-    switch (d_expr->getKind())
+    switch (d_node->getKind())
     {
       case CVC4::Kind::STRING_CONCAT: return SEQ_CONCAT;
       case CVC4::Kind::STRING_LENGTH: return SEQ_LENGTH;
@@ -1427,55 +1468,55 @@ Kind Term::getKindHelper() const
     }
   }
 
-  return intToExtKind(d_expr->getKind());
+  return intToExtKind(d_node->getKind());
 }
 
-bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
+bool Term::operator==(const Term& t) const { return *d_node == *t.d_node; }
 
-bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; }
+bool Term::operator!=(const Term& t) const { return *d_node != *t.d_node; }
 
-bool Term::operator<(const Term& t) const { return *d_expr < *t.d_expr; }
+bool Term::operator<(const Term& t) const { return *d_node < *t.d_node; }
 
-bool Term::operator>(const Term& t) const { return *d_expr > *t.d_expr; }
+bool Term::operator>(const Term& t) const { return *d_node > *t.d_node; }
 
-bool Term::operator<=(const Term& t) const { return *d_expr <= *t.d_expr; }
+bool Term::operator<=(const Term& t) const { return *d_node <= *t.d_node; }
 
-bool Term::operator>=(const Term& t) const { return *d_expr >= *t.d_expr; }
+bool Term::operator>=(const Term& t) const { return *d_node >= *t.d_node; }
 
 size_t Term::getNumChildren() const
 {
   CVC4_API_CHECK_NOT_NULL;
   // special case for apply kinds
-  if (isApplyKind(d_expr->getKind()))
+  if (isApplyKind(d_node->getKind()))
   {
-    return d_expr->getNumChildren() + 1;
+    return d_node->getNumChildren() + 1;
   }
-  return d_expr->getNumChildren();
+  return d_node->getNumChildren();
 }
 
 Term Term::operator[](size_t index) const
 {
   CVC4_API_CHECK_NOT_NULL;
   // special cases for apply kinds
-  if (isApplyKind(d_expr->getKind()))
+  if (isApplyKind(d_node->getKind()))
   {
-    CVC4_API_CHECK(d_expr->hasOperator())
+    CVC4_API_CHECK(d_node->hasOperator())
         << "Expected apply kind to have operator when accessing child of Term";
     if (index == 0)
     {
       // return the operator
-      return Term(d_solver, d_expr->getOperator());
+      return Term(d_solver, d_node->getOperator().toExpr());
     }
     // otherwise we are looking up child at (index-1)
     index--;
   }
-  return Term(d_solver, (*d_expr)[index]);
+  return Term(d_solver, (*d_node)[index].toExpr());
 }
 
 uint64_t Term::getId() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  return d_expr->getId();
+  return d_node->getId();
 }
 
 Kind Term::getKind() const
@@ -1487,7 +1528,8 @@ Kind Term::getKind() const
 Sort Term::getSort() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  return Sort(d_solver, d_expr->getType());
+  NodeManagerScope scope(d_solver->getNodeManager());
+  return Sort(d_solver, d_node->getType().toType());
 }
 
 Term Term::substitute(Term e, Term replacement) const
@@ -1499,7 +1541,8 @@ 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 Term(d_solver, d_expr->substitute(e.getExpr(), replacement.getExpr()));
+  return Term(d_solver,
+              d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node)));
 }
 
 Term Term::substitute(const std::vector<Term> es,
@@ -1517,21 +1560,26 @@ 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";
   }
+
+  std::vector<Node> nodes = termVectorToNodes(es);
+  std::vector<Node> nodeReplacements = termVectorToNodes(replacements);
   return Term(d_solver,
-              d_expr->substitute(termVectorToExprs(es),
-                                 termVectorToExprs(replacements)));
+              d_node->substitute(nodes.begin(),
+                                 nodes.end(),
+                                 nodeReplacements.begin(),
+                                 nodeReplacements.end()));
 }
 
 bool Term::hasOp() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  return d_expr->hasOperator();
+  return d_node->hasOperator();
 }
 
 Op Term::getOp() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  CVC4_API_CHECK(d_expr->hasOperator())
+  CVC4_API_CHECK(d_node->hasOperator())
       << "Expecting Term to have an Op when calling getOp()";
 
   // special cases for parameterized operators that are not indexed operators
@@ -1539,16 +1587,16 @@ Op Term::getOp() const
   // indexed operators are stored in Ops
   // whereas functions and datatype operators are terms, and the Op
   // is one of the APPLY_* kinds
-  if (isApplyKind(d_expr->getKind()))
+  if (isApplyKind(d_node->getKind()))
   {
-    return Op(d_solver, intToExtKind(d_expr->getKind()));
+    return Op(d_solver, intToExtKind(d_node->getKind()));
   }
-  else if (d_expr->isParameterized())
+  else if (d_node->getMetaKind() == kind::metakind::PARAMETERIZED)
   {
     // it's an indexed operator
     // so we should return the indexed op
-    CVC4::Expr op = d_expr->getOperator();
-    return Op(d_solver, intToExtKind(d_expr->getKind()), op);
+    CVC4::Node op = d_node->getOperator();
+    return Op(d_solver, intToExtKind(d_node->getKind()), op);
   }
   // Notice this is the only case where getKindHelper is used, since the
   // cases above do have special cases for intToExtKind.
@@ -1560,7 +1608,7 @@ bool Term::isNull() const { return isNullHelper(); }
 bool Term::isConst() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  return d_expr->isConst();
+  return d_node->isConst();
 }
 
 Term Term::getConstArrayBase() const
@@ -1568,22 +1616,22 @@ Term Term::getConstArrayBase() const
   CVC4::ExprManagerScope exmgrs(*(d_solver->getExprManager()));
   CVC4_API_CHECK_NOT_NULL;
   // CONST_ARRAY kind maps to STORE_ALL internal kind
-  CVC4_API_CHECK(d_expr->getKind() == CVC4::Kind::STORE_ALL)
+  CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::STORE_ALL)
       << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()";
-  return Term(d_solver, d_expr->getConst<ArrayStoreAll>().getValue().toExpr());
+  return Term(d_solver, d_node->getConst<ArrayStoreAll>().getValue());
 }
 
 std::vector<Term> Term::getConstSequenceElements() const
 {
   CVC4_API_CHECK_NOT_NULL;
-  CVC4_API_CHECK(d_expr->getKind() == CVC4::Kind::CONST_SEQUENCE)
+  CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_SEQUENCE)
       << "Expecting a CONST_SEQUENCE Term when calling "
          "getConstSequenceElements()";
-  const std::vector<Node>& elems = d_expr->getConst<Sequence>().getVec();
+  const std::vector<Node>& elems = d_node->getConst<Sequence>().getVec();
   std::vector<Term> terms;
   for (const Node& t : elems)
   {
-    terms.push_back(Term(d_solver, t.toExpr()));
+    terms.push_back(Term(d_solver, t));
   }
   return terms;
 }
@@ -1593,11 +1641,11 @@ Term Term::notTerm() const
   CVC4_API_CHECK_NOT_NULL;
   try
   {
-    Expr res = d_expr->notExpr();
+    Node res = d_node->notNode();
     (void)res.getType(true); /* kick off type checking */
     return Term(d_solver, res);
   }
-  catch (const CVC4::TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingExceptionPrivate& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1609,11 +1657,11 @@ Term Term::andTerm(const Term& t) const
   CVC4_API_ARG_CHECK_NOT_NULL(t);
   try
   {
-    Expr res = d_expr->andExpr(*t.d_expr);
+    Node res = d_node->andNode(*t.d_node);
     (void)res.getType(true); /* kick off type checking */
     return Term(d_solver, res);
   }
-  catch (const CVC4::TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingExceptionPrivate& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1625,11 +1673,11 @@ Term Term::orTerm(const Term& t) const
   CVC4_API_ARG_CHECK_NOT_NULL(t);
   try
   {
-    Expr res = d_expr->orExpr(*t.d_expr);
+    Node res = d_node->orNode(*t.d_node);
     (void)res.getType(true); /* kick off type checking */
     return Term(d_solver, res);
   }
-  catch (const CVC4::TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingExceptionPrivate& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1641,11 +1689,11 @@ Term Term::xorTerm(const Term& t) const
   CVC4_API_ARG_CHECK_NOT_NULL(t);
   try
   {
-    Expr res = d_expr->xorExpr(*t.d_expr);
+    Node res = d_node->xorNode(*t.d_node);
     (void)res.getType(true); /* kick off type checking */
     return Term(d_solver, res);
   }
-  catch (const CVC4::TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingExceptionPrivate& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1657,11 +1705,11 @@ Term Term::eqTerm(const Term& t) const
   CVC4_API_ARG_CHECK_NOT_NULL(t);
   try
   {
-    Expr res = d_expr->eqExpr(*t.d_expr);
+    Node res = d_node->eqNode(*t.d_node);
     (void)res.getType(true); /* kick off type checking */
     return Term(d_solver, res);
   }
-  catch (const CVC4::TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingExceptionPrivate& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1673,11 +1721,11 @@ Term Term::impTerm(const Term& t) const
   CVC4_API_ARG_CHECK_NOT_NULL(t);
   try
   {
-    Expr res = d_expr->impExpr(*t.d_expr);
+    Node res = d_node->impNode(*t.d_node);
     (void)res.getType(true); /* kick off type checking */
     return Term(d_solver, res);
   }
-  catch (const CVC4::TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingExceptionPrivate& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
@@ -1690,37 +1738,37 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const
   CVC4_API_ARG_CHECK_NOT_NULL(else_t);
   try
   {
-    Expr res = d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
+    Node res = d_node->iteNode(*then_t.d_node, *else_t.d_node);
     (void)res.getType(true); /* kick off type checking */
     return Term(d_solver, res);
   }
-  catch (const CVC4::TypeCheckingException& e)
+  catch (const CVC4::TypeCheckingExceptionPrivate& e)
   {
     throw CVC4ApiException(e.getMessage());
   }
 }
 
-std::string Term::toString() const { return d_expr->toString(); }
+std::string Term::toString() const { return d_node->toString(); }
 
 Term::const_iterator::const_iterator()
-    : d_solver(nullptr), d_orig_expr(nullptr), d_pos(0)
+    : d_solver(nullptr), d_origNode(nullptr), d_pos(0)
 {
 }
 
 Term::const_iterator::const_iterator(const Solver* slv,
-                                     const std::shared_ptr<CVC4::Expr>& e,
+                                     const std::shared_ptr<CVC4::Node>& n,
                                      uint32_t p)
-    : d_solver(slv), d_orig_expr(e), d_pos(p)
+    : d_solver(slv), d_origNode(n), d_pos(p)
 {
 }
 
 Term::const_iterator::const_iterator(const const_iterator& it)
-    : d_solver(nullptr), d_orig_expr(nullptr)
+    : d_solver(nullptr), d_origNode(nullptr)
 {
-  if (it.d_orig_expr != nullptr)
+  if (it.d_origNode != nullptr)
   {
     d_solver = it.d_solver;
-    d_orig_expr = it.d_orig_expr;
+    d_origNode = it.d_origNode;
     d_pos = it.d_pos;
   }
 }
@@ -1728,18 +1776,18 @@ Term::const_iterator::const_iterator(const const_iterator& it)
 Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it)
 {
   d_solver = it.d_solver;
-  d_orig_expr = it.d_orig_expr;
+  d_origNode = it.d_origNode;
   d_pos = it.d_pos;
   return *this;
 }
 
 bool Term::const_iterator::operator==(const const_iterator& it) const
 {
-  if (d_orig_expr == nullptr || it.d_orig_expr == nullptr)
+  if (d_origNode == nullptr || it.d_origNode == nullptr)
   {
     return false;
   }
-  return (d_solver == it.d_solver && *d_orig_expr == *it.d_orig_expr)
+  return (d_solver == it.d_solver && *d_origNode == *it.d_origNode)
          && (d_pos == it.d_pos);
 }
 
@@ -1750,14 +1798,14 @@ bool Term::const_iterator::operator!=(const const_iterator& it) const
 
 Term::const_iterator& Term::const_iterator::operator++()
 {
-  Assert(d_orig_expr != nullptr);
+  Assert(d_origNode != nullptr);
   ++d_pos;
   return *this;
 }
 
 Term::const_iterator Term::const_iterator::operator++(int)
 {
-  Assert(d_orig_expr != nullptr);
+  Assert(d_origNode != nullptr);
   const_iterator it = *this;
   ++d_pos;
   return it;
@@ -1765,14 +1813,14 @@ Term::const_iterator Term::const_iterator::operator++(int)
 
 Term Term::const_iterator::operator*() const
 {
-  Assert(d_orig_expr != nullptr);
+  Assert(d_origNode != nullptr);
   // this term has an extra child (mismatch between API and internal structure)
   // the extra child will be the first child
-  bool extra_child = isApplyKind(d_orig_expr->getKind());
+  bool extra_child = isApplyKind(d_origNode->getKind());
 
   if (!d_pos && extra_child)
   {
-    return Term(d_solver, d_orig_expr->getOperator());
+    return Term(d_solver, d_origNode->getOperator());
   }
   else
   {
@@ -1783,35 +1831,47 @@ Term Term::const_iterator::operator*() const
       --idx;
     }
     Assert(idx >= 0);
-    return Term(d_solver, (*d_orig_expr)[idx]);
+    return Term(d_solver, (*d_origNode)[idx]);
   }
 }
 
 Term::const_iterator Term::begin() const
 {
-  return Term::const_iterator(d_solver, d_expr, 0);
+  return Term::const_iterator(d_solver, d_node, 0);
 }
 
 Term::const_iterator Term::end() const
 {
-  int endpos = d_expr->getNumChildren();
+  int endpos = d_node->getNumChildren();
   // special cases for APPLY_*
   // the API differs from the internal structure
   // the API takes a "higher-order" perspective and the applied
   //   function or datatype constructor/selector/tester is a Term
   // which means it needs to be one of the children, even though
   //   internally it is not
-  if (isApplyKind(d_expr->getKind()))
+  if (isApplyKind(d_node->getKind()))
   {
     // one more child if this is a UF application (count the UF as a child)
     ++endpos;
   }
-  return Term::const_iterator(d_solver, d_expr, endpos);
+  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();
 }
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
-CVC4::Expr Term::getExpr(void) const { return *d_expr; }
+const CVC4::Node& Term::getNode(void) const { return *d_node; }
 
 std::ostream& operator<<(std::ostream& out, const Term& t)
 {
@@ -1857,7 +1917,7 @@ std::ostream& operator<<(
 
 size_t TermHashFunction::operator()(const Term& t) const
 {
-  return ExprHashFunction()(*t.d_expr);
+  return ExprHashFunction()(t.d_node->toExpr());
 }
 
 /* -------------------------------------------------------------------------- */
@@ -2413,7 +2473,7 @@ void Grammar::addRule(Term ntSymbol, Term rule)
       d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
       << "ntSymbol to be one of the non-terminal symbols given in the "
          "predeclaration";
-  CVC4_API_CHECK(ntSymbol.d_expr->getType() == rule.d_expr->getType())
+  CVC4_API_CHECK(ntSymbol.d_node->getType() == rule.d_node->getType())
       << "Expected ntSymbol and rule to have the same sort";
 
   d_ntsToTerms[ntSymbol].push_back(rule);
@@ -2434,7 +2494,7 @@ void Grammar::addRules(Term ntSymbol, std::vector<Term> rules)
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !rules[i].isNull(), "parameter rule", rules[i], i)
         << "non-null term";
-    CVC4_API_CHECK(ntSymbol.d_expr->getType() == rules[i].d_expr->getType())
+    CVC4_API_CHECK(ntSymbol.d_node->getType() == rules[i].d_node->getType())
         << "Expected ntSymbol and rule at index " << i
         << " to have the same sort";
   }
@@ -2509,13 +2569,13 @@ Sort Grammar::resolve()
 
     if (d_allowVars.find(ntSym) != d_allowVars.cend())
     {
-      addSygusConstructorVariables(dtDecl,
-                                   Sort(d_solver, ntSym.d_expr->getType()));
+      addSygusConstructorVariables(
+          dtDecl, Sort(d_solver, ntSym.d_node->getType().toType()));
     }
 
     bool aci = d_allowConst.find(ntSym) != d_allowConst.end();
-    Type btt = ntSym.d_expr->getType();
-    dtDecl.d_dtype->setSygus(btt, *bvl.d_expr, aci, false);
+    Type btt = ntSym.d_node->getType().toType();
+    dtDecl.d_dtype->setSygus(btt, bvl.d_node->toExpr(), aci, false);
 
     // We can be in a case where the only rule specified was (Variable T)
     // and there are no variables of type T, in which case this is a bogus
@@ -2560,12 +2620,13 @@ void Grammar::addSygusConstructorTerm(
                      d_solver->getExprManager()->mkExpr(
                          CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(args)));
     // its operator is a lambda
-    op = Term(d_solver,
-              d_solver->getExprManager()->mkExpr(CVC4::kind::LAMBDA,
-                                                 {*lbvl.d_expr, *op.d_expr}));
+    op = Term(
+        d_solver,
+        d_solver->getExprManager()->mkExpr(
+            CVC4::kind::LAMBDA, {lbvl.d_node->toExpr(), op.d_node->toExpr()}));
   }
   dt.d_dtype->addSygusConstructor(
-      *op.d_expr, ssCName.str(), sortVectorToTypes(cargs));
+      op.d_node->toExpr(), ssCName.str(), sortVectorToTypes(cargs));
 }
 
 Term Grammar::purifySygusGTerm(
@@ -2580,38 +2641,40 @@ Term Grammar::purifySygusGTerm(
   {
     Term ret =
         Term(d_solver,
-             d_solver->getExprManager()->mkBoundVar(term.d_expr->getType()));
+             d_solver->getNodeManager()->mkBoundVar(term.d_node->getType()));
     args.push_back(ret);
     cargs.push_back(itn->second);
     return ret;
   }
   std::vector<Term> pchildren;
   bool childChanged = false;
-  for (unsigned i = 0, nchild = term.d_expr->getNumChildren(); i < nchild; i++)
+  for (unsigned i = 0, nchild = term.d_node->getNumChildren(); i < nchild; i++)
   {
     Term ptermc = purifySygusGTerm(
-        Term(d_solver, (*term.d_expr)[i]), args, cargs, ntsToUnres);
+        Term(d_solver, (*term.d_node)[i]), args, cargs, ntsToUnres);
     pchildren.push_back(ptermc);
-    childChanged = childChanged || *ptermc.d_expr != (*term.d_expr)[i];
+    childChanged =
+        childChanged || ptermc.d_node->toExpr() != (term.d_node->toExpr())[i];
   }
   if (!childChanged)
   {
     return term;
   }
 
-  Expr nret;
+  Node nret;
 
-  if (term.d_expr->isParameterized())
+  if (term.d_node->getMetaKind() == kind::metakind::PARAMETERIZED)
   {
     // it's an indexed operator so we should provide the op
-    nret = d_solver->getExprManager()->mkExpr(term.d_expr->getKind(),
-                                              term.d_expr->getOperator(),
-                                              termVectorToExprs(pchildren));
+    NodeBuilder<> nb(term.d_node->getKind());
+    nb << term.d_node->getOperator();
+    nb.append(termVectorToNodes(pchildren));
+    nret = nb.constructNode();
   }
   else
   {
-    nret = d_solver->getExprManager()->mkExpr(term.d_expr->getKind(),
-                                              termVectorToExprs(pchildren));
+    nret = d_solver->getNodeManager()->mkNode(term.d_node->getKind(),
+                                              termVectorToNodes(pchildren));
   }
 
   return Term(d_solver, nret);
@@ -2624,13 +2687,13 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const
   for (unsigned i = 0, size = d_sygusVars.size(); i < size; i++)
   {
     Term v = d_sygusVars[i];
-    if (v.d_expr->getType() == *sort.d_type)
+    if (v.d_node->getType().toType() == *sort.d_type)
     {
       std::stringstream ss;
       ss << v;
       std::vector<Sort> cargs;
       dt.d_dtype->addSygusConstructor(
-          *v.d_expr, ss.str(), sortVectorToTypes(cargs));
+          v.d_node->toExpr(), ss.str(), sortVectorToTypes(cargs));
     }
   }
 }
@@ -2693,7 +2756,8 @@ Solver::~Solver() {}
 template <typename T>
 Term Solver::mkValHelper(T t) const
 {
-  Expr res = d_exprMgr->mkConst(t);
+  NodeManagerScope scope(getNodeManager());
+  Node res = getNodeManager()->mkConst(t);
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
 }
@@ -2798,6 +2862,7 @@ Term Solver::mkTermFromKind(Kind kind) const
 
 Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   for (size_t i = 0, size = children.size(); i < size; ++i)
   {
@@ -2924,7 +2989,7 @@ std::vector<Expr> Solver::termVectorToExprs(
   for (const Term& t : terms)
   {
     CVC4_API_SOLVER_CHECK_TERM(t);
-    res.push_back(*t.d_expr);
+    res.push_back(t.d_node->toExpr());
   }
   return res;
 }
@@ -3519,7 +3584,7 @@ Term Solver::mkConstArray(Sort sort, Term val) const
   CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort()))
       << "Value does not match element sort.";
   Term res = mkValHelper<CVC4::ArrayStoreAll>(CVC4::ArrayStoreAll(
-      TypeNode::fromType(*sort.d_type), Node::fromExpr(*val.d_expr)));
+      TypeNode::fromType(*sort.d_type), Node::fromExpr(val.d_node->toExpr())));
   return res;
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3611,7 +3676,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 Term(this, d_exprMgr->mkConst(CVC4::AbstractValue(idx)));
+  return Term(this, getNodeManager()->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;
@@ -3622,7 +3687,8 @@ 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 Term(this, d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index))));
+  return Term(this,
+              getNodeManager()->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;
@@ -3641,11 +3707,11 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
   CVC4_API_ARG_CHECK_EXPECTED(!val.isNull(), val) << "non-null term";
   CVC4_API_SOLVER_CHECK_TERM(val);
   CVC4_API_ARG_CHECK_EXPECTED(
-      val.getSort().isBitVector() && val.d_expr->isConst(), val)
+      val.getSort().isBitVector() && val.d_node->isConst(), val)
       << "bit-vector constant";
 
   return mkValHelper<CVC4::FloatingPoint>(
-      CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>()));
+      CVC4::FloatingPoint(exp, sig, val.d_node->getConst<BitVector>()));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -3655,6 +3721,7 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
 
 Term Solver::mkConst(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);
@@ -3727,12 +3794,13 @@ Term Solver::mkTerm(Kind kind) const
 
 Term Solver::mkTerm(Kind kind, Term child) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
   CVC4_API_SOLVER_CHECK_TERM(child);
   checkMkTerm(kind, 1);
 
-  Expr res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
+  Node res = getNodeManager()->mkNode(extToIntKind(kind), *child.d_node);
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
 
@@ -3741,6 +3809,7 @@ Term Solver::mkTerm(Kind kind, Term child) const
 
 Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
@@ -3748,8 +3817,8 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
   CVC4_API_SOLVER_CHECK_TERM(child2);
   checkMkTerm(kind, 2);
 
-  Expr res =
-      d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr);
+  Node res = getNodeManager()->mkNode(
+      extToIntKind(kind), *child1.d_node, *child2.d_node);
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
 
@@ -3769,21 +3838,23 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
 
 Term Solver::mkTerm(Op op) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_SOLVER_CHECK_OP(op);
+  checkMkTerm(op.d_kind, 0);
 
   Term res;
   if (op.isIndexedHelper())
   {
     const CVC4::Kind int_kind = extToIntKind(op.d_kind);
-    res = Term(this, d_exprMgr->mkExpr(int_kind, *op.d_expr));
+    res = Term(this, getNodeManager()->mkNode(int_kind, *op.d_node));
   }
   else
   {
     res = mkTermFromKind(op.d_kind);
   }
 
-  (void)res.d_expr->getType(true); /* kick off type checking */
+  (void)res.d_node->getType(true); /* kick off type checking */
   return res;
 
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -3791,20 +3862,22 @@ Term Solver::mkTerm(Op op) const
 
 Term Solver::mkTerm(Op op, Term child) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_SOLVER_CHECK_OP(op);
   CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
   CVC4_API_SOLVER_CHECK_TERM(child);
+  checkMkTerm(op.d_kind, 1);
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
-  Expr res;
+  Node res;
   if (op.isIndexedHelper())
   {
-    res = d_exprMgr->mkExpr(int_kind, *op.d_expr, *child.d_expr);
+    res = getNodeManager()->mkNode(int_kind, *op.d_node, *child.d_node);
   }
   else
   {
-    res = d_exprMgr->mkExpr(int_kind, *child.d_expr);
+    res = getNodeManager()->mkNode(int_kind, *child.d_node);
   }
 
   (void)res.getType(true); /* kick off type checking */
@@ -3815,23 +3888,25 @@ Term Solver::mkTerm(Op op, Term child) const
 
 Term Solver::mkTerm(Op op, Term child1, Term child2) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_SOLVER_CHECK_OP(op);
   CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
   CVC4_API_SOLVER_CHECK_TERM(child1);
   CVC4_API_SOLVER_CHECK_TERM(child2);
+  checkMkTerm(op.d_kind, 2);
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
-  Expr res;
+  Node res;
   if (op.isIndexedHelper())
   {
-    res =
-        d_exprMgr->mkExpr(int_kind, *op.d_expr, *child1.d_expr, *child2.d_expr);
+    res = getNodeManager()->mkNode(
+        int_kind, *op.d_node, *child1.d_node, *child2.d_node);
   }
   else
   {
-    res = d_exprMgr->mkExpr(int_kind, *child1.d_expr, *child2.d_expr);
+    res = getNodeManager()->mkNode(int_kind, *child1.d_node, *child2.d_node);
   }
 
   (void)res.getType(true); /* kick off type checking */
@@ -3841,6 +3916,7 @@ Term Solver::mkTerm(Op op, Term child1, Term child2) const
 
 Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_SOLVER_CHECK_OP(op);
   CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
@@ -3849,18 +3925,19 @@ Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
   CVC4_API_SOLVER_CHECK_TERM(child1);
   CVC4_API_SOLVER_CHECK_TERM(child2);
   CVC4_API_SOLVER_CHECK_TERM(child3);
+  checkMkTerm(op.d_kind, 3);
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
-  Expr res;
+  Node res;
   if (op.isIndexedHelper())
   {
-    res = d_exprMgr->mkExpr(
-        int_kind, *op.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+    res = getNodeManager()->mkNode(
+        int_kind, *op.d_node, *child1.d_node, *child2.d_node, *child3.d_node);
   }
   else
   {
-    res = d_exprMgr->mkExpr(
-        int_kind, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+    res = getNodeManager()->mkNode(
+        int_kind, *child1.d_node, *child2.d_node, *child3.d_node);
   }
 
   (void)res.getType(true); /* kick off type checking */
@@ -3871,8 +3948,10 @@ Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
 
 Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_SOLVER_CHECK_OP(op);
+  checkMkTerm(op.d_kind, children.size());
   for (size_t i = 0, size = children.size(); i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
@@ -3884,15 +3963,18 @@ 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);
-  Expr res;
+  std::vector<Node> echildren = termVectorToNodes(children);
+  Node res;
   if (op.isIndexedHelper())
   {
-    res = d_exprMgr->mkExpr(int_kind, *op.d_expr, echildren);
+    NodeBuilder<> nb(int_kind);
+    nb << *op.d_node;
+    nb.append(echildren);
+    res = nb.constructNode();
   }
   else
   {
-    res = d_exprMgr->mkExpr(int_kind, echildren);
+    res = getNodeManager()->mkNode(int_kind, echildren);
   }
 
   (void)res.getType(true); /* kick off type checking */
@@ -3907,7 +3989,7 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_CHECK(sorts.size() == terms.size())
       << "Expected the same number of sorts and elements";
-  std::vector<CVC4::Expr> args;
+  std::vector<CVC4::Node> args;
   for (size_t i = 0, size = sorts.size(); i < size; i++)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
@@ -3916,14 +3998,15 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         this == sorts[i].d_solver, "child sort", sorts[i], i)
         << "child sort associated to this solver object";
-    args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr);
+    args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_node);
   }
 
   Sort s = mkTupleSort(sorts);
   Datatype dt = s.getDatatype();
-  Expr res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR),
-                               *dt[0].getConstructorTerm().d_expr,
-                               args);
+  NodeBuilder<> nb(extToIntKind(APPLY_CONSTRUCTOR));
+  nb << *dt[0].getConstructorTerm().d_node;
+  nb.append(args);
+  Node res = nb.constructNode();
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
 
@@ -3951,10 +4034,9 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const
   Op res;
   if (kind == RECORD_UPDATE)
   {
-    res = Op(
-        this,
-        kind,
-        *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get());
+    res = Op(this,
+             kind,
+             *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_node);
   }
   else
   {
@@ -3966,7 +4048,7 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const
     res = Op(this,
              kind,
              *mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg)))
-                  .d_expr.get());
+                  .d_node);
   }
   return res;
 
@@ -3982,81 +4064,78 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const
   switch (kind)
   {
     case DIVISIBLE:
-      res =
-          Op(this,
-             kind,
-             *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get());
+      res = Op(this,
+               kind,
+               *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_node);
       break;
     case BITVECTOR_REPEAT:
       res = Op(this,
                kind,
-               *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
-                    .d_expr.get());
+               mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
+                   .d_node->toExpr());
       break;
     case BITVECTOR_ZERO_EXTEND:
       res = Op(this,
                kind,
                *mkValHelper<CVC4::BitVectorZeroExtend>(
                     CVC4::BitVectorZeroExtend(arg))
-                    .d_expr.get());
+                    .d_node);
       break;
     case BITVECTOR_SIGN_EXTEND:
       res = Op(this,
                kind,
                *mkValHelper<CVC4::BitVectorSignExtend>(
                     CVC4::BitVectorSignExtend(arg))
-                    .d_expr.get());
+                    .d_node);
       break;
     case BITVECTOR_ROTATE_LEFT:
       res = Op(this,
                kind,
                *mkValHelper<CVC4::BitVectorRotateLeft>(
                     CVC4::BitVectorRotateLeft(arg))
-                    .d_expr.get());
+                    .d_node);
       break;
     case BITVECTOR_ROTATE_RIGHT:
       res = Op(this,
                kind,
                *mkValHelper<CVC4::BitVectorRotateRight>(
                     CVC4::BitVectorRotateRight(arg))
-                    .d_expr.get());
+                    .d_node);
       break;
     case INT_TO_BITVECTOR:
-      res = Op(this,
-               kind,
-               *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
-                    .d_expr.get());
+      res = Op(
+          this,
+          kind,
+          *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)).d_node);
       break;
     case IAND:
-      res = Op(this,
-               kind,
-               *mkValHelper<CVC4::IntAnd>(CVC4::IntAnd(arg)).d_expr.get());
+      res =
+          Op(this, kind, *mkValHelper<CVC4::IntAnd>(CVC4::IntAnd(arg)).d_node);
       break;
     case FLOATINGPOINT_TO_UBV:
       res = Op(
           this,
           kind,
           *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg))
-               .d_expr.get());
+               .d_node);
       break;
     case FLOATINGPOINT_TO_SBV:
       res = Op(
           this,
           kind,
           *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg))
-               .d_expr.get());
+               .d_node);
       break;
     case TUPLE_UPDATE:
-      res = Op(
-          this,
-          kind,
-          *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get());
-      break;
-    case REGEXP_REPEAT:
       res = Op(this,
                kind,
-               *mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg))
-                    .d_expr.get());
+               *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_node);
+      break;
+    case REGEXP_REPEAT:
+      res =
+          Op(this,
+             kind,
+             *mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg)).d_node);
       break;
     default:
       CVC4_API_KIND_CHECK_EXPECTED(false, kind)
@@ -4081,55 +4160,55 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
                kind,
                *mkValHelper<CVC4::BitVectorExtract>(
                     CVC4::BitVectorExtract(arg1, arg2))
-                    .d_expr.get());
+                    .d_node);
       break;
     case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
       res = Op(this,
                kind,
                *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
                     CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
-                    .d_expr.get());
+                    .d_node);
       break;
     case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
       res = Op(this,
                kind,
                *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
                     CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
-                    .d_expr.get());
+                    .d_node);
       break;
     case FLOATINGPOINT_TO_FP_REAL:
       res = Op(this,
                kind,
                *mkValHelper<CVC4::FloatingPointToFPReal>(
                     CVC4::FloatingPointToFPReal(arg1, arg2))
-                    .d_expr.get());
+                    .d_node);
       break;
     case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
       res = Op(this,
                kind,
                *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
                     CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
-                    .d_expr.get());
+                    .d_node);
       break;
     case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
       res = Op(this,
                kind,
                *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
                     CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
-                    .d_expr.get());
+                    .d_node);
       break;
     case FLOATINGPOINT_TO_FP_GENERIC:
       res = Op(this,
                kind,
                *mkValHelper<CVC4::FloatingPointToFPGeneric>(
                     CVC4::FloatingPointToFPGeneric(arg1, arg2))
-                    .d_expr.get());
+                    .d_node);
       break;
     case REGEXP_LOOP:
-      res = Op(this,
-               kind,
-               *mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2))
-                    .d_expr.get());
+      res = Op(
+          this,
+          kind,
+          *mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2)).d_node);
       break;
     default:
       CVC4_API_KIND_CHECK_EXPECTED(false, kind)
@@ -4147,10 +4226,11 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
 Term Solver::simplify(const Term& term)
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
   CVC4_API_ARG_CHECK_NOT_NULL(term);
   CVC4_API_SOLVER_CHECK_TERM(term);
 
-  return Term(this, d_smtEngine->simplify(*term.d_expr));
+  return Term(this, d_smtEngine->simplify(term.d_node->toExpr()));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4166,7 +4246,7 @@ Result Solver::checkEntailed(Term term) const
   CVC4_API_ARG_CHECK_NOT_NULL(term);
   CVC4_API_SOLVER_CHECK_TERM(term);
 
-  CVC4::Result r = d_smtEngine->checkEntailed(*term.d_expr);
+  CVC4::Result r = d_smtEngine->checkEntailed(term.d_node->toExpr());
   return Result(r);
 
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -4204,7 +4284,7 @@ void Solver::assertFormula(Term term) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_SOLVER_CHECK_TERM(term);
   CVC4_API_ARG_CHECK_NOT_NULL(term);
-  d_smtEngine->assertFormula(Node::fromExpr(*term.d_expr));
+  d_smtEngine->assertFormula(*term.d_node);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -4236,7 +4316,7 @@ Result Solver::checkSatAssuming(Term assumption) const
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC4_API_SOLVER_CHECK_TERM(assumption);
-  CVC4::Result r = d_smtEngine->checkSat(*assumption.d_expr);
+  CVC4::Result r = d_smtEngine->checkSat(assumption.d_node->toExpr());
   return Result(r);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4348,12 +4428,12 @@ Term Solver::defineFun(const std::string& symbol,
         this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
         << "bound variable associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
         "bound variable",
         bound_vars[i],
         i)
         << "a bound variable";
-    CVC4::Type t = bound_vars[i].d_expr->getType();
+    CVC4::Type t = bound_vars[i].d_node->getType().toType();
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         t.isFirstClass(), "sort of parameter", bound_vars[i], i)
         << "first-class sort of parameter of defined function";
@@ -4370,7 +4450,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, global);
+  d_smtEngine->defineFunction(fun, ebound_vars, term.d_node->toExpr(), global);
   return Term(this, fun);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4394,7 +4474,7 @@ Term Solver::defineFun(Term fun,
           this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
           << "bound variable associated to this solver object";
       CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-          bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+          bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
           "bound variable",
           bound_vars[i],
           i)
@@ -4420,7 +4500,8 @@ Term Solver::defineFun(Term fun,
   CVC4_API_SOLVER_CHECK_TERM(term);
 
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
-  d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr, global);
+  d_smtEngine->defineFunction(
+      fun.d_node->toExpr(), ebound_vars, term.d_node->toExpr(), global);
   return fun;
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4434,6 +4515,7 @@ Term Solver::defineFunRec(const std::string& symbol,
                           Term term,
                           bool global) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
 
   CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
@@ -4453,12 +4535,12 @@ Term Solver::defineFunRec(const std::string& symbol,
         this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
         << "bound variable associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
         "bound variable",
         bound_vars[i],
         i)
         << "a bound variable";
-    CVC4::Type t = bound_vars[i].d_expr->getType();
+    CVC4::Type t = bound_vars[i].d_node->getType().toType();
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         t.isFirstClass(), "sort of parameter", bound_vars[i], i)
         << "first-class sort of parameter of defined function";
@@ -4476,7 +4558,8 @@ 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, global);
+  d_smtEngine->defineFunctionRec(
+      fun, ebound_vars, term.d_node->toExpr(), global);
   return Term(this, fun);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4486,6 +4569,7 @@ Term Solver::defineFunRec(Term fun,
                           Term term,
                           bool global) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
 
   CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
@@ -4507,7 +4591,7 @@ Term Solver::defineFunRec(Term fun,
           this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
           << "bound variable associated to this solver object";
       CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-          bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+          bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
           "bound variable",
           bound_vars[i],
           i)
@@ -4533,7 +4617,7 @@ Term Solver::defineFunRec(Term fun,
   CVC4_API_SOLVER_CHECK_TERM(term);
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
   d_smtEngine->defineFunctionRec(
-      *fun.d_expr, ebound_vars, *term.d_expr, global);
+      fun.d_node->toExpr(), ebound_vars, term.d_node->toExpr(), global);
   return fun;
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
@@ -4546,6 +4630,7 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
                            const std::vector<Term>& terms,
                            bool global) const
 {
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
 
   CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
@@ -4583,7 +4668,7 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
               this == bvars[k].d_solver, "bound variable", bvars[k], k)
               << "bound variable associated to this solver object";
           CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-              bvars[k].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+              bvars[k].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
               "bound variable",
               bvars[k],
               k)
@@ -4753,7 +4838,7 @@ Term Solver::getValue(Term term) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_SOLVER_CHECK_TERM(term);
-  return Term(this, d_smtEngine->getValue(*term.d_expr));
+  return Term(this, d_smtEngine->getValue(term.d_node->toExpr()));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -4777,7 +4862,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
         this == terms[i].d_solver, "term", terms[i], i)
         << "term associated to this solver object";
     /* Can not use emplace_back here since constructor is private. */
-    res.push_back(Term(this, d_smtEngine->getValue(*terms[i].d_expr)));
+    res.push_back(Term(this, d_smtEngine->getValue(terms[i].d_node->toExpr())));
   }
   return res;
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -4857,7 +4942,7 @@ bool Solver::getInterpolant(Term conj, Term& output) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   Expr result;
-  bool success = d_smtEngine->getInterpol(*conj.d_expr, result);
+  bool success = d_smtEngine->getInterpol(conj.d_node->toExpr(), result);
   if (success) {
     output = Term(output.d_solver, result);
   }
@@ -4869,7 +4954,7 @@ bool Solver::getInterpolant(Term conj, const Type& gtype, Term& output) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   Expr result;
-  bool success = d_smtEngine->getInterpol(*conj.d_expr, gtype, result);
+  bool success = d_smtEngine->getInterpol(conj.d_node->toExpr(), gtype, result);
   if (success)
   {
     output = Term(output.d_solver, result);
@@ -4997,7 +5082,7 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
     // in the theory.
     res = Term(this,
                d_exprMgr->mkExpr(extToIntKind(DIVISION),
-                                 *res.d_expr,
+                                 res.d_node->toExpr(),
                                  d_exprMgr->mkConst(CVC4::Rational(1))));
   }
   Assert(res.getSort() == sort);
@@ -5033,7 +5118,7 @@ Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars,
         this == boundVars[i].d_solver, "bound variable", boundVars[i], i)
         << "bound variable associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        boundVars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
         "bound variable",
         boundVars[i],
         i)
@@ -5049,7 +5134,7 @@ Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars,
         this == ntSymbols[i].d_solver, "term", ntSymbols[i], i)
         << "term associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        ntSymbols[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        ntSymbols[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
         "bound variable",
         ntSymbols[i],
         i)
@@ -5112,7 +5197,7 @@ Term Solver::synthFunHelper(const std::string& symbol,
         this == boundVars[i].d_solver, "bound variable", boundVars[i], i)
         << "bound variable associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        boundVars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
         "bound variable",
         boundVars[i],
         i)
@@ -5120,13 +5205,13 @@ Term Solver::synthFunHelper(const std::string& symbol,
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !boundVars[i].isNull(), "parameter term", boundVars[i], i)
         << "non-null term";
-    varTypes.push_back(boundVars[i].d_expr->getType());
+    varTypes.push_back(boundVars[i].d_node->getType().toType());
   }
   CVC4_API_SOLVER_CHECK_SORT(sort);
 
   if (g != nullptr)
   {
-    CVC4_API_CHECK(g->d_ntSyms[0].d_expr->getType() == *sort.d_type)
+    CVC4_API_CHECK(g->d_ntSyms[0].d_node->getType().toType() == *sort.d_type)
         << "Invalid Start symbol for Grammar g, Expected Start's sort to be "
         << *sort.d_type;
   }
@@ -5152,13 +5237,14 @@ Term Solver::synthFunHelper(const std::string& symbol,
 void Solver::addSygusConstraint(Term term) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  NodeManagerScope scope(getNodeManager());
   CVC4_API_ARG_CHECK_NOT_NULL(term);
   CVC4_API_SOLVER_CHECK_TERM(term);
   CVC4_API_ARG_CHECK_EXPECTED(
-      term.d_expr->getType() == d_exprMgr->booleanType(), term)
+      term.d_node->getType() == getNodeManager()->booleanType(), term)
       << "boolean term";
 
-  d_smtEngine->assertSygusConstraint(*term.d_expr);
+  d_smtEngine->assertSygusConstraint(*term.d_node);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -5177,18 +5263,18 @@ void Solver::addSygusInvConstraint(Term inv,
   CVC4_API_ARG_CHECK_NOT_NULL(post);
   CVC4_API_SOLVER_CHECK_TERM(post);
 
-  CVC4_API_ARG_CHECK_EXPECTED(inv.d_expr->getType().isFunction(), inv)
+  CVC4_API_ARG_CHECK_EXPECTED(inv.d_node->getType().isFunction(), inv)
       << "a function";
 
-  FunctionType invType = inv.d_expr->getType();
+  FunctionType invType = inv.d_node->getType().toType();
 
   CVC4_API_ARG_CHECK_EXPECTED(invType.getRangeType().isBoolean(), inv)
       << "boolean range";
 
-  CVC4_API_CHECK(pre.d_expr->getType() == invType)
+  CVC4_API_CHECK(pre.d_node->getType().toType() == invType)
       << "Expected inv and pre to have the same sort";
 
-  CVC4_API_CHECK(post.d_expr->getType() == invType)
+  CVC4_API_CHECK(post.d_node->getType().toType() == invType)
       << "Expected inv and post to have the same sort";
 
   const std::vector<Type>& invArgTypes = invType.getArgTypes();
@@ -5205,11 +5291,13 @@ void Solver::addSygusInvConstraint(Term inv,
   expectedTypes.push_back(invType.getRangeType());
   FunctionType expectedTransType = d_exprMgr->mkFunctionType(expectedTypes);
 
-  CVC4_API_CHECK(trans.d_expr->getType() == expectedTransType)
+  CVC4_API_CHECK(trans.d_node->toExpr().getType() == expectedTransType)
       << "Expected trans's sort to be " << invType;
 
-  d_smtEngine->assertSygusInvConstraint(
-      *inv.d_expr, *pre.d_expr, *trans.d_expr, *post.d_expr);
+  d_smtEngine->assertSygusInvConstraint(inv.d_node->toExpr(),
+                                        pre.d_node->toExpr(),
+                                        trans.d_node->toExpr(),
+                                        post.d_node->toExpr());
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -5231,7 +5319,8 @@ Term Solver::getSynthSolution(Term term) const
       << "The solver is not in a state immediately preceeded by a "
          "successful call to checkSynth";
 
-  std::map<CVC4::Expr, CVC4::Expr>::const_iterator it = map.find(*term.d_expr);
+  std::map<CVC4::Expr, CVC4::Expr>::const_iterator it =
+      map.find(term.d_node->toExpr());
 
   CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term";
 
@@ -5266,7 +5355,7 @@ std::vector<Term> Solver::getSynthSolutions(
   for (size_t i = 0, n = terms.size(); i < n; ++i)
   {
     std::map<CVC4::Expr, CVC4::Expr>::const_iterator it =
-        map.find(*terms[i].d_expr);
+        map.find(terms[i].d_node->toExpr());
 
     CVC4_API_CHECK(it != map.cend())
         << "Synth solution not found for term at index " << i;
@@ -5291,6 +5380,15 @@ void Solver::printSynthSolution(std::ostream& out) const
  */
 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();
+}
+
 /**
  * !!! This is only temporarily available until the parser is fully migrated to
  * the new API. !!!
@@ -5317,6 +5415,16 @@ std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms)
   return exprs;
 }
 
+std::vector<Node> termVectorToNodes(const std::vector<Term>& terms)
+{
+  std::vector<Node> res;
+  for (const Term& t : terms)
+  {
+    res.push_back(t.getNode());
+  }
+  return res;
+}
+
 std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts)
 {
   std::vector<Type> types;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 91db4dd58..997616ae3 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -36,11 +36,15 @@
 
 namespace CVC4 {
 
+template <bool ref_count>
+class NodeTemplate;
+typedef NodeTemplate<true> Node;
 class Expr;
 class Datatype;
 class DatatypeConstructor;
 class DatatypeConstructorArg;
 class ExprManager;
+class NodeManager;
 class SmtEngine;
 class Type;
 class Options;
@@ -674,6 +678,17 @@ class CVC4_PUBLIC Op
    */
   Op(const Solver* slv, const Kind k, const CVC4::Expr& e);
 
+  // !!! 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 n the internal node that is to be wrapped by this term
+   * @return the Term
+   */
+  Op(const Solver* slv, const Kind k, const CVC4::Node& n);
+
   /**
    * Destructor.
    */
@@ -763,7 +778,7 @@ class CVC4_PUBLIC Op
    * memory allocation (CVC4::Expr is already ref counted, so this could be
    * a unique_ptr instead).
    */
-  std::shared_ptr<CVC4::Expr> d_expr;
+  std::shared_ptr<CVC4::Node> d_node;
 };
 
 /* -------------------------------------------------------------------------- */
@@ -792,6 +807,16 @@ class CVC4_PUBLIC Term
    */
   Term(const Solver* slv, const CVC4::Expr& e);
 
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param slv the associated solver object
+   * @param n the internal node that is to be wrapped by this term
+   * @return the Term
+   */
+  Term(const Solver* slv, const CVC4::Node& n);
+
   /**
    * Constructor.
    */
@@ -1003,7 +1028,7 @@ class CVC4_PUBLIC Term
      * @param p the position of the iterator (e.g. which child it's on)
      */
     const_iterator(const Solver* slv,
-                   const std::shared_ptr<CVC4::Expr>& e,
+                   const std::shared_ptr<CVC4::Node>& e,
                    uint32_t p);
 
     /**
@@ -1055,8 +1080,8 @@ class CVC4_PUBLIC Term
      * The associated solver object.
      */
     const Solver* d_solver;
-    /* The original expression to be iterated over */
-    std::shared_ptr<CVC4::Expr> d_orig_expr;
+    /* The original node to be iterated over */
+    std::shared_ptr<CVC4::Node> d_origNode;
     /* Keeps track of the iteration position */
     uint32_t d_pos;
   };
@@ -1075,6 +1100,10 @@ class CVC4_PUBLIC Term
   // to the new API. !!!
   CVC4::Expr getExpr(void) const;
 
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  const CVC4::Node& getNode(void) const;
+
  protected:
   /**
    * The associated solver object.
@@ -1101,7 +1130,7 @@ class CVC4_PUBLIC Term
    * memory allocation (CVC4::Expr is already ref counted, so this could be
    * a unique_ptr instead).
    */
-  std::shared_ptr<CVC4::Expr> d_expr;
+  std::shared_ptr<CVC4::Node> d_node;
 };
 
 /**
@@ -3259,6 +3288,10 @@ class CVC4_PUBLIC Solver
   // 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. !!!
   SmtEngine* getSmtEngine(void) const;
@@ -3350,6 +3383,7 @@ class CVC4_PUBLIC Solver
 // !!! Only temporarily public until the parser is fully migrated to the
 // new API. !!!
 std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms);
+std::vector<Node> termVectorToNodes(const std::vector<Term>& terms);
 std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts);
 std::set<Type> sortSetToTypes(const std::set<Sort>& sorts);
 std::vector<Term> exprVectorToTerms(const Solver* slv,
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index f957fe0d0..0d0c17edf 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -763,6 +763,7 @@ inline Type TypeNode::toType() const
 }
 
 inline TypeNode TypeNode::fromType(const Type& t) {
+  NodeManagerScope scope(t.d_nodeManager);
   return NodeManager::fromType(t);
 }
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9ff6ec6f5..d8657c7dd 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1731,14 +1731,14 @@ void SmtEngine::declareSynthFun(const std::string& id,
   setSygusConjectureStale();
 }
 
-void SmtEngine::assertSygusConstraint(Expr constraint)
+void SmtEngine::assertSygusConstraint(const Node& constraint)
 {
   SmtScope smts(this);
   finalOptionsAreSet();
   d_private->d_sygusConstraints.push_back(constraint);
 
   Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n";
-  Dump("raw-benchmark") << SygusConstraintCommand(constraint);
+  Dump("raw-benchmark") << SygusConstraintCommand(constraint.toExpr());
   // sygus conjecture is now stale
   setSygusConjectureStale();
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index b38ec2d7a..a651b8d1e 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -453,7 +453,7 @@ class CVC4_PUBLIC SmtEngine
                        const std::vector<Expr>& vars);
 
   /** Add a regular sygus constraint.*/
-  void assertSygusConstraint(Expr constraint);
+  void assertSygusConstraint(const Node& constraint);
 
   /**
    * Add an invariant constraint.