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