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