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-2016 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(UnsafeInterruptException& e) {
1027     d_commandStatus = new CommandInterrupted();
1028   } catch(exception& e) {
1029     d_commandStatus = new CommandFailure(e.what());
1030   }
1031 }
1032
1033 Expr GetValueCommand::getResult() const throw() {
1034   return d_result;
1035 }
1036
1037 void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const {
1038   if(! ok()) {
1039     this->Command::printResult(out, verbosity);
1040   } else {
1041     expr::ExprDag::Scope scope(out, false);
1042     out << d_result << endl;
1043   }
1044 }
1045
1046 Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1047   vector<Expr> exportedTerms;
1048   for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
1049     exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
1050   }
1051   GetValueCommand* c = new GetValueCommand(exportedTerms);
1052   c->d_result = d_result.exportTo(exprManager, variableMap);
1053   return c;
1054 }
1055
1056 Command* GetValueCommand::clone() const {
1057   GetValueCommand* c = new GetValueCommand(d_terms);
1058   c->d_result = d_result;
1059   return c;
1060 }
1061
1062 std::string GetValueCommand::getCommandName() const throw() {
1063   return "get-value";
1064 }
1065
1066 /* class GetAssignmentCommand */
1067
1068 GetAssignmentCommand::GetAssignmentCommand() throw() {
1069 }
1070
1071 void GetAssignmentCommand::invoke(SmtEngine* smtEngine) {
1072   try {
1073     d_result = smtEngine->getAssignment();
1074     d_commandStatus = CommandSuccess::instance();
1075   } catch(UnsafeInterruptException& e) {
1076     d_commandStatus = new CommandInterrupted();
1077   } catch(exception& e) {
1078     d_commandStatus = new CommandFailure(e.what());
1079   }
1080 }
1081
1082 SExpr GetAssignmentCommand::getResult() const throw() {
1083   return d_result;
1084 }
1085
1086 void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const {
1087   if(! ok()) {
1088     this->Command::printResult(out, verbosity);
1089   } else {
1090     out << d_result << endl;
1091   }
1092 }
1093
1094 Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1095   GetAssignmentCommand* c = new GetAssignmentCommand();
1096   c->d_result = d_result;
1097   return c;
1098 }
1099
1100 Command* GetAssignmentCommand::clone() const {
1101   GetAssignmentCommand* c = new GetAssignmentCommand();
1102   c->d_result = d_result;
1103   return c;
1104 }
1105
1106 std::string GetAssignmentCommand::getCommandName() const throw() {
1107   return "get-assignment";
1108 }
1109
1110 /* class GetModelCommand */
1111
1112 GetModelCommand::GetModelCommand() throw() {
1113 }
1114
1115 void GetModelCommand::invoke(SmtEngine* smtEngine) {
1116   try {
1117     d_result = smtEngine->getModel();
1118     d_smtEngine = smtEngine;
1119     d_commandStatus = CommandSuccess::instance();
1120   } catch(UnsafeInterruptException& e) {
1121     d_commandStatus = new CommandInterrupted();
1122   } catch(exception& e) {
1123     d_commandStatus = new CommandFailure(e.what());
1124   }
1125 }
1126
1127 /* Model is private to the library -- for now
1128 Model* GetModelCommand::getResult() const throw() {
1129   return d_result;
1130 }
1131 */
1132
1133 void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const {
1134   if(! ok()) {
1135     this->Command::printResult(out, verbosity);
1136   } else {
1137     out << *d_result;
1138   }
1139 }
1140
1141 Command* GetModelCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1142   GetModelCommand* c = new GetModelCommand();
1143   c->d_result = d_result;
1144   c->d_smtEngine = d_smtEngine;
1145   return c;
1146 }
1147
1148 Command* GetModelCommand::clone() const {
1149   GetModelCommand* c = new GetModelCommand();
1150   c->d_result = d_result;
1151   c->d_smtEngine = d_smtEngine;
1152   return c;
1153 }
1154
1155 std::string GetModelCommand::getCommandName() const throw() {
1156   return "get-model";
1157 }
1158
1159 /* class GetProofCommand */
1160
1161 GetProofCommand::GetProofCommand() throw() {
1162 }
1163
1164 void GetProofCommand::invoke(SmtEngine* smtEngine) {
1165   try {
1166     d_smtEngine = smtEngine;
1167     d_result = smtEngine->getProof();
1168     d_commandStatus = CommandSuccess::instance();
1169   } catch(UnsafeInterruptException& e) {
1170     d_commandStatus = new CommandInterrupted();
1171   } catch(exception& e) {
1172     d_commandStatus = new CommandFailure(e.what());
1173   }
1174 }
1175
1176 Proof* GetProofCommand::getResult() const throw() {
1177   return d_result;
1178 }
1179
1180 void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const {
1181   if(! ok()) {
1182     this->Command::printResult(out, verbosity);
1183   } else {
1184     smt::SmtScope scope(d_smtEngine);
1185     d_result->toStream(out);
1186   }
1187 }
1188
1189 Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1190   GetProofCommand* c = new GetProofCommand();
1191   c->d_result = d_result;
1192   c->d_smtEngine = d_smtEngine;
1193   return c;
1194 }
1195
1196 Command* GetProofCommand::clone() const {
1197   GetProofCommand* c = new GetProofCommand();
1198   c->d_result = d_result;
1199   c->d_smtEngine = d_smtEngine;
1200   return c;
1201 }
1202
1203 std::string GetProofCommand::getCommandName() const throw() {
1204   return "get-proof";
1205 }
1206
1207 /* class GetInstantiationsCommand */
1208
1209 GetInstantiationsCommand::GetInstantiationsCommand() throw() {
1210 }
1211
1212 void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) {
1213   try {
1214     d_smtEngine = smtEngine;
1215     d_commandStatus = CommandSuccess::instance();
1216   } catch(exception& e) {
1217     d_commandStatus = new CommandFailure(e.what());
1218   }
1219 }
1220
1221 //Instantiations* GetInstantiationsCommand::getResult() const throw() {
1222 //  return d_result;
1223 //}
1224
1225 void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
1226   if(! ok()) {
1227     this->Command::printResult(out, verbosity);
1228   } else {
1229     d_smtEngine->printInstantiations(out);
1230   }
1231 }
1232
1233 Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1234   GetInstantiationsCommand* c = new GetInstantiationsCommand();
1235   //c->d_result = d_result;
1236   c->d_smtEngine = d_smtEngine;
1237   return c;
1238 }
1239
1240 Command* GetInstantiationsCommand::clone() const {
1241   GetInstantiationsCommand* c = new GetInstantiationsCommand();
1242   //c->d_result = d_result;
1243   c->d_smtEngine = d_smtEngine;
1244   return c;
1245 }
1246
1247 std::string GetInstantiationsCommand::getCommandName() const throw() {
1248   return "get-instantiations";
1249 }
1250
1251 /* class GetSynthSolutionCommand */
1252
1253 GetSynthSolutionCommand::GetSynthSolutionCommand() throw() {
1254 }
1255
1256 void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) {
1257   try {
1258     d_smtEngine = smtEngine;
1259     d_commandStatus = CommandSuccess::instance();
1260   } catch(exception& e) {
1261     d_commandStatus = new CommandFailure(e.what());
1262   }
1263 }
1264
1265 void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const {
1266   if(! ok()) {
1267     this->Command::printResult(out, verbosity);
1268   } else {
1269     d_smtEngine->printSynthSolution(out);
1270   }
1271 }
1272
1273 Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1274   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
1275   c->d_smtEngine = d_smtEngine;
1276   return c;
1277 }
1278
1279 Command* GetSynthSolutionCommand::clone() const {
1280   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
1281   c->d_smtEngine = d_smtEngine;
1282   return c;
1283 }
1284
1285 std::string GetSynthSolutionCommand::getCommandName() const throw() {
1286   return "get-instantiations";
1287 }
1288
1289 /* class GetQuantifierEliminationCommand */
1290
1291 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() throw() :
1292   d_expr() {
1293 }
1294
1295 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(const Expr& expr, bool doFull) throw() :
1296   d_expr(expr), d_doFull(doFull) {
1297 }
1298
1299 Expr GetQuantifierEliminationCommand::getExpr() const throw() {
1300   return d_expr;
1301 }
1302 bool GetQuantifierEliminationCommand::getDoFull() const throw() {
1303   return d_doFull;
1304 }
1305
1306 void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) {
1307   try {
1308     d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull);
1309     d_commandStatus = CommandSuccess::instance();
1310   } catch(exception& e) {
1311     d_commandStatus = new CommandFailure(e.what());
1312   }
1313 }
1314
1315 Expr GetQuantifierEliminationCommand::getResult() const throw() {
1316   return d_result;
1317 }
1318
1319 void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const {
1320   if(! ok()) {
1321     this->Command::printResult(out, verbosity);
1322   } else {
1323     out << d_result << endl;
1324   }
1325 }
1326
1327 Command* GetQuantifierEliminationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1328   GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(d_expr.exportTo(exprManager, variableMap), d_doFull);
1329   c->d_result = d_result;
1330   return c;
1331 }
1332
1333 Command* GetQuantifierEliminationCommand::clone() const {
1334   GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(d_expr, d_doFull);
1335   c->d_result = d_result;
1336   return c;
1337 }
1338
1339 std::string GetQuantifierEliminationCommand::getCommandName() const throw() {
1340   return d_doFull ? "get-qe" : "get-qe-disjunct";
1341 }
1342
1343 /* class GetUnsatCoreCommand */
1344
1345 GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
1346 }
1347
1348 GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) {
1349 }
1350
1351 void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) {
1352   try {
1353     d_result = smtEngine->getUnsatCore();
1354     d_commandStatus = CommandSuccess::instance();
1355   } catch(exception& e) {
1356     d_commandStatus = new CommandFailure(e.what());
1357   }
1358 }
1359
1360 void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const {
1361   if(! ok()) {
1362     this->Command::printResult(out, verbosity);
1363   } else {
1364     d_result.toStream(out, d_names);
1365   }
1366 }
1367
1368 const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() {
1369   // of course, this will be empty if the command hasn't been invoked yet
1370   return d_result;
1371 }
1372
1373 Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1374   GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names);
1375   c->d_result = d_result;
1376   return c;
1377 }
1378
1379 Command* GetUnsatCoreCommand::clone() const {
1380   GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names);
1381   c->d_result = d_result;
1382   return c;
1383 }
1384
1385 std::string GetUnsatCoreCommand::getCommandName() const throw() {
1386   return "get-unsat-core";
1387 }
1388
1389 /* class GetAssertionsCommand */
1390
1391 GetAssertionsCommand::GetAssertionsCommand() throw() {
1392 }
1393
1394 void GetAssertionsCommand::invoke(SmtEngine* smtEngine) {
1395   try {
1396     stringstream ss;
1397     const vector<Expr> v = smtEngine->getAssertions();
1398     ss << "(\n";
1399     copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
1400     ss << ")\n";
1401     d_result = ss.str();
1402     d_commandStatus = CommandSuccess::instance();
1403   } catch(exception& e) {
1404     d_commandStatus = new CommandFailure(e.what());
1405   }
1406 }
1407
1408 std::string GetAssertionsCommand::getResult() const throw() {
1409   return d_result;
1410 }
1411
1412 void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const {
1413   if(! ok()) {
1414     this->Command::printResult(out, verbosity);
1415   } else {
1416     out << d_result;
1417   }
1418 }
1419
1420 Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1421   GetAssertionsCommand* c = new GetAssertionsCommand();
1422   c->d_result = d_result;
1423   return c;
1424 }
1425
1426 Command* GetAssertionsCommand::clone() const {
1427   GetAssertionsCommand* c = new GetAssertionsCommand();
1428   c->d_result = d_result;
1429   return c;
1430 }
1431
1432 std::string GetAssertionsCommand::getCommandName() const throw() {
1433   return "get-assertions";
1434 }
1435
1436 /* class SetBenchmarkStatusCommand */
1437
1438 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() :
1439   d_status(status) {
1440 }
1441
1442 BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() {
1443   return d_status;
1444 }
1445
1446 void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
1447   try {
1448     stringstream ss;
1449     ss << d_status;
1450     SExpr status = SExpr(ss.str());
1451     smtEngine->setInfo("status", status);
1452     d_commandStatus = CommandSuccess::instance();
1453   } catch(exception& e) {
1454     d_commandStatus = new CommandFailure(e.what());
1455   }
1456 }
1457
1458 Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1459   return new SetBenchmarkStatusCommand(d_status);
1460 }
1461
1462 Command* SetBenchmarkStatusCommand::clone() const {
1463   return new SetBenchmarkStatusCommand(d_status);
1464 }
1465
1466 std::string SetBenchmarkStatusCommand::getCommandName() const throw() {
1467   return "set-info";
1468 }
1469
1470 /* class SetBenchmarkLogicCommand */
1471
1472 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() :
1473   d_logic(logic) {
1474 }
1475
1476 std::string SetBenchmarkLogicCommand::getLogic() const throw() {
1477   return d_logic;
1478 }
1479
1480 void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
1481   try {
1482     smtEngine->setLogic(d_logic);
1483     d_commandStatus = CommandSuccess::instance();
1484   } catch(exception& e) {
1485     d_commandStatus = new CommandFailure(e.what());
1486   }
1487 }
1488
1489 Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1490   return new SetBenchmarkLogicCommand(d_logic);
1491 }
1492
1493 Command* SetBenchmarkLogicCommand::clone() const {
1494   return new SetBenchmarkLogicCommand(d_logic);
1495 }
1496
1497 std::string SetBenchmarkLogicCommand::getCommandName() const throw() {
1498   return "set-logic";
1499 }
1500
1501 /* class SetInfoCommand */
1502
1503 SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() :
1504   d_flag(flag),
1505   d_sexpr(sexpr) {
1506 }
1507
1508 std::string SetInfoCommand::getFlag() const throw() {
1509   return d_flag;
1510 }
1511
1512 SExpr SetInfoCommand::getSExpr() const throw() {
1513   return d_sexpr;
1514 }
1515
1516 void SetInfoCommand::invoke(SmtEngine* smtEngine) {
1517   try {
1518     smtEngine->setInfo(d_flag, d_sexpr);
1519     d_commandStatus = CommandSuccess::instance();
1520   } catch(UnrecognizedOptionException&) {
1521     // As per SMT-LIB spec, silently accept unknown set-info keys
1522     d_commandStatus = CommandSuccess::instance();
1523   } catch(exception& e) {
1524     d_commandStatus = new CommandFailure(e.what());
1525   }
1526 }
1527
1528 Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1529   return new SetInfoCommand(d_flag, d_sexpr);
1530 }
1531
1532 Command* SetInfoCommand::clone() const {
1533   return new SetInfoCommand(d_flag, d_sexpr);
1534 }
1535
1536 std::string SetInfoCommand::getCommandName() const throw() {
1537   return "set-info";
1538 }
1539
1540 /* class GetInfoCommand */
1541
1542 GetInfoCommand::GetInfoCommand(std::string flag) throw() :
1543   d_flag(flag) {
1544 }
1545
1546 std::string GetInfoCommand::getFlag() const throw() {
1547   return d_flag;
1548 }
1549
1550 void GetInfoCommand::invoke(SmtEngine* smtEngine) {
1551   try {
1552     vector<SExpr> v;
1553     v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
1554     v.push_back(smtEngine->getInfo(d_flag));
1555     stringstream ss;
1556     if(d_flag == "all-options" || d_flag == "all-statistics") {
1557       ss << PrettySExprs(true);
1558     }
1559     ss << SExpr(v);
1560     d_result = ss.str();
1561     d_commandStatus = CommandSuccess::instance();
1562   } catch(UnrecognizedOptionException&) {
1563     d_commandStatus = new CommandUnsupported();
1564   } catch(exception& e) {
1565     d_commandStatus = new CommandFailure(e.what());
1566   }
1567 }
1568
1569 std::string GetInfoCommand::getResult() const throw() {
1570   return d_result;
1571 }
1572
1573 void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const {
1574   if(! ok()) {
1575     this->Command::printResult(out, verbosity);
1576   } else if(d_result != "") {
1577     out << d_result << endl;
1578   }
1579 }
1580
1581 Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1582   GetInfoCommand* c = new GetInfoCommand(d_flag);
1583   c->d_result = d_result;
1584   return c;
1585 }
1586
1587 Command* GetInfoCommand::clone() const {
1588   GetInfoCommand* c = new GetInfoCommand(d_flag);
1589   c->d_result = d_result;
1590   return c;
1591 }
1592
1593 std::string GetInfoCommand::getCommandName() const throw() {
1594   return "get-info";
1595 }
1596
1597 /* class SetOptionCommand */
1598
1599 SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() :
1600   d_flag(flag),
1601   d_sexpr(sexpr) {
1602 }
1603
1604 std::string SetOptionCommand::getFlag() const throw() {
1605   return d_flag;
1606 }
1607
1608 SExpr SetOptionCommand::getSExpr() const throw() {
1609   return d_sexpr;
1610 }
1611
1612 void SetOptionCommand::invoke(SmtEngine* smtEngine) {
1613   try {
1614     smtEngine->setOption(d_flag, d_sexpr);
1615     d_commandStatus = CommandSuccess::instance();
1616   } catch(UnrecognizedOptionException&) {
1617     d_commandStatus = new CommandUnsupported();
1618   } catch(exception& e) {
1619     d_commandStatus = new CommandFailure(e.what());
1620   }
1621 }
1622
1623 Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1624   return new SetOptionCommand(d_flag, d_sexpr);
1625 }
1626
1627 Command* SetOptionCommand::clone() const {
1628   return new SetOptionCommand(d_flag, d_sexpr);
1629 }
1630
1631 std::string SetOptionCommand::getCommandName() const throw() {
1632   return "set-option";
1633 }
1634
1635 /* class GetOptionCommand */
1636
1637 GetOptionCommand::GetOptionCommand(std::string flag) throw() :
1638   d_flag(flag) {
1639 }
1640
1641 std::string GetOptionCommand::getFlag() const throw() {
1642   return d_flag;
1643 }
1644
1645 void GetOptionCommand::invoke(SmtEngine* smtEngine) {
1646   try {
1647     SExpr res = smtEngine->getOption(d_flag);
1648     d_result = res.toString();
1649     d_commandStatus = CommandSuccess::instance();
1650   } catch(UnrecognizedOptionException&) {
1651     d_commandStatus = new CommandUnsupported();
1652   } catch(exception& e) {
1653     d_commandStatus = new CommandFailure(e.what());
1654   }
1655 }
1656
1657 std::string GetOptionCommand::getResult() const throw() {
1658   return d_result;
1659 }
1660
1661 void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const {
1662   if(! ok()) {
1663     this->Command::printResult(out, verbosity);
1664   } else if(d_result != "") {
1665     out << d_result << endl;
1666   }
1667 }
1668
1669 Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1670   GetOptionCommand* c = new GetOptionCommand(d_flag);
1671   c->d_result = d_result;
1672   return c;
1673 }
1674
1675 Command* GetOptionCommand::clone() const {
1676   GetOptionCommand* c = new GetOptionCommand(d_flag);
1677   c->d_result = d_result;
1678   return c;
1679 }
1680
1681 std::string GetOptionCommand::getCommandName() const throw() {
1682   return "get-option";
1683 }
1684
1685 /* class DatatypeDeclarationCommand */
1686
1687 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
1688   d_datatypes() {
1689   d_datatypes.push_back(datatype);
1690 }
1691
1692 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() :
1693   d_datatypes(datatypes) {
1694 }
1695
1696 const std::vector<DatatypeType>&
1697 DatatypeDeclarationCommand::getDatatypes() const throw() {
1698   return d_datatypes;
1699 }
1700
1701 void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
1702   d_commandStatus = CommandSuccess::instance();
1703 }
1704
1705 Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1706   throw ExportUnsupportedException
1707           ("export of DatatypeDeclarationCommand unsupported");
1708 }
1709
1710 Command* DatatypeDeclarationCommand::clone() const {
1711   return new DatatypeDeclarationCommand(d_datatypes);
1712 }
1713
1714 std::string DatatypeDeclarationCommand::getCommandName() const throw() {
1715   return "declare-datatypes";
1716 }
1717
1718 /* class RewriteRuleCommand */
1719
1720 RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
1721                                        const std::vector<Expr>& guards,
1722                                        Expr head, Expr body,
1723                                        const Triggers& triggers) throw() :
1724   d_vars(vars), d_guards(guards), d_head(head), d_body(body), d_triggers(triggers) {
1725 }
1726
1727 RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
1728                                        Expr head, Expr body) throw() :
1729   d_vars(vars), d_head(head), d_body(body) {
1730 }
1731
1732 const std::vector<Expr>& RewriteRuleCommand::getVars() const throw() {
1733   return d_vars;
1734 }
1735
1736 const std::vector<Expr>& RewriteRuleCommand::getGuards() const throw() {
1737   return d_guards;
1738 }
1739
1740 Expr RewriteRuleCommand::getHead() const throw() {
1741   return d_head;
1742 }
1743
1744 Expr RewriteRuleCommand::getBody() const throw() {
1745   return d_body;
1746 }
1747
1748 const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const throw() {
1749   return d_triggers;
1750 }
1751
1752 void RewriteRuleCommand::invoke(SmtEngine* smtEngine) {
1753   try {
1754     ExprManager* em = smtEngine->getExprManager();
1755     /** build vars list */
1756     Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
1757     /** build guards list */
1758     Expr guards;
1759     if(d_guards.size() == 0) guards = em->mkConst<bool>(true);
1760     else if(d_guards.size() == 1) guards = d_guards[0];
1761     else guards = em->mkExpr(kind::AND,d_guards);
1762     /** build expression */
1763     Expr expr;
1764     if( d_triggers.empty() ){
1765       expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body);
1766     } else {
1767       /** build triggers list */
1768       std::vector<Expr> vtriggers;
1769       vtriggers.reserve(d_triggers.size());
1770       for(Triggers::const_iterator i = d_triggers.begin(),
1771             end = d_triggers.end(); i != end; ++i){
1772         vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i));
1773       }
1774       Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers);
1775       expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body,triggers);
1776     }
1777     smtEngine->assertFormula(expr);
1778     d_commandStatus = CommandSuccess::instance();
1779   } catch(exception& e) {
1780     d_commandStatus = new CommandFailure(e.what());
1781   }
1782 }
1783
1784 Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1785   /** Convert variables */
1786   VExpr vars; vars.reserve(d_vars.size());
1787   for(VExpr::iterator i = d_vars.begin(), end = d_vars.end();
1788       i == end; ++i){
1789     vars.push_back(i->exportTo(exprManager, variableMap));
1790   };
1791   /** Convert guards */
1792   VExpr guards; guards.reserve(d_guards.size());
1793   for(VExpr::iterator i = d_guards.begin(), end = d_guards.end();
1794       i == end; ++i){
1795     guards.push_back(i->exportTo(exprManager, variableMap));
1796   };
1797   /** Convert triggers */
1798   Triggers triggers; triggers.resize(d_triggers.size());
1799   for(size_t i = 0, end = d_triggers.size();
1800       i < end; ++i){
1801     triggers[i].reserve(d_triggers[i].size());
1802     for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end();
1803         j == jend; ++i){
1804       triggers[i].push_back(j->exportTo(exprManager, variableMap));
1805     };
1806   };
1807   /** Convert head and body */
1808   Expr head = d_head.exportTo(exprManager, variableMap);
1809   Expr body = d_body.exportTo(exprManager, variableMap);
1810   /** Create the converted rules */
1811   return new RewriteRuleCommand(vars, guards, head, body, triggers);
1812 }
1813
1814 Command* RewriteRuleCommand::clone() const {
1815   return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers);
1816 }
1817
1818 std::string RewriteRuleCommand::getCommandName() const throw() {
1819   return "rewrite-rule";
1820 }
1821
1822 /* class PropagateRuleCommand */
1823
1824 PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
1825                                            const std::vector<Expr>& guards,
1826                                            const std::vector<Expr>& heads,
1827                                            Expr body,
1828                                            const Triggers& triggers,
1829                                            bool deduction) throw() :
1830   d_vars(vars), d_guards(guards), d_heads(heads), d_body(body), d_triggers(triggers), d_deduction(deduction) {
1831 }
1832
1833 PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
1834                                            const std::vector<Expr>& heads,
1835                                            Expr body,
1836                                            bool deduction) throw() :
1837   d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) {
1838 }
1839
1840 const std::vector<Expr>& PropagateRuleCommand::getVars() const throw() {
1841   return d_vars;
1842 }
1843
1844 const std::vector<Expr>& PropagateRuleCommand::getGuards() const throw() {
1845   return d_guards;
1846 }
1847
1848 const std::vector<Expr>& PropagateRuleCommand::getHeads() const throw() {
1849   return d_heads;
1850 }
1851
1852 Expr PropagateRuleCommand::getBody() const throw() {
1853   return d_body;
1854 }
1855
1856 const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const throw() {
1857   return d_triggers;
1858 }
1859
1860 bool PropagateRuleCommand::isDeduction() const throw() {
1861   return d_deduction;
1862 }
1863
1864 void PropagateRuleCommand::invoke(SmtEngine* smtEngine) {
1865   try {
1866     ExprManager* em = smtEngine->getExprManager();
1867     /** build vars list */
1868     Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
1869     /** build guards list */
1870     Expr guards;
1871     if(d_guards.size() == 0) guards = em->mkConst<bool>(true);
1872     else if(d_guards.size() == 1) guards = d_guards[0];
1873     else guards = em->mkExpr(kind::AND,d_guards);
1874     /** build heads list */
1875     Expr heads;
1876     if(d_heads.size() == 1) heads = d_heads[0];
1877     else heads = em->mkExpr(kind::AND,d_heads);
1878     /** build expression */
1879     Expr expr;
1880     if( d_triggers.empty() ){
1881       expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body);
1882     } else {
1883       /** build triggers list */
1884       std::vector<Expr> vtriggers;
1885       vtriggers.reserve(d_triggers.size());
1886       for(Triggers::const_iterator i = d_triggers.begin(),
1887             end = d_triggers.end(); i != end; ++i){
1888         vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i));
1889       }
1890       Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers);
1891       expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body,triggers);
1892     }
1893     smtEngine->assertFormula(expr);
1894     d_commandStatus = CommandSuccess::instance();
1895   } catch(exception& e) {
1896     d_commandStatus = new CommandFailure(e.what());
1897   }
1898 }
1899
1900 Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1901   /** Convert variables */
1902   VExpr vars; vars.reserve(d_vars.size());
1903   for(VExpr::iterator i = d_vars.begin(), end = d_vars.end();
1904       i == end; ++i){
1905     vars.push_back(i->exportTo(exprManager, variableMap));
1906   };
1907   /** Convert guards */
1908   VExpr guards; guards.reserve(d_guards.size());
1909   for(VExpr::iterator i = d_guards.begin(), end = d_guards.end();
1910       i == end; ++i){
1911     guards.push_back(i->exportTo(exprManager, variableMap));
1912   };
1913   /** Convert heads */
1914   VExpr heads; heads.reserve(d_heads.size());
1915   for(VExpr::iterator i = d_heads.begin(), end = d_heads.end();
1916       i == end; ++i){
1917     heads.push_back(i->exportTo(exprManager, variableMap));
1918   };
1919   /** Convert triggers */
1920   Triggers triggers; triggers.resize(d_triggers.size());
1921   for(size_t i = 0, end = d_triggers.size();
1922       i < end; ++i){
1923     triggers[i].reserve(d_triggers[i].size());
1924     for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end();
1925         j == jend; ++i){
1926       triggers[i].push_back(j->exportTo(exprManager, variableMap));
1927     };
1928   };
1929   /** Convert head and body */
1930   Expr body = d_body.exportTo(exprManager, variableMap);
1931   /** Create the converted rules */
1932   return new PropagateRuleCommand(vars, guards, heads, body, triggers);
1933 }
1934
1935 Command* PropagateRuleCommand::clone() const {
1936   return new PropagateRuleCommand(d_vars, d_guards, d_heads, d_body, d_triggers);
1937 }
1938
1939 std::string PropagateRuleCommand::getCommandName() const throw() {
1940   return "propagate-rule";
1941 }
1942
1943 /* output stream insertion operator for benchmark statuses */
1944 std::ostream& operator<<(std::ostream& out,
1945                          BenchmarkStatus status) throw() {
1946   switch(status) {
1947
1948   case SMT_SATISFIABLE:
1949     return out << "sat";
1950
1951   case SMT_UNSATISFIABLE:
1952     return out << "unsat";
1953
1954   case SMT_UNKNOWN:
1955     return out << "unknown";
1956
1957   default:
1958     return out << "BenchmarkStatus::[UNKNOWNSTATUS!]";
1959   }
1960 }
1961
1962 }/* CVC4 namespace */