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