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.

1 files changed, 180 insertions, 0 deletions

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