src/smt/command.cpp

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