src/smt/command.cpp

   1 /*********************                                                        */
   2 /*! \file command.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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) throw() {
 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 throw() {
 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) throw() {
 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) throw() {
 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) throw() {
 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) throw() {
 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) throw() {
 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) throw() {
 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) throw() {
 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 throw() {
 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) throw() {
 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 throw() {
 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 /* class ResetCommand */
 380
 381 void ResetCommand::invoke(SmtEngine* smtEngine) throw() {
 382   try {
 383     smtEngine->reset();
 384     d_commandStatus = CommandSuccess::instance();
 385   } catch(exception& e) {
 386     d_commandStatus = new CommandFailure(e.what());
 387   }
 388 }
 389
 390 Command* ResetCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
 391   return new ResetCommand();
 392 }
 393
 394 Command* ResetCommand::clone() const {
 395   return new ResetCommand();
 396 }
 397
 398 std::string ResetCommand::getCommandName() const throw() {
 399   return "reset";
 400 }
 401
 402 /* class ResetAssertionsCommand */
 403
 404 void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
 405   try {
 406     smtEngine->resetAssertions();
 407     d_commandStatus = CommandSuccess::instance();
 408   } catch(exception& e) {
 409     d_commandStatus = new CommandFailure(e.what());
 410   }
 411 }
 412
 413 Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
 414   return new ResetAssertionsCommand();
 415 }
 416
 417 Command* ResetAssertionsCommand::clone() const {
 418   return new ResetAssertionsCommand();
 419 }
 420
 421 std::string ResetAssertionsCommand::getCommandName() const throw() {
 422   return "reset-assertions";
 423 }
 424
 425 /* class QuitCommand */
 426
 427 void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
 428   Dump("benchmark") << *this;
 429   d_commandStatus = CommandSuccess::instance();
 430 }
 431
 432 Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
 433   return new QuitCommand();
 434 }
 435
 436 Command* QuitCommand::clone() const {
 437   return new QuitCommand();
 438 }
 439
 440 std::string QuitCommand::getCommandName() const throw() {
 441   return "exit";
 442 }
 443
 444 /* class CommentCommand */
 445
 446 CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) {
 447 }
 448
 449 std::string CommentCommand::getComment() const throw() {
 450   return d_comment;
 451 }
 452
 453 void CommentCommand::invoke(SmtEngine* smtEngine) throw() {
 454   Dump("benchmark") << *this;
 455   d_commandStatus = CommandSuccess::instance();
 456 }
 457
 458 Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
 459   return new CommentCommand(d_comment);
 460 }
 461
 462 Command* CommentCommand::clone() const {
 463   return new CommentCommand(d_comment);
 464 }
 465
 466 std::string CommentCommand::getCommandName() const throw() {
 467   return "comment";
 468 }
 469
 470 /* class CommandSequence */
 471
 472 CommandSequence::CommandSequence() throw() :
 473   d_index(0) {
 474 }
 475
 476 CommandSequence::~CommandSequence() throw() {
 477   for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
 478     delete d_commandSequence[i];
 479   }
 480 }
 481
 482 void CommandSequence::addCommand(Command* cmd) throw() {
 483   d_commandSequence.push_back(cmd);
 484 }
 485
 486 void CommandSequence::clear() throw() {
 487   d_commandSequence.clear();
 488 }
 489
 490 void CommandSequence::invoke(SmtEngine* smtEngine) throw() {
 491   for(; d_index < d_commandSequence.size(); ++d_index) {
 492     d_commandSequence[d_index]->invoke(smtEngine);
 493     if(! d_commandSequence[d_index]->ok()) {
 494       // abort execution
 495       d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
 496       return;
 497     }
 498     delete d_commandSequence[d_index];
 499   }
 500
 501   AlwaysAssert(d_commandStatus == NULL);
 502   d_commandStatus = CommandSuccess::instance();
 503 }
 504
 505 void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
 506   for(; d_index < d_commandSequence.size(); ++d_index) {
 507     d_commandSequence[d_index]->invoke(smtEngine, out);
 508     if(! d_commandSequence[d_index]->ok()) {
 509       // abort execution
 510       d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
 511       return;
 512     }
 513     delete d_commandSequence[d_index];
 514   }
 515
 516   AlwaysAssert(d_commandStatus == NULL);
 517   d_commandStatus = CommandSuccess::instance();
 518 }
 519
 520 Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
 521   CommandSequence* seq = new CommandSequence();
 522   for(iterator i = begin(); i != end(); ++i) {
 523     Command* cmd_to_export = *i;
 524     Command* cmd = cmd_to_export->exportTo(exprManager, variableMap);
 525     seq->addCommand(cmd);
 526     Debug("export") << "[export] so far converted: " << seq << endl;
 527   }
 528   seq->d_index = d_index;
 529   return seq;
 530 }
 531
 532 Command* CommandSequence::clone() const {
 533   CommandSequence* seq = new CommandSequence();
 534   for(const_iterator i = begin(); i != end(); ++i) {
 535     seq->addCommand((*i)->clone());
 536   }
 537   seq->d_index = d_index;
 538   return seq;
 539 }
 540
 541 CommandSequence::const_iterator CommandSequence::begin() const throw() {
 542   return d_commandSequence.begin();
 543 }
 544
 545 CommandSequence::const_iterator CommandSequence::end() const throw() {
 546   return d_commandSequence.end();
 547 }
 548
 549 CommandSequence::iterator CommandSequence::begin() throw() {
 550   return d_commandSequence.begin();
 551 }
 552
 553 CommandSequence::iterator CommandSequence::end() throw() {
 554   return d_commandSequence.end();
 555 }
 556
 557 std::string CommandSequence::getCommandName() const throw() {
 558   return "sequence";
 559 }
 560
 561 /* class DeclarationSequenceCommand */
 562
 563 /* class DeclarationDefinitionCommand */
 564
 565 DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() :
 566   d_symbol(id) {
 567 }
 568
 569 std::string DeclarationDefinitionCommand::getSymbol() const throw() {
 570   return d_symbol;
 571 }
 572
 573 /* class DeclareFunctionCommand */
 574
 575 DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, Type t) throw() :
 576   DeclarationDefinitionCommand(id),
 577   d_func(func),
 578   d_type(t),
 579   d_printInModel(true),
 580   d_printInModelSetByUser(false){
 581 }
 582
 583 Expr DeclareFunctionCommand::getFunction() const throw() {
 584   return d_func;
 585 }
 586
 587 Type DeclareFunctionCommand::getType() const throw() {
 588   return d_type;
 589 }
 590
 591 bool DeclareFunctionCommand::getPrintInModel() const throw() {
 592   return d_printInModel;
 593 }
 594
 595 bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() {
 596   return d_printInModelSetByUser;
 597 }
 598
 599 void DeclareFunctionCommand::setPrintInModel( bool p ) {
 600   d_printInModel = p;
 601   d_printInModelSetByUser = true;
 602 }
 603
 604 void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
 605   d_commandStatus = CommandSuccess::instance();
 606 }
 607
 608 Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
 609                                           ExprManagerMapCollection& variableMap) {
 610   DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap),
 611                                                             d_type.exportTo(exprManager, variableMap));
 612   dfc->d_printInModel = d_printInModel;
 613   dfc->d_printInModelSetByUser = d_printInModelSetByUser;
 614   return dfc;
 615 }
 616
 617 Command* DeclareFunctionCommand::clone() const {
 618   DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func, d_type);
 619   dfc->d_printInModel = d_printInModel;
 620   dfc->d_printInModelSetByUser = d_printInModelSetByUser;
 621   return dfc;
 622 }
 623
 624 std::string DeclareFunctionCommand::getCommandName() const throw() {
 625   return "declare-fun";
 626 }
 627
 628 /* class DeclareTypeCommand */
 629
 630 DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() :
 631   DeclarationDefinitionCommand(id),
 632   d_arity(arity),
 633   d_type(t) {
 634 }
 635
 636 size_t DeclareTypeCommand::getArity() const throw() {
 637   return d_arity;
 638 }
 639
 640 Type DeclareTypeCommand::getType() const throw() {
 641   return d_type;
 642 }
 643
 644 void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
 645   d_commandStatus = CommandSuccess::instance();
 646 }
 647
 648 Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
 649                                       ExprManagerMapCollection& variableMap) {
 650   return new DeclareTypeCommand(d_symbol, d_arity,
 651                                 d_type.exportTo(exprManager, variableMap));
 652 }
 653
 654 Command* DeclareTypeCommand::clone() const {
 655   return new DeclareTypeCommand(d_symbol, d_arity, d_type);
 656 }
 657
 658 std::string DeclareTypeCommand::getCommandName() const throw() {
 659   return "declare-sort";
 660 }
 661
 662 /* class DefineTypeCommand */
 663
 664 DefineTypeCommand::DefineTypeCommand(const std::string& id,
 665                                      Type t) throw() :
 666   DeclarationDefinitionCommand(id),
 667   d_params(),
 668   d_type(t) {
 669 }
 670
 671 DefineTypeCommand::DefineTypeCommand(const std::string& id,
 672                                      const std::vector<Type>& params,
 673                                      Type t) throw() :
 674   DeclarationDefinitionCommand(id),
 675   d_params(params),
 676   d_type(t) {
 677 }
 678
 679 const std::vector<Type>& DefineTypeCommand::getParameters() const throw() {
 680   return d_params;
 681 }
 682
 683 Type DefineTypeCommand::getType() const throw() {
 684   return d_type;
 685 }
 686
 687 void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
 688   d_commandStatus = CommandSuccess::instance();
 689 }
 690
 691 Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
 692   vector<Type> params;
 693   transform(d_params.begin(), d_params.end(), back_inserter(params),
 694             ExportTransformer(exprManager, variableMap));
 695   Type type = d_type.exportTo(exprManager, variableMap);
 696   return new DefineTypeCommand(d_symbol, params, type);
 697 }
 698
 699 Command* DefineTypeCommand::clone() const {
 700   return new DefineTypeCommand(d_symbol, d_params, d_type);
 701 }
 702
 703 std::string DefineTypeCommand::getCommandName() const throw() {
 704   return "define-sort";
 705 }
 706
 707 /* class DefineFunctionCommand */
 708
 709 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
 710                                              Expr func,
 711                                              Expr formula) throw() :
 712   DeclarationDefinitionCommand(id),
 713   d_func(func),
 714   d_formals(),
 715   d_formula(formula) {
 716 }
 717
 718 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
 719                                              Expr func,
 720                                              const std::vector<Expr>& formals,
 721                                              Expr formula) throw() :
 722   DeclarationDefinitionCommand(id),
 723   d_func(func),
 724   d_formals(formals),
 725   d_formula(formula) {
 726 }
 727
 728 Expr DefineFunctionCommand::getFunction() const throw() {
 729   return d_func;
 730 }
 731
 732 const std::vector<Expr>& DefineFunctionCommand::getFormals() const throw() {
 733   return d_formals;
 734 }
 735
 736 Expr DefineFunctionCommand::getFormula() const throw() {
 737   return d_formula;
 738 }
 739
 740 void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
 741   try {
 742     if(!d_func.isNull()) {
 743       smtEngine->defineFunction(d_func, d_formals, d_formula);
 744     }
 745     d_commandStatus = CommandSuccess::instance();
 746   } catch(exception& e) {
 747     d_commandStatus = new CommandFailure(e.what());
 748   }
 749 }
 750
 751 Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
 752   Expr func = d_func.exportTo(exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
 753   vector<Expr> formals;
 754   transform(d_formals.begin(), d_formals.end(), back_inserter(formals),
 755             ExportTransformer(exprManager, variableMap));
 756   Expr formula = d_formula.exportTo(exprManager, variableMap);
 757   return new DefineFunctionCommand(d_symbol, func, formals, formula);
 758 }
 759
 760 Command* DefineFunctionCommand::clone() const {
 761   return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula);
 762 }
 763
 764 std::string DefineFunctionCommand::getCommandName() const throw() {
 765   return "define-fun";
 766 }
 767
 768 /* class DefineNamedFunctionCommand */
 769
 770 DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
 771                                                        Expr func,
 772                                                        const std::vector<Expr>& formals,
 773                                                        Expr formula) throw() :
 774   DefineFunctionCommand(id, func, formals, formula) {
 775 }
 776
 777 void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
 778   this->DefineFunctionCommand::invoke(smtEngine);
 779   if(!d_func.isNull() && d_func.getType().isBoolean()) {
 780     smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func));
 781   }
 782   d_commandStatus = CommandSuccess::instance();
 783 }
 784
 785 Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
 786   Expr func = d_func.exportTo(exprManager, variableMap);
 787   vector<Expr> formals;
 788   transform(d_formals.begin(), d_formals.end(), back_inserter(formals),
 789             ExportTransformer(exprManager, variableMap));
 790   Expr formula = d_formula.exportTo(exprManager, variableMap);
 791   return new DefineNamedFunctionCommand(d_symbol, func, formals, formula);
 792 }
 793
 794 Command* DefineNamedFunctionCommand::clone() const {
 795   return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
 796 }
 797
 798 /* class SetUserAttribute */
 799
 800 SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() :
 801   d_attr( attr ), d_expr( expr ){
 802 }
 803
 804 SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr,
 805                                                   std::vector<Expr>& values ) throw() :
 806   d_attr( attr ), d_expr( expr ){
 807   d_expr_values.insert( d_expr_values.begin(), values.begin(), values.end() );
 808 }
 809
 810 SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr,
 811                                                   const std::string& value ) throw() :
 812   d_attr( attr ), d_expr( expr ), d_str_value( value ){
 813 }
 814
 815 void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){
 816   try {
 817     if(!d_expr.isNull()) {
 818       smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value );
 819     }
 820     d_commandStatus = CommandSuccess::instance();
 821   } catch(exception& e) {
 822     d_commandStatus = new CommandFailure(e.what());
 823   }
 824 }
 825
 826 Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){
 827   Expr expr = d_expr.exportTo(exprManager, variableMap);
 828   SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, expr, d_str_value );
 829   c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() );
 830   return c;
 831 }
 832
 833 Command* SetUserAttributeCommand::clone() const{
 834   SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, d_expr, d_str_value );
 835   c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() );
 836   return c;
 837 }
 838
 839 std::string SetUserAttributeCommand::getCommandName() const throw() {
 840   return "set-user-attribute";
 841 }
 842
 843 /* class SimplifyCommand */
 844
 845 SimplifyCommand::SimplifyCommand(Expr term) throw() :
 846   d_term(term) {
 847 }
 848
 849 Expr SimplifyCommand::getTerm() const throw() {
 850   return d_term;
 851 }
 852
 853 void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() {
 854   try {
 855     d_result = smtEngine->simplify(d_term);
 856     d_commandStatus = CommandSuccess::instance();
 857   } catch(UnsafeInterruptException& e) {
 858     d_commandStatus = new CommandInterrupted();
 859   } catch(exception& e) {
 860     d_commandStatus = new CommandFailure(e.what());
 861   }
 862 }
 863
 864 Expr SimplifyCommand::getResult() const throw() {
 865   return d_result;
 866 }
 867
 868 void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
 869   if(! ok()) {
 870     this->Command::printResult(out, verbosity);
 871   } else {
 872     out << d_result << endl;
 873   }
 874 }
 875
 876 Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
 877   SimplifyCommand* c = new SimplifyCommand(d_term.exportTo(exprManager, variableMap));
 878   c->d_result = d_result.exportTo(exprManager, variableMap);
 879   return c;
 880 }
 881
 882 Command* SimplifyCommand::clone() const {
 883   SimplifyCommand* c = new SimplifyCommand(d_term);
 884   c->d_result = d_result;
 885   return c;
 886 }
 887
 888 std::string SimplifyCommand::getCommandName() const throw() {
 889   return "simplify";
 890 }
 891
 892 /* class ExpandDefinitionsCommand */
 893
 894 ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() :
 895   d_term(term) {
 896 }
 897
 898 Expr ExpandDefinitionsCommand::getTerm() const throw() {
 899   return d_term;
 900 }
 901
 902 void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() {
 903   d_result = smtEngine->expandDefinitions(d_term);
 904   d_commandStatus = CommandSuccess::instance();
 905 }
 906
 907 Expr ExpandDefinitionsCommand::getResult() const throw() {
 908   return d_result;
 909 }
 910
 911 void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
 912   if(! ok()) {
 913     this->Command::printResult(out, verbosity);
 914   } else {
 915     out << d_result << endl;
 916   }
 917 }
 918
 919 Command* ExpandDefinitionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
 920   ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap));
 921   c->d_result = d_result.exportTo(exprManager, variableMap);
 922   return c;
 923 }
 924
 925 Command* ExpandDefinitionsCommand::clone() const {
 926   ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term);
 927   c->d_result = d_result;
 928   return c;
 929 }
 930
 931 std::string ExpandDefinitionsCommand::getCommandName() const throw() {
 932   return "expand-definitions";
 933 }
 934
 935 /* class GetValueCommand */
 936
 937 GetValueCommand::GetValueCommand(Expr term) throw() :
 938   d_terms() {
 939   d_terms.push_back(term);
 940 }
 941
 942 GetValueCommand::GetValueCommand(const std::vector<Expr>& terms) throw() :
 943   d_terms(terms) {
 944   PrettyCheckArgument(terms.size() >= 1, terms,
 945                       "cannot get-value of an empty set of terms");
 946 }
 947
 948 const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
 949   return d_terms;
 950 }
 951
 952 void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
 953   try {
 954     vector<Expr> result;
 955     ExprManager* em = smtEngine->getExprManager();
 956     NodeManager* nm = NodeManager::fromExprManager(em);
 957     for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
 958       Assert(nm == NodeManager::fromExprManager((*i).getExprManager()));
 959       smt::SmtScope scope(smtEngine);
 960       Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i);
 961       Node value = Node::fromExpr(smtEngine->getValue(*i));
 962       if(value.getType().isInteger() && request.getType() == nm->realType()) {
 963         // Need to wrap in special marker so that output printers know this
 964         // is an integer-looking constant that really should be output as
 965         // a rational.  Necessary for SMT-LIB standards compliance, but ugly.
 966         value = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
 967                            nm->mkConst(AscriptionType(em->realType())), value);
 968       }
 969       result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr());
 970     }
 971     d_result = em->mkExpr(kind::SEXPR, result);
 972     d_commandStatus = CommandSuccess::instance();
 973   } catch(UnsafeInterruptException& e) {
 974     d_commandStatus = new CommandInterrupted();
 975   } catch(exception& e) {
 976     d_commandStatus = new CommandFailure(e.what());
 977   }
 978 }
 979
 980 Expr GetValueCommand::getResult() const throw() {
 981   return d_result;
 982 }
 983
 984 void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
 985   if(! ok()) {
 986     this->Command::printResult(out, verbosity);
 987   } else {
 988     expr::ExprDag::Scope scope(out, false);
 989     out << d_result << endl;
 990   }
 991 }
 992
 993 Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
 994   vector<Expr> exportedTerms;
 995   for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
 996     exportedTerms.push_back((*i).exportTo(exprManager, variableMap));
 997   }
 998   GetValueCommand* c = new GetValueCommand(exportedTerms);
 999   c->d_result = d_result.exportTo(exprManager, variableMap);
1000   return c;
1001 }
1002
1003 Command* GetValueCommand::clone() const {
1004   GetValueCommand* c = new GetValueCommand(d_terms);
1005   c->d_result = d_result;
1006   return c;
1007 }
1008
1009 std::string GetValueCommand::getCommandName() const throw() {
1010   return "get-value";
1011 }
1012
1013 /* class GetAssignmentCommand */
1014
1015 GetAssignmentCommand::GetAssignmentCommand() throw() {
1016 }
1017
1018 void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() {
1019   try {
1020     d_result = smtEngine->getAssignment();
1021     d_commandStatus = CommandSuccess::instance();
1022   } catch(UnsafeInterruptException& e) {
1023     d_commandStatus = new CommandInterrupted();
1024   } catch(exception& e) {
1025     d_commandStatus = new CommandFailure(e.what());
1026   }
1027 }
1028
1029 SExpr GetAssignmentCommand::getResult() const throw() {
1030   return d_result;
1031 }
1032
1033 void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
1034   if(! ok()) {
1035     this->Command::printResult(out, verbosity);
1036   } else {
1037     out << d_result << endl;
1038   }
1039 }
1040
1041 Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1042   GetAssignmentCommand* c = new GetAssignmentCommand();
1043   c->d_result = d_result;
1044   return c;
1045 }
1046
1047 Command* GetAssignmentCommand::clone() const {
1048   GetAssignmentCommand* c = new GetAssignmentCommand();
1049   c->d_result = d_result;
1050   return c;
1051 }
1052
1053 std::string GetAssignmentCommand::getCommandName() const throw() {
1054   return "get-assignment";
1055 }
1056
1057 /* class GetModelCommand */
1058
1059 GetModelCommand::GetModelCommand() throw() {
1060 }
1061
1062 void GetModelCommand::invoke(SmtEngine* smtEngine) throw() {
1063   try {
1064     d_result = smtEngine->getModel();
1065     d_smtEngine = smtEngine;
1066     d_commandStatus = CommandSuccess::instance();
1067   } catch(UnsafeInterruptException& e) {
1068     d_commandStatus = new CommandInterrupted();
1069   } catch(exception& e) {
1070     d_commandStatus = new CommandFailure(e.what());
1071   }
1072 }
1073
1074 /* Model is private to the library -- for now
1075 Model* GetModelCommand::getResult() const throw() {
1076   return d_result;
1077 }
1078 */
1079
1080 void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
1081   if(! ok()) {
1082     this->Command::printResult(out, verbosity);
1083   } else {
1084     out << *d_result;
1085   }
1086 }
1087
1088 Command* GetModelCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1089   GetModelCommand* c = new GetModelCommand();
1090   c->d_result = d_result;
1091   c->d_smtEngine = d_smtEngine;
1092   return c;
1093 }
1094
1095 Command* GetModelCommand::clone() const {
1096   GetModelCommand* c = new GetModelCommand();
1097   c->d_result = d_result;
1098   c->d_smtEngine = d_smtEngine;
1099   return c;
1100 }
1101
1102 std::string GetModelCommand::getCommandName() const throw() {
1103   return "get-model";
1104 }
1105
1106 /* class GetProofCommand */
1107
1108 GetProofCommand::GetProofCommand() throw() {
1109 }
1110
1111 void GetProofCommand::invoke(SmtEngine* smtEngine) throw() {
1112   try {
1113     d_smtEngine = smtEngine;
1114     d_result = smtEngine->getProof();
1115     d_commandStatus = CommandSuccess::instance();
1116   } catch(UnsafeInterruptException& e) {
1117     d_commandStatus = new CommandInterrupted();
1118   } catch(exception& e) {
1119     d_commandStatus = new CommandFailure(e.what());
1120   }
1121 }
1122
1123 Proof* GetProofCommand::getResult() const throw() {
1124   return d_result;
1125 }
1126
1127 void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
1128   if(! ok()) {
1129     this->Command::printResult(out, verbosity);
1130   } else {
1131     smt::SmtScope scope(d_smtEngine);
1132     d_result->toStream(out);
1133   }
1134 }
1135
1136 Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1137   GetProofCommand* c = new GetProofCommand();
1138   c->d_result = d_result;
1139   c->d_smtEngine = d_smtEngine;
1140   return c;
1141 }
1142
1143 Command* GetProofCommand::clone() const {
1144   GetProofCommand* c = new GetProofCommand();
1145   c->d_result = d_result;
1146   c->d_smtEngine = d_smtEngine;
1147   return c;
1148 }
1149
1150 std::string GetProofCommand::getCommandName() const throw() {
1151   return "get-proof";
1152 }
1153
1154 /* class GetInstantiationsCommand */
1155
1156 GetInstantiationsCommand::GetInstantiationsCommand() throw() {
1157 }
1158
1159 void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() {
1160   try {
1161     d_smtEngine = smtEngine;
1162     d_commandStatus = CommandSuccess::instance();
1163   } catch(exception& e) {
1164     d_commandStatus = new CommandFailure(e.what());
1165   }
1166 }
1167
1168 //Instantiations* GetInstantiationsCommand::getResult() const throw() {
1169 //  return d_result;
1170 //}
1171
1172 void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
1173   if(! ok()) {
1174     this->Command::printResult(out, verbosity);
1175   } else {
1176     d_smtEngine->printInstantiations(out);
1177   }
1178 }
1179
1180 Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1181   GetInstantiationsCommand* c = new GetInstantiationsCommand();
1182   //c->d_result = d_result;
1183   c->d_smtEngine = d_smtEngine;
1184   return c;
1185 }
1186
1187 Command* GetInstantiationsCommand::clone() const {
1188   GetInstantiationsCommand* c = new GetInstantiationsCommand();
1189   //c->d_result = d_result;
1190   c->d_smtEngine = d_smtEngine;
1191   return c;
1192 }
1193
1194 std::string GetInstantiationsCommand::getCommandName() const throw() {
1195   return "get-instantiations";
1196 }
1197
1198 /* class GetSynthSolutionCommand */
1199
1200 GetSynthSolutionCommand::GetSynthSolutionCommand() throw() {
1201 }
1202
1203 void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() {
1204   try {
1205     d_smtEngine = smtEngine;
1206     d_commandStatus = CommandSuccess::instance();
1207   } catch(exception& e) {
1208     d_commandStatus = new CommandFailure(e.what());
1209   }
1210 }
1211
1212 void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
1213   if(! ok()) {
1214     this->Command::printResult(out, verbosity);
1215   } else {
1216     d_smtEngine->printSynthSolution(out);
1217   }
1218 }
1219
1220 Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1221   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
1222   c->d_smtEngine = d_smtEngine;
1223   return c;
1224 }
1225
1226 Command* GetSynthSolutionCommand::clone() const {
1227   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
1228   c->d_smtEngine = d_smtEngine;
1229   return c;
1230 }
1231
1232 std::string GetSynthSolutionCommand::getCommandName() const throw() {
1233   return "get-instantiations";
1234 }
1235
1236 /* class GetQuantifierEliminationCommand */
1237
1238 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() throw() :
1239   d_expr() {
1240 }
1241
1242 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(const Expr& expr, bool doFull) throw() :
1243   d_expr(expr), d_doFull(doFull) {
1244 }
1245
1246 Expr GetQuantifierEliminationCommand::getExpr() const throw() {
1247   return d_expr;
1248 }
1249 bool GetQuantifierEliminationCommand::getDoFull() const throw() {
1250   return d_doFull;
1251 }
1252
1253 void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) throw() {
1254   try {
1255     d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull);
1256     d_commandStatus = CommandSuccess::instance();
1257   } catch(exception& e) {
1258     d_commandStatus = new CommandFailure(e.what());
1259   }
1260 }
1261
1262 Expr GetQuantifierEliminationCommand::getResult() const throw() {
1263   return d_result;
1264 }
1265
1266 void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
1267   if(! ok()) {
1268     this->Command::printResult(out, verbosity);
1269   } else {
1270     out << d_result << endl;
1271   }
1272 }
1273
1274 Command* GetQuantifierEliminationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1275   GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(d_expr.exportTo(exprManager, variableMap), d_doFull);
1276   c->d_result = d_result;
1277   return c;
1278 }
1279
1280 Command* GetQuantifierEliminationCommand::clone() const {
1281   GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(d_expr, d_doFull);
1282   c->d_result = d_result;
1283   return c;
1284 }
1285
1286 std::string GetQuantifierEliminationCommand::getCommandName() const throw() {
1287   return d_doFull ? "get-qe" : "get-qe-disjunct";
1288 }
1289
1290 /* class GetUnsatCoreCommand */
1291
1292 GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
1293 }
1294
1295 GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) {
1296 }
1297
1298 void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
1299   try {
1300     d_result = smtEngine->getUnsatCore();
1301     d_commandStatus = CommandSuccess::instance();
1302   } catch(exception& e) {
1303     d_commandStatus = new CommandFailure(e.what());
1304   }
1305 }
1306
1307 void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
1308   if(! ok()) {
1309     this->Command::printResult(out, verbosity);
1310   } else {
1311     d_result.toStream(out, d_names);
1312   }
1313 }
1314
1315 const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() {
1316   // of course, this will be empty if the command hasn't been invoked yet
1317   return d_result;
1318 }
1319
1320 Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1321   GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names);
1322   c->d_result = d_result;
1323   return c;
1324 }
1325
1326 Command* GetUnsatCoreCommand::clone() const {
1327   GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names);
1328   c->d_result = d_result;
1329   return c;
1330 }
1331
1332 std::string GetUnsatCoreCommand::getCommandName() const throw() {
1333   return "get-unsat-core";
1334 }
1335
1336 /* class GetAssertionsCommand */
1337
1338 GetAssertionsCommand::GetAssertionsCommand() throw() {
1339 }
1340
1341 void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
1342   try {
1343     stringstream ss;
1344     const vector<Expr> v = smtEngine->getAssertions();
1345     ss << "(\n";
1346     copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
1347     ss << ")\n";
1348     d_result = ss.str();
1349     d_commandStatus = CommandSuccess::instance();
1350   } catch(exception& e) {
1351     d_commandStatus = new CommandFailure(e.what());
1352   }
1353 }
1354
1355 std::string GetAssertionsCommand::getResult() const throw() {
1356   return d_result;
1357 }
1358
1359 void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
1360   if(! ok()) {
1361     this->Command::printResult(out, verbosity);
1362   } else {
1363     out << d_result;
1364   }
1365 }
1366
1367 Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1368   GetAssertionsCommand* c = new GetAssertionsCommand();
1369   c->d_result = d_result;
1370   return c;
1371 }
1372
1373 Command* GetAssertionsCommand::clone() const {
1374   GetAssertionsCommand* c = new GetAssertionsCommand();
1375   c->d_result = d_result;
1376   return c;
1377 }
1378
1379 std::string GetAssertionsCommand::getCommandName() const throw() {
1380   return "get-assertions";
1381 }
1382
1383 /* class SetBenchmarkStatusCommand */
1384
1385 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() :
1386   d_status(status) {
1387 }
1388
1389 BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() {
1390   return d_status;
1391 }
1392
1393 void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
1394   try {
1395     stringstream ss;
1396     ss << d_status;
1397     SExpr status = SExpr(ss.str());
1398     smtEngine->setInfo("status", status);
1399     d_commandStatus = CommandSuccess::instance();
1400   } catch(exception& e) {
1401     d_commandStatus = new CommandFailure(e.what());
1402   }
1403 }
1404
1405 Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1406   return new SetBenchmarkStatusCommand(d_status);
1407 }
1408
1409 Command* SetBenchmarkStatusCommand::clone() const {
1410   return new SetBenchmarkStatusCommand(d_status);
1411 }
1412
1413 std::string SetBenchmarkStatusCommand::getCommandName() const throw() {
1414   return "set-info";
1415 }
1416
1417 /* class SetBenchmarkLogicCommand */
1418
1419 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() :
1420   d_logic(logic) {
1421 }
1422
1423 std::string SetBenchmarkLogicCommand::getLogic() const throw() {
1424   return d_logic;
1425 }
1426
1427 void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() {
1428   try {
1429     smtEngine->setLogic(d_logic);
1430     d_commandStatus = CommandSuccess::instance();
1431   } catch(exception& e) {
1432     d_commandStatus = new CommandFailure(e.what());
1433   }
1434 }
1435
1436 Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1437   return new SetBenchmarkLogicCommand(d_logic);
1438 }
1439
1440 Command* SetBenchmarkLogicCommand::clone() const {
1441   return new SetBenchmarkLogicCommand(d_logic);
1442 }
1443
1444 std::string SetBenchmarkLogicCommand::getCommandName() const throw() {
1445   return "set-logic";
1446 }
1447
1448 /* class SetInfoCommand */
1449
1450 SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() :
1451   d_flag(flag),
1452   d_sexpr(sexpr) {
1453 }
1454
1455 std::string SetInfoCommand::getFlag() const throw() {
1456   return d_flag;
1457 }
1458
1459 SExpr SetInfoCommand::getSExpr() const throw() {
1460   return d_sexpr;
1461 }
1462
1463 void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
1464   try {
1465     smtEngine->setInfo(d_flag, d_sexpr);
1466     d_commandStatus = CommandSuccess::instance();
1467   } catch(UnrecognizedOptionException&) {
1468     // As per SMT-LIB spec, silently accept unknown set-info keys
1469     d_commandStatus = CommandSuccess::instance();
1470   } catch(exception& e) {
1471     d_commandStatus = new CommandFailure(e.what());
1472   }
1473 }
1474
1475 Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1476   return new SetInfoCommand(d_flag, d_sexpr);
1477 }
1478
1479 Command* SetInfoCommand::clone() const {
1480   return new SetInfoCommand(d_flag, d_sexpr);
1481 }
1482
1483 std::string SetInfoCommand::getCommandName() const throw() {
1484   return "set-info";
1485 }
1486
1487 /* class GetInfoCommand */
1488
1489 GetInfoCommand::GetInfoCommand(std::string flag) throw() :
1490   d_flag(flag) {
1491 }
1492
1493 std::string GetInfoCommand::getFlag() const throw() {
1494   return d_flag;
1495 }
1496
1497 void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
1498   try {
1499     vector<SExpr> v;
1500     v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
1501     v.push_back(smtEngine->getInfo(d_flag));
1502     stringstream ss;
1503     if(d_flag == "all-options" || d_flag == "all-statistics") {
1504       ss << PrettySExprs(true);
1505     }
1506     ss << SExpr(v);
1507     d_result = ss.str();
1508     d_commandStatus = CommandSuccess::instance();
1509   } catch(UnrecognizedOptionException&) {
1510     d_commandStatus = new CommandUnsupported();
1511   } catch(exception& e) {
1512     d_commandStatus = new CommandFailure(e.what());
1513   }
1514 }
1515
1516 std::string GetInfoCommand::getResult() const throw() {
1517   return d_result;
1518 }
1519
1520 void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
1521   if(! ok()) {
1522     this->Command::printResult(out, verbosity);
1523   } else if(d_result != "") {
1524     out << d_result << endl;
1525   }
1526 }
1527
1528 Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1529   GetInfoCommand* c = new GetInfoCommand(d_flag);
1530   c->d_result = d_result;
1531   return c;
1532 }
1533
1534 Command* GetInfoCommand::clone() const {
1535   GetInfoCommand* c = new GetInfoCommand(d_flag);
1536   c->d_result = d_result;
1537   return c;
1538 }
1539
1540 std::string GetInfoCommand::getCommandName() const throw() {
1541   return "get-info";
1542 }
1543
1544 /* class SetOptionCommand */
1545
1546 SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() :
1547   d_flag(flag),
1548   d_sexpr(sexpr) {
1549 }
1550
1551 std::string SetOptionCommand::getFlag() const throw() {
1552   return d_flag;
1553 }
1554
1555 SExpr SetOptionCommand::getSExpr() const throw() {
1556   return d_sexpr;
1557 }
1558
1559 void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
1560   try {
1561     smtEngine->setOption(d_flag, d_sexpr);
1562     d_commandStatus = CommandSuccess::instance();
1563   } catch(UnrecognizedOptionException&) {
1564     d_commandStatus = new CommandUnsupported();
1565   } catch(exception& e) {
1566     d_commandStatus = new CommandFailure(e.what());
1567   }
1568 }
1569
1570 Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1571   return new SetOptionCommand(d_flag, d_sexpr);
1572 }
1573
1574 Command* SetOptionCommand::clone() const {
1575   return new SetOptionCommand(d_flag, d_sexpr);
1576 }
1577
1578 std::string SetOptionCommand::getCommandName() const throw() {
1579   return "set-option";
1580 }
1581
1582 /* class GetOptionCommand */
1583
1584 GetOptionCommand::GetOptionCommand(std::string flag) throw() :
1585   d_flag(flag) {
1586 }
1587
1588 std::string GetOptionCommand::getFlag() const throw() {
1589   return d_flag;
1590 }
1591
1592 void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
1593   try {
1594     SExpr res = smtEngine->getOption(d_flag);
1595     d_result = res.toString();
1596     d_commandStatus = CommandSuccess::instance();
1597   } catch(UnrecognizedOptionException&) {
1598     d_commandStatus = new CommandUnsupported();
1599   } catch(exception& e) {
1600     d_commandStatus = new CommandFailure(e.what());
1601   }
1602 }
1603
1604 std::string GetOptionCommand::getResult() const throw() {
1605   return d_result;
1606 }
1607
1608 void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
1609   if(! ok()) {
1610     this->Command::printResult(out, verbosity);
1611   } else if(d_result != "") {
1612     out << d_result << endl;
1613   }
1614 }
1615
1616 Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1617   GetOptionCommand* c = new GetOptionCommand(d_flag);
1618   c->d_result = d_result;
1619   return c;
1620 }
1621
1622 Command* GetOptionCommand::clone() const {
1623   GetOptionCommand* c = new GetOptionCommand(d_flag);
1624   c->d_result = d_result;
1625   return c;
1626 }
1627
1628 std::string GetOptionCommand::getCommandName() const throw() {
1629   return "get-option";
1630 }
1631
1632 /* class DatatypeDeclarationCommand */
1633
1634 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
1635   d_datatypes() {
1636   d_datatypes.push_back(datatype);
1637 }
1638
1639 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() :
1640   d_datatypes(datatypes) {
1641 }
1642
1643 const std::vector<DatatypeType>&
1644 DatatypeDeclarationCommand::getDatatypes() const throw() {
1645   return d_datatypes;
1646 }
1647
1648 void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
1649   d_commandStatus = CommandSuccess::instance();
1650 }
1651
1652 Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1653   throw ExportUnsupportedException
1654           ("export of DatatypeDeclarationCommand unsupported");
1655 }
1656
1657 Command* DatatypeDeclarationCommand::clone() const {
1658   return new DatatypeDeclarationCommand(d_datatypes);
1659 }
1660
1661 std::string DatatypeDeclarationCommand::getCommandName() const throw() {
1662   return "declare-datatypes";
1663 }
1664
1665 /* class RewriteRuleCommand */
1666
1667 RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
1668                                        const std::vector<Expr>& guards,
1669                                        Expr head, Expr body,
1670                                        const Triggers& triggers) throw() :
1671   d_vars(vars), d_guards(guards), d_head(head), d_body(body), d_triggers(triggers) {
1672 }
1673
1674 RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
1675                                        Expr head, Expr body) throw() :
1676   d_vars(vars), d_head(head), d_body(body) {
1677 }
1678
1679 const std::vector<Expr>& RewriteRuleCommand::getVars() const throw() {
1680   return d_vars;
1681 }
1682
1683 const std::vector<Expr>& RewriteRuleCommand::getGuards() const throw() {
1684   return d_guards;
1685 }
1686
1687 Expr RewriteRuleCommand::getHead() const throw() {
1688   return d_head;
1689 }
1690
1691 Expr RewriteRuleCommand::getBody() const throw() {
1692   return d_body;
1693 }
1694
1695 const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const throw() {
1696   return d_triggers;
1697 }
1698
1699 void RewriteRuleCommand::invoke(SmtEngine* smtEngine) throw() {
1700   try {
1701     ExprManager* em = smtEngine->getExprManager();
1702     /** build vars list */
1703     Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
1704     /** build guards list */
1705     Expr guards;
1706     if(d_guards.size() == 0) guards = em->mkConst<bool>(true);
1707     else if(d_guards.size() == 1) guards = d_guards[0];
1708     else guards = em->mkExpr(kind::AND,d_guards);
1709     /** build expression */
1710     Expr expr;
1711     if( d_triggers.empty() ){
1712       expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body);
1713     } else {
1714       /** build triggers list */
1715       std::vector<Expr> vtriggers;
1716       vtriggers.reserve(d_triggers.size());
1717       for(Triggers::const_iterator i = d_triggers.begin(),
1718             end = d_triggers.end(); i != end; ++i){
1719         vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i));
1720       }
1721       Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers);
1722       expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body,triggers);
1723     }
1724     smtEngine->assertFormula(expr);
1725     d_commandStatus = CommandSuccess::instance();
1726   } catch(exception& e) {
1727     d_commandStatus = new CommandFailure(e.what());
1728   }
1729 }
1730
1731 Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1732   /** Convert variables */
1733   VExpr vars; vars.reserve(d_vars.size());
1734   for(VExpr::iterator i = d_vars.begin(), end = d_vars.end();
1735       i == end; ++i){
1736     vars.push_back(i->exportTo(exprManager, variableMap));
1737   };
1738   /** Convert guards */
1739   VExpr guards; guards.reserve(d_guards.size());
1740   for(VExpr::iterator i = d_guards.begin(), end = d_guards.end();
1741       i == end; ++i){
1742     guards.push_back(i->exportTo(exprManager, variableMap));
1743   };
1744   /** Convert triggers */
1745   Triggers triggers; triggers.resize(d_triggers.size());
1746   for(size_t i = 0, end = d_triggers.size();
1747       i < end; ++i){
1748     triggers[i].reserve(d_triggers[i].size());
1749     for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end();
1750         j == jend; ++i){
1751       triggers[i].push_back(j->exportTo(exprManager, variableMap));
1752     };
1753   };
1754   /** Convert head and body */
1755   Expr head = d_head.exportTo(exprManager, variableMap);
1756   Expr body = d_body.exportTo(exprManager, variableMap);
1757   /** Create the converted rules */
1758   return new RewriteRuleCommand(vars, guards, head, body, triggers);
1759 }
1760
1761 Command* RewriteRuleCommand::clone() const {
1762   return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers);
1763 }
1764
1765 std::string RewriteRuleCommand::getCommandName() const throw() {
1766   return "rewrite-rule";
1767 }
1768
1769 /* class PropagateRuleCommand */
1770
1771 PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
1772                                            const std::vector<Expr>& guards,
1773                                            const std::vector<Expr>& heads,
1774                                            Expr body,
1775                                            const Triggers& triggers,
1776                                            bool deduction) throw() :
1777   d_vars(vars), d_guards(guards), d_heads(heads), d_body(body), d_triggers(triggers), d_deduction(deduction) {
1778 }
1779
1780 PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
1781                                            const std::vector<Expr>& heads,
1782                                            Expr body,
1783                                            bool deduction) throw() :
1784   d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) {
1785 }
1786
1787 const std::vector<Expr>& PropagateRuleCommand::getVars() const throw() {
1788   return d_vars;
1789 }
1790
1791 const std::vector<Expr>& PropagateRuleCommand::getGuards() const throw() {
1792   return d_guards;
1793 }
1794
1795 const std::vector<Expr>& PropagateRuleCommand::getHeads() const throw() {
1796   return d_heads;
1797 }
1798
1799 Expr PropagateRuleCommand::getBody() const throw() {
1800   return d_body;
1801 }
1802
1803 const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const throw() {
1804   return d_triggers;
1805 }
1806
1807 bool PropagateRuleCommand::isDeduction() const throw() {
1808   return d_deduction;
1809 }
1810
1811 void PropagateRuleCommand::invoke(SmtEngine* smtEngine) throw() {
1812   try {
1813     ExprManager* em = smtEngine->getExprManager();
1814     /** build vars list */
1815     Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
1816     /** build guards list */
1817     Expr guards;
1818     if(d_guards.size() == 0) guards = em->mkConst<bool>(true);
1819     else if(d_guards.size() == 1) guards = d_guards[0];
1820     else guards = em->mkExpr(kind::AND,d_guards);
1821     /** build heads list */
1822     Expr heads;
1823     if(d_heads.size() == 1) heads = d_heads[0];
1824     else heads = em->mkExpr(kind::AND,d_heads);
1825     /** build expression */
1826     Expr expr;
1827     if( d_triggers.empty() ){
1828       expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body);
1829     } else {
1830       /** build triggers list */
1831       std::vector<Expr> vtriggers;
1832       vtriggers.reserve(d_triggers.size());
1833       for(Triggers::const_iterator i = d_triggers.begin(),
1834             end = d_triggers.end(); i != end; ++i){
1835         vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i));
1836       }
1837       Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers);
1838       expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body,triggers);
1839     }
1840     smtEngine->assertFormula(expr);
1841     d_commandStatus = CommandSuccess::instance();
1842   } catch(exception& e) {
1843     d_commandStatus = new CommandFailure(e.what());
1844   }
1845 }
1846
1847 Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
1848   /** Convert variables */
1849   VExpr vars; vars.reserve(d_vars.size());
1850   for(VExpr::iterator i = d_vars.begin(), end = d_vars.end();
1851       i == end; ++i){
1852     vars.push_back(i->exportTo(exprManager, variableMap));
1853   };
1854   /** Convert guards */
1855   VExpr guards; guards.reserve(d_guards.size());
1856   for(VExpr::iterator i = d_guards.begin(), end = d_guards.end();
1857       i == end; ++i){
1858     guards.push_back(i->exportTo(exprManager, variableMap));
1859   };
1860   /** Convert heads */
1861   VExpr heads; heads.reserve(d_heads.size());
1862   for(VExpr::iterator i = d_heads.begin(), end = d_heads.end();
1863       i == end; ++i){
1864     heads.push_back(i->exportTo(exprManager, variableMap));
1865   };
1866   /** Convert triggers */
1867   Triggers triggers; triggers.resize(d_triggers.size());
1868   for(size_t i = 0, end = d_triggers.size();
1869       i < end; ++i){
1870     triggers[i].reserve(d_triggers[i].size());
1871     for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end();
1872         j == jend; ++i){
1873       triggers[i].push_back(j->exportTo(exprManager, variableMap));
1874     };
1875   };
1876   /** Convert head and body */
1877   Expr body = d_body.exportTo(exprManager, variableMap);
1878   /** Create the converted rules */
1879   return new PropagateRuleCommand(vars, guards, heads, body, triggers);
1880 }
1881
1882 Command* PropagateRuleCommand::clone() const {
1883   return new PropagateRuleCommand(d_vars, d_guards, d_heads, d_body, d_triggers);
1884 }
1885
1886 std::string PropagateRuleCommand::getCommandName() const throw() {
1887   return "propagate-rule";
1888 }
1889
1890 /* output stream insertion operator for benchmark statuses */
1891 std::ostream& operator<<(std::ostream& out,
1892                          BenchmarkStatus status) throw() {
1893   switch(status) {
1894
1895   case SMT_SATISFIABLE:
1896     return out << "sat";
1897
1898   case SMT_UNSATISFIABLE:
1899     return out << "unsat";
1900
1901   case SMT_UNKNOWN:
1902     return out << "unknown";
1903
1904   default:
1905     return out << "BenchmarkStatus::[UNKNOWNSTATUS!]";
1906   }
1907 }
1908
1909 }/* CVC4 namespace */