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