src/smt/command.cpp

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