src/smt/command.cpp

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