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