src/smt/command.cpp

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