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