Further simplifications in preparation for removing Expr layer (#5756)

This deletes variable flags from NodeManager::mkVar and moves ExprManager sort flags to NodeManager.

These flags are used for determining when a variable or sort should be printed via the old dump infrastructure. The old dump infrastructure is simplified in this PR accordingly.

This PR should preserve behavior of the previous dumping with a minor exception that the internal trace "declarations" will also included symbols introduced from define-fun. This will be further refactored later. This is in preparation for removing the includes expr.h/expr_manager.h from node_manager.h.

21 files changed, 67 insertions, 110 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 621e3c1c0..e845bf876 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3730,7 +3730,7 @@ Sort Solver::mkParamSort(const std::string& symbol) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   return Sort(
       this,
-      getNodeManager()->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER));
+      getNodeManager()->mkSort(symbol, NodeManager::SORT_FLAG_PLACEHOLDER));
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 37f0e2527..43161fe04 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -679,18 +679,20 @@ Type ExprManager::getType(Expr expr, bool check)
   return t;
 }
 
-Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
+Expr ExprManager::mkVar(const std::string& name, Type type)
+{
   NodeManagerScope nms(d_nodeManager);
-  Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags);
+  Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode);
   Debug("nm") << "set " << name << " on " << *n << std::endl;
   INC_STAT_VAR(type, false);
   return Expr(this, n);
 }
 
-Expr ExprManager::mkVar(Type type, uint32_t flags) {
+Expr ExprManager::mkVar(Type type)
+{
   NodeManagerScope nms(d_nodeManager);
   INC_STAT_VAR(type, false);
-  return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags));
+  return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
 }
 
 Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 1458101ca..f1386b84d 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -352,19 +352,13 @@ class CVC4_PUBLIC ExprManager {
   /** Make the type of sequence with the given parameterization. */
   SequenceType mkSequenceType(Type elementType) const;
 
-  /** Bits for use in mkSort() flags. */
-  enum {
-    SORT_FLAG_NONE = 0,
-    SORT_FLAG_PLACEHOLDER = 1
-  };/* enum */
-
   /** Make a new sort with the given name. */
-  SortType mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE) const;
+  SortType mkSort(const std::string& name, uint32_t flags) const;
 
   /** Make a sort constructor from a name and arity. */
   SortConstructorType mkSortConstructor(const std::string& name,
                                         size_t arity,
-                                        uint32_t flags = SORT_FLAG_NONE) const;
+                                        uint32_t flags) const;
 
   /**
    * Get the type of an expression.
@@ -374,13 +368,6 @@ class CVC4_PUBLIC ExprManager {
    */
   Type getType(Expr e, bool check = false);
 
-  /** Bits for use in mkVar() flags. */
-  enum {
-    VAR_FLAG_NONE = 0,
-    VAR_FLAG_GLOBAL = 1,
-    VAR_FLAG_DEFINED = 2
-  };/* enum */
-
   /**
    * Create a new, fresh variable.  This variable is guaranteed to be
    * distinct from every variable thus far in the ExprManager, even
@@ -390,33 +377,16 @@ class CVC4_PUBLIC ExprManager {
    *
    * @param name a name to associate to the fresh new variable
    * @param type the type for the new variable
-   * @param flags - VAR_FLAG_NONE - no flags;
-   * VAR_FLAG_GLOBAL - whether this variable is to be
-   * considered "global" or not.  Note that this information isn't
-   * used by the ExprManager, but is passed on to the ExprManager's
-   * event subscribers like the model-building service; if isGlobal
-   * is true, this newly-created variable will still available in
-   * models generated after an intervening pop.
-   * VAR_FLAG_DEFINED - if this is to be a "defined" symbol, e.g., for
-   * use with SmtEngine::defineFunction().  This keeps a declaration
-   * from being emitted in API dumps (since a subsequent definition is
-   * expected to be dumped instead).
    */
-  Expr mkVar(const std::string& name, Type type, uint32_t flags = VAR_FLAG_NONE);
+  Expr mkVar(const std::string& name, Type type);
 
   /**
    * Create a (nameless) new, fresh variable.  This variable is guaranteed
    * to be distinct from every variable thus far in the ExprManager.
    *
    * @param type the type for the new variable
-   * @param flags - VAR_FLAG_GLOBAL - whether this variable is to be considered "global"
-   * or not.  Note that this information isn't used by the ExprManager,
-   * but is passed on to the ExprManager's event subscribers like the
-   * model-building service; if isGlobal is true, this newly-created
-   * variable will still available in models generated after an
-   * intervening pop.
-   */
-  Expr mkVar(Type type, uint32_t flags = VAR_FLAG_NONE);
+   */
+  Expr mkVar(Type type);
 
   /**
    * Create a new, fresh variable for use in a binder expression
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index f9a743cf6..67ceaf89c 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -208,16 +208,11 @@ private:
             NodeManagerScope to_nms(to_nm);
             to_e = nn.toExpr();
           } else if(n.getKind() == kind::VARIABLE) {
-            bool isGlobal;
-            Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal);
-
             // Temporarily set the node manager to nullptr; this gets around
             // a check that mkVar isn't called internally
             NodeManagerScope nullScope(nullptr);
             to_e = d_to->mkVar(name,
-                               type,
-                               isGlobal ? ExprManager::VAR_FLAG_GLOBAL
-                                        : d_flags);  // FIXME thread safety
+                               type);  // FIXME thread safety
           } else if(n.getKind() == kind::SKOLEM) {
             // skolems are only available at the Node level (not the Expr level)
             TypeNode typeNode = TypeNode::fromType(type);
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 540e02979..59afec4a6 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -904,27 +904,26 @@ TypeNode NodeManager::mkSortConstructor(const std::string& name,
   return type;
 }
 
-Node NodeManager::mkVar(const std::string& name, const TypeNode& type, uint32_t flags) {
+Node NodeManager::mkVar(const std::string& name, const TypeNode& type)
+{
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
   setAttribute(n, expr::VarNameAttr(), name);
-  setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(n, flags);
+    (*i)->nmNotifyNewVar(n);
   }
   return n;
 }
 
-Node* NodeManager::mkVarPtr(const std::string& name,
-                            const TypeNode& type, uint32_t flags) {
+Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type)
+{
   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
   setAttribute(*n, TypeAttr(), type);
   setAttribute(*n, TypeCheckedAttr(), true);
   setAttribute(*n, expr::VarNameAttr(), name);
-  setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(*n, flags);
+    (*i)->nmNotifyNewVar(*n);
   }
   return n;
 }
@@ -1048,24 +1047,24 @@ Node NodeManager::mkChain(Kind kind, const std::vector<Node>& children)
   return mkNode(kind::AND, cchildren);
 }
 
-Node NodeManager::mkVar(const TypeNode& type, uint32_t flags) {
+Node NodeManager::mkVar(const TypeNode& type)
+{
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
-  setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(n, flags);
+    (*i)->nmNotifyNewVar(n);
   }
   return n;
 }
 
-Node* NodeManager::mkVarPtr(const TypeNode& type, uint32_t flags) {
+Node* NodeManager::mkVarPtr(const TypeNode& type)
+{
   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
   setAttribute(*n, TypeAttr(), type);
   setAttribute(*n, TypeCheckedAttr(), true);
-  setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(*n, flags);
+    (*i)->nmNotifyNewVar(*n);
   }
   return n;
 }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1e70dd766..89cd61e09 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -71,7 +71,7 @@ class NodeManagerListener {
                                     uint32_t flags)
   {
   }
-  virtual void nmNotifyNewVar(TNode n, uint32_t flags) {}
+  virtual void nmNotifyNewVar(TNode n) {}
   virtual void nmNotifyNewSkolem(TNode n, const std::string& comment,
                                  uint32_t flags) {}
   /**
@@ -89,8 +89,8 @@ class NodeManager {
   friend class expr::TypeChecker;
 
   // friends so they can access mkVar() here, which is private
-  friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags);
-  friend Expr ExprManager::mkVar(Type, uint32_t flags);
+  friend Expr ExprManager::mkVar(const std::string&, Type);
+  friend Expr ExprManager::mkVar(Type);
 
   /** Predicate for use with STL algorithms */
   struct NodeValueReferenceCountNonZero {
@@ -373,12 +373,12 @@ class NodeManager {
    * version of this is private to avoid internal uses of mkVar() from
    * within CVC4.  Such uses should employ mkSkolem() instead.
    */
-  Node mkVar(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-  Node* mkVarPtr(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
+  Node mkVar(const std::string& name, const TypeNode& type);
+  Node* mkVarPtr(const std::string& name, const TypeNode& type);
 
   /** Create a variable with the given type. */
-  Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-  Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
+  Node mkVar(const TypeNode& type);
+  Node* mkVarPtr(const TypeNode& type);
 
  public:
 
@@ -1032,21 +1032,28 @@ class NodeManager {
   /** Make a type representing a tester with given parameterization */
   inline TypeNode mkTesterType(TypeNode domain);
 
+  /** Bits for use in mkSort() flags. */
+  enum
+  {
+    SORT_FLAG_NONE = 0,
+    SORT_FLAG_PLACEHOLDER = 1
+  }; /* enum */
+
   /** Make a new (anonymous) sort of arity 0. */
-  TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE);
+  TypeNode mkSort(uint32_t flags = SORT_FLAG_NONE);
 
   /** Make a new sort with the given name of arity 0. */
-  TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE);
+  TypeNode mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE);
 
   /** Make a new sort by parameterizing the given sort constructor. */
   TypeNode mkSort(TypeNode constructor,
                   const std::vector<TypeNode>& children,
-                  uint32_t flags = ExprManager::SORT_FLAG_NONE);
+                  uint32_t flags = SORT_FLAG_NONE);
 
   /** Make a new sort with the given name and arity. */
   TypeNode mkSortConstructor(const std::string& name,
                              size_t arity,
-                             uint32_t flags = ExprManager::SORT_FLAG_NONE);
+                             uint32_t flags = SORT_FLAG_NONE);
 
   /**
    * Get the type for the given node and optionally do type checking.
diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h
index ba8df6fd0..ba19a3bbb 100644
--- a/src/expr/node_manager_attributes.h
+++ b/src/expr/node_manager_attributes.h
@@ -26,14 +26,12 @@ namespace expr {
 // TODO: hide this attribute behind a NodeManager interface.
 namespace attr {
   struct VarNameTag { };
-  struct GlobalVarTag { };
   struct SortArityTag { };
   struct TypeTag { };
   struct TypeCheckedTag { };
 }/* CVC4::expr::attr namespace */
 
 typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
-typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr;
 typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
 typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr;
 typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr;
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 0bb386697..23a17c939 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -156,7 +156,7 @@ MipLibTrick::~MipLibTrick()
   }
 }
 
-void MipLibTrick::nmNotifyNewVar(TNode n, uint32_t flags)
+void MipLibTrick::nmNotifyNewVar(TNode n)
 {
   if (n.getType().isBoolean())
   {
diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h
index d3cf9da53..f7be87f18 100644
--- a/src/preprocessing/passes/miplib_trick.h
+++ b/src/preprocessing/passes/miplib_trick.h
@@ -32,7 +32,7 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener
   ~MipLibTrick();
 
   // NodeManagerListener callbacks to collect d_boolVars.
-  void nmNotifyNewVar(TNode n, uint32_t flags) override;
+  void nmNotifyNewVar(TNode n) override;
   void nmNotifyNewSkolem(TNode n,
                          const std::string& comment,
                          uint32_t flags) override;
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index ecf1e281d..7b54fee61 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -252,7 +252,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     std::stringstream ss;
     ss << "T" << i;
     std::string tname = ss.str();
-    TypeNode tnu = nm->mkSort(tname, ExprManager::SORT_FLAG_PLACEHOLDER);
+    TypeNode tnu = nm->mkSort(tname, NodeManager::SORT_FLAG_PLACEHOLDER);
     cterm_to_utype[ct] = tnu;
     unres.insert(tnu);
     sdts.push_back(SygusDatatype(tname));
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index ea0d1b267..ab792f6fe 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -20,7 +20,6 @@
 #include <typeinfo>
 #include <vector>
 
-#include "expr/expr.h"                     // for ExprSetDepth etc..
 #include "expr/node_manager_attributes.h"  // for VarNameAttr
 #include "expr/node_visitor.h"
 #include "options/language.h"  // for LANG_AST
diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp
index 706c2e886..77f5f7d0d 100644
--- a/src/smt/dump_manager.cpp
+++ b/src/smt/dump_manager.cpp
@@ -49,12 +49,9 @@ void DumpManager::resetAssertions()
   // currently, do nothing
 }
 
-void DumpManager::addToModelCommandAndDump(const NodeCommand& c,
-                                           uint32_t flags,
-                                           bool userVisible,
-                                           const char* dumpTag)
+void DumpManager::addToDump(const NodeCommand& c, const char* dumpTag)
 {
-  Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << std::endl;
+  Trace("smt") << "SMT addToDump(" << c << ")" << std::endl;
   if (Dump.isOn(dumpTag))
   {
     if (d_fullyInited)
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index 3238d3a8d..192bb2324 100644
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -49,13 +49,10 @@ class DumpManager
    */
   void resetAssertions();
   /**
-   * Add to Model command.  This is used for recording a command
-   * that should be reported during a get-model call.
+   * Add to dump command.  This is used for recording a command
+   * that should be reported via the dumpTag trace.
    */
-  void addToModelCommandAndDump(const NodeCommand& c,
-                                uint32_t flags = 0,
-                                bool userVisible = true,
-                                const char* dumpTag = "declarations");
+  void addToDump(const NodeCommand& c, const char* dumpTag = "declarations");
 
   /**
    * Set that function f should print in the model if and only if p is true.
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 356cfa8a6..0347a24ef 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -45,9 +45,9 @@ SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm,
 void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags)
 {
   DeclareTypeNodeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn);
-  if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
+  if ((flags & NodeManager::SORT_FLAG_PLACEHOLDER) == 0)
   {
-    d_dm.addToModelCommandAndDump(c, flags);
+    d_dm.addToDump(c);
   }
 }
 
@@ -57,9 +57,9 @@ void SmtNodeManagerListener::nmNotifyNewSortConstructor(TypeNode tn,
   DeclareTypeNodeCommand c(tn.getAttribute(expr::VarNameAttr()),
                            tn.getAttribute(expr::SortArityAttr()),
                            tn);
-  if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
+  if ((flags & NodeManager::SORT_FLAG_PLACEHOLDER) == 0)
   {
-    d_dm.addToModelCommandAndDump(c);
+    d_dm.addToDump(c);
   }
 }
 
@@ -76,18 +76,15 @@ void SmtNodeManagerListener::nmNotifyNewDatatypes(
       }
     }
     DeclareDatatypeNodeCommand c(dtts);
-    d_dm.addToModelCommandAndDump(c);
+    d_dm.addToDump(c);
   }
 }
 
-void SmtNodeManagerListener::nmNotifyNewVar(TNode n, uint32_t flags)
+void SmtNodeManagerListener::nmNotifyNewVar(TNode n)
 {
   DeclareFunctionNodeCommand c(
       n.getAttribute(expr::VarNameAttr()), n, n.getType());
-  if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0)
-  {
-    d_dm.addToModelCommandAndDump(c, flags);
-  }
+  d_dm.addToDump(c);
 }
 
 void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n,
@@ -101,10 +98,7 @@ void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n,
     d_outMgr.getPrinter().toStreamCmdComment(d_outMgr.getDumpOut(),
                                              id + " is " + comment);
   }
-  if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0)
-  {
-    d_dm.addToModelCommandAndDump(c, flags, false, "skolems");
-  }
+  d_dm.addToDump(c, "skolems");
 }
 
 }  // namespace smt
diff --git a/src/smt/listeners.h b/src/smt/listeners.h
index ce174e872..d586dfe75 100644
--- a/src/smt/listeners.h
+++ b/src/smt/listeners.h
@@ -59,7 +59,7 @@ class SmtNodeManagerListener : public NodeManagerListener
   void nmNotifyNewDatatypes(const std::vector<TypeNode>& dtts,
                             uint32_t flags) override;
   /** Notify when new variable is created */
-  void nmNotifyNewVar(TNode n, uint32_t flags) override;
+  void nmNotifyNewVar(TNode n) override;
   /** Notify when new skolem is created */
   void nmNotifyNewSkolem(TNode n,
                          const std::string& comment,
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d89b6e802..6f775f6b5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -675,8 +675,7 @@ void SmtEngine::defineFunction(Node func,
   }
 
   DefineFunctionNodeCommand nc(ss.str(), func, nFormals, formula);
-  d_dumpm->addToModelCommandAndDump(
-      nc, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
+  d_dumpm->addToDump(nc, "declarations");
 
   // type check body
   debugCheckFunctionBody(formula, formals, func);
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 1b251f8e0..6bb473f87 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -21,7 +21,6 @@
 
 #include "expr/node.h"
 #include "expr/type_node.h"
-#include "expr/expr.h"
 #include "theory/rewriter.h"
 #include "theory/builtin/theory_builtin_rewriter.h" // for array and lambda representation
 
diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index f99f58969..60bf36139 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -670,7 +670,7 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt,
   std::stringstream ssutn0;
   ssutn0 << sdtd.getName() << "_s";
   TypeNode abdTNew =
-      nm->mkSort(ssutn0.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
+      nm->mkSort(ssutn0.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
   unres.insert(abdTNew);
   dtProcessed[sdt] = abdTNew;
 
@@ -712,7 +712,7 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt,
             std::stringstream ssutn;
             ssutn << argt.getDType().getName() << "_s";
             argtNew =
-                nm->mkSort(ssutn.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
+                nm->mkSort(ssutn.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
             Trace("dtsygus-gen-debug") << "    ...unresolved type " << argtNew
                                        << " for " << argt << std::endl;
             unres.insert(argtNew);
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 9c98d6608..4588e8952 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -464,7 +464,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
       Node bvl;
       std::string veName("_virtual_enum_grammar");
       SygusDatatype sdt(veName);
-      TypeNode u = nm->mkSort(veName, ExprManager::SORT_FLAG_PLACEHOLDER);
+      TypeNode u = nm->mkSort(veName, NodeManager::SORT_FLAG_PLACEHOLDER);
       std::set<TypeNode> unresolvedTypes;
       unresolvedTypes.insert(u);
       std::vector<TypeNode> cargsEmpty;
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 23d924581..00a72cbcb 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -377,7 +377,8 @@ Node CegGrammarConstructor::convertToEmbedding(Node n)
 TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name,
                                                  std::set<TypeNode>& unres)
 {
-  TypeNode unresolved = NodeManager::currentNM()->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER);
+  TypeNode unresolved = NodeManager::currentNM()->mkSort(
+      name, NodeManager::SORT_FLAG_PLACEHOLDER);
   unres.insert(unresolved);
   return unresolved;
 }
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index bbb16dfd5..644d50a95 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -58,7 +58,7 @@ bool OpPosTrie::getOrMakeType(TypeNode tn,
       ss << "_" << std::to_string(op_pos[i]);
     }
     d_unres_tn = NodeManager::currentNM()->mkSort(
-        ss.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
+        ss.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
     Trace("sygus-grammar-normalize-trie")
         << "\tCreating type " << d_unres_tn << "\n";
     unres_tn = d_unres_tn;