Introduce an internal version of Commands. (#4988)

This PR is a step towards the migration of Commands to the public API. Node versions of some Commands are introduced for internal use (as necessary). The DumpManager is refactored to make use of those commands.

9 files changed, 392 insertions, 31 deletions

diff --git a/src/smt/dump.h b/src/smt/dump.h
index 050935422..4c0efeb6e 100644
--- a/src/smt/dump.h
+++ b/src/smt/dump.h
@@ -21,6 +21,7 @@
 
 #include "base/output.h"
 #include "smt/command.h"
+#include "smt/node_command.h"
 
 namespace CVC4 {
 
@@ -40,6 +41,20 @@ class CVC4_PUBLIC CVC4dumpstream
     return *this;
   }
 
+  /** A convenience function for dumping internal commands.
+   *
+   * Since Commands are now part of the public API, internal code should use
+   * NodeCommands and this function (instead of the one above) to dump them.
+   */
+  CVC4dumpstream& operator<<(const NodeCommand& nc)
+  {
+    if (d_os != nullptr)
+    {
+      (*d_os) << nc << std::endl;
+    }
+    return *this;
+  }
+
  private:
   std::ostream* d_os;
 }; /* class CVC4dumpstream */
@@ -56,6 +71,7 @@ class CVC4_PUBLIC CVC4dumpstream
   CVC4dumpstream() {}
   CVC4dumpstream(std::ostream& os) {}
   CVC4dumpstream& operator<<(const Command& c) { return *this; }
+  CVC4dumpstream& operator<<(const NodeCommand& nc) { return *this; }
 }; /* class CVC4dumpstream */
 
 #endif /* CVC4_DUMPING && !CVC4_MUZZLE */
diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp
index d5fd65c4c..033be405f 100644
--- a/src/smt/dump_manager.cpp
+++ b/src/smt/dump_manager.cpp
@@ -51,7 +51,7 @@ void DumpManager::finishInit()
 
 void DumpManager::resetAssertions() { d_modelGlobalCommands.clear(); }
 
-void DumpManager::addToModelCommandAndDump(const Command& c,
+void DumpManager::addToModelCommandAndDump(const NodeCommand& c,
                                            uint32_t flags,
                                            bool userVisible,
                                            const char* dumpTag)
@@ -70,14 +70,14 @@ void DumpManager::addToModelCommandAndDump(const Command& c,
   {
     if (flags & ExprManager::VAR_FLAG_GLOBAL)
     {
-      d_modelGlobalCommands.push_back(std::unique_ptr<Command>(c.clone()));
+      d_modelGlobalCommands.push_back(std::unique_ptr<NodeCommand>(c.clone()));
     }
     else
     {
-      Command* cc = c.clone();
+      NodeCommand* cc = c.clone();
       d_modelCommands.push_back(cc);
       // also remember for memory management purposes
-      d_modelCommandsAlloc.push_back(std::unique_ptr<Command>(cc));
+      d_modelCommandsAlloc.push_back(std::unique_ptr<NodeCommand>(cc));
     }
   }
   if (Dump.isOn(dumpTag))
@@ -88,7 +88,7 @@ void DumpManager::addToModelCommandAndDump(const Command& c,
     }
     else
     {
-      d_dumpCommands.push_back(std::unique_ptr<Command>(c.clone()));
+      d_dumpCommands.push_back(std::unique_ptr<NodeCommand>(c.clone()));
     }
   }
 }
@@ -96,7 +96,7 @@ void DumpManager::addToModelCommandAndDump(const Command& c,
 void DumpManager::setPrintFuncInModel(Node f, bool p)
 {
   Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
-  for (std::unique_ptr<Command>& c : d_modelGlobalCommands)
+  for (std::unique_ptr<NodeCommand>& c : d_modelGlobalCommands)
   {
     DeclareFunctionCommand* dfc =
         dynamic_cast<DeclareFunctionCommand*>(c.get());
@@ -109,7 +109,7 @@ void DumpManager::setPrintFuncInModel(Node f, bool p)
       }
     }
   }
-  for (Command* c : d_modelCommands)
+  for (NodeCommand* c : d_modelCommands)
   {
     DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
     if (dfc != NULL)
@@ -128,7 +128,7 @@ size_t DumpManager::getNumModelCommands() const
   return d_modelCommands.size() + d_modelGlobalCommands.size();
 }
 
-const Command* DumpManager::getModelCommand(size_t i) const
+const NodeCommand* DumpManager::getModelCommand(size_t i) const
 {
   Assert(i < getNumModelCommands());
   // index the global commands first, then the locals
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index 6f2ee37a1..2ce0570e4 100644
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -22,7 +22,7 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "smt/command.h"
+#include "smt/node_command.h"
 
 namespace CVC4 {
 namespace smt {
@@ -36,7 +36,7 @@ namespace smt {
  */
 class DumpManager
 {
-  typedef context::CDList<Command*> CommandList;
+  typedef context::CDList<NodeCommand*> CommandList;
 
  public:
   DumpManager(context::UserContext* u);
@@ -54,7 +54,7 @@ class DumpManager
    * Add to Model command.  This is used for recording a command
    * that should be reported during a get-model call.
    */
-  void addToModelCommandAndDump(const Command& c,
+  void addToModelCommandAndDump(const NodeCommand& c,
                                 uint32_t flags = 0,
                                 bool userVisible = true,
                                 const char* dumpTag = "declarations");
@@ -66,7 +66,7 @@ class DumpManager
   /** get number of commands to report in a model */
   size_t getNumModelCommands() const;
   /** get model command at index i */
-  const Command* getModelCommand(size_t i) const;
+  const NodeCommand* getModelCommand(size_t i) const;
 
  private:
   /** Fully inited */
@@ -77,7 +77,7 @@ class DumpManager
    * regardless of push/pop).  Only maintained if produce-models option
    * is on.
    */
-  std::vector<std::unique_ptr<Command>> d_modelGlobalCommands;
+  std::vector<std::unique_ptr<NodeCommand>> d_modelGlobalCommands;
 
   /**
    * A list of commands that should be in the Model locally (i.e.,
@@ -89,7 +89,7 @@ class DumpManager
    * A list of model commands allocated to d_modelCommands at any time. This
    * is maintained for memory management purposes.
    */
-  std::vector<std::unique_ptr<Command>> d_modelCommandsAlloc;
+  std::vector<std::unique_ptr<NodeCommand>> d_modelCommandsAlloc;
 
   /**
    * A vector of declaration commands waiting to be dumped out.
@@ -97,7 +97,7 @@ class DumpManager
    * This ensures the declarations come after the set-logic and
    * any necessary set-option commands are dumped.
    */
-  std::vector<std::unique_ptr<Command>> d_dumpCommands;
+  std::vector<std::unique_ptr<NodeCommand>> d_dumpCommands;
 };
 
 }  // namespace smt
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 539d6ba2f..52ddcf156 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -18,7 +18,7 @@
 #include "expr/expr.h"
 #include "expr/node_manager_attributes.h"
 #include "options/smt_options.h"
-#include "smt/command.h"
+#include "smt/node_command.h"
 #include "smt/dump.h"
 #include "smt/dump_manager.h"
 #include "smt/smt_engine.h"
@@ -40,7 +40,7 @@ SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm) : d_dm(dm) {}
 
 void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags)
 {
-  DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn.toType());
+  DeclareTypeNodeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn);
   if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
   {
     d_dm.addToModelCommandAndDump(c, flags);
@@ -50,9 +50,9 @@ void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags)
 void SmtNodeManagerListener::nmNotifyNewSortConstructor(TypeNode tn,
                                                         uint32_t flags)
 {
-  DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
-                       tn.getAttribute(expr::SortArityAttr()),
-                       tn.toType());
+  DeclareTypeNodeCommand c(tn.getAttribute(expr::VarNameAttr()),
+                           tn.getAttribute(expr::SortArityAttr()),
+                           tn);
   if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
   {
     d_dm.addToModelCommandAndDump(c);
@@ -68,17 +68,16 @@ void SmtNodeManagerListener::nmNotifyNewDatatypes(
     for (const TypeNode& dt : dtts)
     {
       Assert(dt.isDatatype());
-      types.push_back(dt.toType());
     }
-    DatatypeDeclarationCommand c(types);
+    DeclareDatatypeNodeCommand c(dtts);
     d_dm.addToModelCommandAndDump(c);
   }
 }
 
 void SmtNodeManagerListener::nmNotifyNewVar(TNode n, uint32_t flags)
 {
-  DeclareFunctionCommand c(
-      n.getAttribute(expr::VarNameAttr()), n.toExpr(), n.getType().toType());
+  DeclareFunctionNodeCommand c(
+      n.getAttribute(expr::VarNameAttr()), n, n.getType());
   if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0)
   {
     d_dm.addToModelCommandAndDump(c, flags);
@@ -90,7 +89,7 @@ void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n,
                                                uint32_t flags)
 {
   std::string id = n.getAttribute(expr::VarNameAttr());
-  DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType());
+  DeclareFunctionNodeCommand c(id, n, n.getType());
   if (Dump.isOn("skolems") && comment != "")
   {
     Dump("skolems") << CommentCommand(id + " is " + comment);
diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index 7924698ff..a23b885ff 100644
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -19,8 +19,8 @@
 #include "expr/expr_iomanip.h"
 #include "options/base_options.h"
 #include "printer/printer.h"
-#include "smt/command.h"
 #include "smt/dump_manager.h"
+#include "smt/node_command.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 
@@ -42,7 +42,7 @@ size_t Model::getNumCommands() const
   return d_smt.getDumpManager()->getNumModelCommands();
 }
 
-const Command* Model::getCommand(size_t i) const
+const NodeCommand* Model::getCommand(size_t i) const
 {
   return d_smt.getDumpManager()->getModelCommand(i);
 }
diff --git a/src/smt/model.h b/src/smt/model.h
index 8f4409b07..4c28704c3 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -25,7 +25,7 @@
 
 namespace CVC4 {
 
-class Command;
+class NodeCommand;
 class SmtEngine;
 class Model;
 
@@ -48,7 +48,7 @@ class Model {
   /** get number of commands to report */
   size_t getNumCommands() const;
   /** get command */
-  const Command* getCommand(size_t i) const;
+  const NodeCommand* getCommand(size_t i) const;
   /** get the smt engine that this model is hooked up to */
   SmtEngine* getSmtEngine() { return &d_smt; }
   /** get the smt engine (as a pointer-to-const) that this model is hooked up to */
diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp
new file mode 100644
index 000000000..265b35b3e
--- /dev/null
+++ b/src/smt/node_command.cpp
@@ -0,0 +1,180 @@
+/*********************                                                        */
+/*! \file node_command.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of NodeCommand functions.
+ **
+ ** Implementation of NodeCommand functions.
+ **/
+
+#include "smt/node_command.h"
+
+#include "printer/printer.h"
+
+namespace CVC4 {
+
+/* -------------------------------------------------------------------------- */
+/* class NodeCommand                                                          */
+/* -------------------------------------------------------------------------- */
+
+NodeCommand::~NodeCommand() {}
+
+std::string NodeCommand::toString() const
+{
+  std::stringstream ss;
+  toStream(ss);
+  return ss.str();
+}
+
+std::ostream& operator<<(std::ostream& out, const NodeCommand& nc)
+{
+  nc.toStream(out,
+              Node::setdepth::getDepth(out),
+              Node::printtypes::getPrintTypes(out),
+              Node::dag::getDag(out),
+              Node::setlanguage::getLanguage(out));
+  return out;
+}
+
+/* -------------------------------------------------------------------------- */
+/* class DeclareFunctionNodeCommand                                           */
+/* -------------------------------------------------------------------------- */
+
+DeclareFunctionNodeCommand::DeclareFunctionNodeCommand(const std::string& id,
+                                                       Node expr,
+                                                       TypeNode type)
+    : d_id(id),
+      d_fun(expr),
+      d_type(type),
+      d_printInModel(true),
+      d_printInModelSetByUser(false)
+{
+}
+
+void DeclareFunctionNodeCommand::toStream(std::ostream& out,
+                                          int toDepth,
+                                          bool types,
+                                          size_t dag,
+                                          OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDeclareFunction(out, d_id, d_type);
+}
+
+NodeCommand* DeclareFunctionNodeCommand::clone() const
+{
+  return new DeclareFunctionNodeCommand(d_id, d_fun, d_type);
+}
+
+const Node& DeclareFunctionNodeCommand::getFunction() const { return d_fun; }
+
+bool DeclareFunctionNodeCommand::getPrintInModel() const
+{
+  return d_printInModel;
+}
+
+bool DeclareFunctionNodeCommand::getPrintInModelSetByUser() const
+{
+  return d_printInModelSetByUser;
+}
+
+void DeclareFunctionNodeCommand::setPrintInModel(bool p)
+{
+  d_printInModel = p;
+  d_printInModelSetByUser = true;
+}
+
+/* -------------------------------------------------------------------------- */
+/* class DeclareTypeNodeCommand                                               */
+/* -------------------------------------------------------------------------- */
+
+DeclareTypeNodeCommand::DeclareTypeNodeCommand(const std::string& id,
+                                               size_t arity,
+                                               TypeNode type)
+    : d_id(id), d_arity(arity), d_type(type)
+{
+}
+
+void DeclareTypeNodeCommand::toStream(std::ostream& out,
+                                      int toDepth,
+                                      bool types,
+                                      size_t dag,
+                                      OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDeclareType(
+      out, d_id, d_arity, d_type);
+}
+
+NodeCommand* DeclareTypeNodeCommand::clone() const
+{
+  return new DeclareTypeNodeCommand(d_id, d_arity, d_type);
+}
+
+const std::string DeclareTypeNodeCommand::getSymbol() const { return d_id; }
+
+const TypeNode& DeclareTypeNodeCommand::getType() const { return d_type; }
+
+/* -------------------------------------------------------------------------- */
+/* class DeclareDatatypeNodeCommand                                           */
+/* -------------------------------------------------------------------------- */
+
+DeclareDatatypeNodeCommand::DeclareDatatypeNodeCommand(
+    const std::vector<TypeNode>& datatypes)
+    : d_datatypes(datatypes)
+{
+}
+
+void DeclareDatatypeNodeCommand::toStream(std::ostream& out,
+                                          int toDepth,
+                                          bool types,
+                                          size_t dag,
+                                          OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(out,
+                                                                d_datatypes);
+}
+
+NodeCommand* DeclareDatatypeNodeCommand::clone() const
+{
+  return new DeclareDatatypeNodeCommand(d_datatypes);
+}
+
+/* -------------------------------------------------------------------------- */
+/* class DefineFunctionNodeCommand                                            */
+/* -------------------------------------------------------------------------- */
+
+DefineFunctionNodeCommand::DefineFunctionNodeCommand(
+    const std::string& id,
+    Node fun,
+    const std::vector<Node>& formals,
+    Node formula)
+    : d_id(id), d_fun(fun), d_formals(formals), d_formula(formula)
+{
+}
+
+void DefineFunctionNodeCommand::toStream(std::ostream& out,
+                                         int toDepth,
+                                         bool types,
+                                         size_t dag,
+                                         OutputLanguage language) const
+{
+  Printer::getPrinter(language)->toStreamCmdDefineFunction(
+      out,
+      d_fun.toString(),
+      d_formals,
+      d_fun.getType().getRangeType(),
+      d_formula);
+}
+
+NodeCommand* DefineFunctionNodeCommand::clone() const
+{
+  return new DefineFunctionNodeCommand(d_id, d_fun, d_formals, d_formula);
+}
+
+}  // namespace CVC4
diff --git a/src/smt/node_command.h b/src/smt/node_command.h
new file mode 100644
index 000000000..2ca166bb6
--- /dev/null
+++ b/src/smt/node_command.h
@@ -0,0 +1,157 @@
+/*********************                                                        */
+/*! \file node_command.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Datastructures used for printing commands internally.
+ **
+ ** Datastructures used for printing commands internally.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__NODE_COMMAND_H
+#define CVC4__SMT__NODE_COMMAND_H
+
+#include <string>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "options/language.h"
+
+namespace CVC4 {
+
+/**
+ * A node version of Command. DO NOT use this version unless there is a need
+ * to buffer commands for later use (e.g., printing models).
+ */
+class NodeCommand
+{
+ public:
+  /** Destructor */
+  virtual ~NodeCommand();
+
+  /** Print this NodeCommand to output stream */
+  virtual void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const = 0;
+
+  /** Get a string representation of this NodeCommand */
+  std::string toString() const;
+
+  /** Clone this NodeCommand (make a shallow copy). */
+  virtual NodeCommand* clone() const = 0;
+};
+
+std::ostream& operator<<(std::ostream& out, const NodeCommand& nc);
+
+/**
+ * Declare n-ary function symbol.
+ * SMT-LIB: ( declare-fun <id> ( <type.getArgTypes()> ) <type.getRangeType()> )
+ */
+class DeclareFunctionNodeCommand : public NodeCommand
+{
+ public:
+  DeclareFunctionNodeCommand(const std::string& id, Node fun, TypeNode type);
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
+  NodeCommand* clone() const override;
+  const Node& getFunction() const;
+  bool getPrintInModel() const;
+  bool getPrintInModelSetByUser() const;
+  void setPrintInModel(bool p);
+
+ private:
+  std::string d_id;
+  Node d_fun;
+  TypeNode d_type;
+  bool d_printInModel;
+  bool d_printInModelSetByUser;
+};
+
+/**
+ * Create datatype sort.
+ * SMT-LIB: ( declare-datatypes ( <datatype decls>{n+1} ) ( <datatypes>{n+1} ) )
+ */
+class DeclareDatatypeNodeCommand : public NodeCommand
+{
+ public:
+  DeclareDatatypeNodeCommand(const std::vector<TypeNode>& datatypes);
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
+  NodeCommand* clone() const override;
+
+ private:
+  std::vector<TypeNode> d_datatypes;
+};
+
+/**
+ * Declare uninterpreted sort.
+ * SMT-LIB: ( declare-sort <id> <arity> )
+ */
+class DeclareTypeNodeCommand : public NodeCommand
+{
+ public:
+  DeclareTypeNodeCommand(const std::string& id, size_t arity, TypeNode type);
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
+  NodeCommand* clone() const override;
+  const std::string getSymbol() const;
+  const TypeNode& getType() const;
+
+ private:
+  std::string d_id;
+  size_t d_arity;
+  TypeNode d_type;
+};
+
+/**
+ * Define n-ary function.
+ * SMT-LIB: ( define-fun <id> ( <formals> ) <fun.getType()> <formula> )
+ */
+class DefineFunctionNodeCommand : public NodeCommand
+{
+ public:
+  DefineFunctionNodeCommand(const std::string& id,
+                            Node fun,
+                            const std::vector<Node>& formals,
+                            Node formula);
+  void toStream(
+      std::ostream& out,
+      int toDepth = -1,
+      bool types = false,
+      size_t dag = 1,
+      OutputLanguage language = language::output::LANG_AUTO) const override;
+  NodeCommand* clone() const override;
+
+ private:
+  std::string d_id;
+  Node d_fun;
+  std::vector<Node> d_formals;
+  Node d_formula;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__NODE_COMMAND_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 531dbff0d..81d4f594d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -688,9 +688,18 @@ void SmtEngine::defineFunction(Expr func,
   ss << language::SetLanguage(
             language::SetLanguage::getLanguage(Dump.getStream()))
      << func;
-  DefineFunctionCommand c(ss.str(), func, formals, formula, global);
+  std::vector<Node> nFormals;
+  nFormals.reserve(formals.size());
+
+  for (const Expr& formal : formals)
+  {
+    nFormals.push_back(formal.getNode());
+  }
+
+  DefineFunctionNodeCommand nc(
+      ss.str(), func.getNode(), nFormals, formula.getNode());
   d_dumpm->addToModelCommandAndDump(
-      c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
+      nc, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
 
   // type check body
   debugCheckFunctionBody(formula, formals, func);