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.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 621e3c1c004c3ddd9e8c523984e984713556ae16..e845bf876efb428033135098f4ef245ce2aaf8bd 100644 (file)
--- 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 37f0e25279e3ac0105d3ae6cc03481bda44122c3..43161fe04728a082747633135eb8a938442c8c08 100644 (file)
--- 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 1458101caa45f02f95faa500b6c187d50a253cff..f1386b84d971907e130d88f46fe43bd3e1244b50 100644 (file)
--- 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 f9a743cf6fe5d418031707f3851a853aacef4cdc..67ceaf89c278c8f6e8812a53b01b038c2ddaaf01 100644 (file)
--- 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 540e02979d8531511d3d5bd347ce64d3b9f8c083..59afec4a6883a122b52e7c1f748593c7007650a9 100644 (file)
--- 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 1e70dd7662240a5b0ce226b2d8a381dc6937c1d0..89cd61e09bafe135c84c005075faa5cbaee39fa7 100644 (file)
--- 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 ba8df6fd0a9d6d4354077e3660ce7f7608941a50..ba19a3bbb7ba3e3b4fb0adf018c0e6361696f75d 100644 (file)
--- 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 0bb386697cdfdd1522e0bccbcf068b424853f029..23a17c939f6d3267f0d5c1d59cf1f5414683c493 100644 (file)
--- 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 d3cf9da53cea21fe8f10dfb9a2d37b917dfecec8..f7be87f18d4b03fbcfaec5a69fd56c2d7eb59eed 100644 (file)
--- 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 ecf1e281da187770b7875e5416010c2387364e38..7b54fee6152e2dcfb5fb558abdd06ff30ebe5dbf 100644 (file)
--- 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 ea0d1b267db882aed9dbd6a4981de3e671fff1ef..ab792f6fe5ad9ad6dfe849ee657ef12c37ec110b 100644 (file)
--- 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 706c2e8861a511e59fae16ff5493c607b1df10ee..77f5f7d0d14ff4c18b12b731808c108a005223f4 100644 (file)
--- 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 3238d3a8d18b1159c0451f94a0f23c945ed78bdd..192bb232411203e2b4b6ded474f8f6a86d167bda 100644 (file)
--- 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 356cfa8a6e47b8beb34213bce8878553a9c814d1..0347a24efbd83ed89b13b06e294ffe8c01364954 100644 (file)
--- 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 ce174e87214a44ee96de6f82f1c990a8acc95760..d586dfe75816c24f0aec8c91b0814edb11b2d4e5 100644 (file)
--- 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 d89b6e802c0056f99e94bdcde05962771856903b..6f775f6b5a7f1671350a0d4518ec7e2c38a4d4dd 100644 (file)
--- 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 1b251f8e08ea7b17947e58b84f5dd3c0e9f187d7..6bb473f87931f0f09f3ebce4f96f98479a0d4c64 100644 (file)
--- 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 f99f589697e0d184d98605e35ed396238bfc08a6..60bf36139ce3f845dda961d3007ed31298fd5961 100644 (file)
--- 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 9c98d6608325b930ee7cac0e030364178088d7d7..4588e8952b4d12bbdee2b309f1a55fe23e86f588 100644 (file)
--- 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 23d9245818b9c37860012e1dd0d7c8859b907cb8..00a72cbcbc8b7bd1e4ae157d2966a84cb6ce5231 100644 (file)
--- 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 bbb16dfd5f4ad0cb3d7f575400fad5265aab2648..644d50a951d25d7532ddaeedbabf23bf1333c821 100644 (file)
--- 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;

diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h
index 9f5ffdf3e50cf2afa7366c09684a6483bec96d95..40a8b58dcdd9a00470358ae3c95ff9d9115d132d 100644 (file)
--- a/test/unit/expr/type_cardinality_public.h
+++ b/test/unit/expr/type_cardinality_public.h
@@ -203,7 +203,7 @@ class TypeCardinalityPublic : public CxxTest::TestSuite {
   }
 
   void testUndefinedSorts() {
-    Type foo = d_em->mkSort("foo");
+    Type foo = d_em->mkSort("foo", NodeManager::SORT_FLAG_NONE);
     // We've currently assigned them a specific Beth number, which
     // isn't really correct, but...
     TS_ASSERT( !foo.getCardinality().isFinite() );

diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index 5fe27752098d37b07368e9834c8495422feebe39..9909a8a7bb55f47253989e24bf0d5d1b518c0f1c 100644 (file)
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -243,10 +243,10 @@ class DatatypeBlack : public CxxTest::TestSuite {
      */
     std::set<TypeNode> unresolvedTypes;
     TypeNode unresList =
-        d_nm->mkSort("list", ExprManager::SORT_FLAG_PLACEHOLDER);
+        d_nm->mkSort("list", NodeManager::SORT_FLAG_PLACEHOLDER);
     unresolvedTypes.insert(unresList);
     TypeNode unresTree =
-        d_nm->mkSort("tree", ExprManager::SORT_FLAG_PLACEHOLDER);
+        d_nm->mkSort("tree", NodeManager::SORT_FLAG_PLACEHOLDER);
     unresolvedTypes.insert(unresTree);
 
     DType tree("tree");
@@ -309,10 +309,10 @@ class DatatypeBlack : public CxxTest::TestSuite {
   {
     std::set<TypeNode> unresolvedTypes;
     TypeNode unresList =
-        d_nm->mkSort("list", ExprManager::SORT_FLAG_PLACEHOLDER);
+        d_nm->mkSort("list", NodeManager::SORT_FLAG_PLACEHOLDER);
     unresolvedTypes.insert(unresList);
     TypeNode unresTree =
-        d_nm->mkSort("tree", ExprManager::SORT_FLAG_PLACEHOLDER);
+        d_nm->mkSort("tree", NodeManager::SORT_FLAG_PLACEHOLDER);
     unresolvedTypes.insert(unresTree);
 
     DType tree("tree");