src/smt/command.cpp

   1 /*********************                                                        */
   2 /*! \file command.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Morgan Deters, Andrew Reynolds
   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 command objects.
  13  **
  14  ** Implementation of command objects.
  15  **/
  16
  17 #include "smt/command.h"
  18
  19 #include <exception>
  20 #include <iostream>
  21 #include <iterator>
  22 #include <sstream>
  23 #include <utility>
  24 #include <vector>
  25
  26 #include "api/cvc4cpp.h"
  27 #include "base/check.h"
  28 #include "base/output.h"
  29 #include "expr/expr_iomanip.h"
  30 #include "expr/node.h"
  31 #include "expr/type.h"
  32 #include "options/options.h"
  33 #include "options/smt_options.h"
  34 #include "printer/printer.h"
  35 #include "proof/unsat_core.h"
  36 #include "smt/dump.h"
  37 #include "smt/model.h"
  38 #include "smt/smt_engine.h"
  39 #include "smt/smt_engine_scope.h"
  40 #include "util/sexpr.h"
  41 #include "util/utility.h"
  42
  43 using namespace std;
  44
  45 namespace CVC4 {
  46
  47 const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
  48 const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
  49 const CommandInterrupted* CommandInterrupted::s_instance =
  50     new CommandInterrupted();
  51
  52 std::ostream& operator<<(std::ostream& out, const Command& c)
  53 {
  54   c.toStream(out,
  55              Node::setdepth::getDepth(out),
  56              Node::printtypes::getPrintTypes(out),
  57              Node::dag::getDag(out),
  58              Node::setlanguage::getLanguage(out));
  59   return out;
  60 }
  61
  62 ostream& operator<<(ostream& out, const Command* c)
  63 {
  64   if (c == NULL)
  65   {
  66     out << "null";
  67   }
  68   else
  69   {
  70     out << *c;
  71   }
  72   return out;
  73 }
  74
  75 std::ostream& operator<<(std::ostream& out, const CommandStatus& s)
  76 {
  77   s.toStream(out, Node::setlanguage::getLanguage(out));
  78   return out;
  79 }
  80
  81 ostream& operator<<(ostream& out, const CommandStatus* s)
  82 {
  83   if (s == NULL)
  84   {
  85     out << "null";
  86   }
  87   else
  88   {
  89     out << *s;
  90   }
  91   return out;
  92 }
  93
  94 /* output stream insertion operator for benchmark statuses */
  95 std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
  96 {
  97   switch (status)
  98   {
  99     case SMT_SATISFIABLE: return out << "sat";
 100
 101     case SMT_UNSATISFIABLE: return out << "unsat";
 102
 103     case SMT_UNKNOWN: return out << "unknown";
 104
 105     default: return out << "BenchmarkStatus::[UNKNOWNSTATUS!]";
 106   }
 107 }
 108
 109 /* -------------------------------------------------------------------------- */
 110 /* class CommandPrintSuccess                                                  */
 111 /* -------------------------------------------------------------------------- */
 112
 113 void CommandPrintSuccess::applyPrintSuccess(std::ostream& out)
 114 {
 115   out.iword(s_iosIndex) = d_printSuccess;
 116 }
 117
 118 bool CommandPrintSuccess::getPrintSuccess(std::ostream& out)
 119 {
 120   return out.iword(s_iosIndex);
 121 }
 122
 123 void CommandPrintSuccess::setPrintSuccess(std::ostream& out, bool printSuccess)
 124 {
 125   out.iword(s_iosIndex) = printSuccess;
 126 }
 127
 128 std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps)
 129 {
 130   cps.applyPrintSuccess(out);
 131   return out;
 132 }
 133
 134 /* -------------------------------------------------------------------------- */
 135 /* class Command                                                              */
 136 /* -------------------------------------------------------------------------- */
 137
 138 Command::Command() : d_commandStatus(nullptr), d_muted(false) {}
 139
 140 Command::Command(const api::Solver* solver)
 141     : d_commandStatus(nullptr), d_muted(false)
 142 {
 143 }
 144
 145 Command::Command(const Command& cmd)
 146 {
 147   d_commandStatus =
 148       (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone();
 149   d_muted = cmd.d_muted;
 150 }
 151
 152 Command::~Command()
 153 {
 154   if (d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance())
 155   {
 156     delete d_commandStatus;
 157   }
 158 }
 159
 160 bool Command::ok() const
 161 {
 162   // either we haven't run the command yet, or it ran successfully
 163   return d_commandStatus == NULL
 164          || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL;
 165 }
 166
 167 bool Command::fail() const
 168 {
 169   return d_commandStatus != NULL
 170          && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL;
 171 }
 172
 173 bool Command::interrupted() const
 174 {
 175   return d_commandStatus != NULL
 176          && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
 177 }
 178
 179 void Command::invoke(api::Solver* solver, std::ostream& out)
 180 {
 181   invoke(solver);
 182   if (!(isMuted() && ok()))
 183   {
 184     printResult(
 185         out,
 186         std::stoul(solver->getOption("command-verbosity:" + getCommandName())));
 187   }
 188 }
 189
 190 std::string Command::toString() const
 191 {
 192   std::stringstream ss;
 193   toStream(ss);
 194   return ss.str();
 195 }
 196
 197 void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const
 198 {
 199   Printer::getPrinter(language)->toStream(out, this);
 200 }
 201
 202 void Command::printResult(std::ostream& out, uint32_t verbosity) const
 203 {
 204   if (d_commandStatus != NULL)
 205   {
 206     if ((!ok() && verbosity >= 1) || verbosity >= 2)
 207     {
 208       out << *d_commandStatus;
 209     }
 210   }
 211 }
 212
 213 /* -------------------------------------------------------------------------- */
 214 /* class EmptyCommand                                                         */
 215 /* -------------------------------------------------------------------------- */
 216
 217 EmptyCommand::EmptyCommand(std::string name) : d_name(name) {}
 218 std::string EmptyCommand::getName() const { return d_name; }
 219 void EmptyCommand::invoke(api::Solver* solver)
 220 {
 221   /* empty commands have no implementation */
 222   d_commandStatus = CommandSuccess::instance();
 223 }
 224
 225 Command* EmptyCommand::clone() const { return new EmptyCommand(d_name); }
 226 std::string EmptyCommand::getCommandName() const { return "empty"; }
 227
 228 void EmptyCommand::toStream(std::ostream& out,
 229                             int toDepth,
 230                             bool types,
 231                             size_t dag,
 232                             OutputLanguage language) const
 233 {
 234   Printer::getPrinter(language)->toStreamCmdEmpty(out, d_name);
 235 }
 236
 237 /* -------------------------------------------------------------------------- */
 238 /* class EchoCommand                                                          */
 239 /* -------------------------------------------------------------------------- */
 240
 241 EchoCommand::EchoCommand(std::string output) : d_output(output) {}
 242 std::string EchoCommand::getOutput() const { return d_output; }
 243 void EchoCommand::invoke(api::Solver* solver)
 244 {
 245   /* we don't have an output stream here, nothing to do */
 246   d_commandStatus = CommandSuccess::instance();
 247 }
 248
 249 void EchoCommand::invoke(api::Solver* solver, std::ostream& out)
 250 {
 251   out << d_output << std::endl;
 252   Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
 253                            << std::endl;
 254   d_commandStatus = CommandSuccess::instance();
 255   printResult(
 256       out,
 257       std::stoul(solver->getOption("command-verbosity:" + getCommandName())));
 258 }
 259
 260 Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
 261 std::string EchoCommand::getCommandName() const { return "echo"; }
 262
 263 void EchoCommand::toStream(std::ostream& out,
 264                            int toDepth,
 265                            bool types,
 266                            size_t dag,
 267                            OutputLanguage language) const
 268 {
 269   Printer::getPrinter(language)->toStreamCmdEcho(out, d_output);
 270 }
 271
 272 /* -------------------------------------------------------------------------- */
 273 /* class AssertCommand                                                        */
 274 /* -------------------------------------------------------------------------- */
 275
 276 AssertCommand::AssertCommand(const api::Term& t, bool inUnsatCore)
 277     : d_term(t), d_inUnsatCore(inUnsatCore)
 278 {
 279 }
 280
 281 api::Term AssertCommand::getTerm() const { return d_term; }
 282 void AssertCommand::invoke(api::Solver* solver)
 283 {
 284   try
 285   {
 286     solver->getSmtEngine()->assertFormula(d_term.getNode(), d_inUnsatCore);
 287     d_commandStatus = CommandSuccess::instance();
 288   }
 289   catch (UnsafeInterruptException& e)
 290   {
 291     d_commandStatus = new CommandInterrupted();
 292   }
 293   catch (exception& e)
 294   {
 295     d_commandStatus = new CommandFailure(e.what());
 296   }
 297 }
 298
 299 Command* AssertCommand::clone() const
 300 {
 301   return new AssertCommand(d_term, d_inUnsatCore);
 302 }
 303
 304 std::string AssertCommand::getCommandName() const { return "assert"; }
 305
 306 void AssertCommand::toStream(std::ostream& out,
 307                              int toDepth,
 308                              bool types,
 309                              size_t dag,
 310                              OutputLanguage language) const
 311 {
 312   Printer::getPrinter(language)->toStreamCmdAssert(out, d_term.getNode());
 313 }
 314
 315 /* -------------------------------------------------------------------------- */
 316 /* class PushCommand                                                          */
 317 /* -------------------------------------------------------------------------- */
 318
 319 void PushCommand::invoke(api::Solver* solver)
 320 {
 321   try
 322   {
 323     solver->push();
 324     d_commandStatus = CommandSuccess::instance();
 325   }
 326   catch (UnsafeInterruptException& e)
 327   {
 328     d_commandStatus = new CommandInterrupted();
 329   }
 330   catch (exception& e)
 331   {
 332     d_commandStatus = new CommandFailure(e.what());
 333   }
 334 }
 335
 336 Command* PushCommand::clone() const { return new PushCommand(); }
 337 std::string PushCommand::getCommandName() const { return "push"; }
 338
 339 void PushCommand::toStream(std::ostream& out,
 340                            int toDepth,
 341                            bool types,
 342                            size_t dag,
 343                            OutputLanguage language) const
 344 {
 345   Printer::getPrinter(language)->toStreamCmdPush(out);
 346 }
 347
 348 /* -------------------------------------------------------------------------- */
 349 /* class PopCommand                                                           */
 350 /* -------------------------------------------------------------------------- */
 351
 352 void PopCommand::invoke(api::Solver* solver)
 353 {
 354   try
 355   {
 356     solver->pop();
 357     d_commandStatus = CommandSuccess::instance();
 358   }
 359   catch (UnsafeInterruptException& e)
 360   {
 361     d_commandStatus = new CommandInterrupted();
 362   }
 363   catch (exception& e)
 364   {
 365     d_commandStatus = new CommandFailure(e.what());
 366   }
 367 }
 368
 369 Command* PopCommand::clone() const { return new PopCommand(); }
 370 std::string PopCommand::getCommandName() const { return "pop"; }
 371
 372 void PopCommand::toStream(std::ostream& out,
 373                           int toDepth,
 374                           bool types,
 375                           size_t dag,
 376                           OutputLanguage language) const
 377 {
 378   Printer::getPrinter(language)->toStreamCmdPop(out);
 379 }
 380
 381 /* -------------------------------------------------------------------------- */
 382 /* class CheckSatCommand                                                      */
 383 /* -------------------------------------------------------------------------- */
 384
 385 CheckSatCommand::CheckSatCommand() : d_term() {}
 386
 387 CheckSatCommand::CheckSatCommand(const api::Term& term) : d_term(term) {}
 388
 389 api::Term CheckSatCommand::getTerm() const { return d_term; }
 390 void CheckSatCommand::invoke(api::Solver* solver)
 391 {
 392   Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
 393                            << std::endl;
 394   try
 395   {
 396     d_result =
 397         d_term.isNull() ? solver->checkSat() : solver->checkSatAssuming(d_term);
 398
 399     d_commandStatus = CommandSuccess::instance();
 400   }
 401   catch (exception& e)
 402   {
 403     d_commandStatus = new CommandFailure(e.what());
 404   }
 405 }
 406
 407 api::Result CheckSatCommand::getResult() const { return d_result; }
 408 void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
 409 {
 410   if (!ok())
 411   {
 412     this->Command::printResult(out, verbosity);
 413   }
 414   else
 415   {
 416     Trace("dtview::command") << "* RESULT: " << d_result << std::endl;
 417     out << d_result << endl;
 418   }
 419 }
 420
 421 Command* CheckSatCommand::clone() const
 422 {
 423   CheckSatCommand* c = new CheckSatCommand(d_term);
 424   c->d_result = d_result;
 425   return c;
 426 }
 427
 428 std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
 429
 430 void CheckSatCommand::toStream(std::ostream& out,
 431                                int toDepth,
 432                                bool types,
 433                                size_t dag,
 434                                OutputLanguage language) const
 435 {
 436   Printer::getPrinter(language)->toStreamCmdCheckSat(out, d_term.getNode());
 437 }
 438
 439 /* -------------------------------------------------------------------------- */
 440 /* class CheckSatAssumingCommand                                              */
 441 /* -------------------------------------------------------------------------- */
 442
 443 CheckSatAssumingCommand::CheckSatAssumingCommand(api::Term term)
 444     : d_terms({term})
 445 {
 446 }
 447
 448 CheckSatAssumingCommand::CheckSatAssumingCommand(
 449     const std::vector<api::Term>& terms)
 450     : d_terms(terms)
 451 {
 452 }
 453
 454 const std::vector<api::Term>& CheckSatAssumingCommand::getTerms() const
 455 {
 456   return d_terms;
 457 }
 458
 459 void CheckSatAssumingCommand::invoke(api::Solver* solver)
 460 {
 461   Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms
 462                            << " )~" << std::endl;
 463   try
 464   {
 465     d_result = solver->checkSatAssuming(d_terms);
 466     d_commandStatus = CommandSuccess::instance();
 467   }
 468   catch (exception& e)
 469   {
 470     d_commandStatus = new CommandFailure(e.what());
 471   }
 472 }
 473
 474 api::Result CheckSatAssumingCommand::getResult() const
 475 {
 476   Trace("dtview::command") << "* ~RESULT: " << d_result << "~" << std::endl;
 477   return d_result;
 478 }
 479
 480 void CheckSatAssumingCommand::printResult(std::ostream& out,
 481                                           uint32_t verbosity) const
 482 {
 483   if (!ok())
 484   {
 485     this->Command::printResult(out, verbosity);
 486   }
 487   else
 488   {
 489     out << d_result << endl;
 490   }
 491 }
 492
 493 Command* CheckSatAssumingCommand::clone() const
 494 {
 495   CheckSatAssumingCommand* c = new CheckSatAssumingCommand(d_terms);
 496   c->d_result = d_result;
 497   return c;
 498 }
 499
 500 std::string CheckSatAssumingCommand::getCommandName() const
 501 {
 502   return "check-sat-assuming";
 503 }
 504
 505 void CheckSatAssumingCommand::toStream(std::ostream& out,
 506                                        int toDepth,
 507                                        bool types,
 508                                        size_t dag,
 509                                        OutputLanguage language) const
 510 {
 511   Printer::getPrinter(language)->toStreamCmdCheckSatAssuming(
 512       out, api::termVectorToNodes(d_terms));
 513 }
 514
 515 /* -------------------------------------------------------------------------- */
 516 /* class QueryCommand                                                         */
 517 /* -------------------------------------------------------------------------- */
 518
 519 QueryCommand::QueryCommand(const api::Term& t, bool inUnsatCore)
 520     : d_term(t), d_inUnsatCore(inUnsatCore)
 521 {
 522 }
 523
 524 api::Term QueryCommand::getTerm() const { return d_term; }
 525 void QueryCommand::invoke(api::Solver* solver)
 526 {
 527   try
 528   {
 529     d_result = solver->checkEntailed(d_term);
 530     d_commandStatus = CommandSuccess::instance();
 531   }
 532   catch (exception& e)
 533   {
 534     d_commandStatus = new CommandFailure(e.what());
 535   }
 536 }
 537
 538 api::Result QueryCommand::getResult() const { return d_result; }
 539 void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const
 540 {
 541   if (!ok())
 542   {
 543     this->Command::printResult(out, verbosity);
 544   }
 545   else
 546   {
 547     out << d_result << endl;
 548   }
 549 }
 550
 551 Command* QueryCommand::clone() const
 552 {
 553   QueryCommand* c = new QueryCommand(d_term, d_inUnsatCore);
 554   c->d_result = d_result;
 555   return c;
 556 }
 557
 558 std::string QueryCommand::getCommandName() const { return "query"; }
 559
 560 void QueryCommand::toStream(std::ostream& out,
 561                             int toDepth,
 562                             bool types,
 563                             size_t dag,
 564                             OutputLanguage language) const
 565 {
 566   Printer::getPrinter(language)->toStreamCmdQuery(out, d_term.getNode());
 567 }
 568
 569 /* -------------------------------------------------------------------------- */
 570 /* class DeclareSygusVarCommand */
 571 /* -------------------------------------------------------------------------- */
 572
 573 DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id,
 574                                                api::Term var,
 575                                                api::Sort sort)
 576     : DeclarationDefinitionCommand(id), d_var(var), d_sort(sort)
 577 {
 578 }
 579
 580 api::Term DeclareSygusVarCommand::getVar() const { return d_var; }
 581 api::Sort DeclareSygusVarCommand::getSort() const { return d_sort; }
 582
 583 void DeclareSygusVarCommand::invoke(api::Solver* solver)
 584 {
 585   d_commandStatus = CommandSuccess::instance();
 586 }
 587
 588 Command* DeclareSygusVarCommand::clone() const
 589 {
 590   return new DeclareSygusVarCommand(d_symbol, d_var, d_sort);
 591 }
 592
 593 std::string DeclareSygusVarCommand::getCommandName() const
 594 {
 595   return "declare-var";
 596 }
 597
 598 void DeclareSygusVarCommand::toStream(std::ostream& out,
 599                                       int toDepth,
 600                                       bool types,
 601                                       size_t dag,
 602                                       OutputLanguage language) const
 603 {
 604   Printer::getPrinter(language)->toStreamCmdDeclareVar(
 605       out, d_var.getNode(), TypeNode::fromType(d_sort.getType()));
 606 }
 607
 608 /* -------------------------------------------------------------------------- */
 609 /* class SynthFunCommand                                                      */
 610 /* -------------------------------------------------------------------------- */
 611
 612 SynthFunCommand::SynthFunCommand(const std::string& id,
 613                                  api::Term fun,
 614                                  const std::vector<api::Term>& vars,
 615                                  api::Sort sort,
 616                                  bool isInv,
 617                                  api::Grammar* g)
 618     : DeclarationDefinitionCommand(id),
 619       d_fun(fun),
 620       d_vars(vars),
 621       d_sort(sort),
 622       d_isInv(isInv),
 623       d_grammar(g)
 624 {
 625 }
 626
 627 api::Term SynthFunCommand::getFunction() const { return d_fun; }
 628
 629 const std::vector<api::Term>& SynthFunCommand::getVars() const
 630 {
 631   return d_vars;
 632 }
 633
 634 api::Sort SynthFunCommand::getSort() const { return d_sort; }
 635 bool SynthFunCommand::isInv() const { return d_isInv; }
 636
 637 const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
 638
 639 void SynthFunCommand::invoke(api::Solver* solver)
 640 {
 641   d_commandStatus = CommandSuccess::instance();
 642 }
 643
 644 Command* SynthFunCommand::clone() const
 645 {
 646   return new SynthFunCommand(
 647       d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar);
 648 }
 649
 650 std::string SynthFunCommand::getCommandName() const
 651 {
 652   return d_isInv ? "synth-inv" : "synth-fun";
 653 }
 654
 655 void SynthFunCommand::toStream(std::ostream& out,
 656                                int toDepth,
 657                                bool types,
 658                                size_t dag,
 659                                OutputLanguage language) const
 660 {
 661   std::vector<Node> nodeVars = termVectorToNodes(d_vars);
 662   Printer::getPrinter(language)->toStreamCmdSynthFun(
 663       out,
 664       d_symbol,
 665       nodeVars,
 666       TypeNode::fromType(d_sort.getType()),
 667       d_isInv,
 668       TypeNode::fromType(d_grammar->resolve().getType()));
 669 }
 670
 671 /* -------------------------------------------------------------------------- */
 672 /* class SygusConstraintCommand */
 673 /* -------------------------------------------------------------------------- */
 674
 675 SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t)
 676 {
 677 }
 678
 679 void SygusConstraintCommand::invoke(api::Solver* solver)
 680 {
 681   try
 682   {
 683     solver->addSygusConstraint(d_term);
 684     d_commandStatus = CommandSuccess::instance();
 685   }
 686   catch (exception& e)
 687   {
 688     d_commandStatus = new CommandFailure(e.what());
 689   }
 690 }
 691
 692 api::Term SygusConstraintCommand::getTerm() const { return d_term; }
 693
 694 Command* SygusConstraintCommand::clone() const
 695 {
 696   return new SygusConstraintCommand(d_term);
 697 }
 698
 699 std::string SygusConstraintCommand::getCommandName() const
 700 {
 701   return "constraint";
 702 }
 703
 704 void SygusConstraintCommand::toStream(std::ostream& out,
 705                                       int toDepth,
 706                                       bool types,
 707                                       size_t dag,
 708                                       OutputLanguage language) const
 709 {
 710   Printer::getPrinter(language)->toStreamCmdConstraint(out, d_term.getNode());
 711 }
 712
 713 /* -------------------------------------------------------------------------- */
 714 /* class SygusInvConstraintCommand */
 715 /* -------------------------------------------------------------------------- */
 716
 717 SygusInvConstraintCommand::SygusInvConstraintCommand(
 718     const std::vector<api::Term>& predicates)
 719     : d_predicates(predicates)
 720 {
 721 }
 722
 723 SygusInvConstraintCommand::SygusInvConstraintCommand(const api::Term& inv,
 724                                                      const api::Term& pre,
 725                                                      const api::Term& trans,
 726                                                      const api::Term& post)
 727     : SygusInvConstraintCommand(std::vector<api::Term>{inv, pre, trans, post})
 728 {
 729 }
 730
 731 void SygusInvConstraintCommand::invoke(api::Solver* solver)
 732 {
 733   try
 734   {
 735     solver->addSygusInvConstraint(
 736         d_predicates[0], d_predicates[1], d_predicates[2], d_predicates[3]);
 737     d_commandStatus = CommandSuccess::instance();
 738   }
 739   catch (exception& e)
 740   {
 741     d_commandStatus = new CommandFailure(e.what());
 742   }
 743 }
 744
 745 const std::vector<api::Term>& SygusInvConstraintCommand::getPredicates() const
 746 {
 747   return d_predicates;
 748 }
 749
 750 Command* SygusInvConstraintCommand::clone() const
 751 {
 752   return new SygusInvConstraintCommand(d_predicates);
 753 }
 754
 755 std::string SygusInvConstraintCommand::getCommandName() const
 756 {
 757   return "inv-constraint";
 758 }
 759
 760 void SygusInvConstraintCommand::toStream(std::ostream& out,
 761                                          int toDepth,
 762                                          bool types,
 763                                          size_t dag,
 764                                          OutputLanguage language) const
 765 {
 766   Printer::getPrinter(language)->toStreamCmdInvConstraint(
 767       out,
 768       d_predicates[0].getNode(),
 769       d_predicates[1].getNode(),
 770       d_predicates[2].getNode(),
 771       d_predicates[3].getNode());
 772 }
 773
 774 /* -------------------------------------------------------------------------- */
 775 /* class CheckSynthCommand                                                    */
 776 /* -------------------------------------------------------------------------- */
 777
 778 void CheckSynthCommand::invoke(api::Solver* solver)
 779 {
 780   try
 781   {
 782     d_result = solver->checkSynth();
 783     d_commandStatus = CommandSuccess::instance();
 784     d_solution.clear();
 785     // check whether we should print the status
 786     if (!d_result.isUnsat()
 787         || options::sygusOut() == options::SygusSolutionOutMode::STATUS_AND_DEF
 788         || options::sygusOut() == options::SygusSolutionOutMode::STATUS)
 789     {
 790       if (options::sygusOut() == options::SygusSolutionOutMode::STANDARD)
 791       {
 792         d_solution << "(fail)" << endl;
 793       }
 794       else
 795       {
 796         d_solution << d_result << endl;
 797       }
 798     }
 799     // check whether we should print the solution
 800     if (d_result.isUnsat()
 801         && options::sygusOut() != options::SygusSolutionOutMode::STATUS)
 802     {
 803       // printing a synthesis solution is a non-constant
 804       // method, since it invokes a sophisticated algorithm
 805       // (Figure 5 of Reynolds et al. CAV 2015).
 806       // Hence, we must call here print solution here,
 807       // instead of during printResult.
 808       solver->printSynthSolution(d_solution);
 809     }
 810   }
 811   catch (exception& e)
 812   {
 813     d_commandStatus = new CommandFailure(e.what());
 814   }
 815 }
 816
 817 api::Result CheckSynthCommand::getResult() const { return d_result; }
 818 void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const
 819 {
 820   if (!ok())
 821   {
 822     this->Command::printResult(out, verbosity);
 823   }
 824   else
 825   {
 826     out << d_solution.str();
 827   }
 828 }
 829
 830 Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
 831
 832 std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
 833
 834 void CheckSynthCommand::toStream(std::ostream& out,
 835                                  int toDepth,
 836                                  bool types,
 837                                  size_t dag,
 838                                  OutputLanguage language) const
 839 {
 840   Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
 841 }
 842
 843 /* -------------------------------------------------------------------------- */
 844 /* class ResetCommand                                                         */
 845 /* -------------------------------------------------------------------------- */
 846
 847 void ResetCommand::invoke(api::Solver* solver)
 848 {
 849   try
 850   {
 851     solver->getSmtEngine()->reset();
 852     d_commandStatus = CommandSuccess::instance();
 853   }
 854   catch (exception& e)
 855   {
 856     d_commandStatus = new CommandFailure(e.what());
 857   }
 858 }
 859
 860 Command* ResetCommand::clone() const { return new ResetCommand(); }
 861 std::string ResetCommand::getCommandName() const { return "reset"; }
 862
 863 void ResetCommand::toStream(std::ostream& out,
 864                             int toDepth,
 865                             bool types,
 866                             size_t dag,
 867                             OutputLanguage language) const
 868 {
 869   Printer::getPrinter(language)->toStreamCmdReset(out);
 870 }
 871
 872 /* -------------------------------------------------------------------------- */
 873 /* class ResetAssertionsCommand                                               */
 874 /* -------------------------------------------------------------------------- */
 875
 876 void ResetAssertionsCommand::invoke(api::Solver* solver)
 877 {
 878   try
 879   {
 880     solver->resetAssertions();
 881     d_commandStatus = CommandSuccess::instance();
 882   }
 883   catch (exception& e)
 884   {
 885     d_commandStatus = new CommandFailure(e.what());
 886   }
 887 }
 888
 889 Command* ResetAssertionsCommand::clone() const
 890 {
 891   return new ResetAssertionsCommand();
 892 }
 893
 894 std::string ResetAssertionsCommand::getCommandName() const
 895 {
 896   return "reset-assertions";
 897 }
 898
 899 void ResetAssertionsCommand::toStream(std::ostream& out,
 900                                       int toDepth,
 901                                       bool types,
 902                                       size_t dag,
 903                                       OutputLanguage language) const
 904 {
 905   Printer::getPrinter(language)->toStreamCmdResetAssertions(out);
 906 }
 907
 908 /* -------------------------------------------------------------------------- */
 909 /* class QuitCommand                                                          */
 910 /* -------------------------------------------------------------------------- */
 911
 912 void QuitCommand::invoke(api::Solver* solver)
 913 {
 914   Dump("benchmark") << *this;
 915   d_commandStatus = CommandSuccess::instance();
 916 }
 917
 918 Command* QuitCommand::clone() const { return new QuitCommand(); }
 919 std::string QuitCommand::getCommandName() const { return "exit"; }
 920
 921 void QuitCommand::toStream(std::ostream& out,
 922                            int toDepth,
 923                            bool types,
 924                            size_t dag,
 925                            OutputLanguage language) const
 926 {
 927   Printer::getPrinter(language)->toStreamCmdQuit(out);
 928 }
 929
 930 /* -------------------------------------------------------------------------- */
 931 /* class CommentCommand                                                       */
 932 /* -------------------------------------------------------------------------- */
 933
 934 CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {}
 935 std::string CommentCommand::getComment() const { return d_comment; }
 936 void CommentCommand::invoke(api::Solver* solver)
 937 {
 938   Dump("benchmark") << *this;
 939   d_commandStatus = CommandSuccess::instance();
 940 }
 941
 942 Command* CommentCommand::clone() const { return new CommentCommand(d_comment); }
 943 std::string CommentCommand::getCommandName() const { return "comment"; }
 944
 945 void CommentCommand::toStream(std::ostream& out,
 946                               int toDepth,
 947                               bool types,
 948                               size_t dag,
 949                               OutputLanguage language) const
 950 {
 951   Printer::getPrinter(language)->toStreamCmdComment(out, d_comment);
 952 }
 953
 954 /* -------------------------------------------------------------------------- */
 955 /* class CommandSequence                                                      */
 956 /* -------------------------------------------------------------------------- */
 957
 958 CommandSequence::CommandSequence() : d_index(0) {}
 959 CommandSequence::~CommandSequence()
 960 {
 961   for (unsigned i = d_index; i < d_commandSequence.size(); ++i)
 962   {
 963     delete d_commandSequence[i];
 964   }
 965 }
 966
 967 void CommandSequence::addCommand(Command* cmd)
 968 {
 969   d_commandSequence.push_back(cmd);
 970 }
 971
 972 void CommandSequence::clear() { d_commandSequence.clear(); }
 973 void CommandSequence::invoke(api::Solver* solver)
 974 {
 975   for (; d_index < d_commandSequence.size(); ++d_index)
 976   {
 977     d_commandSequence[d_index]->invoke(solver);
 978     if (!d_commandSequence[d_index]->ok())
 979     {
 980       // abort execution
 981       d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
 982       return;
 983     }
 984     delete d_commandSequence[d_index];
 985   }
 986
 987   AlwaysAssert(d_commandStatus == NULL);
 988   d_commandStatus = CommandSuccess::instance();
 989 }
 990
 991 void CommandSequence::invoke(api::Solver* solver, std::ostream& out)
 992 {
 993   for (; d_index < d_commandSequence.size(); ++d_index)
 994   {
 995     d_commandSequence[d_index]->invoke(solver, out);
 996     if (!d_commandSequence[d_index]->ok())
 997     {
 998       // abort execution
 999       d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
1000       return;
1001     }
1002     delete d_commandSequence[d_index];
1003   }
1004
1005   AlwaysAssert(d_commandStatus == NULL);
1006   d_commandStatus = CommandSuccess::instance();
1007 }
1008
1009 Command* CommandSequence::clone() const
1010 {
1011   CommandSequence* seq = new CommandSequence();
1012   for (const_iterator i = begin(); i != end(); ++i)
1013   {
1014     seq->addCommand((*i)->clone());
1015   }
1016   seq->d_index = d_index;
1017   return seq;
1018 }
1019
1020 CommandSequence::const_iterator CommandSequence::begin() const
1021 {
1022   return d_commandSequence.begin();
1023 }
1024
1025 CommandSequence::const_iterator CommandSequence::end() const
1026 {
1027   return d_commandSequence.end();
1028 }
1029
1030 CommandSequence::iterator CommandSequence::begin()
1031 {
1032   return d_commandSequence.begin();
1033 }
1034
1035 CommandSequence::iterator CommandSequence::end()
1036 {
1037   return d_commandSequence.end();
1038 }
1039
1040 std::string CommandSequence::getCommandName() const { return "sequence"; }
1041
1042 void CommandSequence::toStream(std::ostream& out,
1043                                int toDepth,
1044                                bool types,
1045                                size_t dag,
1046                                OutputLanguage language) const
1047 {
1048   Printer::getPrinter(language)->toStreamCmdCommandSequence(out,
1049                                                             d_commandSequence);
1050 }
1051
1052 /* -------------------------------------------------------------------------- */
1053 /* class DeclarationSequence                                                  */
1054 /* -------------------------------------------------------------------------- */
1055
1056 void DeclarationSequence::toStream(std::ostream& out,
1057                                    int toDepth,
1058                                    bool types,
1059                                    size_t dag,
1060                                    OutputLanguage language) const
1061 {
1062   Printer::getPrinter(language)->toStreamCmdDeclarationSequence(
1063       out, d_commandSequence);
1064 }
1065
1066 /* -------------------------------------------------------------------------- */
1067 /* class DeclarationDefinitionCommand                                         */
1068 /* -------------------------------------------------------------------------- */
1069
1070 DeclarationDefinitionCommand::DeclarationDefinitionCommand(
1071     const std::string& id)
1072     : d_symbol(id)
1073 {
1074 }
1075
1076 std::string DeclarationDefinitionCommand::getSymbol() const { return d_symbol; }
1077
1078 /* -------------------------------------------------------------------------- */
1079 /* class DeclareFunctionCommand                                               */
1080 /* -------------------------------------------------------------------------- */
1081
1082 DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id,
1083                                                api::Term func,
1084                                                api::Sort sort)
1085     : DeclarationDefinitionCommand(id),
1086       d_func(func),
1087       d_sort(sort),
1088       d_printInModel(true),
1089       d_printInModelSetByUser(false)
1090 {
1091 }
1092
1093 api::Term DeclareFunctionCommand::getFunction() const { return d_func; }
1094 api::Sort DeclareFunctionCommand::getSort() const { return d_sort; }
1095 bool DeclareFunctionCommand::getPrintInModel() const { return d_printInModel; }
1096 bool DeclareFunctionCommand::getPrintInModelSetByUser() const
1097 {
1098   return d_printInModelSetByUser;
1099 }
1100
1101 void DeclareFunctionCommand::setPrintInModel(bool p)
1102 {
1103   d_printInModel = p;
1104   d_printInModelSetByUser = true;
1105 }
1106
1107 void DeclareFunctionCommand::invoke(api::Solver* solver)
1108 {
1109   d_commandStatus = CommandSuccess::instance();
1110 }
1111
1112 Command* DeclareFunctionCommand::clone() const
1113 {
1114   DeclareFunctionCommand* dfc =
1115       new DeclareFunctionCommand(d_symbol, d_func, d_sort);
1116   dfc->d_printInModel = d_printInModel;
1117   dfc->d_printInModelSetByUser = d_printInModelSetByUser;
1118   return dfc;
1119 }
1120
1121 std::string DeclareFunctionCommand::getCommandName() const
1122 {
1123   return "declare-fun";
1124 }
1125
1126 void DeclareFunctionCommand::toStream(std::ostream& out,
1127                                       int toDepth,
1128                                       bool types,
1129                                       size_t dag,
1130                                       OutputLanguage language) const
1131 {
1132   Printer::getPrinter(language)->toStreamCmdDeclareFunction(
1133       out, d_func.toString(), TypeNode::fromType(d_sort.getType()));
1134 }
1135
1136 /* -------------------------------------------------------------------------- */
1137 /* class DeclareSortCommand                                                   */
1138 /* -------------------------------------------------------------------------- */
1139
1140 DeclareSortCommand::DeclareSortCommand(const std::string& id,
1141                                        size_t arity,
1142                                        api::Sort sort)
1143     : DeclarationDefinitionCommand(id), d_arity(arity), d_sort(sort)
1144 {
1145 }
1146
1147 size_t DeclareSortCommand::getArity() const { return d_arity; }
1148 api::Sort DeclareSortCommand::getSort() const { return d_sort; }
1149 void DeclareSortCommand::invoke(api::Solver* solver)
1150 {
1151   d_commandStatus = CommandSuccess::instance();
1152 }
1153
1154 Command* DeclareSortCommand::clone() const
1155 {
1156   return new DeclareSortCommand(d_symbol, d_arity, d_sort);
1157 }
1158
1159 std::string DeclareSortCommand::getCommandName() const
1160 {
1161   return "declare-sort";
1162 }
1163
1164 void DeclareSortCommand::toStream(std::ostream& out,
1165                                   int toDepth,
1166                                   bool types,
1167                                   size_t dag,
1168                                   OutputLanguage language) const
1169 {
1170   Printer::getPrinter(language)->toStreamCmdDeclareType(
1171       out, d_sort.toString(), d_arity, TypeNode::fromType(d_sort.getType()));
1172 }
1173
1174 /* -------------------------------------------------------------------------- */
1175 /* class DefineSortCommand                                                    */
1176 /* -------------------------------------------------------------------------- */
1177
1178 DefineSortCommand::DefineSortCommand(const std::string& id, api::Sort sort)
1179     : DeclarationDefinitionCommand(id), d_params(), d_sort(sort)
1180 {
1181 }
1182
1183 DefineSortCommand::DefineSortCommand(const std::string& id,
1184                                      const std::vector<api::Sort>& params,
1185                                      api::Sort sort)
1186     : DeclarationDefinitionCommand(id), d_params(params), d_sort(sort)
1187 {
1188 }
1189
1190 const std::vector<api::Sort>& DefineSortCommand::getParameters() const
1191 {
1192   return d_params;
1193 }
1194
1195 api::Sort DefineSortCommand::getSort() const { return d_sort; }
1196 void DefineSortCommand::invoke(api::Solver* solver)
1197 {
1198   d_commandStatus = CommandSuccess::instance();
1199 }
1200
1201 Command* DefineSortCommand::clone() const
1202 {
1203   return new DefineSortCommand(d_symbol, d_params, d_sort);
1204 }
1205
1206 std::string DefineSortCommand::getCommandName() const { return "define-sort"; }
1207
1208 void DefineSortCommand::toStream(std::ostream& out,
1209                                  int toDepth,
1210                                  bool types,
1211                                  size_t dag,
1212                                  OutputLanguage language) const
1213 {
1214   Printer::getPrinter(language)->toStreamCmdDefineType(
1215       out,
1216       d_symbol,
1217       api::sortVectorToTypeNodes(d_params),
1218       TypeNode::fromType(d_sort.getType()));
1219 }
1220
1221 /* -------------------------------------------------------------------------- */
1222 /* class DefineFunctionCommand                                                */
1223 /* -------------------------------------------------------------------------- */
1224
1225 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
1226                                              api::Term func,
1227                                              api::Term formula,
1228                                              bool global)
1229     : DeclarationDefinitionCommand(id),
1230       d_func(func),
1231       d_formals(),
1232       d_formula(formula),
1233       d_global(global)
1234 {
1235 }
1236
1237 DefineFunctionCommand::DefineFunctionCommand(
1238     const std::string& id,
1239     api::Term func,
1240     const std::vector<api::Term>& formals,
1241     api::Term formula,
1242     bool global)
1243     : DeclarationDefinitionCommand(id),
1244       d_func(func),
1245       d_formals(formals),
1246       d_formula(formula),
1247       d_global(global)
1248 {
1249 }
1250
1251 api::Term DefineFunctionCommand::getFunction() const { return d_func; }
1252 const std::vector<api::Term>& DefineFunctionCommand::getFormals() const
1253 {
1254   return d_formals;
1255 }
1256
1257 api::Term DefineFunctionCommand::getFormula() const { return d_formula; }
1258 void DefineFunctionCommand::invoke(api::Solver* solver)
1259 {
1260   try
1261   {
1262     if (!d_func.isNull())
1263     {
1264       solver->defineFun(d_func, d_formals, d_formula, d_global);
1265     }
1266     d_commandStatus = CommandSuccess::instance();
1267   }
1268   catch (exception& e)
1269   {
1270     d_commandStatus = new CommandFailure(e.what());
1271   }
1272 }
1273
1274 Command* DefineFunctionCommand::clone() const
1275 {
1276   return new DefineFunctionCommand(
1277       d_symbol, d_func, d_formals, d_formula, d_global);
1278 }
1279
1280 std::string DefineFunctionCommand::getCommandName() const
1281 {
1282   return "define-fun";
1283 }
1284
1285 void DefineFunctionCommand::toStream(std::ostream& out,
1286                                      int toDepth,
1287                                      bool types,
1288                                      size_t dag,
1289                                      OutputLanguage language) const
1290 {
1291   Printer::getPrinter(language)->toStreamCmdDefineFunction(
1292       out,
1293       d_func.toString(),
1294       api::termVectorToNodes(d_formals),
1295       d_func.getNode().getType().getRangeType(),
1296       d_formula.getNode());
1297 }
1298
1299 /* -------------------------------------------------------------------------- */
1300 /* class DefineNamedFunctionCommand                                           */
1301 /* -------------------------------------------------------------------------- */
1302
1303 DefineNamedFunctionCommand::DefineNamedFunctionCommand(
1304
1305     const std::string& id,
1306     api::Term func,
1307     const std::vector<api::Term>& formals,
1308     api::Term formula,
1309     bool global)
1310     : DefineFunctionCommand(id, func, formals, formula, global)
1311 {
1312 }
1313
1314 void DefineNamedFunctionCommand::invoke(api::Solver* solver)
1315 {
1316   this->DefineFunctionCommand::invoke(solver);
1317   if (!d_func.isNull() && d_func.getSort().isBoolean())
1318   {
1319     solver->getSmtEngine()->addToAssignment(d_func.getExpr());
1320   }
1321   d_commandStatus = CommandSuccess::instance();
1322 }
1323
1324 Command* DefineNamedFunctionCommand::clone() const
1325 {
1326   return new DefineNamedFunctionCommand(
1327       d_symbol, d_func, d_formals, d_formula, d_global);
1328 }
1329
1330 void DefineNamedFunctionCommand::toStream(std::ostream& out,
1331                                           int toDepth,
1332                                           bool types,
1333                                           size_t dag,
1334                                           OutputLanguage language) const
1335 {
1336   Printer::getPrinter(language)->toStreamCmdDefineNamedFunction(
1337       out,
1338       d_func.toString(),
1339       api::termVectorToNodes(d_formals),
1340       TypeNode::fromType(d_func.getSort().getFunctionCodomainSort().getType()),
1341       d_formula.getNode());
1342 }
1343
1344 /* -------------------------------------------------------------------------- */
1345 /* class DefineFunctionRecCommand                                             */
1346 /* -------------------------------------------------------------------------- */
1347
1348 DefineFunctionRecCommand::DefineFunctionRecCommand(
1349
1350     api::Term func,
1351     const std::vector<api::Term>& formals,
1352     api::Term formula,
1353     bool global)
1354     : d_global(global)
1355 {
1356   d_funcs.push_back(func);
1357   d_formals.push_back(formals);
1358   d_formulas.push_back(formula);
1359 }
1360
1361 DefineFunctionRecCommand::DefineFunctionRecCommand(
1362
1363     const std::vector<api::Term>& funcs,
1364     const std::vector<std::vector<api::Term>>& formals,
1365     const std::vector<api::Term>& formulas,
1366     bool global)
1367     : d_funcs(funcs), d_formals(formals), d_formulas(formulas), d_global(global)
1368 {
1369 }
1370
1371 const std::vector<api::Term>& DefineFunctionRecCommand::getFunctions() const
1372 {
1373   return d_funcs;
1374 }
1375
1376 const std::vector<std::vector<api::Term>>&
1377 DefineFunctionRecCommand::getFormals() const
1378 {
1379   return d_formals;
1380 }
1381
1382 const std::vector<api::Term>& DefineFunctionRecCommand::getFormulas() const
1383 {
1384   return d_formulas;
1385 }
1386
1387 void DefineFunctionRecCommand::invoke(api::Solver* solver)
1388 {
1389   try
1390   {
1391     solver->defineFunsRec(d_funcs, d_formals, d_formulas, d_global);
1392     d_commandStatus = CommandSuccess::instance();
1393   }
1394   catch (exception& e)
1395   {
1396     d_commandStatus = new CommandFailure(e.what());
1397   }
1398 }
1399
1400 Command* DefineFunctionRecCommand::clone() const
1401 {
1402   return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas, d_global);
1403 }
1404
1405 std::string DefineFunctionRecCommand::getCommandName() const
1406 {
1407   return "define-fun-rec";
1408 }
1409
1410 void DefineFunctionRecCommand::toStream(std::ostream& out,
1411                                         int toDepth,
1412                                         bool types,
1413                                         size_t dag,
1414                                         OutputLanguage language) const
1415 {
1416   std::vector<std::vector<Node>> formals;
1417   formals.reserve(d_formals.size());
1418   for (const std::vector<api::Term>& formal : d_formals)
1419   {
1420     formals.push_back(api::termVectorToNodes(formal));
1421   }
1422
1423   Printer::getPrinter(language)->toStreamCmdDefineFunctionRec(
1424       out,
1425       api::termVectorToNodes(d_funcs),
1426       formals,
1427       api::termVectorToNodes(d_formulas));
1428 }
1429
1430 /* -------------------------------------------------------------------------- */
1431 /* class SetUserAttribute                                                     */
1432 /* -------------------------------------------------------------------------- */
1433
1434 SetUserAttributeCommand::SetUserAttributeCommand(
1435     const std::string& attr,
1436     api::Term term,
1437     const std::vector<api::Term>& termValues,
1438     const std::string& strValue)
1439     : d_attr(attr), d_term(term), d_termValues(termValues), d_strValue(strValue)
1440 {
1441 }
1442
1443 SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
1444                                                  api::Term term)
1445     : SetUserAttributeCommand(attr, term, {}, "")
1446 {
1447 }
1448
1449 SetUserAttributeCommand::SetUserAttributeCommand(
1450     const std::string& attr,
1451     api::Term term,
1452     const std::vector<api::Term>& values)
1453     : SetUserAttributeCommand(attr, term, values, "")
1454 {
1455 }
1456
1457 SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
1458                                                  api::Term term,
1459                                                  const std::string& value)
1460     : SetUserAttributeCommand(attr, term, {}, value)
1461 {
1462 }
1463
1464 void SetUserAttributeCommand::invoke(api::Solver* solver)
1465 {
1466   try
1467   {
1468     if (!d_term.isNull())
1469     {
1470       solver->getSmtEngine()->setUserAttribute(
1471           d_attr,
1472           d_term.getExpr(),
1473           api::termVectorToExprs(d_termValues),
1474           d_strValue);
1475     }
1476     d_commandStatus = CommandSuccess::instance();
1477   }
1478   catch (exception& e)
1479   {
1480     d_commandStatus = new CommandFailure(e.what());
1481   }
1482 }
1483
1484 Command* SetUserAttributeCommand::clone() const
1485 {
1486   return new SetUserAttributeCommand(d_attr, d_term, d_termValues, d_strValue);
1487 }
1488
1489 std::string SetUserAttributeCommand::getCommandName() const
1490 {
1491   return "set-user-attribute";
1492 }
1493
1494 void SetUserAttributeCommand::toStream(std::ostream& out,
1495                                        int toDepth,
1496                                        bool types,
1497                                        size_t dag,
1498                                        OutputLanguage language) const
1499 {
1500   Printer::getPrinter(language)->toStreamCmdSetUserAttribute(
1501       out, d_attr, d_term.getNode());
1502 }
1503
1504 /* -------------------------------------------------------------------------- */
1505 /* class SimplifyCommand                                                      */
1506 /* -------------------------------------------------------------------------- */
1507
1508 SimplifyCommand::SimplifyCommand(api::Term term) : d_term(term) {}
1509 api::Term SimplifyCommand::getTerm() const { return d_term; }
1510 void SimplifyCommand::invoke(api::Solver* solver)
1511 {
1512   try
1513   {
1514     d_result = solver->simplify(d_term);
1515     d_commandStatus = CommandSuccess::instance();
1516   }
1517   catch (UnsafeInterruptException& e)
1518   {
1519     d_commandStatus = new CommandInterrupted();
1520   }
1521   catch (exception& e)
1522   {
1523     d_commandStatus = new CommandFailure(e.what());
1524   }
1525 }
1526
1527 api::Term SimplifyCommand::getResult() const { return d_result; }
1528 void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const
1529 {
1530   if (!ok())
1531   {
1532     this->Command::printResult(out, verbosity);
1533   }
1534   else
1535   {
1536     out << d_result << endl;
1537   }
1538 }
1539
1540 Command* SimplifyCommand::clone() const
1541 {
1542   SimplifyCommand* c = new SimplifyCommand(d_term);
1543   c->d_result = d_result;
1544   return c;
1545 }
1546
1547 std::string SimplifyCommand::getCommandName() const { return "simplify"; }
1548
1549 void SimplifyCommand::toStream(std::ostream& out,
1550                                int toDepth,
1551                                bool types,
1552                                size_t dag,
1553                                OutputLanguage language) const
1554 {
1555   Printer::getPrinter(language)->toStreamCmdSimplify(out, d_term.getNode());
1556 }
1557
1558 /* -------------------------------------------------------------------------- */
1559 /* class GetValueCommand                                                      */
1560 /* -------------------------------------------------------------------------- */
1561
1562 GetValueCommand::GetValueCommand(api::Term term) : d_terms()
1563 {
1564   d_terms.push_back(term);
1565 }
1566
1567 GetValueCommand::GetValueCommand(const std::vector<api::Term>& terms)
1568     : d_terms(terms)
1569 {
1570   PrettyCheckArgument(
1571       terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
1572 }
1573
1574 const std::vector<api::Term>& GetValueCommand::getTerms() const
1575 {
1576   return d_terms;
1577 }
1578 void GetValueCommand::invoke(api::Solver* solver)
1579 {
1580   try
1581   {
1582     std::vector<api::Term> result = solver->getValue(d_terms);
1583     Assert(result.size() == d_terms.size());
1584     for (int i = 0, size = d_terms.size(); i < size; i++)
1585     {
1586       api::Term request = d_terms[i];
1587       api::Term value = result[i];
1588       if (value.getSort().isInteger()
1589           && request.getSort() == solver->getRealSort())
1590       {
1591         // Need to wrap in division-by-one so that output printers know this
1592         // is an integer-looking constant that really should be output as
1593         // a rational.  Necessary for SMT-LIB standards compliance.
1594         value = solver->mkTerm(api::DIVISION, value, solver->mkReal(1));
1595       }
1596       result[i] = solver->mkTerm(api::SEXPR, request, value);
1597     }
1598     d_result = solver->mkTerm(api::SEXPR, result);
1599     d_commandStatus = CommandSuccess::instance();
1600   }
1601   catch (api::CVC4ApiRecoverableException& e)
1602   {
1603     d_commandStatus = new CommandRecoverableFailure(e.what());
1604   }
1605   catch (UnsafeInterruptException& e)
1606   {
1607     d_commandStatus = new CommandInterrupted();
1608   }
1609   catch (exception& e)
1610   {
1611     d_commandStatus = new CommandFailure(e.what());
1612   }
1613 }
1614
1615 api::Term GetValueCommand::getResult() const { return d_result; }
1616 void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
1617 {
1618   if (!ok())
1619   {
1620     this->Command::printResult(out, verbosity);
1621   }
1622   else
1623   {
1624     expr::ExprDag::Scope scope(out, false);
1625     out << d_result << endl;
1626   }
1627 }
1628
1629 Command* GetValueCommand::clone() const
1630 {
1631   GetValueCommand* c = new GetValueCommand(d_terms);
1632   c->d_result = d_result;
1633   return c;
1634 }
1635
1636 std::string GetValueCommand::getCommandName() const { return "get-value"; }
1637
1638 void GetValueCommand::toStream(std::ostream& out,
1639                                int toDepth,
1640                                bool types,
1641                                size_t dag,
1642                                OutputLanguage language) const
1643 {
1644   Printer::getPrinter(language)->toStreamCmdGetValue(
1645       out, api::termVectorToNodes(d_terms));
1646 }
1647
1648 /* -------------------------------------------------------------------------- */
1649 /* class GetAssignmentCommand                                                 */
1650 /* -------------------------------------------------------------------------- */
1651
1652 GetAssignmentCommand::GetAssignmentCommand() {}
1653 void GetAssignmentCommand::invoke(api::Solver* solver)
1654 {
1655   try
1656   {
1657     std::vector<std::pair<Expr, Expr>> assignments =
1658         solver->getSmtEngine()->getAssignment();
1659     vector<SExpr> sexprs;
1660     for (const auto& p : assignments)
1661     {
1662       vector<SExpr> v;
1663       v.emplace_back(SExpr::Keyword(p.first.toString()));
1664       v.emplace_back(SExpr::Keyword(p.second.toString()));
1665       sexprs.emplace_back(v);
1666     }
1667     d_result = SExpr(sexprs);
1668     d_commandStatus = CommandSuccess::instance();
1669   }
1670   catch (RecoverableModalException& e)
1671   {
1672     d_commandStatus = new CommandRecoverableFailure(e.what());
1673   }
1674   catch (UnsafeInterruptException& e)
1675   {
1676     d_commandStatus = new CommandInterrupted();
1677   }
1678   catch (exception& e)
1679   {
1680     d_commandStatus = new CommandFailure(e.what());
1681   }
1682 }
1683
1684 SExpr GetAssignmentCommand::getResult() const { return d_result; }
1685 void GetAssignmentCommand::printResult(std::ostream& out,
1686                                        uint32_t verbosity) const
1687 {
1688   if (!ok())
1689   {
1690     this->Command::printResult(out, verbosity);
1691   }
1692   else
1693   {
1694     out << d_result << endl;
1695   }
1696 }
1697
1698 Command* GetAssignmentCommand::clone() const
1699 {
1700   GetAssignmentCommand* c = new GetAssignmentCommand();
1701   c->d_result = d_result;
1702   return c;
1703 }
1704
1705 std::string GetAssignmentCommand::getCommandName() const
1706 {
1707   return "get-assignment";
1708 }
1709
1710 void GetAssignmentCommand::toStream(std::ostream& out,
1711                                     int toDepth,
1712                                     bool types,
1713                                     size_t dag,
1714                                     OutputLanguage language) const
1715 {
1716   Printer::getPrinter(language)->toStreamCmdGetAssignment(out);
1717 }
1718
1719 /* -------------------------------------------------------------------------- */
1720 /* class GetModelCommand                                                      */
1721 /* -------------------------------------------------------------------------- */
1722
1723 GetModelCommand::GetModelCommand() : d_result(nullptr) {}
1724 void GetModelCommand::invoke(api::Solver* solver)
1725 {
1726   try
1727   {
1728     d_result = solver->getSmtEngine()->getModel();
1729     d_commandStatus = CommandSuccess::instance();
1730   }
1731   catch (RecoverableModalException& e)
1732   {
1733     d_commandStatus = new CommandRecoverableFailure(e.what());
1734   }
1735   catch (UnsafeInterruptException& e)
1736   {
1737     d_commandStatus = new CommandInterrupted();
1738   }
1739   catch (exception& e)
1740   {
1741     d_commandStatus = new CommandFailure(e.what());
1742   }
1743 }
1744
1745 /* Model is private to the library -- for now
1746 Model* GetModelCommand::getResult() const  {
1747   return d_result;
1748 }
1749 */
1750
1751 void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
1752 {
1753   if (!ok())
1754   {
1755     this->Command::printResult(out, verbosity);
1756   }
1757   else
1758   {
1759     out << *d_result;
1760   }
1761 }
1762
1763 Command* GetModelCommand::clone() const
1764 {
1765   GetModelCommand* c = new GetModelCommand();
1766   c->d_result = d_result;
1767   return c;
1768 }
1769
1770 std::string GetModelCommand::getCommandName() const { return "get-model"; }
1771
1772 void GetModelCommand::toStream(std::ostream& out,
1773                                int toDepth,
1774                                bool types,
1775                                size_t dag,
1776                                OutputLanguage language) const
1777 {
1778   Printer::getPrinter(language)->toStreamCmdGetModel(out);
1779 }
1780
1781 /* -------------------------------------------------------------------------- */
1782 /* class BlockModelCommand */
1783 /* -------------------------------------------------------------------------- */
1784
1785 BlockModelCommand::BlockModelCommand() {}
1786 void BlockModelCommand::invoke(api::Solver* solver)
1787 {
1788   try
1789   {
1790     solver->blockModel();
1791     d_commandStatus = CommandSuccess::instance();
1792   }
1793   catch (api::CVC4ApiRecoverableException& e)
1794   {
1795     d_commandStatus = new CommandRecoverableFailure(e.what());
1796   }
1797   catch (UnsafeInterruptException& e)
1798   {
1799     d_commandStatus = new CommandInterrupted();
1800   }
1801   catch (exception& e)
1802   {
1803     d_commandStatus = new CommandFailure(e.what());
1804   }
1805 }
1806
1807 Command* BlockModelCommand::clone() const
1808 {
1809   BlockModelCommand* c = new BlockModelCommand();
1810   return c;
1811 }
1812
1813 std::string BlockModelCommand::getCommandName() const { return "block-model"; }
1814
1815 void BlockModelCommand::toStream(std::ostream& out,
1816                                  int toDepth,
1817                                  bool types,
1818                                  size_t dag,
1819                                  OutputLanguage language) const
1820 {
1821   Printer::getPrinter(language)->toStreamCmdBlockModel(out);
1822 }
1823
1824 /* -------------------------------------------------------------------------- */
1825 /* class BlockModelValuesCommand */
1826 /* -------------------------------------------------------------------------- */
1827
1828 BlockModelValuesCommand::BlockModelValuesCommand(
1829     const std::vector<api::Term>& terms)
1830     : d_terms(terms)
1831 {
1832   PrettyCheckArgument(terms.size() >= 1,
1833                       terms,
1834                       "cannot block-model-values of an empty set of terms");
1835 }
1836
1837 const std::vector<api::Term>& BlockModelValuesCommand::getTerms() const
1838 {
1839   return d_terms;
1840 }
1841 void BlockModelValuesCommand::invoke(api::Solver* solver)
1842 {
1843   try
1844   {
1845     solver->blockModelValues(d_terms);
1846     d_commandStatus = CommandSuccess::instance();
1847   }
1848   catch (RecoverableModalException& e)
1849   {
1850     d_commandStatus = new CommandRecoverableFailure(e.what());
1851   }
1852   catch (UnsafeInterruptException& e)
1853   {
1854     d_commandStatus = new CommandInterrupted();
1855   }
1856   catch (exception& e)
1857   {
1858     d_commandStatus = new CommandFailure(e.what());
1859   }
1860 }
1861
1862 Command* BlockModelValuesCommand::clone() const
1863 {
1864   BlockModelValuesCommand* c = new BlockModelValuesCommand(d_terms);
1865   return c;
1866 }
1867
1868 std::string BlockModelValuesCommand::getCommandName() const
1869 {
1870   return "block-model-values";
1871 }
1872
1873 void BlockModelValuesCommand::toStream(std::ostream& out,
1874                                        int toDepth,
1875                                        bool types,
1876                                        size_t dag,
1877                                        OutputLanguage language) const
1878 {
1879   Printer::getPrinter(language)->toStreamCmdBlockModelValues(
1880       out, api::termVectorToNodes(d_terms));
1881 }
1882
1883 /* -------------------------------------------------------------------------- */
1884 /* class GetProofCommand                                                      */
1885 /* -------------------------------------------------------------------------- */
1886
1887 GetProofCommand::GetProofCommand() {}
1888 void GetProofCommand::invoke(api::Solver* solver)
1889 {
1890   Unimplemented() << "Unimplemented get-proof\n";
1891 }
1892
1893 Command* GetProofCommand::clone() const
1894 {
1895   GetProofCommand* c = new GetProofCommand();
1896   return c;
1897 }
1898
1899 std::string GetProofCommand::getCommandName() const { return "get-proof"; }
1900
1901 void GetProofCommand::toStream(std::ostream& out,
1902                                int toDepth,
1903                                bool types,
1904                                size_t dag,
1905                                OutputLanguage language) const
1906 {
1907   Printer::getPrinter(language)->toStreamCmdGetProof(out);
1908 }
1909
1910 /* -------------------------------------------------------------------------- */
1911 /* class GetInstantiationsCommand                                             */
1912 /* -------------------------------------------------------------------------- */
1913
1914 GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {}
1915 void GetInstantiationsCommand::invoke(api::Solver* solver)
1916 {
1917   try
1918   {
1919     d_solver = solver;
1920     d_commandStatus = CommandSuccess::instance();
1921   }
1922   catch (exception& e)
1923   {
1924     d_commandStatus = new CommandFailure(e.what());
1925   }
1926 }
1927
1928 void GetInstantiationsCommand::printResult(std::ostream& out,
1929                                            uint32_t verbosity) const
1930 {
1931   if (!ok())
1932   {
1933     this->Command::printResult(out, verbosity);
1934   }
1935   else
1936   {
1937     d_solver->printInstantiations(out);
1938   }
1939 }
1940
1941 Command* GetInstantiationsCommand::clone() const
1942 {
1943   GetInstantiationsCommand* c = new GetInstantiationsCommand();
1944   // c->d_result = d_result;
1945   c->d_solver = d_solver;
1946   return c;
1947 }
1948
1949 std::string GetInstantiationsCommand::getCommandName() const
1950 {
1951   return "get-instantiations";
1952 }
1953
1954 void GetInstantiationsCommand::toStream(std::ostream& out,
1955                                         int toDepth,
1956                                         bool types,
1957                                         size_t dag,
1958                                         OutputLanguage language) const
1959 {
1960   Printer::getPrinter(language)->toStreamCmdGetInstantiations(out);
1961 }
1962
1963 /* -------------------------------------------------------------------------- */
1964 /* class GetSynthSolutionCommand                                              */
1965 /* -------------------------------------------------------------------------- */
1966
1967 GetSynthSolutionCommand::GetSynthSolutionCommand() : d_solver(nullptr) {}
1968 void GetSynthSolutionCommand::invoke(api::Solver* solver)
1969 {
1970   try
1971   {
1972     d_solver = solver;
1973     d_commandStatus = CommandSuccess::instance();
1974   }
1975   catch (exception& e)
1976   {
1977     d_commandStatus = new CommandFailure(e.what());
1978   }
1979 }
1980
1981 void GetSynthSolutionCommand::printResult(std::ostream& out,
1982                                           uint32_t verbosity) const
1983 {
1984   if (!ok())
1985   {
1986     this->Command::printResult(out, verbosity);
1987   }
1988   else
1989   {
1990     d_solver->printSynthSolution(out);
1991   }
1992 }
1993
1994 Command* GetSynthSolutionCommand::clone() const
1995 {
1996   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
1997   c->d_solver = d_solver;
1998   return c;
1999 }
2000
2001 std::string GetSynthSolutionCommand::getCommandName() const
2002 {
2003   return "get-synth-solution";
2004 }
2005
2006 void GetSynthSolutionCommand::toStream(std::ostream& out,
2007                                        int toDepth,
2008                                        bool types,
2009                                        size_t dag,
2010                                        OutputLanguage language) const
2011 {
2012   Printer::getPrinter(language)->toStreamCmdGetSynthSolution(out);
2013 }
2014
2015 /* -------------------------------------------------------------------------- */
2016 /* class GetInterpolCommand                                                   */
2017 /* -------------------------------------------------------------------------- */
2018
2019 GetInterpolCommand::GetInterpolCommand(const std::string& name, api::Term conj)
2020     : d_name(name), d_conj(conj), d_resultStatus(false)
2021 {
2022 }
2023 GetInterpolCommand::GetInterpolCommand(const std::string& name,
2024                                        api::Term conj,
2025                                        api::Grammar* g)
2026     : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false)
2027 {
2028 }
2029
2030 api::Term GetInterpolCommand::getConjecture() const { return d_conj; }
2031
2032 const api::Grammar* GetInterpolCommand::getGrammar() const
2033 {
2034   return d_sygus_grammar;
2035 }
2036
2037 api::Term GetInterpolCommand::getResult() const { return d_result; }
2038
2039 void GetInterpolCommand::invoke(api::Solver* solver)
2040 {
2041   try
2042   {
2043     if (d_sygus_grammar == nullptr)
2044     {
2045       d_resultStatus = solver->getInterpolant(d_conj, d_result);
2046     }
2047     else
2048     {
2049       d_resultStatus =
2050           solver->getInterpolant(d_conj, *d_sygus_grammar, d_result);
2051     }
2052     d_commandStatus = CommandSuccess::instance();
2053   }
2054   catch (exception& e)
2055   {
2056     d_commandStatus = new CommandFailure(e.what());
2057   }
2058 }
2059
2060 void GetInterpolCommand::printResult(std::ostream& out,
2061                                      uint32_t verbosity) const
2062 {
2063   if (!ok())
2064   {
2065     this->Command::printResult(out, verbosity);
2066   }
2067   else
2068   {
2069     expr::ExprDag::Scope scope(out, false);
2070     if (d_resultStatus)
2071     {
2072       out << "(define-fun " << d_name << " () Bool " << d_result << ")"
2073           << std::endl;
2074     }
2075     else
2076     {
2077       out << "none" << std::endl;
2078     }
2079   }
2080 }
2081
2082 Command* GetInterpolCommand::clone() const
2083 {
2084   GetInterpolCommand* c =
2085       new GetInterpolCommand(d_name, d_conj, d_sygus_grammar);
2086   c->d_result = d_result;
2087   c->d_resultStatus = d_resultStatus;
2088   return c;
2089 }
2090
2091 std::string GetInterpolCommand::getCommandName() const
2092 {
2093   return "get-interpol";
2094 }
2095
2096 void GetInterpolCommand::toStream(std::ostream& out,
2097                                   int toDepth,
2098                                   bool types,
2099                                   size_t dag,
2100                                   OutputLanguage language) const
2101 {
2102   Printer::getPrinter(language)->toStreamCmdGetInterpol(
2103       out,
2104       d_name,
2105       d_conj.getNode(),
2106       TypeNode::fromType(d_sygus_grammar->resolve().getType()));
2107 }
2108
2109 /* -------------------------------------------------------------------------- */
2110 /* class GetAbductCommand                                                     */
2111 /* -------------------------------------------------------------------------- */
2112
2113 GetAbductCommand::GetAbductCommand(const std::string& name, api::Term conj)
2114     : d_name(name), d_conj(conj), d_resultStatus(false)
2115 {
2116 }
2117 GetAbductCommand::GetAbductCommand(const std::string& name,
2118                                    api::Term conj,
2119                                    api::Grammar* g)
2120     : d_name(name), d_conj(conj), d_sygus_grammar(g), d_resultStatus(false)
2121 {
2122 }
2123
2124 api::Term GetAbductCommand::getConjecture() const { return d_conj; }
2125
2126 const api::Grammar* GetAbductCommand::getGrammar() const
2127 {
2128   return d_sygus_grammar;
2129 }
2130
2131 std::string GetAbductCommand::getAbductName() const { return d_name; }
2132 api::Term GetAbductCommand::getResult() const { return d_result; }
2133
2134 void GetAbductCommand::invoke(api::Solver* solver)
2135 {
2136   try
2137   {
2138     if (d_sygus_grammar == nullptr)
2139     {
2140       d_resultStatus = solver->getAbduct(d_conj, d_result);
2141     }
2142     else
2143     {
2144       d_resultStatus = solver->getAbduct(d_conj, *d_sygus_grammar, d_result);
2145     }
2146     d_commandStatus = CommandSuccess::instance();
2147   }
2148   catch (exception& e)
2149   {
2150     d_commandStatus = new CommandFailure(e.what());
2151   }
2152 }
2153
2154 void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const
2155 {
2156   if (!ok())
2157   {
2158     this->Command::printResult(out, verbosity);
2159   }
2160   else
2161   {
2162     expr::ExprDag::Scope scope(out, false);
2163     if (d_resultStatus)
2164     {
2165       out << "(define-fun " << d_name << " () Bool " << d_result << ")"
2166           << std::endl;
2167     }
2168     else
2169     {
2170       out << "none" << std::endl;
2171     }
2172   }
2173 }
2174
2175 Command* GetAbductCommand::clone() const
2176 {
2177   GetAbductCommand* c = new GetAbductCommand(d_name, d_conj, d_sygus_grammar);
2178   c->d_result = d_result;
2179   c->d_resultStatus = d_resultStatus;
2180   return c;
2181 }
2182
2183 std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
2184
2185 void GetAbductCommand::toStream(std::ostream& out,
2186                                 int toDepth,
2187                                 bool types,
2188                                 size_t dag,
2189                                 OutputLanguage language) const
2190 {
2191   Printer::getPrinter(language)->toStreamCmdGetAbduct(
2192       out,
2193       d_name,
2194       d_conj.getNode(),
2195       TypeNode::fromType(d_sygus_grammar->resolve().getType()));
2196 }
2197
2198 /* -------------------------------------------------------------------------- */
2199 /* class GetQuantifierEliminationCommand                                      */
2200 /* -------------------------------------------------------------------------- */
2201
2202 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand()
2203     : d_term(), d_doFull(true)
2204 {
2205 }
2206 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
2207     const api::Term& term, bool doFull)
2208     : d_term(term), d_doFull(doFull)
2209 {
2210 }
2211
2212 api::Term GetQuantifierEliminationCommand::getTerm() const { return d_term; }
2213 bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
2214 void GetQuantifierEliminationCommand::invoke(api::Solver* solver)
2215 {
2216   try
2217   {
2218     if (d_doFull)
2219     {
2220       d_result = solver->getQuantifierElimination(d_term);
2221     }
2222     else
2223     {
2224       d_result = solver->getQuantifierEliminationDisjunct(d_term);
2225     }
2226     d_commandStatus = CommandSuccess::instance();
2227   }
2228   catch (exception& e)
2229   {
2230     d_commandStatus = new CommandFailure(e.what());
2231   }
2232 }
2233
2234 api::Term GetQuantifierEliminationCommand::getResult() const
2235 {
2236   return d_result;
2237 }
2238 void GetQuantifierEliminationCommand::printResult(std::ostream& out,
2239                                                   uint32_t verbosity) const
2240 {
2241   if (!ok())
2242   {
2243     this->Command::printResult(out, verbosity);
2244   }
2245   else
2246   {
2247     out << d_result << endl;
2248   }
2249 }
2250
2251 Command* GetQuantifierEliminationCommand::clone() const
2252 {
2253   GetQuantifierEliminationCommand* c =
2254       new GetQuantifierEliminationCommand(d_term, d_doFull);
2255   c->d_result = d_result;
2256   return c;
2257 }
2258
2259 std::string GetQuantifierEliminationCommand::getCommandName() const
2260 {
2261   return d_doFull ? "get-qe" : "get-qe-disjunct";
2262 }
2263
2264 void GetQuantifierEliminationCommand::toStream(std::ostream& out,
2265                                                int toDepth,
2266                                                bool types,
2267                                                size_t dag,
2268                                                OutputLanguage language) const
2269 {
2270   Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination(
2271       out, d_term.getNode());
2272 }
2273
2274 /* -------------------------------------------------------------------------- */
2275 /* class GetUnsatAssumptionsCommand                                           */
2276 /* -------------------------------------------------------------------------- */
2277
2278 GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
2279
2280 void GetUnsatAssumptionsCommand::invoke(api::Solver* solver)
2281 {
2282   try
2283   {
2284     d_result = solver->getUnsatAssumptions();
2285     d_commandStatus = CommandSuccess::instance();
2286   }
2287   catch (api::CVC4ApiRecoverableException& e)
2288   {
2289     d_commandStatus = new CommandRecoverableFailure(e.what());
2290   }
2291   catch (exception& e)
2292   {
2293     d_commandStatus = new CommandFailure(e.what());
2294   }
2295 }
2296
2297 std::vector<api::Term> GetUnsatAssumptionsCommand::getResult() const
2298 {
2299   return d_result;
2300 }
2301
2302 void GetUnsatAssumptionsCommand::printResult(std::ostream& out,
2303                                              uint32_t verbosity) const
2304 {
2305   if (!ok())
2306   {
2307     this->Command::printResult(out, verbosity);
2308   }
2309   else
2310   {
2311     container_to_stream(out, d_result, "(", ")\n", " ");
2312   }
2313 }
2314
2315 Command* GetUnsatAssumptionsCommand::clone() const
2316 {
2317   GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
2318   c->d_result = d_result;
2319   return c;
2320 }
2321
2322 std::string GetUnsatAssumptionsCommand::getCommandName() const
2323 {
2324   return "get-unsat-assumptions";
2325 }
2326
2327 void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
2328                                           int toDepth,
2329                                           bool types,
2330                                           size_t dag,
2331                                           OutputLanguage language) const
2332 {
2333   Printer::getPrinter(language)->toStreamCmdGetUnsatAssumptions(out);
2334 }
2335
2336 /* -------------------------------------------------------------------------- */
2337 /* class GetUnsatCoreCommand                                                  */
2338 /* -------------------------------------------------------------------------- */
2339
2340 GetUnsatCoreCommand::GetUnsatCoreCommand() {}
2341 void GetUnsatCoreCommand::invoke(api::Solver* solver)
2342 {
2343   try
2344   {
2345     d_solver = solver;
2346     d_result = solver->getUnsatCore();
2347
2348     d_commandStatus = CommandSuccess::instance();
2349   }
2350   catch (api::CVC4ApiRecoverableException& e)
2351   {
2352     d_commandStatus = new CommandRecoverableFailure(e.what());
2353   }
2354   catch (exception& e)
2355   {
2356     d_commandStatus = new CommandFailure(e.what());
2357   }
2358 }
2359
2360 void GetUnsatCoreCommand::printResult(std::ostream& out,
2361                                       uint32_t verbosity) const
2362 {
2363   if (!ok())
2364   {
2365     this->Command::printResult(out, verbosity);
2366   }
2367   else
2368   {
2369     UnsatCore ucr(d_solver->getSmtEngine(), api::termVectorToNodes(d_result));
2370     ucr.toStream(out);
2371   }
2372 }
2373
2374 const std::vector<api::Term>& GetUnsatCoreCommand::getUnsatCore() const
2375 {
2376   // of course, this will be empty if the command hasn't been invoked yet
2377   return d_result;
2378 }
2379
2380 Command* GetUnsatCoreCommand::clone() const
2381 {
2382   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
2383   c->d_solver = d_solver;
2384   c->d_result = d_result;
2385   return c;
2386 }
2387
2388 std::string GetUnsatCoreCommand::getCommandName() const
2389 {
2390   return "get-unsat-core";
2391 }
2392
2393 void GetUnsatCoreCommand::toStream(std::ostream& out,
2394                                    int toDepth,
2395                                    bool types,
2396                                    size_t dag,
2397                                    OutputLanguage language) const
2398 {
2399   Printer::getPrinter(language)->toStreamCmdGetUnsatCore(out);
2400 }
2401
2402 /* -------------------------------------------------------------------------- */
2403 /* class GetAssertionsCommand                                                 */
2404 /* -------------------------------------------------------------------------- */
2405
2406 GetAssertionsCommand::GetAssertionsCommand() {}
2407 void GetAssertionsCommand::invoke(api::Solver* solver)
2408 {
2409   try
2410   {
2411     stringstream ss;
2412     const vector<api::Term> v = solver->getAssertions();
2413     ss << "(\n";
2414     copy(v.begin(), v.end(), ostream_iterator<api::Term>(ss, "\n"));
2415     ss << ")\n";
2416     d_result = ss.str();
2417     d_commandStatus = CommandSuccess::instance();
2418   }
2419   catch (exception& e)
2420   {
2421     d_commandStatus = new CommandFailure(e.what());
2422   }
2423 }
2424
2425 std::string GetAssertionsCommand::getResult() const { return d_result; }
2426 void GetAssertionsCommand::printResult(std::ostream& out,
2427                                        uint32_t verbosity) const
2428 {
2429   if (!ok())
2430   {
2431     this->Command::printResult(out, verbosity);
2432   }
2433   else
2434   {
2435     out << d_result;
2436   }
2437 }
2438
2439 Command* GetAssertionsCommand::clone() const
2440 {
2441   GetAssertionsCommand* c = new GetAssertionsCommand();
2442   c->d_result = d_result;
2443   return c;
2444 }
2445
2446 std::string GetAssertionsCommand::getCommandName() const
2447 {
2448   return "get-assertions";
2449 }
2450
2451 void GetAssertionsCommand::toStream(std::ostream& out,
2452                                     int toDepth,
2453                                     bool types,
2454                                     size_t dag,
2455                                     OutputLanguage language) const
2456 {
2457   Printer::getPrinter(language)->toStreamCmdGetAssertions(out);
2458 }
2459
2460 /* -------------------------------------------------------------------------- */
2461 /* class SetBenchmarkStatusCommand                                            */
2462 /* -------------------------------------------------------------------------- */
2463
2464 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status)
2465     : d_status(status)
2466 {
2467 }
2468
2469 BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
2470 {
2471   return d_status;
2472 }
2473
2474 void SetBenchmarkStatusCommand::invoke(api::Solver* solver)
2475 {
2476   try
2477   {
2478     stringstream ss;
2479     ss << d_status;
2480     solver->setInfo("status", ss.str());
2481     d_commandStatus = CommandSuccess::instance();
2482   }
2483   catch (exception& e)
2484   {
2485     d_commandStatus = new CommandFailure(e.what());
2486   }
2487 }
2488
2489 Command* SetBenchmarkStatusCommand::clone() const
2490 {
2491   return new SetBenchmarkStatusCommand(d_status);
2492 }
2493
2494 std::string SetBenchmarkStatusCommand::getCommandName() const
2495 {
2496   return "set-info";
2497 }
2498
2499 void SetBenchmarkStatusCommand::toStream(std::ostream& out,
2500                                          int toDepth,
2501                                          bool types,
2502                                          size_t dag,
2503                                          OutputLanguage language) const
2504 {
2505   Result::Sat status = Result::SAT_UNKNOWN;
2506   switch (d_status)
2507   {
2508     case BenchmarkStatus::SMT_SATISFIABLE: status = Result::SAT; break;
2509     case BenchmarkStatus::SMT_UNSATISFIABLE: status = Result::UNSAT; break;
2510     case BenchmarkStatus::SMT_UNKNOWN: status = Result::SAT_UNKNOWN; break;
2511   }
2512
2513   Printer::getPrinter(language)->toStreamCmdSetBenchmarkStatus(out, status);
2514 }
2515
2516 /* -------------------------------------------------------------------------- */
2517 /* class SetBenchmarkLogicCommand                                             */
2518 /* -------------------------------------------------------------------------- */
2519
2520 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
2521     : d_logic(logic)
2522 {
2523 }
2524
2525 std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
2526 void SetBenchmarkLogicCommand::invoke(api::Solver* solver)
2527 {
2528   try
2529   {
2530     solver->setLogic(d_logic);
2531     d_commandStatus = CommandSuccess::instance();
2532   }
2533   catch (exception& e)
2534   {
2535     d_commandStatus = new CommandFailure(e.what());
2536   }
2537 }
2538
2539 Command* SetBenchmarkLogicCommand::clone() const
2540 {
2541   return new SetBenchmarkLogicCommand(d_logic);
2542 }
2543
2544 std::string SetBenchmarkLogicCommand::getCommandName() const
2545 {
2546   return "set-logic";
2547 }
2548
2549 void SetBenchmarkLogicCommand::toStream(std::ostream& out,
2550                                         int toDepth,
2551                                         bool types,
2552                                         size_t dag,
2553                                         OutputLanguage language) const
2554 {
2555   Printer::getPrinter(language)->toStreamCmdSetBenchmarkLogic(out, d_logic);
2556 }
2557
2558 /* -------------------------------------------------------------------------- */
2559 /* class SetInfoCommand                                                       */
2560 /* -------------------------------------------------------------------------- */
2561
2562 SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
2563     : d_flag(flag), d_sexpr(sexpr)
2564 {
2565 }
2566
2567 std::string SetInfoCommand::getFlag() const { return d_flag; }
2568 SExpr SetInfoCommand::getSExpr() const { return d_sexpr; }
2569 void SetInfoCommand::invoke(api::Solver* solver)
2570 {
2571   try
2572   {
2573     solver->getSmtEngine()->setInfo(d_flag, d_sexpr);
2574     d_commandStatus = CommandSuccess::instance();
2575   }
2576   catch (UnrecognizedOptionException&)
2577   {
2578     // As per SMT-LIB spec, silently accept unknown set-info keys
2579     d_commandStatus = CommandSuccess::instance();
2580   }
2581   catch (exception& e)
2582   {
2583     d_commandStatus = new CommandFailure(e.what());
2584   }
2585 }
2586
2587 Command* SetInfoCommand::clone() const
2588 {
2589   return new SetInfoCommand(d_flag, d_sexpr);
2590 }
2591
2592 std::string SetInfoCommand::getCommandName() const { return "set-info"; }
2593
2594 void SetInfoCommand::toStream(std::ostream& out,
2595                               int toDepth,
2596                               bool types,
2597                               size_t dag,
2598                               OutputLanguage language) const
2599 {
2600   Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_sexpr);
2601 }
2602
2603 /* -------------------------------------------------------------------------- */
2604 /* class GetInfoCommand                                                       */
2605 /* -------------------------------------------------------------------------- */
2606
2607 GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
2608 std::string GetInfoCommand::getFlag() const { return d_flag; }
2609 void GetInfoCommand::invoke(api::Solver* solver)
2610 {
2611   try
2612   {
2613     vector<SExpr> v;
2614     v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
2615     v.emplace_back(solver->getSmtEngine()->getInfo(d_flag));
2616     stringstream ss;
2617     if (d_flag == "all-options" || d_flag == "all-statistics")
2618     {
2619       ss << PrettySExprs(true);
2620     }
2621     ss << SExpr(v);
2622     d_result = ss.str();
2623     d_commandStatus = CommandSuccess::instance();
2624   }
2625   catch (UnrecognizedOptionException&)
2626   {
2627     d_commandStatus = new CommandUnsupported();
2628   }
2629   catch (RecoverableModalException& e)
2630   {
2631     d_commandStatus = new CommandRecoverableFailure(e.what());
2632   }
2633   catch (exception& e)
2634   {
2635     d_commandStatus = new CommandFailure(e.what());
2636   }
2637 }
2638
2639 std::string GetInfoCommand::getResult() const { return d_result; }
2640 void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const
2641 {
2642   if (!ok())
2643   {
2644     this->Command::printResult(out, verbosity);
2645   }
2646   else if (d_result != "")
2647   {
2648     out << d_result << endl;
2649   }
2650 }
2651
2652 Command* GetInfoCommand::clone() const
2653 {
2654   GetInfoCommand* c = new GetInfoCommand(d_flag);
2655   c->d_result = d_result;
2656   return c;
2657 }
2658
2659 std::string GetInfoCommand::getCommandName() const { return "get-info"; }
2660
2661 void GetInfoCommand::toStream(std::ostream& out,
2662                               int toDepth,
2663                               bool types,
2664                               size_t dag,
2665                               OutputLanguage language) const
2666 {
2667   Printer::getPrinter(language)->toStreamCmdGetInfo(out, d_flag);
2668 }
2669
2670 /* -------------------------------------------------------------------------- */
2671 /* class SetOptionCommand                                                     */
2672 /* -------------------------------------------------------------------------- */
2673
2674 SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
2675     : d_flag(flag), d_sexpr(sexpr)
2676 {
2677 }
2678
2679 std::string SetOptionCommand::getFlag() const { return d_flag; }
2680 SExpr SetOptionCommand::getSExpr() const { return d_sexpr; }
2681 void SetOptionCommand::invoke(api::Solver* solver)
2682 {
2683   try
2684   {
2685     solver->getSmtEngine()->setOption(d_flag, d_sexpr);
2686     d_commandStatus = CommandSuccess::instance();
2687   }
2688   catch (UnrecognizedOptionException&)
2689   {
2690     d_commandStatus = new CommandUnsupported();
2691   }
2692   catch (exception& e)
2693   {
2694     d_commandStatus = new CommandFailure(e.what());
2695   }
2696 }
2697
2698 Command* SetOptionCommand::clone() const
2699 {
2700   return new SetOptionCommand(d_flag, d_sexpr);
2701 }
2702
2703 std::string SetOptionCommand::getCommandName() const { return "set-option"; }
2704
2705 void SetOptionCommand::toStream(std::ostream& out,
2706                                 int toDepth,
2707                                 bool types,
2708                                 size_t dag,
2709                                 OutputLanguage language) const
2710 {
2711   Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_sexpr);
2712 }
2713
2714 /* -------------------------------------------------------------------------- */
2715 /* class GetOptionCommand                                                     */
2716 /* -------------------------------------------------------------------------- */
2717
2718 GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
2719 std::string GetOptionCommand::getFlag() const { return d_flag; }
2720 void GetOptionCommand::invoke(api::Solver* solver)
2721 {
2722   try
2723   {
2724     d_result = solver->getOption(d_flag);
2725     d_commandStatus = CommandSuccess::instance();
2726   }
2727   catch (UnrecognizedOptionException&)
2728   {
2729     d_commandStatus = new CommandUnsupported();
2730   }
2731   catch (exception& e)
2732   {
2733     d_commandStatus = new CommandFailure(e.what());
2734   }
2735 }
2736
2737 std::string GetOptionCommand::getResult() const { return d_result; }
2738 void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const
2739 {
2740   if (!ok())
2741   {
2742     this->Command::printResult(out, verbosity);
2743   }
2744   else if (d_result != "")
2745   {
2746     out << d_result << endl;
2747   }
2748 }
2749
2750 Command* GetOptionCommand::clone() const
2751 {
2752   GetOptionCommand* c = new GetOptionCommand(d_flag);
2753   c->d_result = d_result;
2754   return c;
2755 }
2756
2757 std::string GetOptionCommand::getCommandName() const { return "get-option"; }
2758
2759 void GetOptionCommand::toStream(std::ostream& out,
2760                                 int toDepth,
2761                                 bool types,
2762                                 size_t dag,
2763                                 OutputLanguage language) const
2764 {
2765   Printer::getPrinter(language)->toStreamCmdGetOption(out, d_flag);
2766 }
2767
2768 /* -------------------------------------------------------------------------- */
2769 /* class SetExpressionNameCommand                                             */
2770 /* -------------------------------------------------------------------------- */
2771
2772 SetExpressionNameCommand::SetExpressionNameCommand(api::Term term,
2773                                                    std::string name)
2774     : d_term(term), d_name(name)
2775 {
2776 }
2777
2778 void SetExpressionNameCommand::invoke(api::Solver* solver)
2779 {
2780   solver->getSmtEngine()->setExpressionName(d_term.getExpr(), d_name);
2781   d_commandStatus = CommandSuccess::instance();
2782 }
2783
2784 Command* SetExpressionNameCommand::clone() const
2785 {
2786   SetExpressionNameCommand* c = new SetExpressionNameCommand(d_term, d_name);
2787   return c;
2788 }
2789
2790 std::string SetExpressionNameCommand::getCommandName() const
2791 {
2792   return "set-expr-name";
2793 }
2794
2795 void SetExpressionNameCommand::toStream(std::ostream& out,
2796                                         int toDepth,
2797                                         bool types,
2798                                         size_t dag,
2799                                         OutputLanguage language) const
2800 {
2801   Printer::getPrinter(language)->toStreamCmdSetExpressionName(
2802       out, d_term.getNode(), d_name);
2803 }
2804
2805 /* -------------------------------------------------------------------------- */
2806 /* class DatatypeDeclarationCommand                                           */
2807 /* -------------------------------------------------------------------------- */
2808
2809 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
2810     const api::Sort& datatype)
2811     : d_datatypes()
2812 {
2813   d_datatypes.push_back(datatype);
2814 }
2815
2816 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
2817     const std::vector<api::Sort>& datatypes)
2818     : d_datatypes(datatypes)
2819 {
2820 }
2821
2822 const std::vector<api::Sort>& DatatypeDeclarationCommand::getDatatypes() const
2823 {
2824   return d_datatypes;
2825 }
2826
2827 void DatatypeDeclarationCommand::invoke(api::Solver* solver)
2828 {
2829   d_commandStatus = CommandSuccess::instance();
2830 }
2831
2832 Command* DatatypeDeclarationCommand::clone() const
2833 {
2834   return new DatatypeDeclarationCommand(d_datatypes);
2835 }
2836
2837 std::string DatatypeDeclarationCommand::getCommandName() const
2838 {
2839   return "declare-datatypes";
2840 }
2841
2842 void DatatypeDeclarationCommand::toStream(std::ostream& out,
2843                                           int toDepth,
2844                                           bool types,
2845                                           size_t dag,
2846                                           OutputLanguage language) const
2847 {
2848   Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(
2849       out, api::sortVectorToTypeNodes(d_datatypes));
2850 }
2851
2852 }  // namespace CVC4