src/printer/printer.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Abdalrhman Mohamed, Andrew Reynolds, Morgan Deters
   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  * Base of the pretty-printer interface.
  14  */
  15 #include "printer/printer.h"
  16
  17 #include <string>
  18
  19 #include "expr/node_manager_attributes.h"
  20 #include "options/base_options.h"
  21 #include "options/language.h"
  22 #include "printer/ast/ast_printer.h"
  23 #include "printer/smt2/smt2_printer.h"
  24 #include "printer/tptp/tptp_printer.h"
  25 #include "proof/unsat_core.h"
  26 #include "smt/command.h"
  27 #include "theory/quantifiers/instantiation_list.h"
  28
  29 using namespace std;
  30
  31 namespace cvc5 {
  32
  33 unique_ptr<Printer>
  34     Printer::d_printers[static_cast<size_t>(Language::LANG_MAX)];
  35
  36 unique_ptr<Printer> Printer::makePrinter(Language lang)
  37 {
  38   switch(lang) {
  39     case Language::LANG_SMTLIB_V2_6:
  40       return unique_ptr<Printer>(
  41           new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant));
  42
  43     case Language::LANG_TPTP:
  44       return unique_ptr<Printer>(new printer::tptp::TptpPrinter());
  45
  46     case Language::LANG_SYGUS_V2:
  47       // sygus version 2.0 does not have discrepancies with smt2, hence we use
  48       // a normal smt2 variant here.
  49       return unique_ptr<Printer>(
  50           new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant));
  51
  52     case Language::LANG_AST:
  53       return unique_ptr<Printer>(new printer::ast::AstPrinter());
  54
  55     default: Unhandled() << lang;
  56   }
  57 }
  58
  59 void Printer::toStream(std::ostream& out, const smt::Model& m) const
  60 {
  61   // print the declared sorts
  62   const std::vector<TypeNode>& dsorts = m.getDeclaredSorts();
  63   for (const TypeNode& tn : dsorts)
  64   {
  65     toStreamModelSort(out, tn, m.getDomainElements(tn));
  66   }
  67   // print the declared terms
  68   const std::vector<Node>& dterms = m.getDeclaredTerms();
  69   for (const Node& n : dterms)
  70   {
  71     toStreamModelTerm(out, n, m.getValue(n));
  72   }
  73 }
  74
  75 void Printer::toStreamUsing(Language lang,
  76                             std::ostream& out,
  77                             const smt::Model& m) const
  78 {
  79   getPrinter(lang)->toStream(out, m);
  80 }
  81
  82 void Printer::toStream(std::ostream& out, const UnsatCore& core) const
  83 {
  84   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
  85     toStreamCmdAssert(out, *i);
  86     out << std::endl;
  87   }
  88 }/* Printer::toStream(UnsatCore) */
  89
  90 void Printer::toStream(std::ostream& out, const InstantiationList& is) const
  91 {
  92   out << "(instantiations " << is.d_quant << std::endl;
  93   for (const InstantiationVec& i : is.d_inst)
  94   {
  95     out << "  ";
  96     if (i.d_id != theory::InferenceId::UNKNOWN)
  97     {
  98       out << "(! ";
  99     }
 100     out << "( ";
 101     for (const Node& n : i.d_vec)
 102     {
 103       out << n << " ";
 104     }
 105     out << ")";
 106     if (i.d_id != theory::InferenceId::UNKNOWN)
 107     {
 108       out << " :source " << i.d_id;
 109       if (!i.d_pfArg.isNull())
 110       {
 111         out << " " << i.d_pfArg;
 112       }
 113       out << ")";
 114     }
 115     out << std::endl;
 116   }
 117   out << ")" << std::endl;
 118 }
 119
 120 void Printer::toStream(std::ostream& out, const SkolemList& sks) const
 121 {
 122   out << "(skolem " << sks.d_quant << std::endl;
 123   out << "  ( ";
 124   for (const Node& n : sks.d_sks)
 125   {
 126     out << n << " ";
 127   }
 128   out << ")" << std::endl;
 129   out << ")" << std::endl;
 130 }
 131
 132 Printer* Printer::getPrinter(Language lang)
 133 {
 134   if (lang == Language::LANG_AUTO)
 135   {
 136     // Infer the language to use for output.
 137     //
 138     // Options can be null in certain circumstances (e.g., when printing
 139     // the singleton "null" expr.  So we guard against segfault
 140     if (not Options::isCurrentNull())
 141     {
 142       if (Options::current().base.outputLanguageWasSetByUser)
 143       {
 144         lang = options::outputLanguage();
 145       }
 146       if (lang == Language::LANG_AUTO
 147           && Options::current().base.inputLanguageWasSetByUser)
 148       {
 149         lang = options::inputLanguage();
 150       }
 151     }
 152     if (lang == Language::LANG_AUTO)
 153     {
 154       lang = Language::LANG_SMTLIB_V2_6;  // default
 155     }
 156   }
 157   if (d_printers[static_cast<size_t>(lang)] == nullptr)
 158   {
 159     d_printers[static_cast<size_t>(lang)] = makePrinter(lang);
 160   }
 161   return d_printers[static_cast<size_t>(lang)].get();
 162 }
 163
 164 void Printer::printUnknownCommand(std::ostream& out,
 165                                   const std::string& name) const
 166 {
 167   out << "ERROR: don't know how to print " << name << " command" << std::endl;
 168 }
 169
 170 void Printer::toStreamCmdEmpty(std::ostream& out, const std::string& name) const
 171 {
 172   printUnknownCommand(out, "empty");
 173 }
 174
 175 void Printer::toStreamCmdEcho(std::ostream& out,
 176                               const std::string& output) const
 177 {
 178   printUnknownCommand(out, "echo");
 179 }
 180
 181 void Printer::toStreamCmdAssert(std::ostream& out, Node n) const
 182 {
 183   printUnknownCommand(out, "assert");
 184 }
 185
 186 void Printer::toStreamCmdPush(std::ostream& out) const
 187 {
 188   printUnknownCommand(out, "push");
 189 }
 190
 191 void Printer::toStreamCmdPop(std::ostream& out) const
 192 {
 193   printUnknownCommand(out, "pop");
 194 }
 195
 196 void Printer::toStreamCmdDeclareFunction(std::ostream& out,
 197                                          const std::string& id,
 198                                          TypeNode type) const
 199 {
 200   printUnknownCommand(out, "declare-fun");
 201 }
 202
 203 void Printer::toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const
 204 {
 205   std::string vs = v.getAttribute(expr::VarNameAttr());
 206   toStreamCmdDeclareFunction(out, vs, v.getType());
 207 }
 208
 209 void Printer::toStreamCmdDeclarePool(std::ostream& out,
 210                                      const std::string& id,
 211                                      TypeNode type,
 212                                      const std::vector<Node>& initValue) const
 213 {
 214   printUnknownCommand(out, "declare-pool");
 215 }
 216
 217 void Printer::toStreamCmdDeclareType(std::ostream& out,
 218                                      TypeNode type) const
 219 {
 220   printUnknownCommand(out, "declare-sort");
 221 }
 222
 223 void Printer::toStreamCmdDefineType(std::ostream& out,
 224                                     const std::string& id,
 225                                     const std::vector<TypeNode>& params,
 226                                     TypeNode t) const
 227 {
 228   printUnknownCommand(out, "define-sort");
 229 }
 230
 231 void Printer::toStreamCmdDefineFunction(std::ostream& out,
 232                                         const std::string& id,
 233                                         const std::vector<Node>& formals,
 234                                         TypeNode range,
 235                                         Node formula) const
 236 {
 237   printUnknownCommand(out, "define-fun");
 238 }
 239
 240 void Printer::toStreamCmdDefineFunction(std::ostream& out,
 241                                         Node v,
 242                                         Node lambda) const
 243 {
 244   std::stringstream vs;
 245   vs << v;
 246   std::vector<Node> formals;
 247   Node body = lambda;
 248   TypeNode rangeType = v.getType();
 249   if (body.getKind() == kind::LAMBDA)
 250   {
 251     formals.insert(formals.end(), lambda[0].begin(), lambda[0].end());
 252     body = lambda[1];
 253     Assert(rangeType.isFunction());
 254     rangeType = rangeType.getRangeType();
 255   }
 256   toStreamCmdDefineFunction(out, vs.str(), formals, rangeType, body);
 257 }
 258
 259 void Printer::toStreamCmdDefineFunctionRec(
 260     std::ostream& out,
 261     const std::vector<Node>& funcs,
 262     const std::vector<std::vector<Node>>& formals,
 263     const std::vector<Node>& formulas) const
 264 {
 265   printUnknownCommand(out, "define-fun-rec");
 266 }
 267
 268 void Printer::toStreamCmdDefineFunctionRec(
 269     std::ostream& out,
 270     const std::vector<Node>& funcs,
 271     const std::vector<Node>& lambdas) const
 272 {
 273   std::vector<std::vector<Node>> formals;
 274   std::vector<Node> formulas;
 275   for (const Node& l : lambdas)
 276   {
 277     std::vector<Node> formalsVec;
 278     Node formula;
 279     if (l.getKind() == kind::LAMBDA)
 280     {
 281       formalsVec.insert(formalsVec.end(), l[0].begin(), l[0].end());
 282       formula = l[1];
 283     }
 284     else
 285     {
 286       formula = l;
 287     }
 288     formals.emplace_back(formalsVec);
 289     formulas.emplace_back(formula);
 290   }
 291   toStreamCmdDefineFunctionRec(out, funcs, formals, formulas);
 292 }
 293
 294 void Printer::toStreamCmdSetUserAttribute(std::ostream& out,
 295                                           const std::string& attr,
 296                                           Node n) const
 297 {
 298   printUnknownCommand(out, "set-user-attribute");
 299 }
 300
 301 void Printer::toStreamCmdCheckSat(std::ostream& out) const
 302 {
 303   printUnknownCommand(out, "check-sat");
 304 }
 305
 306 void Printer::toStreamCmdCheckSatAssuming(std::ostream& out,
 307                                           const std::vector<Node>& nodes) const
 308 {
 309   printUnknownCommand(out, "check-sat-assuming");
 310 }
 311
 312 void Printer::toStreamCmdQuery(std::ostream& out, Node n) const
 313 {
 314   printUnknownCommand(out, "query");
 315 }
 316
 317 void Printer::toStreamCmdDeclareVar(std::ostream& out,
 318                                     Node var,
 319                                     TypeNode type) const
 320 {
 321   printUnknownCommand(out, "declare-var");
 322 }
 323
 324 void Printer::toStreamCmdSynthFun(std::ostream& out,
 325                                   Node f,
 326                                   const std::vector<Node>& vars,
 327                                   bool isInv,
 328                                   TypeNode sygusType) const
 329 {
 330   printUnknownCommand(out, isInv ? "synth-inv" : "synth-fun");
 331 }
 332
 333 void Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
 334 {
 335   printUnknownCommand(out, "constraint");
 336 }
 337
 338 void Printer::toStreamCmdAssume(std::ostream& out, Node n) const
 339 {
 340   printUnknownCommand(out, "assume");
 341 }
 342
 343 void Printer::toStreamCmdInvConstraint(
 344     std::ostream& out, Node inv, Node pre, Node trans, Node post) const
 345 {
 346   printUnknownCommand(out, "inv-constraint");
 347 }
 348
 349 void Printer::toStreamCmdCheckSynth(std::ostream& out) const
 350 {
 351   printUnknownCommand(out, "check-synth");
 352 }
 353 void Printer::toStreamCmdCheckSynthNext(std::ostream& out) const
 354 {
 355   printUnknownCommand(out, "check-synth-next");
 356 }
 357
 358 void Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
 359 {
 360   printUnknownCommand(out, "simplify");
 361 }
 362
 363 void Printer::toStreamCmdGetValue(std::ostream& out,
 364                                   const std::vector<Node>& nodes) const
 365 {
 366   printUnknownCommand(out, "get-value");
 367 }
 368
 369 void Printer::toStreamCmdGetAssignment(std::ostream& out) const
 370 {
 371   printUnknownCommand(out, "get-assignment");
 372 }
 373
 374 void Printer::toStreamCmdGetModel(std::ostream& out) const
 375 {
 376   printUnknownCommand(out, "ge-model");
 377 }
 378
 379 void Printer::toStreamCmdBlockModel(std::ostream& out) const
 380 {
 381   printUnknownCommand(out, "block-model");
 382 }
 383
 384 void Printer::toStreamCmdBlockModelValues(std::ostream& out,
 385                                           const std::vector<Node>& nodes) const
 386 {
 387   printUnknownCommand(out, "block-model-values");
 388 }
 389
 390 void Printer::toStreamCmdGetProof(std::ostream& out) const
 391 {
 392   printUnknownCommand(out, "get-proof");
 393 }
 394
 395 void Printer::toStreamCmdGetInstantiations(std::ostream& out) const
 396 {
 397   printUnknownCommand(out, "get-instantiations");
 398 }
 399
 400 void Printer::toStreamCmdGetInterpol(std::ostream& out,
 401                                      const std::string& name,
 402                                      Node conj,
 403                                      TypeNode sygusType) const
 404 {
 405   printUnknownCommand(out, "get-interpol");
 406 }
 407
 408 void Printer::toStreamCmdGetAbduct(std::ostream& out,
 409                                    const std::string& name,
 410                                    Node conj,
 411                                    TypeNode sygusType) const
 412 {
 413   printUnknownCommand(out, "get-abduct");
 414 }
 415
 416 void Printer::toStreamCmdGetAbductNext(std::ostream& out) const
 417 {
 418   printUnknownCommand(out, "get-abduct-next");
 419 }
 420
 421 void Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
 422                                                   Node n,
 423                                                   bool doFull) const
 424 {
 425   printUnknownCommand(out, "get-quantifier-elimination");
 426 }
 427
 428 void Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
 429 {
 430   printUnknownCommand(out, "get-unsat-assumption");
 431 }
 432
 433 void Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
 434 {
 435   printUnknownCommand(out, "get-unsat-core");
 436 }
 437
 438 void Printer::toStreamCmdGetDifficulty(std::ostream& out) const
 439 {
 440   printUnknownCommand(out, "get-difficulty");
 441 }
 442
 443 void Printer::toStreamCmdGetAssertions(std::ostream& out) const
 444 {
 445   printUnknownCommand(out, "get-assertions");
 446 }
 447
 448 void Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
 449                                            const std::string& logic) const
 450 {
 451   printUnknownCommand(out, "set-logic");
 452 }
 453
 454 void Printer::toStreamCmdSetInfo(std::ostream& out,
 455                                  const std::string& flag,
 456                                  const std::string& value) const
 457 {
 458   printUnknownCommand(out, "set-info");
 459 }
 460
 461 void Printer::toStreamCmdGetInfo(std::ostream& out,
 462                                  const std::string& flag) const
 463 {
 464   printUnknownCommand(out, "get-info");
 465 }
 466
 467 void Printer::toStreamCmdSetOption(std::ostream& out,
 468                                    const std::string& flag,
 469                                    const std::string& value) const
 470 {
 471   printUnknownCommand(out, "set-option");
 472 }
 473
 474 void Printer::toStreamCmdGetOption(std::ostream& out,
 475                                    const std::string& flag) const
 476 {
 477   printUnknownCommand(out, "get-option");
 478 }
 479
 480 void Printer::toStreamCmdSetExpressionName(std::ostream& out,
 481                                            Node n,
 482                                            const std::string& name) const
 483 {
 484   printUnknownCommand(out, "set-expression-name");
 485 }
 486
 487 void Printer::toStreamCmdDatatypeDeclaration(
 488     std::ostream& out, const std::vector<TypeNode>& datatypes) const
 489 {
 490   printUnknownCommand(
 491       out, datatypes.size() == 1 ? "declare-datatype" : "declare-datatypes");
 492 }
 493
 494 void Printer::toStreamCmdReset(std::ostream& out) const
 495 {
 496   printUnknownCommand(out, "reset");
 497 }
 498
 499 void Printer::toStreamCmdResetAssertions(std::ostream& out) const
 500 {
 501   printUnknownCommand(out, "reset-assertions");
 502 }
 503
 504 void Printer::toStreamCmdQuit(std::ostream& out) const
 505 {
 506   printUnknownCommand(out, "quit");
 507 }
 508
 509 void Printer::toStreamCmdDeclareHeap(std::ostream& out,
 510                                      TypeNode locType,
 511                                      TypeNode dataType) const
 512 {
 513   printUnknownCommand(out, "declare-heap");
 514 }
 515
 516 void Printer::toStreamCmdCommandSequence(
 517     std::ostream& out, const std::vector<Command*>& sequence) const
 518 {
 519   printUnknownCommand(out, "sequence");
 520 }
 521
 522 void Printer::toStreamCmdDeclarationSequence(
 523     std::ostream& out, const std::vector<Command*>& sequence) const
 524 {
 525   printUnknownCommand(out, "sequence");
 526 }
 527
 528 }  // namespace cvc5