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-2019 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(d_func);
1362   }
1363   d_commandStatus = CommandSuccess::instance();
1364 }
1365
1366 Command* DefineNamedFunctionCommand::exportTo(
1367     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1368 {
1369   Expr func = d_func.exportTo(exprManager, variableMap);
1370   vector<Expr> formals;
1371   transform(d_formals.begin(),
1372             d_formals.end(),
1373             back_inserter(formals),
1374             ExportTransformer(exprManager, variableMap));
1375   Expr formula = d_formula.exportTo(exprManager, variableMap);
1376   return new DefineNamedFunctionCommand(d_symbol, func, formals, formula);
1377 }
1378
1379 Command* DefineNamedFunctionCommand::clone() const
1380 {
1381   return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
1382 }
1383
1384 /* -------------------------------------------------------------------------- */
1385 /* class DefineFunctionRecCommand                                             */
1386 /* -------------------------------------------------------------------------- */
1387
1388 DefineFunctionRecCommand::DefineFunctionRecCommand(
1389     Expr func, const std::vector<Expr>& formals, Expr formula)
1390 {
1391   d_funcs.push_back(func);
1392   d_formals.push_back(formals);
1393   d_formulas.push_back(formula);
1394 }
1395
1396 DefineFunctionRecCommand::DefineFunctionRecCommand(
1397     const std::vector<Expr>& funcs,
1398     const std::vector<std::vector<Expr>>& formals,
1399     const std::vector<Expr>& formulas)
1400 {
1401   d_funcs.insert(d_funcs.end(), funcs.begin(), funcs.end());
1402   d_formals.insert(d_formals.end(), formals.begin(), formals.end());
1403   d_formulas.insert(d_formulas.end(), formulas.begin(), formulas.end());
1404 }
1405
1406 const std::vector<Expr>& DefineFunctionRecCommand::getFunctions() const
1407 {
1408   return d_funcs;
1409 }
1410
1411 const std::vector<std::vector<Expr>>& DefineFunctionRecCommand::getFormals()
1412     const
1413 {
1414   return d_formals;
1415 }
1416
1417 const std::vector<Expr>& DefineFunctionRecCommand::getFormulas() const
1418 {
1419   return d_formulas;
1420 }
1421
1422 void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine)
1423 {
1424   try
1425   {
1426     smtEngine->defineFunctionsRec(d_funcs, d_formals, d_formulas);
1427     d_commandStatus = CommandSuccess::instance();
1428   }
1429   catch (exception& e)
1430   {
1431     d_commandStatus = new CommandFailure(e.what());
1432   }
1433 }
1434
1435 Command* DefineFunctionRecCommand::exportTo(
1436     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1437 {
1438   std::vector<Expr> funcs;
1439   for (unsigned i = 0, size = d_funcs.size(); i < size; i++)
1440   {
1441     Expr func = d_funcs[i].exportTo(
1442         exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
1443     funcs.push_back(func);
1444   }
1445   std::vector<std::vector<Expr>> formals;
1446   for (unsigned i = 0, size = d_formals.size(); i < size; i++)
1447   {
1448     std::vector<Expr> formals_c;
1449     transform(d_formals[i].begin(),
1450               d_formals[i].end(),
1451               back_inserter(formals_c),
1452               ExportTransformer(exprManager, variableMap));
1453     formals.push_back(formals_c);
1454   }
1455   std::vector<Expr> formulas;
1456   for (unsigned i = 0, size = d_formulas.size(); i < size; i++)
1457   {
1458     Expr formula = d_formulas[i].exportTo(exprManager, variableMap);
1459     formulas.push_back(formula);
1460   }
1461   return new DefineFunctionRecCommand(funcs, formals, formulas);
1462 }
1463
1464 Command* DefineFunctionRecCommand::clone() const
1465 {
1466   return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas);
1467 }
1468
1469 std::string DefineFunctionRecCommand::getCommandName() const
1470 {
1471   return "define-fun-rec";
1472 }
1473
1474 /* -------------------------------------------------------------------------- */
1475 /* class SetUserAttribute                                                     */
1476 /* -------------------------------------------------------------------------- */
1477
1478 SetUserAttributeCommand::SetUserAttributeCommand(
1479     const std::string& attr,
1480     Expr expr,
1481     const std::vector<Expr>& expr_values,
1482     const std::string& str_value)
1483     : d_attr(attr),
1484       d_expr(expr),
1485       d_expr_values(expr_values),
1486       d_str_value(str_value)
1487 {
1488 }
1489
1490 SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
1491                                                  Expr expr)
1492     : SetUserAttributeCommand(attr, expr, {}, "")
1493 {
1494 }
1495
1496 SetUserAttributeCommand::SetUserAttributeCommand(
1497     const std::string& attr, Expr expr, const std::vector<Expr>& values)
1498     : SetUserAttributeCommand(attr, expr, values, "")
1499 {
1500 }
1501
1502 SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
1503                                                  Expr expr,
1504                                                  const std::string& value)
1505     : SetUserAttributeCommand(attr, expr, {}, value)
1506 {
1507 }
1508
1509 void SetUserAttributeCommand::invoke(SmtEngine* smtEngine)
1510 {
1511   try
1512   {
1513     if (!d_expr.isNull())
1514     {
1515       smtEngine->setUserAttribute(d_attr, d_expr, d_expr_values, d_str_value);
1516     }
1517     d_commandStatus = CommandSuccess::instance();
1518   }
1519   catch (exception& e)
1520   {
1521     d_commandStatus = new CommandFailure(e.what());
1522   }
1523 }
1524
1525 Command* SetUserAttributeCommand::exportTo(
1526     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1527 {
1528   Expr expr = d_expr.exportTo(exprManager, variableMap);
1529   return new SetUserAttributeCommand(d_attr, expr, d_expr_values, d_str_value);
1530 }
1531
1532 Command* SetUserAttributeCommand::clone() const
1533 {
1534   return new SetUserAttributeCommand(
1535       d_attr, d_expr, d_expr_values, d_str_value);
1536 }
1537
1538 std::string SetUserAttributeCommand::getCommandName() const
1539 {
1540   return "set-user-attribute";
1541 }
1542
1543 /* -------------------------------------------------------------------------- */
1544 /* class SimplifyCommand                                                      */
1545 /* -------------------------------------------------------------------------- */
1546
1547 SimplifyCommand::SimplifyCommand(Expr term) : d_term(term) {}
1548 Expr SimplifyCommand::getTerm() const { return d_term; }
1549 void SimplifyCommand::invoke(SmtEngine* smtEngine)
1550 {
1551   try
1552   {
1553     d_result = smtEngine->simplify(d_term);
1554     d_commandStatus = CommandSuccess::instance();
1555   }
1556   catch (UnsafeInterruptException& e)
1557   {
1558     d_commandStatus = new CommandInterrupted();
1559   }
1560   catch (exception& e)
1561   {
1562     d_commandStatus = new CommandFailure(e.what());
1563   }
1564 }
1565
1566 Expr SimplifyCommand::getResult() const { return d_result; }
1567 void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const
1568 {
1569   if (!ok())
1570   {
1571     this->Command::printResult(out, verbosity);
1572   }
1573   else
1574   {
1575     out << d_result << endl;
1576   }
1577 }
1578
1579 Command* SimplifyCommand::exportTo(ExprManager* exprManager,
1580                                    ExprManagerMapCollection& variableMap)
1581 {
1582   SimplifyCommand* c =
1583       new SimplifyCommand(d_term.exportTo(exprManager, variableMap));
1584   c->d_result = d_result.exportTo(exprManager, variableMap);
1585   return c;
1586 }
1587
1588 Command* SimplifyCommand::clone() const
1589 {
1590   SimplifyCommand* c = new SimplifyCommand(d_term);
1591   c->d_result = d_result;
1592   return c;
1593 }
1594
1595 std::string SimplifyCommand::getCommandName() const { return "simplify"; }
1596
1597 /* -------------------------------------------------------------------------- */
1598 /* class ExpandDefinitionsCommand                                             */
1599 /* -------------------------------------------------------------------------- */
1600
1601 ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) : d_term(term) {}
1602 Expr ExpandDefinitionsCommand::getTerm() const { return d_term; }
1603 void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine)
1604 {
1605   d_result = smtEngine->expandDefinitions(d_term);
1606   d_commandStatus = CommandSuccess::instance();
1607 }
1608
1609 Expr ExpandDefinitionsCommand::getResult() const { return d_result; }
1610 void ExpandDefinitionsCommand::printResult(std::ostream& out,
1611                                            uint32_t verbosity) const
1612 {
1613   if (!ok())
1614   {
1615     this->Command::printResult(out, verbosity);
1616   }
1617   else
1618   {
1619     out << d_result << endl;
1620   }
1621 }
1622
1623 Command* ExpandDefinitionsCommand::exportTo(
1624     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1625 {
1626   ExpandDefinitionsCommand* c =
1627       new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap));
1628   c->d_result = d_result.exportTo(exprManager, variableMap);
1629   return c;
1630 }
1631
1632 Command* ExpandDefinitionsCommand::clone() const
1633 {
1634   ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term);
1635   c->d_result = d_result;
1636   return c;
1637 }
1638
1639 std::string ExpandDefinitionsCommand::getCommandName() const
1640 {
1641   return "expand-definitions";
1642 }
1643
1644 /* -------------------------------------------------------------------------- */
1645 /* class GetValueCommand                                                      */
1646 /* -------------------------------------------------------------------------- */
1647
1648 GetValueCommand::GetValueCommand(Expr term) : d_terms()
1649 {
1650   d_terms.push_back(term);
1651 }
1652
1653 GetValueCommand::GetValueCommand(const std::vector<Expr>& terms)
1654     : d_terms(terms)
1655 {
1656   PrettyCheckArgument(
1657       terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
1658 }
1659
1660 const std::vector<Expr>& GetValueCommand::getTerms() const { return d_terms; }
1661 void GetValueCommand::invoke(SmtEngine* smtEngine)
1662 {
1663   try
1664   {
1665     vector<Expr> result;
1666     ExprManager* em = smtEngine->getExprManager();
1667     NodeManager* nm = NodeManager::fromExprManager(em);
1668     for (const Expr& e : d_terms)
1669     {
1670       Assert(nm == NodeManager::fromExprManager(e.getExprManager()));
1671       smt::SmtScope scope(smtEngine);
1672       Node request = Node::fromExpr(
1673           options::expandDefinitions() ? smtEngine->expandDefinitions(e) : e);
1674       Node value = Node::fromExpr(smtEngine->getValue(e));
1675       if (value.getType().isInteger() && request.getType() == nm->realType())
1676       {
1677         // Need to wrap in division-by-one so that output printers know this
1678         // is an integer-looking constant that really should be output as
1679         // a rational.  Necessary for SMT-LIB standards compliance.
1680         value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1)));
1681       }
1682       result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr());
1683     }
1684     d_result = em->mkExpr(kind::SEXPR, result);
1685     d_commandStatus = CommandSuccess::instance();
1686   }
1687   catch (RecoverableModalException& e)
1688   {
1689     d_commandStatus = new CommandRecoverableFailure(e.what());
1690   }
1691   catch (UnsafeInterruptException& e)
1692   {
1693     d_commandStatus = new CommandInterrupted();
1694   }
1695   catch (exception& e)
1696   {
1697     d_commandStatus = new CommandFailure(e.what());
1698   }
1699 }
1700
1701 Expr GetValueCommand::getResult() const { return d_result; }
1702 void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
1703 {
1704   if (!ok())
1705   {
1706     this->Command::printResult(out, verbosity);
1707   }
1708   else
1709   {
1710     expr::ExprDag::Scope scope(out, false);
1711     out << d_result << endl;
1712   }
1713 }
1714
1715 Command* GetValueCommand::exportTo(ExprManager* exprManager,
1716                                    ExprManagerMapCollection& variableMap)
1717 {
1718   vector<Expr> exportedTerms;
1719   for (std::vector<Expr>::const_iterator i = d_terms.begin();
1720        i != d_terms.end();
1721        ++i)
1722   {
1723     exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
1724   }
1725   GetValueCommand* c = new GetValueCommand(exportedTerms);
1726   c->d_result = d_result.exportTo(exprManager, variableMap);
1727   return c;
1728 }
1729
1730 Command* GetValueCommand::clone() const
1731 {
1732   GetValueCommand* c = new GetValueCommand(d_terms);
1733   c->d_result = d_result;
1734   return c;
1735 }
1736
1737 std::string GetValueCommand::getCommandName() const { return "get-value"; }
1738
1739 /* -------------------------------------------------------------------------- */
1740 /* class GetAssignmentCommand                                                 */
1741 /* -------------------------------------------------------------------------- */
1742
1743 GetAssignmentCommand::GetAssignmentCommand() {}
1744 void GetAssignmentCommand::invoke(SmtEngine* smtEngine)
1745 {
1746   try
1747   {
1748     std::vector<std::pair<Expr, Expr>> assignments = smtEngine->getAssignment();
1749     vector<SExpr> sexprs;
1750     for (const auto& p : assignments)
1751     {
1752       vector<SExpr> v;
1753       v.emplace_back(SExpr::Keyword(p.first.toString()));
1754       v.emplace_back(SExpr::Keyword(p.second.toString()));
1755       sexprs.emplace_back(v);
1756     }
1757     d_result = SExpr(sexprs);
1758     d_commandStatus = CommandSuccess::instance();
1759   }
1760   catch (RecoverableModalException& e)
1761   {
1762     d_commandStatus = new CommandRecoverableFailure(e.what());
1763   }
1764   catch (UnsafeInterruptException& e)
1765   {
1766     d_commandStatus = new CommandInterrupted();
1767   }
1768   catch (exception& e)
1769   {
1770     d_commandStatus = new CommandFailure(e.what());
1771   }
1772 }
1773
1774 SExpr GetAssignmentCommand::getResult() const { return d_result; }
1775 void GetAssignmentCommand::printResult(std::ostream& out,
1776                                        uint32_t verbosity) const
1777 {
1778   if (!ok())
1779   {
1780     this->Command::printResult(out, verbosity);
1781   }
1782   else
1783   {
1784     out << d_result << endl;
1785   }
1786 }
1787
1788 Command* GetAssignmentCommand::exportTo(ExprManager* exprManager,
1789                                         ExprManagerMapCollection& variableMap)
1790 {
1791   GetAssignmentCommand* c = new GetAssignmentCommand();
1792   c->d_result = d_result;
1793   return c;
1794 }
1795
1796 Command* GetAssignmentCommand::clone() const
1797 {
1798   GetAssignmentCommand* c = new GetAssignmentCommand();
1799   c->d_result = d_result;
1800   return c;
1801 }
1802
1803 std::string GetAssignmentCommand::getCommandName() const
1804 {
1805   return "get-assignment";
1806 }
1807
1808 /* -------------------------------------------------------------------------- */
1809 /* class GetModelCommand                                                      */
1810 /* -------------------------------------------------------------------------- */
1811
1812 GetModelCommand::GetModelCommand() : d_result(nullptr), d_smtEngine(nullptr) {}
1813 void GetModelCommand::invoke(SmtEngine* smtEngine)
1814 {
1815   try
1816   {
1817     d_result = smtEngine->getModel();
1818     d_smtEngine = smtEngine;
1819     d_commandStatus = CommandSuccess::instance();
1820   }
1821   catch (RecoverableModalException& e)
1822   {
1823     d_commandStatus = new CommandRecoverableFailure(e.what());
1824   }
1825   catch (UnsafeInterruptException& e)
1826   {
1827     d_commandStatus = new CommandInterrupted();
1828   }
1829   catch (exception& e)
1830   {
1831     d_commandStatus = new CommandFailure(e.what());
1832   }
1833 }
1834
1835 /* Model is private to the library -- for now
1836 Model* GetModelCommand::getResult() const  {
1837   return d_result;
1838 }
1839 */
1840
1841 void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
1842 {
1843   if (!ok())
1844   {
1845     this->Command::printResult(out, verbosity);
1846   }
1847   else
1848   {
1849     out << *d_result;
1850   }
1851 }
1852
1853 Command* GetModelCommand::exportTo(ExprManager* exprManager,
1854                                    ExprManagerMapCollection& variableMap)
1855 {
1856   GetModelCommand* c = new GetModelCommand();
1857   c->d_result = d_result;
1858   c->d_smtEngine = d_smtEngine;
1859   return c;
1860 }
1861
1862 Command* GetModelCommand::clone() const
1863 {
1864   GetModelCommand* c = new GetModelCommand();
1865   c->d_result = d_result;
1866   c->d_smtEngine = d_smtEngine;
1867   return c;
1868 }
1869
1870 std::string GetModelCommand::getCommandName() const { return "get-model"; }
1871
1872 /* -------------------------------------------------------------------------- */
1873 /* class GetProofCommand                                                      */
1874 /* -------------------------------------------------------------------------- */
1875
1876 GetProofCommand::GetProofCommand() : d_smtEngine(nullptr), d_result(nullptr) {}
1877 void GetProofCommand::invoke(SmtEngine* smtEngine)
1878 {
1879   try
1880   {
1881     d_smtEngine = smtEngine;
1882     d_result = &smtEngine->getProof();
1883     d_commandStatus = CommandSuccess::instance();
1884   }
1885   catch (RecoverableModalException& e)
1886   {
1887     d_commandStatus = new CommandRecoverableFailure(e.what());
1888   }
1889   catch (UnsafeInterruptException& e)
1890   {
1891     d_commandStatus = new CommandInterrupted();
1892   }
1893   catch (exception& e)
1894   {
1895     d_commandStatus = new CommandFailure(e.what());
1896   }
1897 }
1898
1899 const Proof& GetProofCommand::getResult() const { return *d_result; }
1900 void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const
1901 {
1902   if (!ok())
1903   {
1904     this->Command::printResult(out, verbosity);
1905   }
1906   else
1907   {
1908     smt::SmtScope scope(d_smtEngine);
1909     d_result->toStream(out);
1910   }
1911 }
1912
1913 Command* GetProofCommand::exportTo(ExprManager* exprManager,
1914                                    ExprManagerMapCollection& variableMap)
1915 {
1916   GetProofCommand* c = new GetProofCommand();
1917   c->d_result = d_result;
1918   c->d_smtEngine = d_smtEngine;
1919   return c;
1920 }
1921
1922 Command* GetProofCommand::clone() const
1923 {
1924   GetProofCommand* c = new GetProofCommand();
1925   c->d_result = d_result;
1926   c->d_smtEngine = d_smtEngine;
1927   return c;
1928 }
1929
1930 std::string GetProofCommand::getCommandName() const { return "get-proof"; }
1931
1932 /* -------------------------------------------------------------------------- */
1933 /* class GetInstantiationsCommand                                             */
1934 /* -------------------------------------------------------------------------- */
1935
1936 GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {}
1937 void GetInstantiationsCommand::invoke(SmtEngine* smtEngine)
1938 {
1939   try
1940   {
1941     d_smtEngine = smtEngine;
1942     d_commandStatus = CommandSuccess::instance();
1943   }
1944   catch (exception& e)
1945   {
1946     d_commandStatus = new CommandFailure(e.what());
1947   }
1948 }
1949
1950 void GetInstantiationsCommand::printResult(std::ostream& out,
1951                                            uint32_t verbosity) const
1952 {
1953   if (!ok())
1954   {
1955     this->Command::printResult(out, verbosity);
1956   }
1957   else
1958   {
1959     d_smtEngine->printInstantiations(out);
1960   }
1961 }
1962
1963 Command* GetInstantiationsCommand::exportTo(
1964     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
1965 {
1966   GetInstantiationsCommand* c = new GetInstantiationsCommand();
1967   // c->d_result = d_result;
1968   c->d_smtEngine = d_smtEngine;
1969   return c;
1970 }
1971
1972 Command* GetInstantiationsCommand::clone() const
1973 {
1974   GetInstantiationsCommand* c = new GetInstantiationsCommand();
1975   // c->d_result = d_result;
1976   c->d_smtEngine = d_smtEngine;
1977   return c;
1978 }
1979
1980 std::string GetInstantiationsCommand::getCommandName() const
1981 {
1982   return "get-instantiations";
1983 }
1984
1985 /* -------------------------------------------------------------------------- */
1986 /* class GetSynthSolutionCommand                                              */
1987 /* -------------------------------------------------------------------------- */
1988
1989 GetSynthSolutionCommand::GetSynthSolutionCommand() : d_smtEngine(nullptr) {}
1990 void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine)
1991 {
1992   try
1993   {
1994     d_smtEngine = smtEngine;
1995     d_commandStatus = CommandSuccess::instance();
1996   }
1997   catch (exception& e)
1998   {
1999     d_commandStatus = new CommandFailure(e.what());
2000   }
2001 }
2002
2003 void GetSynthSolutionCommand::printResult(std::ostream& out,
2004                                           uint32_t verbosity) const
2005 {
2006   if (!ok())
2007   {
2008     this->Command::printResult(out, verbosity);
2009   }
2010   else
2011   {
2012     d_smtEngine->printSynthSolution(out);
2013   }
2014 }
2015
2016 Command* GetSynthSolutionCommand::exportTo(
2017     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2018 {
2019   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
2020   c->d_smtEngine = d_smtEngine;
2021   return c;
2022 }
2023
2024 Command* GetSynthSolutionCommand::clone() const
2025 {
2026   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
2027   c->d_smtEngine = d_smtEngine;
2028   return c;
2029 }
2030
2031 std::string GetSynthSolutionCommand::getCommandName() const
2032 {
2033   return "get-instantiations";
2034 }
2035
2036 GetAbductCommand::GetAbductCommand() {}
2037 GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj)
2038     : d_name(name), d_conj(conj), d_resultStatus(false)
2039 {
2040 }
2041 GetAbductCommand::GetAbductCommand(const std::string& name,
2042                                    Expr conj,
2043                                    const Type& gtype)
2044     : d_name(name),
2045       d_conj(conj),
2046       d_sygus_grammar_type(gtype),
2047       d_resultStatus(false)
2048 {
2049 }
2050
2051 Expr GetAbductCommand::getConjecture() const { return d_conj; }
2052 Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; }
2053 Expr GetAbductCommand::getResult() const { return d_result; }
2054
2055 void GetAbductCommand::invoke(SmtEngine* smtEngine)
2056 {
2057   try
2058   {
2059     if (d_sygus_grammar_type.isNull())
2060     {
2061       d_resultStatus = smtEngine->getAbduct(d_conj, d_result);
2062     }
2063     else
2064     {
2065       d_resultStatus =
2066           smtEngine->getAbduct(d_conj, d_sygus_grammar_type, d_result);
2067     }
2068     d_commandStatus = CommandSuccess::instance();
2069   }
2070   catch (exception& e)
2071   {
2072     d_commandStatus = new CommandFailure(e.what());
2073   }
2074 }
2075
2076 void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const
2077 {
2078   if (!ok())
2079   {
2080     this->Command::printResult(out, verbosity);
2081   }
2082   else
2083   {
2084     expr::ExprDag::Scope scope(out, false);
2085     if (d_resultStatus)
2086     {
2087       out << "(define-fun " << d_name << " () Bool " << d_result << ")"
2088           << std::endl;
2089     }
2090     else
2091     {
2092       out << "none" << std::endl;
2093     }
2094   }
2095 }
2096
2097 Command* GetAbductCommand::exportTo(ExprManager* exprManager,
2098                                     ExprManagerMapCollection& variableMap)
2099 {
2100   GetAbductCommand* c =
2101       new GetAbductCommand(d_name, d_conj.exportTo(exprManager, variableMap));
2102   c->d_sygus_grammar_type =
2103       d_sygus_grammar_type.exportTo(exprManager, variableMap);
2104   c->d_result = d_result.exportTo(exprManager, variableMap);
2105   c->d_resultStatus = d_resultStatus;
2106   return c;
2107 }
2108
2109 Command* GetAbductCommand::clone() const
2110 {
2111   GetAbductCommand* c = new GetAbductCommand(d_name, d_conj);
2112   c->d_sygus_grammar_type = d_sygus_grammar_type;
2113   c->d_result = d_result;
2114   c->d_resultStatus = d_resultStatus;
2115   return c;
2116 }
2117
2118 std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
2119
2120 /* -------------------------------------------------------------------------- */
2121 /* class GetQuantifierEliminationCommand                                      */
2122 /* -------------------------------------------------------------------------- */
2123
2124 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand()
2125     : d_expr(), d_doFull(true)
2126 {
2127 }
2128 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
2129     const Expr& expr, bool doFull)
2130     : d_expr(expr), d_doFull(doFull)
2131 {
2132 }
2133
2134 Expr GetQuantifierEliminationCommand::getExpr() const { return d_expr; }
2135 bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
2136 void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine)
2137 {
2138   try
2139   {
2140     d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull);
2141     d_commandStatus = CommandSuccess::instance();
2142   }
2143   catch (exception& e)
2144   {
2145     d_commandStatus = new CommandFailure(e.what());
2146   }
2147 }
2148
2149 Expr GetQuantifierEliminationCommand::getResult() const { return d_result; }
2150 void GetQuantifierEliminationCommand::printResult(std::ostream& out,
2151                                                   uint32_t verbosity) const
2152 {
2153   if (!ok())
2154   {
2155     this->Command::printResult(out, verbosity);
2156   }
2157   else
2158   {
2159     out << d_result << endl;
2160   }
2161 }
2162
2163 Command* GetQuantifierEliminationCommand::exportTo(
2164     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2165 {
2166   GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(
2167       d_expr.exportTo(exprManager, variableMap), d_doFull);
2168   c->d_result = d_result;
2169   return c;
2170 }
2171
2172 Command* GetQuantifierEliminationCommand::clone() const
2173 {
2174   GetQuantifierEliminationCommand* c =
2175       new GetQuantifierEliminationCommand(d_expr, d_doFull);
2176   c->d_result = d_result;
2177   return c;
2178 }
2179
2180 std::string GetQuantifierEliminationCommand::getCommandName() const
2181 {
2182   return d_doFull ? "get-qe" : "get-qe-disjunct";
2183 }
2184
2185 /* -------------------------------------------------------------------------- */
2186 /* class GetUnsatAssumptionsCommand                                           */
2187 /* -------------------------------------------------------------------------- */
2188
2189 GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
2190
2191 void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine)
2192 {
2193   try
2194   {
2195     d_result = smtEngine->getUnsatAssumptions();
2196     d_commandStatus = CommandSuccess::instance();
2197   }
2198   catch (RecoverableModalException& e)
2199   {
2200     d_commandStatus = new CommandRecoverableFailure(e.what());
2201   }
2202   catch (exception& e)
2203   {
2204     d_commandStatus = new CommandFailure(e.what());
2205   }
2206 }
2207
2208 std::vector<Expr> GetUnsatAssumptionsCommand::getResult() const
2209 {
2210   return d_result;
2211 }
2212
2213 void GetUnsatAssumptionsCommand::printResult(std::ostream& out,
2214                                              uint32_t verbosity) const
2215 {
2216   if (!ok())
2217   {
2218     this->Command::printResult(out, verbosity);
2219   }
2220   else
2221   {
2222     container_to_stream(out, d_result, "(", ")\n", " ");
2223   }
2224 }
2225
2226 Command* GetUnsatAssumptionsCommand::exportTo(
2227     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2228 {
2229   GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
2230   c->d_result = d_result;
2231   return c;
2232 }
2233
2234 Command* GetUnsatAssumptionsCommand::clone() const
2235 {
2236   GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
2237   c->d_result = d_result;
2238   return c;
2239 }
2240
2241 std::string GetUnsatAssumptionsCommand::getCommandName() const
2242 {
2243   return "get-unsat-assumptions";
2244 }
2245
2246 /* -------------------------------------------------------------------------- */
2247 /* class GetUnsatCoreCommand                                                  */
2248 /* -------------------------------------------------------------------------- */
2249
2250 GetUnsatCoreCommand::GetUnsatCoreCommand() {}
2251 void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine)
2252 {
2253   try
2254   {
2255     d_result = smtEngine->getUnsatCore();
2256     d_commandStatus = CommandSuccess::instance();
2257   }
2258   catch (RecoverableModalException& e)
2259   {
2260     d_commandStatus = new CommandRecoverableFailure(e.what());
2261   }
2262   catch (exception& e)
2263   {
2264     d_commandStatus = new CommandFailure(e.what());
2265   }
2266 }
2267
2268 void GetUnsatCoreCommand::printResult(std::ostream& out,
2269                                       uint32_t verbosity) const
2270 {
2271   if (!ok())
2272   {
2273     this->Command::printResult(out, verbosity);
2274   }
2275   else
2276   {
2277     d_result.toStream(out);
2278   }
2279 }
2280
2281 const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const
2282 {
2283   // of course, this will be empty if the command hasn't been invoked yet
2284   return d_result;
2285 }
2286
2287 Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager,
2288                                        ExprManagerMapCollection& variableMap)
2289 {
2290   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
2291   c->d_result = d_result;
2292   return c;
2293 }
2294
2295 Command* GetUnsatCoreCommand::clone() const
2296 {
2297   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
2298   c->d_result = d_result;
2299   return c;
2300 }
2301
2302 std::string GetUnsatCoreCommand::getCommandName() const
2303 {
2304   return "get-unsat-core";
2305 }
2306
2307 /* -------------------------------------------------------------------------- */
2308 /* class GetAssertionsCommand                                                 */
2309 /* -------------------------------------------------------------------------- */
2310
2311 GetAssertionsCommand::GetAssertionsCommand() {}
2312 void GetAssertionsCommand::invoke(SmtEngine* smtEngine)
2313 {
2314   try
2315   {
2316     stringstream ss;
2317     const vector<Expr> v = smtEngine->getAssertions();
2318     ss << "(\n";
2319     copy(v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n"));
2320     ss << ")\n";
2321     d_result = ss.str();
2322     d_commandStatus = CommandSuccess::instance();
2323   }
2324   catch (exception& e)
2325   {
2326     d_commandStatus = new CommandFailure(e.what());
2327   }
2328 }
2329
2330 std::string GetAssertionsCommand::getResult() const { return d_result; }
2331 void GetAssertionsCommand::printResult(std::ostream& out,
2332                                        uint32_t verbosity) const
2333 {
2334   if (!ok())
2335   {
2336     this->Command::printResult(out, verbosity);
2337   }
2338   else
2339   {
2340     out << d_result;
2341   }
2342 }
2343
2344 Command* GetAssertionsCommand::exportTo(ExprManager* exprManager,
2345                                         ExprManagerMapCollection& variableMap)
2346 {
2347   GetAssertionsCommand* c = new GetAssertionsCommand();
2348   c->d_result = d_result;
2349   return c;
2350 }
2351
2352 Command* GetAssertionsCommand::clone() const
2353 {
2354   GetAssertionsCommand* c = new GetAssertionsCommand();
2355   c->d_result = d_result;
2356   return c;
2357 }
2358
2359 std::string GetAssertionsCommand::getCommandName() const
2360 {
2361   return "get-assertions";
2362 }
2363
2364 /* -------------------------------------------------------------------------- */
2365 /* class SetBenchmarkStatusCommand                                            */
2366 /* -------------------------------------------------------------------------- */
2367
2368 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status)
2369     : d_status(status)
2370 {
2371 }
2372
2373 BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
2374 {
2375   return d_status;
2376 }
2377
2378 void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine)
2379 {
2380   try
2381   {
2382     stringstream ss;
2383     ss << d_status;
2384     SExpr status = SExpr(ss.str());
2385     smtEngine->setInfo("status", status);
2386     d_commandStatus = CommandSuccess::instance();
2387   }
2388   catch (exception& e)
2389   {
2390     d_commandStatus = new CommandFailure(e.what());
2391   }
2392 }
2393
2394 Command* SetBenchmarkStatusCommand::exportTo(
2395     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2396 {
2397   return new SetBenchmarkStatusCommand(d_status);
2398 }
2399
2400 Command* SetBenchmarkStatusCommand::clone() const
2401 {
2402   return new SetBenchmarkStatusCommand(d_status);
2403 }
2404
2405 std::string SetBenchmarkStatusCommand::getCommandName() const
2406 {
2407   return "set-info";
2408 }
2409
2410 /* -------------------------------------------------------------------------- */
2411 /* class SetBenchmarkLogicCommand                                             */
2412 /* -------------------------------------------------------------------------- */
2413
2414 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
2415     : d_logic(logic)
2416 {
2417 }
2418
2419 std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
2420 void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine)
2421 {
2422   try
2423   {
2424     smtEngine->setLogic(d_logic);
2425     d_commandStatus = CommandSuccess::instance();
2426   }
2427   catch (exception& e)
2428   {
2429     d_commandStatus = new CommandFailure(e.what());
2430   }
2431 }
2432
2433 Command* SetBenchmarkLogicCommand::exportTo(
2434     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2435 {
2436   return new SetBenchmarkLogicCommand(d_logic);
2437 }
2438
2439 Command* SetBenchmarkLogicCommand::clone() const
2440 {
2441   return new SetBenchmarkLogicCommand(d_logic);
2442 }
2443
2444 std::string SetBenchmarkLogicCommand::getCommandName() const
2445 {
2446   return "set-logic";
2447 }
2448
2449 /* -------------------------------------------------------------------------- */
2450 /* class SetInfoCommand                                                       */
2451 /* -------------------------------------------------------------------------- */
2452
2453 SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
2454     : d_flag(flag), d_sexpr(sexpr)
2455 {
2456 }
2457
2458 std::string SetInfoCommand::getFlag() const { return d_flag; }
2459 SExpr SetInfoCommand::getSExpr() const { return d_sexpr; }
2460 void SetInfoCommand::invoke(SmtEngine* smtEngine)
2461 {
2462   try
2463   {
2464     smtEngine->setInfo(d_flag, d_sexpr);
2465     d_commandStatus = CommandSuccess::instance();
2466   }
2467   catch (UnrecognizedOptionException&)
2468   {
2469     // As per SMT-LIB spec, silently accept unknown set-info keys
2470     d_commandStatus = CommandSuccess::instance();
2471   }
2472   catch (exception& e)
2473   {
2474     d_commandStatus = new CommandFailure(e.what());
2475   }
2476 }
2477
2478 Command* SetInfoCommand::exportTo(ExprManager* exprManager,
2479                                   ExprManagerMapCollection& variableMap)
2480 {
2481   return new SetInfoCommand(d_flag, d_sexpr);
2482 }
2483
2484 Command* SetInfoCommand::clone() const
2485 {
2486   return new SetInfoCommand(d_flag, d_sexpr);
2487 }
2488
2489 std::string SetInfoCommand::getCommandName() const { return "set-info"; }
2490
2491 /* -------------------------------------------------------------------------- */
2492 /* class GetInfoCommand                                                       */
2493 /* -------------------------------------------------------------------------- */
2494
2495 GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
2496 std::string GetInfoCommand::getFlag() const { return d_flag; }
2497 void GetInfoCommand::invoke(SmtEngine* smtEngine)
2498 {
2499   try
2500   {
2501     vector<SExpr> v;
2502     v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
2503     v.push_back(smtEngine->getInfo(d_flag));
2504     stringstream ss;
2505     if (d_flag == "all-options" || d_flag == "all-statistics")
2506     {
2507       ss << PrettySExprs(true);
2508     }
2509     ss << SExpr(v);
2510     d_result = ss.str();
2511     d_commandStatus = CommandSuccess::instance();
2512   }
2513   catch (UnrecognizedOptionException&)
2514   {
2515     d_commandStatus = new CommandUnsupported();
2516   }
2517   catch (RecoverableModalException& e)
2518   {
2519     d_commandStatus = new CommandRecoverableFailure(e.what());
2520   }
2521   catch (exception& e)
2522   {
2523     d_commandStatus = new CommandFailure(e.what());
2524   }
2525 }
2526
2527 std::string GetInfoCommand::getResult() const { return d_result; }
2528 void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const
2529 {
2530   if (!ok())
2531   {
2532     this->Command::printResult(out, verbosity);
2533   }
2534   else if (d_result != "")
2535   {
2536     out << d_result << endl;
2537   }
2538 }
2539
2540 Command* GetInfoCommand::exportTo(ExprManager* exprManager,
2541                                   ExprManagerMapCollection& variableMap)
2542 {
2543   GetInfoCommand* c = new GetInfoCommand(d_flag);
2544   c->d_result = d_result;
2545   return c;
2546 }
2547
2548 Command* GetInfoCommand::clone() const
2549 {
2550   GetInfoCommand* c = new GetInfoCommand(d_flag);
2551   c->d_result = d_result;
2552   return c;
2553 }
2554
2555 std::string GetInfoCommand::getCommandName() const { return "get-info"; }
2556
2557 /* -------------------------------------------------------------------------- */
2558 /* class SetOptionCommand                                                     */
2559 /* -------------------------------------------------------------------------- */
2560
2561 SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
2562     : d_flag(flag), d_sexpr(sexpr)
2563 {
2564 }
2565
2566 std::string SetOptionCommand::getFlag() const { return d_flag; }
2567 SExpr SetOptionCommand::getSExpr() const { return d_sexpr; }
2568 void SetOptionCommand::invoke(SmtEngine* smtEngine)
2569 {
2570   try
2571   {
2572     smtEngine->setOption(d_flag, d_sexpr);
2573     d_commandStatus = CommandSuccess::instance();
2574   }
2575   catch (UnrecognizedOptionException&)
2576   {
2577     d_commandStatus = new CommandUnsupported();
2578   }
2579   catch (exception& e)
2580   {
2581     d_commandStatus = new CommandFailure(e.what());
2582   }
2583 }
2584
2585 Command* SetOptionCommand::exportTo(ExprManager* exprManager,
2586                                     ExprManagerMapCollection& variableMap)
2587 {
2588   return new SetOptionCommand(d_flag, d_sexpr);
2589 }
2590
2591 Command* SetOptionCommand::clone() const
2592 {
2593   return new SetOptionCommand(d_flag, d_sexpr);
2594 }
2595
2596 std::string SetOptionCommand::getCommandName() const { return "set-option"; }
2597
2598 /* -------------------------------------------------------------------------- */
2599 /* class GetOptionCommand                                                     */
2600 /* -------------------------------------------------------------------------- */
2601
2602 GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
2603 std::string GetOptionCommand::getFlag() const { return d_flag; }
2604 void GetOptionCommand::invoke(SmtEngine* smtEngine)
2605 {
2606   try
2607   {
2608     SExpr res = smtEngine->getOption(d_flag);
2609     d_result = res.toString();
2610     d_commandStatus = CommandSuccess::instance();
2611   }
2612   catch (UnrecognizedOptionException&)
2613   {
2614     d_commandStatus = new CommandUnsupported();
2615   }
2616   catch (exception& e)
2617   {
2618     d_commandStatus = new CommandFailure(e.what());
2619   }
2620 }
2621
2622 std::string GetOptionCommand::getResult() const { return d_result; }
2623 void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const
2624 {
2625   if (!ok())
2626   {
2627     this->Command::printResult(out, verbosity);
2628   }
2629   else if (d_result != "")
2630   {
2631     out << d_result << endl;
2632   }
2633 }
2634
2635 Command* GetOptionCommand::exportTo(ExprManager* exprManager,
2636                                     ExprManagerMapCollection& variableMap)
2637 {
2638   GetOptionCommand* c = new GetOptionCommand(d_flag);
2639   c->d_result = d_result;
2640   return c;
2641 }
2642
2643 Command* GetOptionCommand::clone() const
2644 {
2645   GetOptionCommand* c = new GetOptionCommand(d_flag);
2646   c->d_result = d_result;
2647   return c;
2648 }
2649
2650 std::string GetOptionCommand::getCommandName() const { return "get-option"; }
2651
2652 /* -------------------------------------------------------------------------- */
2653 /* class SetExpressionNameCommand                                             */
2654 /* -------------------------------------------------------------------------- */
2655
2656 SetExpressionNameCommand::SetExpressionNameCommand(Expr expr, std::string name)
2657     : d_expr(expr), d_name(name)
2658 {
2659 }
2660
2661 void SetExpressionNameCommand::invoke(SmtEngine* smtEngine)
2662 {
2663   smtEngine->setExpressionName(d_expr, d_name);
2664   d_commandStatus = CommandSuccess::instance();
2665 }
2666
2667 Command* SetExpressionNameCommand::exportTo(
2668     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2669 {
2670   SetExpressionNameCommand* c = new SetExpressionNameCommand(
2671       d_expr.exportTo(exprManager, variableMap), d_name);
2672   return c;
2673 }
2674
2675 Command* SetExpressionNameCommand::clone() const
2676 {
2677   SetExpressionNameCommand* c = new SetExpressionNameCommand(d_expr, d_name);
2678   return c;
2679 }
2680
2681 std::string SetExpressionNameCommand::getCommandName() const
2682 {
2683   return "set-expr-name";
2684 }
2685
2686 /* -------------------------------------------------------------------------- */
2687 /* class DatatypeDeclarationCommand                                           */
2688 /* -------------------------------------------------------------------------- */
2689
2690 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
2691     const DatatypeType& datatype)
2692     : d_datatypes()
2693 {
2694   d_datatypes.push_back(datatype);
2695 }
2696
2697 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
2698     const std::vector<DatatypeType>& datatypes)
2699     : d_datatypes(datatypes)
2700 {
2701 }
2702
2703 const std::vector<DatatypeType>& DatatypeDeclarationCommand::getDatatypes()
2704     const
2705 {
2706   return d_datatypes;
2707 }
2708
2709 void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine)
2710 {
2711   d_commandStatus = CommandSuccess::instance();
2712 }
2713
2714 Command* DatatypeDeclarationCommand::exportTo(
2715     ExprManager* exprManager, ExprManagerMapCollection& variableMap)
2716 {
2717   throw ExportUnsupportedException(
2718       "export of DatatypeDeclarationCommand unsupported");
2719 }
2720
2721 Command* DatatypeDeclarationCommand::clone() const
2722 {
2723   return new DatatypeDeclarationCommand(d_datatypes);
2724 }
2725
2726 std::string DatatypeDeclarationCommand::getCommandName() const
2727 {
2728   return "declare-datatypes";
2729 }
2730
2731 /* -------------------------------------------------------------------------- */
2732 /* class RewriteRuleCommand                                                   */
2733 /* -------------------------------------------------------------------------- */
2734
2735 RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
2736                                        const std::vector<Expr>& guards,
2737                                        Expr head,
2738                                        Expr body,
2739                                        const Triggers& triggers)
2740     : d_vars(vars),
2741       d_guards(guards),
2742       d_head(head),
2743       d_body(body),
2744       d_triggers(triggers)
2745 {
2746 }
2747
2748 RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
2749                                        Expr head,
2750                                        Expr body)
2751     : d_vars(vars), d_head(head), d_body(body)
2752 {
2753 }
2754
2755 const std::vector<Expr>& RewriteRuleCommand::getVars() const { return d_vars; }
2756 const std::vector<Expr>& RewriteRuleCommand::getGuards() const
2757 {
2758   return d_guards;
2759 }
2760
2761 Expr RewriteRuleCommand::getHead() const { return d_head; }
2762 Expr RewriteRuleCommand::getBody() const { return d_body; }
2763 const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const
2764 {
2765   return d_triggers;
2766 }
2767
2768 void RewriteRuleCommand::invoke(SmtEngine* smtEngine)
2769 {
2770   try
2771   {
2772     ExprManager* em = smtEngine->getExprManager();
2773     /** build vars list */
2774     Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
2775     /** build guards list */
2776     Expr guards;
2777     if (d_guards.size() == 0)
2778       guards = em->mkConst<bool>(true);
2779     else if (d_guards.size() == 1)
2780       guards = d_guards[0];
2781     else
2782       guards = em->mkExpr(kind::AND, d_guards);
2783     /** build expression */
2784     Expr expr;
2785     if (d_triggers.empty())
2786     {
2787       expr = em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body);
2788     }
2789     else
2790     {
2791       /** build triggers list */
2792       std::vector<Expr> vtriggers;
2793       vtriggers.reserve(d_triggers.size());
2794       for (Triggers::const_iterator i = d_triggers.begin(),
2795                                     end = d_triggers.end();
2796            i != end;
2797            ++i)
2798       {
2799         vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i));
2800       }
2801       Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers);
2802       expr =
2803           em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body, triggers);
2804     }
2805     smtEngine->assertFormula(expr);
2806     d_commandStatus = CommandSuccess::instance();
2807   }
2808   catch (exception& e)
2809   {
2810     d_commandStatus = new CommandFailure(e.what());
2811   }
2812 }
2813
2814 Command* RewriteRuleCommand::exportTo(ExprManager* exprManager,
2815                                       ExprManagerMapCollection& variableMap)
2816 {
2817   /** Convert variables */
2818   VExpr vars = ExportTo(exprManager, variableMap, d_vars);
2819   /** Convert guards */
2820   VExpr guards = ExportTo(exprManager, variableMap, d_guards);
2821   /** Convert triggers */
2822   Triggers triggers;
2823   triggers.reserve(d_triggers.size());
2824   for (const std::vector<Expr>& trigger_list : d_triggers)
2825   {
2826     triggers.push_back(ExportTo(exprManager, variableMap, trigger_list));
2827   }
2828   /** Convert head and body */
2829   Expr head = d_head.exportTo(exprManager, variableMap);
2830   Expr body = d_body.exportTo(exprManager, variableMap);
2831   /** Create the converted rules */
2832   return new RewriteRuleCommand(vars, guards, head, body, triggers);
2833 }
2834
2835 Command* RewriteRuleCommand::clone() const
2836 {
2837   return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers);
2838 }
2839
2840 std::string RewriteRuleCommand::getCommandName() const
2841 {
2842   return "rewrite-rule";
2843 }
2844
2845 /* -------------------------------------------------------------------------- */
2846 /* class PropagateRuleCommand                                                 */
2847 /* -------------------------------------------------------------------------- */
2848
2849 PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
2850                                            const std::vector<Expr>& guards,
2851                                            const std::vector<Expr>& heads,
2852                                            Expr body,
2853                                            const Triggers& triggers,
2854                                            bool deduction)
2855     : d_vars(vars),
2856       d_guards(guards),
2857       d_heads(heads),
2858       d_body(body),
2859       d_triggers(triggers),
2860       d_deduction(deduction)
2861 {
2862 }
2863
2864 PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
2865                                            const std::vector<Expr>& heads,
2866                                            Expr body,
2867                                            bool deduction)
2868     : d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction)
2869 {
2870 }
2871
2872 const std::vector<Expr>& PropagateRuleCommand::getVars() const
2873 {
2874   return d_vars;
2875 }
2876
2877 const std::vector<Expr>& PropagateRuleCommand::getGuards() const
2878 {
2879   return d_guards;
2880 }
2881
2882 const std::vector<Expr>& PropagateRuleCommand::getHeads() const
2883 {
2884   return d_heads;
2885 }
2886
2887 Expr PropagateRuleCommand::getBody() const { return d_body; }
2888 const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const
2889 {
2890   return d_triggers;
2891 }
2892
2893 bool PropagateRuleCommand::isDeduction() const { return d_deduction; }
2894 void PropagateRuleCommand::invoke(SmtEngine* smtEngine)
2895 {
2896   try
2897   {
2898     ExprManager* em = smtEngine->getExprManager();
2899     /** build vars list */
2900     Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
2901     /** build guards list */
2902     Expr guards;
2903     if (d_guards.size() == 0)
2904       guards = em->mkConst<bool>(true);
2905     else if (d_guards.size() == 1)
2906       guards = d_guards[0];
2907     else
2908       guards = em->mkExpr(kind::AND, d_guards);
2909     /** build heads list */
2910     Expr heads;
2911     if (d_heads.size() == 1)
2912       heads = d_heads[0];
2913     else
2914       heads = em->mkExpr(kind::AND, d_heads);
2915     /** build expression */
2916     Expr expr;
2917     if (d_triggers.empty())
2918     {
2919       expr = em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body);
2920     }
2921     else
2922     {
2923       /** build triggers list */
2924       std::vector<Expr> vtriggers;
2925       vtriggers.reserve(d_triggers.size());
2926       for (Triggers::const_iterator i = d_triggers.begin(),
2927                                     end = d_triggers.end();
2928            i != end;
2929            ++i)
2930       {
2931         vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i));
2932       }
2933       Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers);
2934       expr =
2935           em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body, triggers);
2936     }
2937     smtEngine->assertFormula(expr);
2938     d_commandStatus = CommandSuccess::instance();
2939   }
2940   catch (exception& e)
2941   {
2942     d_commandStatus = new CommandFailure(e.what());
2943   }
2944 }
2945
2946 Command* PropagateRuleCommand::exportTo(ExprManager* exprManager,
2947                                         ExprManagerMapCollection& variableMap)
2948 {
2949   /** Convert variables */
2950   VExpr vars = ExportTo(exprManager, variableMap, d_vars);
2951   /** Convert guards */
2952   VExpr guards = ExportTo(exprManager, variableMap, d_guards);
2953   /** Convert heads */
2954   VExpr heads = ExportTo(exprManager, variableMap, d_heads);
2955   /** Convert triggers */
2956   Triggers triggers;
2957   triggers.reserve(d_triggers.size());
2958   for (const std::vector<Expr>& trigger_list : d_triggers)
2959   {
2960     triggers.push_back(ExportTo(exprManager, variableMap, trigger_list));
2961   }
2962   /** Convert head and body */
2963   Expr body = d_body.exportTo(exprManager, variableMap);
2964   /** Create the converted rules */
2965   return new PropagateRuleCommand(vars, guards, heads, body, triggers);
2966 }
2967
2968 Command* PropagateRuleCommand::clone() const
2969 {
2970   return new PropagateRuleCommand(
2971       d_vars, d_guards, d_heads, d_body, d_triggers);
2972 }
2973
2974 std::string PropagateRuleCommand::getCommandName() const
2975 {
2976   return "propagate-rule";
2977 }
2978 }  // namespace CVC4