src/smt/node_command.cpp

   1 /*********************                                                        */
   2 /*! \file node_command.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Abdalrhman Mohamed
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of NodeCommand functions.
  13  **
  14  ** Implementation of NodeCommand functions.
  15  **/
  16
  17 #include "smt/node_command.h"
  18
  19 #include "printer/printer.h"
  20
  21 namespace CVC4 {
  22
  23 /* -------------------------------------------------------------------------- */
  24 /* class NodeCommand                                                          */
  25 /* -------------------------------------------------------------------------- */
  26
  27 NodeCommand::~NodeCommand() {}
  28
  29 std::string NodeCommand::toString() const
  30 {
  31   std::stringstream ss;
  32   toStream(ss);
  33   return ss.str();
  34 }
  35
  36 std::ostream& operator<<(std::ostream& out, const NodeCommand& nc)
  37 {
  38   nc.toStream(out,
  39               Node::setdepth::getDepth(out),
  40               Node::dag::getDag(out),
  41               Node::setlanguage::getLanguage(out));
  42   return out;
  43 }
  44
  45 /* -------------------------------------------------------------------------- */
  46 /* class DeclareFunctionNodeCommand                                           */
  47 /* -------------------------------------------------------------------------- */
  48
  49 DeclareFunctionNodeCommand::DeclareFunctionNodeCommand(const std::string& id,
  50                                                        Node expr,
  51                                                        TypeNode type)
  52     : d_id(id),
  53       d_fun(expr),
  54       d_type(type),
  55       d_printInModel(true),
  56       d_printInModelSetByUser(false)
  57 {
  58 }
  59
  60 void DeclareFunctionNodeCommand::toStream(std::ostream& out,
  61                                           int toDepth,
  62                                           size_t dag,
  63                                           OutputLanguage language) const
  64 {
  65   Printer::getPrinter(language)->toStreamCmdDeclareFunction(out, d_id, d_type);
  66 }
  67
  68 NodeCommand* DeclareFunctionNodeCommand::clone() const
  69 {
  70   return new DeclareFunctionNodeCommand(d_id, d_fun, d_type);
  71 }
  72
  73 const Node& DeclareFunctionNodeCommand::getFunction() const { return d_fun; }
  74
  75 bool DeclareFunctionNodeCommand::getPrintInModel() const
  76 {
  77   return d_printInModel;
  78 }
  79
  80 bool DeclareFunctionNodeCommand::getPrintInModelSetByUser() const
  81 {
  82   return d_printInModelSetByUser;
  83 }
  84
  85 void DeclareFunctionNodeCommand::setPrintInModel(bool p)
  86 {
  87   d_printInModel = p;
  88   d_printInModelSetByUser = true;
  89 }
  90
  91 /* -------------------------------------------------------------------------- */
  92 /* class DeclareTypeNodeCommand                                               */
  93 /* -------------------------------------------------------------------------- */
  94
  95 DeclareTypeNodeCommand::DeclareTypeNodeCommand(const std::string& id,
  96                                                size_t arity,
  97                                                TypeNode type)
  98     : d_id(id), d_arity(arity), d_type(type)
  99 {
 100 }
 101
 102 void DeclareTypeNodeCommand::toStream(std::ostream& out,
 103                                       int toDepth,
 104                                       size_t dag,
 105                                       OutputLanguage language) const
 106 {
 107   Printer::getPrinter(language)->toStreamCmdDeclareType(
 108       out, d_id, d_arity, d_type);
 109 }
 110
 111 NodeCommand* DeclareTypeNodeCommand::clone() const
 112 {
 113   return new DeclareTypeNodeCommand(d_id, d_arity, d_type);
 114 }
 115
 116 const std::string DeclareTypeNodeCommand::getSymbol() const { return d_id; }
 117
 118 const TypeNode& DeclareTypeNodeCommand::getType() const { return d_type; }
 119
 120 /* -------------------------------------------------------------------------- */
 121 /* class DeclareDatatypeNodeCommand                                           */
 122 /* -------------------------------------------------------------------------- */
 123
 124 DeclareDatatypeNodeCommand::DeclareDatatypeNodeCommand(
 125     const std::vector<TypeNode>& datatypes)
 126     : d_datatypes(datatypes)
 127 {
 128 }
 129
 130 void DeclareDatatypeNodeCommand::toStream(std::ostream& out,
 131                                           int toDepth,
 132                                           size_t dag,
 133                                           OutputLanguage language) const
 134 {
 135   Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(out,
 136                                                                 d_datatypes);
 137 }
 138
 139 NodeCommand* DeclareDatatypeNodeCommand::clone() const
 140 {
 141   return new DeclareDatatypeNodeCommand(d_datatypes);
 142 }
 143
 144 /* -------------------------------------------------------------------------- */
 145 /* class DefineFunctionNodeCommand                                            */
 146 /* -------------------------------------------------------------------------- */
 147
 148 DefineFunctionNodeCommand::DefineFunctionNodeCommand(
 149     const std::string& id,
 150     Node fun,
 151     const std::vector<Node>& formals,
 152     Node formula)
 153     : d_id(id), d_fun(fun), d_formals(formals), d_formula(formula)
 154 {
 155 }
 156
 157 void DefineFunctionNodeCommand::toStream(std::ostream& out,
 158                                          int toDepth,
 159                                          size_t dag,
 160                                          OutputLanguage language) const
 161 {
 162   TypeNode tn = d_fun.getType();
 163   bool hasRange =
 164       (tn.isFunction() || tn.isConstructor() || tn.isSelector());
 165   Printer::getPrinter(language)->toStreamCmdDefineFunction(
 166       out,
 167       d_fun.toString(),
 168       d_formals,
 169       (hasRange ? d_fun.getType().getRangeType() : tn),
 170       d_formula);
 171 }
 172
 173 NodeCommand* DefineFunctionNodeCommand::clone() const
 174 {
 175   return new DefineFunctionNodeCommand(d_id, d_fun, d_formals, d_formula);
 176 }
 177
 178 }  // namespace CVC4