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

3 files changed, 17 insertions, 8 deletions

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);