src/printer/ast/ast_printer.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Morgan Deters, Abdalrhman Mohamed, Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * The pretty-printer interface for the AST output language.
  14  */
  15 #include "printer/ast/ast_printer.h"
  16
  17 #include <iostream>
  18 #include <string>
  19 #include <typeinfo>
  20 #include <vector>
  21
  22 #include "expr/node_manager_attributes.h"  // for VarNameAttr
  23 #include "expr/node_visitor.h"
  24 #include "options/language.h"  // for LANG_AST
  25 #include "printer/let_binding.h"
  26 #include "smt/command.h"
  27
  28 using namespace std;
  29
  30 namespace cvc5 {
  31 namespace printer {
  32 namespace ast {
  33
  34 void AstPrinter::toStream(std::ostream& out,
  35                           TNode n,
  36                           int toDepth,
  37                           size_t dag) const
  38 {
  39   if(dag != 0) {
  40     LetBinding lbind(dag + 1);
  41     toStreamWithLetify(out, n, toDepth, &lbind);
  42   } else {
  43     toStream(out, n, toDepth);
  44   }
  45 }
  46
  47 void AstPrinter::toStream(std::ostream& out,
  48                           TNode n,
  49                           int toDepth,
  50                           LetBinding* lbind) const
  51 {
  52   // null
  53   if(n.getKind() == kind::NULL_EXPR) {
  54     out << "null";
  55     return;
  56   }
  57
  58   // variable
  59   if(n.getMetaKind() == kind::metakind::VARIABLE) {
  60     string s;
  61     if(n.getAttribute(expr::VarNameAttr(), s)) {
  62       out << s;
  63     } else {
  64       out << "var_" << n.getId();
  65     }
  66     return;
  67   }
  68
  69   out << '(' << n.getKind();
  70   if(n.getMetaKind() == kind::metakind::CONSTANT) {
  71     // constant
  72     out << ' ';
  73     n.constToStream(out);
  74   }
  75   else if (n.isClosure())
  76   {
  77     for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
  78     {
  79       // body is re-letified
  80       if (i == 1)
  81       {
  82         toStreamWithLetify(out, n[i], toDepth, lbind);
  83         continue;
  84       }
  85       toStream(out, n[i], toDepth < 0 ? toDepth : toDepth - 1, lbind);
  86     }
  87   }
  88   else
  89   {
  90     // operator
  91     if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
  92       out << ' ';
  93       if(toDepth != 0) {
  94         toStream(
  95             out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind);
  96       } else {
  97         out << "(...)";
  98       }
  99     }
 100     for(TNode::iterator i = n.begin(),
 101           iend = n.end();
 102         i != iend;
 103         ++i) {
 104       if(i != iend) {
 105         out << ' ';
 106       }
 107       if(toDepth != 0) {
 108         toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, lbind);
 109       } else {
 110         out << "(...)";
 111       }
 112     }
 113   }
 114   out << ')';
 115 }/* AstPrinter::toStream(TNode) */
 116
 117 template <class T>
 118 static bool tryToStream(std::ostream& out, const Command* c);
 119
 120 template <class T>
 121 static bool tryToStream(std::ostream& out, const CommandStatus* s);
 122
 123 void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const
 124 {
 125   if(tryToStream<CommandSuccess>(out, s) ||
 126      tryToStream<CommandFailure>(out, s) ||
 127      tryToStream<CommandUnsupported>(out, s) ||
 128      tryToStream<CommandInterrupted>(out, s)) {
 129     return;
 130   }
 131
 132   out << "ERROR: don't know how to print a CommandStatus of class: "
 133       << typeid(*s).name() << endl;
 134
 135 }/* AstPrinter::toStream(CommandStatus*) */
 136
 137 void AstPrinter::toStream(std::ostream& out, const smt::Model& m) const
 138 {
 139   out << "Model()";
 140 }
 141
 142 void AstPrinter::toStreamModelSort(std::ostream& out,
 143                                    TypeNode tn,
 144                                    const std::vector<Node>& elements) const
 145 {
 146   // shouldn't be called; only the non-Command* version above should be
 147   Unreachable();
 148 }
 149
 150 void AstPrinter::toStreamModelTerm(std::ostream& out,
 151                                    const Node& n,
 152                                    const Node& value) const
 153 {
 154   // shouldn't be called; only the non-Command* version above should be
 155   Unreachable();
 156 }
 157
 158 void AstPrinter::toStreamCmdEmpty(std::ostream& out,
 159                                   const std::string& name) const
 160 {
 161   out << "EmptyCommand(" << name << ')' << std::endl;
 162 }
 163
 164 void AstPrinter::toStreamCmdEcho(std::ostream& out,
 165                                  const std::string& output) const
 166 {
 167   out << "EchoCommand(" << output << ')' << std::endl;
 168 }
 169
 170 void AstPrinter::toStreamCmdAssert(std::ostream& out, Node n) const
 171 {
 172   out << "Assert(" << n << ')' << std::endl;
 173 }
 174
 175 void AstPrinter::toStreamCmdPush(std::ostream& out) const
 176 {
 177   out << "Push()" << std::endl;
 178 }
 179
 180 void AstPrinter::toStreamCmdPop(std::ostream& out) const {
 181   out << "Pop()" << std::endl;
 182 }
 183
 184 void AstPrinter::toStreamCmdCheckSat(std::ostream& out) const
 185 {
 186   out << "CheckSat()" << std::endl;
 187 }
 188
 189 void AstPrinter::toStreamCmdCheckSatAssuming(
 190     std::ostream& out, const std::vector<Node>& nodes) const
 191 {
 192   out << "CheckSatAssuming( << ";
 193   copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
 194   out << ">> )" << std::endl;
 195 }
 196
 197 void AstPrinter::toStreamCmdQuery(std::ostream& out, Node n) const
 198 {
 199   out << "Query(" << n << ')' << std::endl;
 200 }
 201
 202 void AstPrinter::toStreamCmdReset(std::ostream& out) const
 203 {
 204   out << "Reset()" << std::endl;
 205 }
 206
 207 void AstPrinter::toStreamCmdResetAssertions(std::ostream& out) const
 208 {
 209   out << "ResetAssertions()" << std::endl;
 210 }
 211
 212 void AstPrinter::toStreamCmdQuit(std::ostream& out) const
 213 {
 214   out << "Quit()" << std::endl;
 215 }
 216
 217 void AstPrinter::toStreamCmdDeclarationSequence(
 218     std::ostream& out, const std::vector<Command*>& sequence) const
 219 {
 220   out << "DeclarationSequence[" << endl;
 221   for (CommandSequence::const_iterator i = sequence.cbegin();
 222        i != sequence.cend();
 223        ++i)
 224   {
 225     out << *i << endl;
 226   }
 227   out << "]" << std::endl;
 228 }
 229
 230 void AstPrinter::toStreamCmdCommandSequence(
 231     std::ostream& out, const std::vector<Command*>& sequence) const
 232 {
 233   out << "CommandSequence[" << endl;
 234   for (CommandSequence::const_iterator i = sequence.cbegin();
 235        i != sequence.cend();
 236        ++i)
 237   {
 238     out << *i << endl;
 239   }
 240   out << "]" << std::endl;
 241 }
 242
 243 void AstPrinter::toStreamCmdDeclareFunction(std::ostream& out,
 244                                             const std::string& id,
 245                                             TypeNode type) const
 246 {
 247   out << "Declare(" << id << "," << type << ')' << std::endl;
 248 }
 249
 250 void AstPrinter::toStreamCmdDefineFunction(std::ostream& out,
 251                                            const std::string& id,
 252                                            const std::vector<Node>& formals,
 253                                            TypeNode range,
 254                                            Node formula) const
 255 {
 256   out << "DefineFunction( \"" << id << "\", [";
 257   if (formals.size() > 0)
 258   {
 259     copy(formals.begin(), formals.end() - 1, ostream_iterator<Node>(out, ", "));
 260     out << formals.back();
 261   }
 262   out << "], << " << formula << " >> )" << std::endl;
 263 }
 264
 265 void AstPrinter::toStreamCmdDeclareType(std::ostream& out,
 266                                         TypeNode type) const
 267 {
 268   out << "DeclareType(" << type << ')' << std::endl;
 269 }
 270
 271 void AstPrinter::toStreamCmdDefineType(std::ostream& out,
 272                                        const std::string& id,
 273                                        const std::vector<TypeNode>& params,
 274                                        TypeNode t) const
 275 {
 276   out << "DefineType(" << id << ",[";
 277   if (params.size() > 0)
 278   {
 279     copy(params.begin(),
 280          params.end() - 1,
 281          ostream_iterator<TypeNode>(out, ", "));
 282     out << params.back();
 283   }
 284   out << "]," << t << ')' << std::endl;
 285 }
 286
 287 void AstPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const
 288 {
 289   out << "Simplify( << " << n << " >> )" << std::endl;
 290 }
 291
 292 void AstPrinter::toStreamCmdGetValue(std::ostream& out,
 293                                      const std::vector<Node>& nodes) const
 294 {
 295   out << "GetValue( << ";
 296   copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, ", "));
 297   out << ">> )" << std::endl;
 298 }
 299
 300 void AstPrinter::toStreamCmdGetModel(std::ostream& out) const
 301 {
 302   out << "GetModel()" << std::endl;
 303 }
 304
 305 void AstPrinter::toStreamCmdGetAssignment(std::ostream& out) const
 306 {
 307   out << "GetAssignment()" << std::endl;
 308 }
 309
 310 void AstPrinter::toStreamCmdGetAssertions(std::ostream& out) const
 311 {
 312   out << "GetAssertions()" << std::endl;
 313 }
 314
 315 void AstPrinter::toStreamCmdGetProof(std::ostream& out) const
 316 {
 317   out << "GetProof()" << std::endl;
 318 }
 319
 320 void AstPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const
 321 {
 322   out << "GetUnsatCore()" << std::endl;
 323 }
 324
 325 void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
 326                                               const std::string& logic) const
 327 {
 328   out << "SetBenchmarkLogic(" << logic << ')' << std::endl;
 329 }
 330
 331 void AstPrinter::toStreamCmdSetInfo(std::ostream& out,
 332                                     const std::string& flag,
 333                                     const std::string& value) const
 334 {
 335   out << "SetInfo(" << flag << ", " << value << ')' << std::endl;
 336 }
 337
 338 void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
 339                                     const std::string& flag) const
 340 {
 341   out << "GetInfo(" << flag << ')' << std::endl;
 342 }
 343
 344 void AstPrinter::toStreamCmdSetOption(std::ostream& out,
 345                                       const std::string& flag,
 346                                       const std::string& value) const
 347 {
 348   out << "SetOption(" << flag << ", " << value << ')' << std::endl;
 349 }
 350
 351 void AstPrinter::toStreamCmdGetOption(std::ostream& out,
 352                                       const std::string& flag) const
 353 {
 354   out << "GetOption(" << flag << ')' << std::endl;
 355 }
 356
 357 void AstPrinter::toStreamCmdDatatypeDeclaration(
 358     std::ostream& out, const std::vector<TypeNode>& datatypes) const
 359 {
 360   out << "DatatypeDeclarationCommand([";
 361   for (const TypeNode& t : datatypes)
 362   {
 363     out << t << ";" << endl;
 364   }
 365   out << "])" << std::endl;
 366 }
 367
 368 void AstPrinter::toStreamWithLetify(std::ostream& out,
 369                                     Node n,
 370                                     int toDepth,
 371                                     LetBinding* lbind) const
 372 {
 373   if (lbind == nullptr)
 374   {
 375     toStream(out, n, toDepth);
 376     return;
 377   }
 378   std::stringstream cparen;
 379   std::vector<Node> letList;
 380   lbind->letify(n, letList);
 381   if (!letList.empty())
 382   {
 383     std::map<Node, uint32_t>::const_iterator it;
 384     out << "(LET ";
 385     cparen << ")";
 386     bool first = true;
 387     for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
 388     {
 389       if (!first)
 390       {
 391         out << ", ";
 392       }
 393       else
 394       {
 395         first = false;
 396       }
 397       Node nl = letList[i];
 398       uint32_t id = lbind->getId(nl);
 399       out << "_let_" << id << " := ";
 400       Node nlc = lbind->convert(nl, "_let_", false);
 401       toStream(out, nlc, toDepth, lbind);
 402     }
 403     out << " IN ";
 404   }
 405   Node nc = lbind->convert(n, "_let_");
 406   // print the body, passing the lbind object
 407   toStream(out, nc, toDepth, lbind);
 408   out << cparen.str();
 409   lbind->popScope();
 410 }
 411
 412 template <class T>
 413 static bool tryToStream(std::ostream& out, const Command* c)
 414 {
 415   if(typeid(*c) == typeid(T)) {
 416     toStream(out, dynamic_cast<const T*>(c));
 417     return true;
 418   }
 419   return false;
 420 }
 421
 422 static void toStream(std::ostream& out, const CommandSuccess* s)
 423 {
 424   if(Command::printsuccess::getPrintSuccess(out)) {
 425     out << "OK" << endl;
 426   }
 427 }
 428
 429 static void toStream(std::ostream& out, const CommandInterrupted* s)
 430 {
 431   out << "INTERRUPTED" << endl;
 432 }
 433
 434 static void toStream(std::ostream& out, const CommandUnsupported* s)
 435 {
 436   out << "UNSUPPORTED" << endl;
 437 }
 438
 439 static void toStream(std::ostream& out, const CommandFailure* s)
 440 {
 441   out << s->getMessage() << endl;
 442 }
 443
 444 template <class T>
 445 static bool tryToStream(std::ostream& out, const CommandStatus* s)
 446 {
 447   if(typeid(*s) == typeid(T)) {
 448     toStream(out, dynamic_cast<const T*>(s));
 449     return true;
 450   }
 451   return false;
 452 }
 453
 454 }  // namespace ast
 455 }  // namespace printer
 456 }  // namespace cvc5