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
  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 division-by-one 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.
1414         value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1)));
1415       }
1416       result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr());
1417     }
1418     d_result = em->mkExpr(kind::SEXPR, result);
1419     d_commandStatus = CommandSuccess::instance();
1420   }
1421   catch (RecoverableModalException& e)
1422   {
1423     d_commandStatus = new CommandRecoverableFailure(e.what());
1424   }
1425   catch (UnsafeInterruptException& e)
1426   {
1427     d_commandStatus = new CommandInterrupted();
1428   }
1429   catch (exception& e)
1430   {
1431     d_commandStatus = new CommandFailure(e.what());
1432   }
1433 }
1434
1435 Expr GetValueCommand::getResult() const { return d_result; }
1436 void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
1437 {
1438   if (!ok())
1439   {
1440     this->Command::printResult(out, verbosity);
1441   }
1442   else
1443   {
1444     expr::ExprDag::Scope scope(out, false);
1445     out << d_result << endl;
1446   }
1447 }
1448
1449 Command* GetValueCommand::exportTo(ExprManager* exprManager,
1450                                    ExprManagerMapCollection& variableMap)
1451 {
1452   vector<Expr> exportedTerms;
1453   for (std::vector<Expr>::const_iterator i = d_terms.begin();
1454        i != d_terms.end();
1455        ++i)
1456   {
1457     exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
1458   }
1459   GetValueCommand* c = new GetValueCommand(exportedTerms);
1460   c->d_result = d_result.exportTo(exprManager, variableMap);
1461   return c;
1462 }
1463
1464 Command* GetValueCommand::clone() const
1465 {
1466   GetValueCommand* c = new GetValueCommand(d_terms);
1467   c->d_result = d_result;
1468   return c;
1469 }
1470
1471 std::string GetValueCommand::getCommandName() const { return "get-value"; }
1472
1473 /* -------------------------------------------------------------------------- */
1474 /* class GetAssignmentCommand                                                 */
1475 /* -------------------------------------------------------------------------- */
1476
1477 GetAssignmentCommand::GetAssignmentCommand() {}
1478 void GetAssignmentCommand::invoke(SmtEngine* smtEngine)
1479 {
1480   try
1481   {
1482     std::vector<std::pair<Expr, Expr>> assignments = smtEngine->getAssignment();
1483     vector<SExpr> sexprs;
1484     for (const auto& p : assignments)
1485     {
1486       vector<SExpr> v;
1487       if (p.first.getKind() == kind::APPLY)
1488       {
1489         v.emplace_back(SExpr::Keyword(p.first.getOperator().toString()));
1490       }
1491       else
1492       {
1493         v.emplace_back(SExpr::Keyword(p.first.toString()));
1494       }
1495       v.emplace_back(SExpr::Keyword(p.second.toString()));
1496       sexprs.emplace_back(v);
1497     }
1498     d_result = SExpr(sexprs);
1499     d_commandStatus = CommandSuccess::instance();
1500   }
1501   catch (RecoverableModalException& e)
1502   {
1503     d_commandStatus = new CommandRecoverableFailure(e.what());
1504   }
1505   catch (UnsafeInterruptException& e)
1506   {
1507     d_commandStatus = new CommandInterrupted();
1508   }
1509   catch (exception& e)
1510   {
1511     d_commandStatus = new CommandFailure(e.what());
1512   }
1513 }
1514
1515 SExpr GetAssignmentCommand::getResult() const { return d_result; }
1516 void GetAssignmentCommand::printResult(std::ostream& out,
1517                                        uint32_t verbosity) const
1518 {
1519   if (!ok())
1520   {
1521     this->Command::printResult(out, verbosity);
1522   }
1523   else
1524   {
1525     out << d_result << endl;
1526   }
1527 }
1528
1529 Command* GetAssignmentCommand::exportTo(ExprManager* exprManager,
1530                                         ExprManagerMapCollection& variableMap)
1531 {
1532   GetAssignmentCommand* c = new GetAssignmentCommand();
1533   c->d_result = d_result;
1534   return c;
1535 }
1536
1537 Command* GetAssignmentCommand::clone() const
1538 {
1539   GetAssignmentCommand* c = new GetAssignmentCommand();
1540   c->d_result = d_result;
1541   return c;
1542 }
1543
1544 std::string GetAssignmentCommand::getCommandName() const
1545 {
1546   return "get-assignment";
1547 }
1548
1549 /* -------------------------------------------------------------------------- */
1550 /* class GetModelCommand                                                      */
1551 /* -------------------------------------------------------------------------- */
1552
1553 GetModelCommand::GetModelCommand() : d_result(nullptr), d_smtEngine(nullptr) {}
1554 void GetModelCommand::invoke(SmtEngine* smtEngine)
1555 {
1556   try
1557   {
1558     d_result = smtEngine->getModel();
1559     d_smtEngine = smtEngine;
1560     d_commandStatus = CommandSuccess::instance();
1561   }
1562   catch (RecoverableModalException& e)
1563   {
1564     d_commandStatus = new CommandRecoverableFailure(e.what());
1565   }
1566   catch (UnsafeInterruptException& e)
1567   {
1568     d_commandStatus = new CommandInterrupted();
1569   }
1570   catch (exception& e)
1571   {
1572     d_commandStatus = new CommandFailure(e.what());
1573   }
1574 }
1575
1576 /* Model is private to the library -- for now
1577 Model* GetModelCommand::getResult() const  {
1578   return d_result;
1579 }
1580 */
1581
1582 void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
1583 {
1584   if (!ok())
1585   {
1586     this->Command::printResult(out, verbosity);
1587   }
1588   else
1589   {
1590     out << *d_result;
1591   }
1592 }
1593
1594 Command* GetModelCommand::exportTo(ExprManager* exprManager,
1595                                    ExprManagerMapCollection& variableMap)
1596 {
1597   GetModelCommand* c = new GetModelCommand();
1598   c->d_result = d_result;
1599   c->d_smtEngine = d_smtEngine;
1600   return c;
1601 }
1602
1603 Command* GetModelCommand::clone() const
1604 {
1605   GetModelCommand* c = new GetModelCommand();
1606   c->d_result = d_result;
1607   c->d_smtEngine = d_smtEngine;
1608   return c;
1609 }
1610
1611 std::string GetModelCommand::getCommandName() const { return "get-model"; }
1612
1613 /* -------------------------------------------------------------------------- */
1614 /* class GetProofCommand                                                      */
1615 /* -------------------------------------------------------------------------- */
1616
1617 GetProofCommand::GetProofCommand() : d_smtEngine(nullptr), d_result(nullptr) {}
1618 void GetProofCommand::invoke(SmtEngine* smtEngine)
1619 {
1620   try
1621   {
1622     d_smtEngine = smtEngine;
1623     d_result = &smtEngine->getProof();
1624     d_commandStatus = CommandSuccess::instance();
1625   }
1626   catch (RecoverableModalException& e)
1627   {
1628     d_commandStatus = new CommandRecoverableFailure(e.what());
1629   }
1630   catch (UnsafeInterruptException& e)
1631   {
1632     d_commandStatus = new CommandInterrupted();
1633   }
1634   catch (exception& e)
1635   {
1636     d_commandStatus = new CommandFailure(e.what());
1637   }
1638 }
1639
1640 const Proof& GetProofCommand::getResult() const { return *d_result; }
1641 void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const
1642 {
1643   if (!ok())
1644   {
1645     this->Command::printResult(out, verbosity);
1646   }
1647   else
1648   {
1649     smt::SmtScope scope(d_smtEngine);
1650     d_result->toStream(out);
1651   }
1652 }
1653
1654 Command* GetProofCommand::exportTo(ExprManager* exprManager,
1655                                    ExprManagerMapCollection& variableMap)
1656 {
1657   GetProofCommand* c = new GetProofCommand();
1658   c->d_result = d_result;
1659   c->d_smtEngine = d_smtEngine;
1660   return c;
1661 }
1662
1663 Command* GetProofCommand::clone() const
1664 {
1665   GetProofCommand* c = new GetProofCommand();
1666   c->d_result = d_result;
1667   c->d_smtEngine = d_smtEngine;
1668   return c;
1669 }
1670
1671 std::string GetProofCommand::getCommandName() const { return "get-proof"; }
1672
1673 /* -------------------------------------------------------------------------- */
1674 /* class GetInstantiationsCommand                                             */
1675 /* -------------------------------------------------------------------------- */
1676
1677 GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {}
1678 void GetInstantiationsCommand::invoke(SmtEngine* smtEngine)
1679 {
1680   try
1681   {
1682     d_smtEngine = smtEngine;
1683     d_commandStatus = CommandSuccess::instance();
1684   }
1685   catch (exception& e)
1686   {
1687     d_commandStatus = new CommandFailure(e.what());
1688   }
1689 }
1690
1691 void GetInstantiationsCommand::printResult(std::ostream& out,
1692                                            uint32_t verbosity) const
1693 {
1694   if (!ok())
1695   {
1696     this->Command::printResult(out, verbosity);
1697   }
1698   else
1699   {
1700     d_smtEngine->printInstantiations(out);
1701   }
1702 }
1703
1704 Command* GetInstantiationsCommand::exportTo(
1705     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1706 {
1707   GetInstantiationsCommand* c = new GetInstantiationsCommand();
1708   // c->d_result = d_result;
1709   c->d_smtEngine = d_smtEngine;
1710   return c;
1711 }
1712
1713 Command* GetInstantiationsCommand::clone() const
1714 {
1715   GetInstantiationsCommand* c = new GetInstantiationsCommand();
1716   // c->d_result = d_result;
1717   c->d_smtEngine = d_smtEngine;
1718   return c;
1719 }
1720
1721 std::string GetInstantiationsCommand::getCommandName() const
1722 {
1723   return "get-instantiations";
1724 }
1725
1726 /* -------------------------------------------------------------------------- */
1727 /* class GetSynthSolutionCommand                                              */
1728 /* -------------------------------------------------------------------------- */
1729
1730 GetSynthSolutionCommand::GetSynthSolutionCommand() : d_smtEngine(nullptr) {}
1731 void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine)
1732 {
1733   try
1734   {
1735     d_smtEngine = smtEngine;
1736     d_commandStatus = CommandSuccess::instance();
1737   }
1738   catch (exception& e)
1739   {
1740     d_commandStatus = new CommandFailure(e.what());
1741   }
1742 }
1743
1744 void GetSynthSolutionCommand::printResult(std::ostream& out,
1745                                           uint32_t verbosity) const
1746 {
1747   if (!ok())
1748   {
1749     this->Command::printResult(out, verbosity);
1750   }
1751   else
1752   {
1753     d_smtEngine->printSynthSolution(out);
1754   }
1755 }
1756
1757 Command* GetSynthSolutionCommand::exportTo(
1758     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1759 {
1760   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
1761   c->d_smtEngine = d_smtEngine;
1762   return c;
1763 }
1764
1765 Command* GetSynthSolutionCommand::clone() const
1766 {
1767   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
1768   c->d_smtEngine = d_smtEngine;
1769   return c;
1770 }
1771
1772 std::string GetSynthSolutionCommand::getCommandName() const
1773 {
1774   return "get-instantiations";
1775 }
1776
1777 /* -------------------------------------------------------------------------- */
1778 /* class GetQuantifierEliminationCommand                                      */
1779 /* -------------------------------------------------------------------------- */
1780
1781 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() : d_expr() {}
1782 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
1783     const Expr& expr, bool doFull)
1784     : d_expr(expr), d_doFull(doFull)
1785 {
1786 }
1787
1788 Expr GetQuantifierEliminationCommand::getExpr() const { return d_expr; }
1789 bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
1790 void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine)
1791 {
1792   try
1793   {
1794     d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull);
1795     d_commandStatus = CommandSuccess::instance();
1796   }
1797   catch (exception& e)
1798   {
1799     d_commandStatus = new CommandFailure(e.what());
1800   }
1801 }
1802
1803 Expr GetQuantifierEliminationCommand::getResult() const { return d_result; }
1804 void GetQuantifierEliminationCommand::printResult(std::ostream& out,
1805                                                   uint32_t verbosity) const
1806 {
1807   if (!ok())
1808   {
1809     this->Command::printResult(out, verbosity);
1810   }
1811   else
1812   {
1813     out << d_result << endl;
1814   }
1815 }
1816
1817 Command* GetQuantifierEliminationCommand::exportTo(
1818     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1819 {
1820   GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(
1821       d_expr.exportTo(exprManager, variableMap), d_doFull);
1822   c->d_result = d_result;
1823   return c;
1824 }
1825
1826 Command* GetQuantifierEliminationCommand::clone() const
1827 {
1828   GetQuantifierEliminationCommand* c =
1829       new GetQuantifierEliminationCommand(d_expr, d_doFull);
1830   c->d_result = d_result;
1831   return c;
1832 }
1833
1834 std::string GetQuantifierEliminationCommand::getCommandName() const
1835 {
1836   return d_doFull ? "get-qe" : "get-qe-disjunct";
1837 }
1838
1839 /* -------------------------------------------------------------------------- */
1840 /* class GetUnsatAssumptionsCommand                                           */
1841 /* -------------------------------------------------------------------------- */
1842
1843 GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
1844
1845 void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine)
1846 {
1847   try
1848   {
1849     d_result = smtEngine->getUnsatAssumptions();
1850     d_commandStatus = CommandSuccess::instance();
1851   }
1852   catch (RecoverableModalException& e)
1853   {
1854     d_commandStatus = new CommandRecoverableFailure(e.what());
1855   }
1856   catch (exception& e)
1857   {
1858     d_commandStatus = new CommandFailure(e.what());
1859   }
1860 }
1861
1862 std::vector<Expr> GetUnsatAssumptionsCommand::getResult() const
1863 {
1864   return d_result;
1865 }
1866
1867 void GetUnsatAssumptionsCommand::printResult(std::ostream& out,
1868                                              uint32_t verbosity) const
1869 {
1870   if (!ok())
1871   {
1872     this->Command::printResult(out, verbosity);
1873   }
1874   else
1875   {
1876     out << d_result << endl;
1877   }
1878 }
1879
1880 Command* GetUnsatAssumptionsCommand::exportTo(
1881     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1882 {
1883   GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
1884   c->d_result = d_result;
1885   return c;
1886 }
1887
1888 Command* GetUnsatAssumptionsCommand::clone() const
1889 {
1890   GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
1891   c->d_result = d_result;
1892   return c;
1893 }
1894
1895 std::string GetUnsatAssumptionsCommand::getCommandName() const
1896 {
1897   return "get-unsat-assumptions";
1898 }
1899
1900 /* -------------------------------------------------------------------------- */
1901 /* class GetUnsatCoreCommand                                                  */
1902 /* -------------------------------------------------------------------------- */
1903
1904 GetUnsatCoreCommand::GetUnsatCoreCommand() {}
1905 void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine)
1906 {
1907   try
1908   {
1909     d_result = smtEngine->getUnsatCore();
1910     d_commandStatus = CommandSuccess::instance();
1911   }
1912   catch (RecoverableModalException& e)
1913   {
1914     d_commandStatus = new CommandRecoverableFailure(e.what());
1915   }
1916   catch (exception& e)
1917   {
1918     d_commandStatus = new CommandFailure(e.what());
1919   }
1920 }
1921
1922 void GetUnsatCoreCommand::printResult(std::ostream& out,
1923                                       uint32_t verbosity) const
1924 {
1925   if (!ok())
1926   {
1927     this->Command::printResult(out, verbosity);
1928   }
1929   else
1930   {
1931     d_result.toStream(out);
1932   }
1933 }
1934
1935 const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const
1936 {
1937   // of course, this will be empty if the command hasn't been invoked yet
1938   return d_result;
1939 }
1940
1941 Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager,
1942                                        ExprManagerMapCollection& variableMap)
1943 {
1944   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
1945   c->d_result = d_result;
1946   return c;
1947 }
1948
1949 Command* GetUnsatCoreCommand::clone() const
1950 {
1951   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
1952   c->d_result = d_result;
1953   return c;
1954 }
1955
1956 std::string GetUnsatCoreCommand::getCommandName() const
1957 {
1958   return "get-unsat-core";
1959 }
1960
1961 /* -------------------------------------------------------------------------- */
1962 /* class GetAssertionsCommand                                                 */
1963 /* -------------------------------------------------------------------------- */
1964
1965 GetAssertionsCommand::GetAssertionsCommand() {}
1966 void GetAssertionsCommand::invoke(SmtEngine* smtEngine)
1967 {
1968   try
1969   {
1970     stringstream ss;
1971     const vector<Expr> v = smtEngine->getAssertions();
1972     ss << "(\n";
1973     copy(v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n"));
1974     ss << ")\n";
1975     d_result = ss.str();
1976     d_commandStatus = CommandSuccess::instance();
1977   }
1978   catch (exception& e)
1979   {
1980     d_commandStatus = new CommandFailure(e.what());
1981   }
1982 }
1983
1984 std::string GetAssertionsCommand::getResult() const { return d_result; }
1985 void GetAssertionsCommand::printResult(std::ostream& out,
1986                                        uint32_t verbosity) const
1987 {
1988   if (!ok())
1989   {
1990     this->Command::printResult(out, verbosity);
1991   }
1992   else
1993   {
1994     out << d_result;
1995   }
1996 }
1997
1998 Command* GetAssertionsCommand::exportTo(ExprManager* exprManager,
1999                                         ExprManagerMapCollection& variableMap)
2000 {
2001   GetAssertionsCommand* c = new GetAssertionsCommand();
2002   c->d_result = d_result;
2003   return c;
2004 }
2005
2006 Command* GetAssertionsCommand::clone() const
2007 {
2008   GetAssertionsCommand* c = new GetAssertionsCommand();
2009   c->d_result = d_result;
2010   return c;
2011 }
2012
2013 std::string GetAssertionsCommand::getCommandName() const
2014 {
2015   return "get-assertions";
2016 }
2017
2018 /* -------------------------------------------------------------------------- */
2019 /* class SetBenchmarkStatusCommand                                            */
2020 /* -------------------------------------------------------------------------- */
2021
2022 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status)
2023     : d_status(status)
2024 {
2025 }
2026
2027 BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
2028 {
2029   return d_status;
2030 }
2031
2032 void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine)
2033 {
2034   try
2035   {
2036     stringstream ss;
2037     ss << d_status;
2038     SExpr status = SExpr(ss.str());
2039     smtEngine->setInfo("status", status);
2040     d_commandStatus = CommandSuccess::instance();
2041   }
2042   catch (exception& e)
2043   {
2044     d_commandStatus = new CommandFailure(e.what());
2045   }
2046 }
2047
2048 Command* SetBenchmarkStatusCommand::exportTo(
2049     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2050 {
2051   return new SetBenchmarkStatusCommand(d_status);
2052 }
2053
2054 Command* SetBenchmarkStatusCommand::clone() const
2055 {
2056   return new SetBenchmarkStatusCommand(d_status);
2057 }
2058
2059 std::string SetBenchmarkStatusCommand::getCommandName() const
2060 {
2061   return "set-info";
2062 }
2063
2064 /* -------------------------------------------------------------------------- */
2065 /* class SetBenchmarkLogicCommand                                             */
2066 /* -------------------------------------------------------------------------- */
2067
2068 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
2069     : d_logic(logic)
2070 {
2071 }
2072
2073 std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
2074 void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine)
2075 {
2076   try
2077   {
2078     smtEngine->setLogic(d_logic);
2079     d_commandStatus = CommandSuccess::instance();
2080   }
2081   catch (exception& e)
2082   {
2083     d_commandStatus = new CommandFailure(e.what());
2084   }
2085 }
2086
2087 Command* SetBenchmarkLogicCommand::exportTo(
2088     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2089 {
2090   return new SetBenchmarkLogicCommand(d_logic);
2091 }
2092
2093 Command* SetBenchmarkLogicCommand::clone() const
2094 {
2095   return new SetBenchmarkLogicCommand(d_logic);
2096 }
2097
2098 std::string SetBenchmarkLogicCommand::getCommandName() const
2099 {
2100   return "set-logic";
2101 }
2102
2103 /* -------------------------------------------------------------------------- */
2104 /* class SetInfoCommand                                                       */
2105 /* -------------------------------------------------------------------------- */
2106
2107 SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
2108     : d_flag(flag), d_sexpr(sexpr)
2109 {
2110 }
2111
2112 std::string SetInfoCommand::getFlag() const { return d_flag; }
2113 SExpr SetInfoCommand::getSExpr() const { return d_sexpr; }
2114 void SetInfoCommand::invoke(SmtEngine* smtEngine)
2115 {
2116   try
2117   {
2118     smtEngine->setInfo(d_flag, d_sexpr);
2119     d_commandStatus = CommandSuccess::instance();
2120   }
2121   catch (UnrecognizedOptionException&)
2122   {
2123     // As per SMT-LIB spec, silently accept unknown set-info keys
2124     d_commandStatus = CommandSuccess::instance();
2125   }
2126   catch (exception& e)
2127   {
2128     d_commandStatus = new CommandFailure(e.what());
2129   }
2130 }
2131
2132 Command* SetInfoCommand::exportTo(ExprManager* exprManager,
2133                                   ExprManagerMapCollection& variableMap)
2134 {
2135   return new SetInfoCommand(d_flag, d_sexpr);
2136 }
2137
2138 Command* SetInfoCommand::clone() const
2139 {
2140   return new SetInfoCommand(d_flag, d_sexpr);
2141 }
2142
2143 std::string SetInfoCommand::getCommandName() const { return "set-info"; }
2144
2145 /* -------------------------------------------------------------------------- */
2146 /* class GetInfoCommand                                                       */
2147 /* -------------------------------------------------------------------------- */
2148
2149 GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
2150 std::string GetInfoCommand::getFlag() const { return d_flag; }
2151 void GetInfoCommand::invoke(SmtEngine* smtEngine)
2152 {
2153   try
2154   {
2155     vector<SExpr> v;
2156     v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
2157     v.push_back(smtEngine->getInfo(d_flag));
2158     stringstream ss;
2159     if (d_flag == "all-options" || d_flag == "all-statistics")
2160     {
2161       ss << PrettySExprs(true);
2162     }
2163     ss << SExpr(v);
2164     d_result = ss.str();
2165     d_commandStatus = CommandSuccess::instance();
2166   }
2167   catch (UnrecognizedOptionException&)
2168   {
2169     d_commandStatus = new CommandUnsupported();
2170   }
2171   catch (exception& e)
2172   {
2173     d_commandStatus = new CommandFailure(e.what());
2174   }
2175 }
2176
2177 std::string GetInfoCommand::getResult() const { return d_result; }
2178 void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const
2179 {
2180   if (!ok())
2181   {
2182     this->Command::printResult(out, verbosity);
2183   }
2184   else if (d_result != "")
2185   {
2186     out << d_result << endl;
2187   }
2188 }
2189
2190 Command* GetInfoCommand::exportTo(ExprManager* exprManager,
2191                                   ExprManagerMapCollection& variableMap)
2192 {
2193   GetInfoCommand* c = new GetInfoCommand(d_flag);
2194   c->d_result = d_result;
2195   return c;
2196 }
2197
2198 Command* GetInfoCommand::clone() const
2199 {
2200   GetInfoCommand* c = new GetInfoCommand(d_flag);
2201   c->d_result = d_result;
2202   return c;
2203 }
2204
2205 std::string GetInfoCommand::getCommandName() const { return "get-info"; }
2206
2207 /* -------------------------------------------------------------------------- */
2208 /* class SetOptionCommand                                                     */
2209 /* -------------------------------------------------------------------------- */
2210
2211 SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
2212     : d_flag(flag), d_sexpr(sexpr)
2213 {
2214 }
2215
2216 std::string SetOptionCommand::getFlag() const { return d_flag; }
2217 SExpr SetOptionCommand::getSExpr() const { return d_sexpr; }
2218 void SetOptionCommand::invoke(SmtEngine* smtEngine)
2219 {
2220   try
2221   {
2222     smtEngine->setOption(d_flag, d_sexpr);
2223     d_commandStatus = CommandSuccess::instance();
2224   }
2225   catch (UnrecognizedOptionException&)
2226   {
2227     d_commandStatus = new CommandUnsupported();
2228   }
2229   catch (exception& e)
2230   {
2231     d_commandStatus = new CommandFailure(e.what());
2232   }
2233 }
2234
2235 Command* SetOptionCommand::exportTo(ExprManager* exprManager,
2236                                     ExprManagerMapCollection& variableMap)
2237 {
2238   return new SetOptionCommand(d_flag, d_sexpr);
2239 }
2240
2241 Command* SetOptionCommand::clone() const
2242 {
2243   return new SetOptionCommand(d_flag, d_sexpr);
2244 }
2245
2246 std::string SetOptionCommand::getCommandName() const { return "set-option"; }
2247
2248 /* -------------------------------------------------------------------------- */
2249 /* class GetOptionCommand                                                     */
2250 /* -------------------------------------------------------------------------- */
2251
2252 GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
2253 std::string GetOptionCommand::getFlag() const { return d_flag; }
2254 void GetOptionCommand::invoke(SmtEngine* smtEngine)
2255 {
2256   try
2257   {
2258     SExpr res = smtEngine->getOption(d_flag);
2259     d_result = res.toString();
2260     d_commandStatus = CommandSuccess::instance();
2261   }
2262   catch (UnrecognizedOptionException&)
2263   {
2264     d_commandStatus = new CommandUnsupported();
2265   }
2266   catch (exception& e)
2267   {
2268     d_commandStatus = new CommandFailure(e.what());
2269   }
2270 }
2271
2272 std::string GetOptionCommand::getResult() const { return d_result; }
2273 void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const
2274 {
2275   if (!ok())
2276   {
2277     this->Command::printResult(out, verbosity);
2278   }
2279   else if (d_result != "")
2280   {
2281     out << d_result << endl;
2282   }
2283 }
2284
2285 Command* GetOptionCommand::exportTo(ExprManager* exprManager,
2286                                     ExprManagerMapCollection& variableMap)
2287 {
2288   GetOptionCommand* c = new GetOptionCommand(d_flag);
2289   c->d_result = d_result;
2290   return c;
2291 }
2292
2293 Command* GetOptionCommand::clone() const
2294 {
2295   GetOptionCommand* c = new GetOptionCommand(d_flag);
2296   c->d_result = d_result;
2297   return c;
2298 }
2299
2300 std::string GetOptionCommand::getCommandName() const { return "get-option"; }
2301
2302 /* -------------------------------------------------------------------------- */
2303 /* class SetExpressionNameCommand                                             */
2304 /* -------------------------------------------------------------------------- */
2305
2306 SetExpressionNameCommand::SetExpressionNameCommand(Expr expr, std::string name)
2307     : d_expr(expr), d_name(name)
2308 {
2309 }
2310
2311 void SetExpressionNameCommand::invoke(SmtEngine* smtEngine)
2312 {
2313   smtEngine->setExpressionName(d_expr, d_name);
2314   d_commandStatus = CommandSuccess::instance();
2315 }
2316
2317 Command* SetExpressionNameCommand::exportTo(
2318     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2319 {
2320   SetExpressionNameCommand* c = new SetExpressionNameCommand(
2321       d_expr.exportTo(exprManager, variableMap), d_name);
2322   return c;
2323 }
2324
2325 Command* SetExpressionNameCommand::clone() const
2326 {
2327   SetExpressionNameCommand* c = new SetExpressionNameCommand(d_expr, d_name);
2328   return c;
2329 }
2330
2331 std::string SetExpressionNameCommand::getCommandName() const
2332 {
2333   return "set-expr-name";
2334 }
2335
2336 /* -------------------------------------------------------------------------- */
2337 /* class DatatypeDeclarationCommand                                           */
2338 /* -------------------------------------------------------------------------- */
2339
2340 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
2341     const DatatypeType& datatype)
2342     : d_datatypes()
2343 {
2344   d_datatypes.push_back(datatype);
2345 }
2346
2347 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
2348     const std::vector<DatatypeType>& datatypes)
2349     : d_datatypes(datatypes)
2350 {
2351 }
2352
2353 const std::vector<DatatypeType>& DatatypeDeclarationCommand::getDatatypes()
2354     const
2355 {
2356   return d_datatypes;
2357 }
2358
2359 void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine)
2360 {
2361   d_commandStatus = CommandSuccess::instance();
2362 }
2363
2364 Command* DatatypeDeclarationCommand::exportTo(
2365     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2366 {
2367   throw ExportUnsupportedException(
2368       "export of DatatypeDeclarationCommand unsupported");
2369 }
2370
2371 Command* DatatypeDeclarationCommand::clone() const
2372 {
2373   return new DatatypeDeclarationCommand(d_datatypes);
2374 }
2375
2376 std::string DatatypeDeclarationCommand::getCommandName() const
2377 {
2378   return "declare-datatypes";
2379 }
2380
2381 /* -------------------------------------------------------------------------- */
2382 /* class RewriteRuleCommand                                                   */
2383 /* -------------------------------------------------------------------------- */
2384
2385 RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
2386                                        const std::vector<Expr>& guards,
2387                                        Expr head,
2388                                        Expr body,
2389                                        const Triggers& triggers)
2390     : d_vars(vars),
2391       d_guards(guards),
2392       d_head(head),
2393       d_body(body),
2394       d_triggers(triggers)
2395 {
2396 }
2397
2398 RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
2399                                        Expr head,
2400                                        Expr body)
2401     : d_vars(vars), d_head(head), d_body(body)
2402 {
2403 }
2404
2405 const std::vector<Expr>& RewriteRuleCommand::getVars() const { return d_vars; }
2406 const std::vector<Expr>& RewriteRuleCommand::getGuards() const
2407 {
2408   return d_guards;
2409 }
2410
2411 Expr RewriteRuleCommand::getHead() const { return d_head; }
2412 Expr RewriteRuleCommand::getBody() const { return d_body; }
2413 const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const
2414 {
2415   return d_triggers;
2416 }
2417
2418 void RewriteRuleCommand::invoke(SmtEngine* smtEngine)
2419 {
2420   try
2421   {
2422     ExprManager* em = smtEngine->getExprManager();
2423     /** build vars list */
2424     Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
2425     /** build guards list */
2426     Expr guards;
2427     if (d_guards.size() == 0)
2428       guards = em->mkConst<bool>(true);
2429     else if (d_guards.size() == 1)
2430       guards = d_guards[0];
2431     else
2432       guards = em->mkExpr(kind::AND, d_guards);
2433     /** build expression */
2434     Expr expr;
2435     if (d_triggers.empty())
2436     {
2437       expr = em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body);
2438     }
2439     else
2440     {
2441       /** build triggers list */
2442       std::vector<Expr> vtriggers;
2443       vtriggers.reserve(d_triggers.size());
2444       for (Triggers::const_iterator i = d_triggers.begin(),
2445                                     end = d_triggers.end();
2446            i != end;
2447            ++i)
2448       {
2449         vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i));
2450       }
2451       Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers);
2452       expr =
2453           em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body, triggers);
2454     }
2455     smtEngine->assertFormula(expr);
2456     d_commandStatus = CommandSuccess::instance();
2457   }
2458   catch (exception& e)
2459   {
2460     d_commandStatus = new CommandFailure(e.what());
2461   }
2462 }
2463
2464 Command* RewriteRuleCommand::exportTo(ExprManager* exprManager,
2465                                       ExprManagerMapCollection& variableMap)
2466 {
2467   /** Convert variables */
2468   VExpr vars = ExportTo(exprManager, variableMap, d_vars);
2469   /** Convert guards */
2470   VExpr guards = ExportTo(exprManager, variableMap, d_guards);
2471   /** Convert triggers */
2472   Triggers triggers;
2473   triggers.reserve(d_triggers.size());
2474   for (const std::vector<Expr>& trigger_list : d_triggers)
2475   {
2476     triggers.push_back(ExportTo(exprManager, variableMap, trigger_list));
2477   }
2478   /** Convert head and body */
2479   Expr head = d_head.exportTo(exprManager, variableMap);
2480   Expr body = d_body.exportTo(exprManager, variableMap);
2481   /** Create the converted rules */
2482   return new RewriteRuleCommand(vars, guards, head, body, triggers);
2483 }
2484
2485 Command* RewriteRuleCommand::clone() const
2486 {
2487   return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers);
2488 }
2489
2490 std::string RewriteRuleCommand::getCommandName() const
2491 {
2492   return "rewrite-rule";
2493 }
2494
2495 /* -------------------------------------------------------------------------- */
2496 /* class PropagateRuleCommand                                                 */
2497 /* -------------------------------------------------------------------------- */
2498
2499 PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
2500                                            const std::vector<Expr>& guards,
2501                                            const std::vector<Expr>& heads,
2502                                            Expr body,
2503                                            const Triggers& triggers,
2504                                            bool deduction)
2505     : d_vars(vars),
2506       d_guards(guards),
2507       d_heads(heads),
2508       d_body(body),
2509       d_triggers(triggers),
2510       d_deduction(deduction)
2511 {
2512 }
2513
2514 PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
2515                                            const std::vector<Expr>& heads,
2516                                            Expr body,
2517                                            bool deduction)
2518     : d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction)
2519 {
2520 }
2521
2522 const std::vector<Expr>& PropagateRuleCommand::getVars() const
2523 {
2524   return d_vars;
2525 }
2526
2527 const std::vector<Expr>& PropagateRuleCommand::getGuards() const
2528 {
2529   return d_guards;
2530 }
2531
2532 const std::vector<Expr>& PropagateRuleCommand::getHeads() const
2533 {
2534   return d_heads;
2535 }
2536
2537 Expr PropagateRuleCommand::getBody() const { return d_body; }
2538 const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const
2539 {
2540   return d_triggers;
2541 }
2542
2543 bool PropagateRuleCommand::isDeduction() const { return d_deduction; }
2544 void PropagateRuleCommand::invoke(SmtEngine* smtEngine)
2545 {
2546   try
2547   {
2548     ExprManager* em = smtEngine->getExprManager();
2549     /** build vars list */
2550     Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
2551     /** build guards list */
2552     Expr guards;
2553     if (d_guards.size() == 0)
2554       guards = em->mkConst<bool>(true);
2555     else if (d_guards.size() == 1)
2556       guards = d_guards[0];
2557     else
2558       guards = em->mkExpr(kind::AND, d_guards);
2559     /** build heads list */
2560     Expr heads;
2561     if (d_heads.size() == 1)
2562       heads = d_heads[0];
2563     else
2564       heads = em->mkExpr(kind::AND, d_heads);
2565     /** build expression */
2566     Expr expr;
2567     if (d_triggers.empty())
2568     {
2569       expr = em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body);
2570     }
2571     else
2572     {
2573       /** build triggers list */
2574       std::vector<Expr> vtriggers;
2575       vtriggers.reserve(d_triggers.size());
2576       for (Triggers::const_iterator i = d_triggers.begin(),
2577                                     end = d_triggers.end();
2578            i != end;
2579            ++i)
2580       {
2581         vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i));
2582       }
2583       Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers);
2584       expr =
2585           em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body, triggers);
2586     }
2587     smtEngine->assertFormula(expr);
2588     d_commandStatus = CommandSuccess::instance();
2589   }
2590   catch (exception& e)
2591   {
2592     d_commandStatus = new CommandFailure(e.what());
2593   }
2594 }
2595
2596 Command* PropagateRuleCommand::exportTo(ExprManager* exprManager,
2597                                         ExprManagerMapCollection& variableMap)
2598 {
2599   /** Convert variables */
2600   VExpr vars = ExportTo(exprManager, variableMap, d_vars);
2601   /** Convert guards */
2602   VExpr guards = ExportTo(exprManager, variableMap, d_guards);
2603   /** Convert heads */
2604   VExpr heads = ExportTo(exprManager, variableMap, d_heads);
2605   /** Convert triggers */
2606   Triggers triggers;
2607   triggers.reserve(d_triggers.size());
2608   for (const std::vector<Expr>& trigger_list : d_triggers)
2609   {
2610     triggers.push_back(ExportTo(exprManager, variableMap, trigger_list));
2611   }
2612   /** Convert head and body */
2613   Expr body = d_body.exportTo(exprManager, variableMap);
2614   /** Create the converted rules */
2615   return new PropagateRuleCommand(vars, guards, heads, body, triggers);
2616 }
2617
2618 Command* PropagateRuleCommand::clone() const
2619 {
2620   return new PropagateRuleCommand(
2621       d_vars, d_guards, d_heads, d_body, d_triggers);
2622 }
2623
2624 std::string PropagateRuleCommand::getCommandName() const
2625 {
2626   return "propagate-rule";
2627 }
2628 }  // namespace CVC4