src/smt/command.cpp

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