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