src/expr/command.h

   1 /*********************                                                        */
   2 /*! \file command.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Kshitij Bansal, Christopher L. Conway, Dejan Jovanovic, Francois Bobot, Andrew Reynolds
   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 the command pattern on SmtEngines.
  13  **
  14  ** Implementation of the command pattern on SmtEngines.  Command
  15  ** objects are generated by the parser (typically) to implement the
  16  ** commands in parsed input (see Parser::parseNextCommand()), or by
  17  ** client code.
  18  **/
  19
  20 #include "cvc4_public.h"
  21
  22 #ifndef __CVC4__COMMAND_H
  23 #define __CVC4__COMMAND_H
  24
  25 #include <iostream>
  26 #include <sstream>
  27 #include <string>
  28 #include <vector>
  29 #include <map>
  30
  31 #include "expr/expr.h"
  32 #include "expr/type.h"
  33 #include "expr/variable_type_map.h"
  34 #include "util/result.h"
  35 #include "util/sexpr.h"
  36 #include "util/datatype.h"
  37 #include "util/proof.h"
  38
  39 namespace CVC4 {
  40
  41 class SmtEngine;
  42 class Command;
  43 class CommandStatus;
  44 class Model;
  45
  46 std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC;
  47 std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
  48 std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
  49 std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC;
  50
  51 /** The status an SMT benchmark can have */
  52 enum BenchmarkStatus {
  53   /** Benchmark is satisfiable */
  54   SMT_SATISFIABLE,
  55   /** Benchmark is unsatisfiable */
  56   SMT_UNSATISFIABLE,
  57   /** The status of the benchmark is unknown */
  58   SMT_UNKNOWN
  59 };/* enum BenchmarkStatus */
  60
  61 std::ostream& operator<<(std::ostream& out,
  62                          BenchmarkStatus status) throw() CVC4_PUBLIC;
  63
  64 /**
  65  * IOStream manipulator to print success messages or not.
  66  *
  67  *   out << Command::printsuccess(false) << CommandSuccess();
  68  *
  69  * prints nothing, but
  70  *
  71  *   out << Command::printsuccess(true) << CommandSuccess();
  72  *
  73  * prints a success message (in a manner appropriate for the current
  74  * output language).
  75  */
  76 class CVC4_PUBLIC CommandPrintSuccess {
  77   /**
  78    * The allocated index in ios_base for our depth setting.
  79    */
  80   static const int s_iosIndex;
  81
  82   /**
  83    * The default setting, for ostreams that haven't yet had a
  84    * setdepth() applied to them.
  85    */
  86   static const int s_defaultPrintSuccess = false;
  87
  88   /**
  89    * When this manipulator is used, the setting is stored here.
  90    */
  91   bool d_printSuccess;
  92
  93 public:
  94   /**
  95    * Construct a CommandPrintSuccess with the given setting.
  96    */
  97   CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {}
  98
  99   inline void applyPrintSuccess(std::ostream& out) throw() {
 100     out.iword(s_iosIndex) = d_printSuccess;
 101   }
 102
 103   static inline bool getPrintSuccess(std::ostream& out) throw() {
 104     return out.iword(s_iosIndex);
 105   }
 106
 107   static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() {
 108     out.iword(s_iosIndex) = printSuccess;
 109   }
 110
 111   /**
 112    * Set the print-success state on the output stream for the current
 113    * stack scope.  This makes sure the old state is reset on the
 114    * stream after normal OR exceptional exit from the scope, using the
 115    * RAII C++ idiom.
 116    */
 117   class Scope {
 118     std::ostream& d_out;
 119     bool d_oldPrintSuccess;
 120
 121   public:
 122
 123     inline Scope(std::ostream& out, bool printSuccess) throw() :
 124       d_out(out),
 125       d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) {
 126       CommandPrintSuccess::setPrintSuccess(out, printSuccess);
 127     }
 128
 129     inline ~Scope() throw() {
 130       CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess);
 131     }
 132
 133   };/* class CommandPrintSuccess::Scope */
 134
 135 };/* class CommandPrintSuccess */
 136
 137 /**
 138  * Sets the default print-success setting when pretty-printing an Expr
 139  * to an ostream.  Use like this:
 140  *
 141  *   // let out be an ostream, e an Expr
 142  *   out << Expr::setdepth(n) << e << endl;
 143  *
 144  * The depth stays permanently (until set again) with the stream.
 145  */
 146 inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC;
 147 inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() {
 148   cps.applyPrintSuccess(out);
 149   return out;
 150 }
 151
 152 class CVC4_PUBLIC CommandStatus {
 153 protected:
 154   // shouldn't construct a CommandStatus (use a derived class)
 155   CommandStatus() throw() {}
 156 public:
 157   virtual ~CommandStatus() throw() {}
 158   void toStream(std::ostream& out,
 159                 OutputLanguage language = language::output::LANG_AUTO) const throw();
 160   virtual CommandStatus& clone() const = 0;
 161 };/* class CommandStatus */
 162
 163 class CVC4_PUBLIC CommandSuccess : public CommandStatus {
 164   static const CommandSuccess* s_instance;
 165 public:
 166   static const CommandSuccess* instance() throw() { return s_instance; }
 167   CommandStatus& clone() const { return const_cast<CommandSuccess&>(*this); }
 168 };/* class CommandSuccess */
 169
 170 class CVC4_PUBLIC CommandUnsupported : public CommandStatus {
 171 public:
 172   CommandStatus& clone() const { return *new CommandUnsupported(*this); }
 173 };/* class CommandSuccess */
 174
 175 class CVC4_PUBLIC CommandFailure : public CommandStatus {
 176   std::string d_message;
 177 public:
 178   CommandFailure(std::string message) throw() : d_message(message) {}
 179   CommandFailure& clone() const { return *new CommandFailure(*this); }
 180   ~CommandFailure() throw() {}
 181   std::string getMessage() const throw() { return d_message; }
 182 };/* class CommandFailure */
 183
 184 class CVC4_PUBLIC Command {
 185 protected:
 186   /**
 187    * This field contains a command status if the command has been
 188    * invoked, or NULL if it has not.  This field is either a
 189    * dynamically-allocated pointer, or it's a pointer to the singleton
 190    * CommandSuccess instance.  Doing so is somewhat asymmetric, but
 191    * it avoids the need to dynamically allocate memory in the common
 192    * case of a successful command.
 193    */
 194   const CommandStatus* d_commandStatus;
 195
 196   /**
 197    * True if this command is "muted"---i.e., don't print "success" on
 198    * successful execution.
 199    */
 200   bool d_muted;
 201
 202 public:
 203   typedef CommandPrintSuccess printsuccess;
 204
 205   Command() throw();
 206   Command(const Command& cmd);
 207
 208   virtual ~Command() throw();
 209
 210   virtual void invoke(SmtEngine* smtEngine) throw() = 0;
 211   virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
 212
 213   virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
 214                         OutputLanguage language = language::output::LANG_AUTO) const throw();
 215
 216   std::string toString() const throw();
 217
 218   virtual std::string getCommandName() const throw() = 0;
 219
 220   /**
 221    * If false, instruct this Command not to print a success message.
 222    */
 223   void setMuted(bool muted) throw() { d_muted = muted; }
 224
 225   /**
 226    * Determine whether this Command will print a success message.
 227    */
 228   bool isMuted() throw() { return d_muted; }
 229
 230   /**
 231    * Either the command hasn't run yet, or it completed successfully
 232    * (CommandSuccess, not CommandUnsupported or CommandFailure).
 233    */
 234   bool ok() const throw();
 235
 236   /**
 237    * The command completed in a failure state (CommandFailure, not
 238    * CommandSuccess or CommandUnsupported).
 239    */
 240   bool fail() const throw();
 241
 242   /** Get the command status (it's NULL if we haven't run yet). */
 243   const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
 244
 245   virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 246
 247   /**
 248    * Maps this Command into one for a different ExprManager, using
 249    * variableMap for the translation and extending it with any new
 250    * mappings.
 251    */
 252   virtual Command* exportTo(ExprManager* exprManager,
 253                             ExprManagerMapCollection& variableMap) = 0;
 254
 255   /**
 256    * Clone this Command (make a shallow copy).
 257    */
 258   virtual Command* clone() const = 0;
 259
 260 protected:
 261   class ExportTransformer {
 262     ExprManager* d_exprManager;
 263     ExprManagerMapCollection& d_variableMap;
 264   public:
 265     ExportTransformer(ExprManager* exprManager, ExprManagerMapCollection& variableMap) :
 266       d_exprManager(exprManager),
 267       d_variableMap(variableMap) {
 268     }
 269     Expr operator()(Expr e) {
 270       return e.exportTo(d_exprManager, d_variableMap);
 271     }
 272     Type operator()(Type t) {
 273       return t.exportTo(d_exprManager, d_variableMap);
 274     }
 275   };/* class Command::ExportTransformer */
 276 };/* class Command */
 277
 278 /**
 279  * EmptyCommands are the residue of a command after the parser handles
 280  * them (and there's nothing left to do).
 281  */
 282 class CVC4_PUBLIC EmptyCommand : public Command {
 283 protected:
 284   std::string d_name;
 285 public:
 286   EmptyCommand(std::string name = "") throw();
 287   ~EmptyCommand() throw() {}
 288   std::string getName() const throw();
 289   void invoke(SmtEngine* smtEngine) throw();
 290   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 291   Command* clone() const;
 292   std::string getCommandName() const throw();
 293 };/* class EmptyCommand */
 294
 295 class CVC4_PUBLIC EchoCommand : public Command {
 296 protected:
 297   std::string d_output;
 298 public:
 299   EchoCommand(std::string output = "") throw();
 300   ~EchoCommand() throw() {}
 301   std::string getOutput() const throw();
 302   void invoke(SmtEngine* smtEngine) throw();
 303   void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
 304   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 305   Command* clone() const;
 306   std::string getCommandName() const throw();
 307 };/* class EchoCommand */
 308
 309 class CVC4_PUBLIC AssertCommand : public Command {
 310 protected:
 311   Expr d_expr;
 312 public:
 313   AssertCommand(const Expr& e) throw();
 314   ~AssertCommand() throw() {}
 315   Expr getExpr() const throw();
 316   void invoke(SmtEngine* smtEngine) throw();
 317   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 318   Command* clone() const;
 319   std::string getCommandName() const throw();
 320 };/* class AssertCommand */
 321
 322 class CVC4_PUBLIC PushCommand : public Command {
 323 public:
 324   ~PushCommand() throw() {}
 325   void invoke(SmtEngine* smtEngine) throw();
 326   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 327   Command* clone() const;
 328   std::string getCommandName() const throw();
 329 };/* class PushCommand */
 330
 331 class CVC4_PUBLIC PopCommand : public Command {
 332 public:
 333   ~PopCommand() throw() {}
 334   void invoke(SmtEngine* smtEngine) throw();
 335   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 336   Command* clone() const;
 337   std::string getCommandName() const throw();
 338 };/* class PopCommand */
 339
 340 class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
 341 protected:
 342   std::string d_symbol;
 343 public:
 344   DeclarationDefinitionCommand(const std::string& id) throw();
 345   ~DeclarationDefinitionCommand() throw() {}
 346   virtual void invoke(SmtEngine* smtEngine) throw() = 0;
 347   std::string getSymbol() const throw();
 348 };/* class DeclarationDefinitionCommand */
 349
 350 class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand {
 351 protected:
 352   Expr d_func;
 353   Type d_type;
 354   bool d_printInModel;
 355   bool d_printInModelSetByUser;
 356 public:
 357   DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw();
 358   ~DeclareFunctionCommand() throw() {}
 359   Expr getFunction() const throw();
 360   Type getType() const throw();
 361   bool getPrintInModel() const throw();
 362   bool getPrintInModelSetByUser() const throw();
 363   void setPrintInModel( bool p );
 364   void invoke(SmtEngine* smtEngine) throw();
 365   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 366   Command* clone() const;
 367   std::string getCommandName() const throw();
 368 };/* class DeclareFunctionCommand */
 369
 370 class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
 371 protected:
 372   size_t d_arity;
 373   Type d_type;
 374 public:
 375   DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw();
 376   ~DeclareTypeCommand() throw() {}
 377   size_t getArity() const throw();
 378   Type getType() const throw();
 379   void invoke(SmtEngine* smtEngine) throw();
 380   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 381   Command* clone() const;
 382   std::string getCommandName() const throw();
 383 };/* class DeclareTypeCommand */
 384
 385 class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
 386 protected:
 387   std::vector<Type> d_params;
 388   Type d_type;
 389 public:
 390   DefineTypeCommand(const std::string& id, Type t) throw();
 391   DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw();
 392   ~DefineTypeCommand() throw() {}
 393   const std::vector<Type>& getParameters() const throw();
 394   Type getType() const throw();
 395   void invoke(SmtEngine* smtEngine) throw();
 396   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 397   Command* clone() const;
 398   std::string getCommandName() const throw();
 399 };/* class DefineTypeCommand */
 400
 401 class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
 402 protected:
 403   Expr d_func;
 404   std::vector<Expr> d_formals;
 405   Expr d_formula;
 406 public:
 407   DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw();
 408   DefineFunctionCommand(const std::string& id, Expr func,
 409                         const std::vector<Expr>& formals, Expr formula) throw();
 410   ~DefineFunctionCommand() throw() {}
 411   Expr getFunction() const throw();
 412   const std::vector<Expr>& getFormals() const throw();
 413   Expr getFormula() const throw();
 414   void invoke(SmtEngine* smtEngine) throw();
 415   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 416   Command* clone() const;
 417   std::string getCommandName() const throw();
 418 };/* class DefineFunctionCommand */
 419
 420 /**
 421  * This differs from DefineFunctionCommand only in that it instructs
 422  * the SmtEngine to "remember" this function for later retrieval with
 423  * getAssignment().  Used for :named attributes in SMT-LIBv2.
 424  */
 425 class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand {
 426 public:
 427   DefineNamedFunctionCommand(const std::string& id, Expr func,
 428                              const std::vector<Expr>& formals, Expr formula) throw();
 429   void invoke(SmtEngine* smtEngine) throw();
 430   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 431   Command* clone() const;
 432 };/* class DefineNamedFunctionCommand */
 433
 434 /**
 435  * The command when an attribute is set by a user.  In SMT-LIBv2 this is done
 436  *  via the syntax (! expr :attr)
 437  */
 438 class CVC4_PUBLIC SetUserAttributeCommand : public Command {
 439 protected:
 440   std::string d_attr;
 441   Expr d_expr;
 442   //std::vector<Expr> d_expr_values;
 443   //std::string d_str_value;
 444 public:
 445   SetUserAttributeCommand( const std::string& attr, Expr expr ) throw();
 446   //SetUserAttributeCommand( const std::string& id, Expr expr, std::vector<Expr>& values ) throw();
 447   //SetUserAttributeCommand( const std::string& id, Expr expr, std::string& value ) throw();
 448   ~SetUserAttributeCommand() throw() {}
 449   void invoke(SmtEngine* smtEngine) throw();
 450   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 451   Command* clone() const;
 452   std::string getCommandName() const throw();
 453 };/* class SetUserAttributeCommand */
 454
 455
 456 class CVC4_PUBLIC CheckSatCommand : public Command {
 457 protected:
 458   Expr d_expr;
 459   Result d_result;
 460 public:
 461   CheckSatCommand() throw();
 462   CheckSatCommand(const Expr& expr) throw();
 463   ~CheckSatCommand() throw() {}
 464   Expr getExpr() const throw();
 465   void invoke(SmtEngine* smtEngine) throw();
 466   Result getResult() const throw();
 467   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 468   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 469   Command* clone() const;
 470   std::string getCommandName() const throw();
 471 };/* class CheckSatCommand */
 472
 473 class CVC4_PUBLIC QueryCommand : public Command {
 474 protected:
 475   Expr d_expr;
 476   Result d_result;
 477 public:
 478   QueryCommand(const Expr& e) throw();
 479   ~QueryCommand() throw() {}
 480   Expr getExpr() const throw();
 481   void invoke(SmtEngine* smtEngine) throw();
 482   Result getResult() const throw();
 483   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 484   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 485   Command* clone() const;
 486   std::string getCommandName() const throw();
 487 };/* class QueryCommand */
 488
 489 // this is TRANSFORM in the CVC presentation language
 490 class CVC4_PUBLIC SimplifyCommand : public Command {
 491 protected:
 492   Expr d_term;
 493   Expr d_result;
 494 public:
 495   SimplifyCommand(Expr term) throw();
 496   ~SimplifyCommand() throw() {}
 497   Expr getTerm() const throw();
 498   void invoke(SmtEngine* smtEngine) throw();
 499   Expr getResult() const throw();
 500   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 501   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 502   Command* clone() const;
 503   std::string getCommandName() const throw();
 504 };/* class SimplifyCommand */
 505
 506 class CVC4_PUBLIC ExpandDefinitionsCommand : public Command {
 507 protected:
 508   Expr d_term;
 509   Expr d_result;
 510 public:
 511   ExpandDefinitionsCommand(Expr term) throw();
 512   ~ExpandDefinitionsCommand() throw() {}
 513   Expr getTerm() const throw();
 514   void invoke(SmtEngine* smtEngine) throw();
 515   Expr getResult() const throw();
 516   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 517   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 518   Command* clone() const;
 519   std::string getCommandName() const throw();
 520 };/* class ExpandDefinitionsCommand */
 521
 522 class CVC4_PUBLIC GetValueCommand : public Command {
 523 protected:
 524   std::vector<Expr> d_terms;
 525   Expr d_result;
 526 public:
 527   GetValueCommand(Expr term) throw();
 528   GetValueCommand(const std::vector<Expr>& terms) throw();
 529   ~GetValueCommand() throw() {}
 530   const std::vector<Expr>& getTerms() const throw();
 531   void invoke(SmtEngine* smtEngine) throw();
 532   Expr getResult() const throw();
 533   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 534   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 535   Command* clone() const;
 536   std::string getCommandName() const throw();
 537 };/* class GetValueCommand */
 538
 539 class CVC4_PUBLIC GetAssignmentCommand : public Command {
 540 protected:
 541   SExpr d_result;
 542 public:
 543   GetAssignmentCommand() throw();
 544   ~GetAssignmentCommand() throw() {}
 545   void invoke(SmtEngine* smtEngine) throw();
 546   SExpr getResult() const throw();
 547   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 548   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 549   Command* clone() const;
 550   std::string getCommandName() const throw();
 551 };/* class GetAssignmentCommand */
 552
 553 class CVC4_PUBLIC GetModelCommand : public Command {
 554 protected:
 555   Model* d_result;
 556   SmtEngine* d_smtEngine;
 557 public:
 558   GetModelCommand() throw();
 559   ~GetModelCommand() throw() {}
 560   void invoke(SmtEngine* smtEngine) throw();
 561   // Model is private to the library -- for now
 562   //Model* getResult() const throw();
 563   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 564   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 565   Command* clone() const;
 566   std::string getCommandName() const throw();
 567 };/* class GetModelCommand */
 568
 569 class CVC4_PUBLIC GetProofCommand : public Command {
 570 protected:
 571   Proof* d_result;
 572 public:
 573   GetProofCommand() throw();
 574   ~GetProofCommand() throw() {}
 575   void invoke(SmtEngine* smtEngine) throw();
 576   Proof* getResult() const throw();
 577   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 578   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 579   Command* clone() const;
 580   std::string getCommandName() const throw();
 581 };/* class GetProofCommand */
 582
 583 class CVC4_PUBLIC GetInstantiationsCommand : public Command {
 584 protected:
 585   //Instantiations* d_result;
 586   SmtEngine* d_smtEngine;
 587 public:
 588   GetInstantiationsCommand() throw();
 589   ~GetInstantiationsCommand() throw() {}
 590   void invoke(SmtEngine* smtEngine) throw();
 591   //Instantiations* getResult() const throw();
 592   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 593   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 594   Command* clone() const;
 595   std::string getCommandName() const throw();
 596 };/* class GetInstantiationsCommand */
 597
 598 class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
 599 protected:
 600   //UnsatCore* d_result;
 601 public:
 602   GetUnsatCoreCommand() throw();
 603   ~GetUnsatCoreCommand() throw() {}
 604   void invoke(SmtEngine* smtEngine) throw();
 605   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 606   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 607   Command* clone() const;
 608   std::string getCommandName() const throw();
 609 };/* class GetUnsatCoreCommand */
 610
 611 class CVC4_PUBLIC GetAssertionsCommand : public Command {
 612 protected:
 613   std::string d_result;
 614 public:
 615   GetAssertionsCommand() throw();
 616   ~GetAssertionsCommand() throw() {}
 617   void invoke(SmtEngine* smtEngine) throw();
 618   std::string getResult() const throw();
 619   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 620   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 621   Command* clone() const;
 622   std::string getCommandName() const throw();
 623 };/* class GetAssertionsCommand */
 624
 625 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
 626 protected:
 627   BenchmarkStatus d_status;
 628 public:
 629   SetBenchmarkStatusCommand(BenchmarkStatus status) throw();
 630   ~SetBenchmarkStatusCommand() throw() {}
 631   BenchmarkStatus getStatus() const throw();
 632   void invoke(SmtEngine* smtEngine) throw();
 633   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 634   Command* clone() const;
 635   std::string getCommandName() const throw();
 636 };/* class SetBenchmarkStatusCommand */
 637
 638 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
 639 protected:
 640   std::string d_logic;
 641 public:
 642   SetBenchmarkLogicCommand(std::string logic) throw();
 643   ~SetBenchmarkLogicCommand() throw() {}
 644   std::string getLogic() const throw();
 645   void invoke(SmtEngine* smtEngine) throw();
 646   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 647   Command* clone() const;
 648   std::string getCommandName() const throw();
 649 };/* class SetBenchmarkLogicCommand */
 650
 651 class CVC4_PUBLIC SetInfoCommand : public Command {
 652 protected:
 653   std::string d_flag;
 654   SExpr d_sexpr;
 655 public:
 656   SetInfoCommand(std::string flag, const SExpr& sexpr) throw();
 657   ~SetInfoCommand() throw() {}
 658   std::string getFlag() const throw();
 659   SExpr getSExpr() const throw();
 660   void invoke(SmtEngine* smtEngine) throw();
 661   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 662   Command* clone() const;
 663   std::string getCommandName() const throw();
 664 };/* class SetInfoCommand */
 665
 666 class CVC4_PUBLIC GetInfoCommand : public Command {
 667 protected:
 668   std::string d_flag;
 669   std::string d_result;
 670 public:
 671   GetInfoCommand(std::string flag) throw();
 672   ~GetInfoCommand() throw() {}
 673   std::string getFlag() const throw();
 674   void invoke(SmtEngine* smtEngine) throw();
 675   std::string getResult() const throw();
 676   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 677   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 678   Command* clone() const;
 679   std::string getCommandName() const throw();
 680 };/* class GetInfoCommand */
 681
 682 class CVC4_PUBLIC SetOptionCommand : public Command {
 683 protected:
 684   std::string d_flag;
 685   SExpr d_sexpr;
 686 public:
 687   SetOptionCommand(std::string flag, const SExpr& sexpr) throw();
 688   ~SetOptionCommand() throw() {}
 689   std::string getFlag() const throw();
 690   SExpr getSExpr() const throw();
 691   void invoke(SmtEngine* smtEngine) throw();
 692   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 693   Command* clone() const;
 694   std::string getCommandName() const throw();
 695 };/* class SetOptionCommand */
 696
 697 class CVC4_PUBLIC GetOptionCommand : public Command {
 698 protected:
 699   std::string d_flag;
 700   std::string d_result;
 701 public:
 702   GetOptionCommand(std::string flag) throw();
 703   ~GetOptionCommand() throw() {}
 704   std::string getFlag() const throw();
 705   void invoke(SmtEngine* smtEngine) throw();
 706   std::string getResult() const throw();
 707   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
 708   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 709   Command* clone() const;
 710   std::string getCommandName() const throw();
 711 };/* class GetOptionCommand */
 712
 713 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
 714 private:
 715   std::vector<DatatypeType> d_datatypes;
 716 public:
 717   DatatypeDeclarationCommand(const DatatypeType& datatype) throw();
 718   ~DatatypeDeclarationCommand() throw() {}
 719   DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
 720   const std::vector<DatatypeType>& getDatatypes() const throw();
 721   void invoke(SmtEngine* smtEngine) throw();
 722   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 723   Command* clone() const;
 724   std::string getCommandName() const throw();
 725 };/* class DatatypeDeclarationCommand */
 726
 727 class CVC4_PUBLIC RewriteRuleCommand : public Command {
 728 public:
 729   typedef std::vector< std::vector< Expr > > Triggers;
 730 protected:
 731   typedef std::vector< Expr > VExpr;
 732   VExpr d_vars;
 733   VExpr d_guards;
 734   Expr d_head;
 735   Expr d_body;
 736   Triggers d_triggers;
 737 public:
 738   RewriteRuleCommand(const std::vector<Expr>& vars,
 739                      const std::vector<Expr>& guards,
 740                      Expr head,
 741                      Expr body,
 742                      const Triggers& d_triggers) throw();
 743   RewriteRuleCommand(const std::vector<Expr>& vars,
 744                      Expr head,
 745                      Expr body) throw();
 746   ~RewriteRuleCommand() throw() {}
 747   const std::vector<Expr>& getVars() const throw();
 748   const std::vector<Expr>& getGuards() const throw();
 749   Expr getHead() const throw();
 750   Expr getBody() const throw();
 751   const Triggers& getTriggers() const throw();
 752   void invoke(SmtEngine* smtEngine) throw();
 753   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 754   Command* clone() const;
 755   std::string getCommandName() const throw();
 756 };/* class RewriteRuleCommand */
 757
 758 class CVC4_PUBLIC PropagateRuleCommand : public Command {
 759 public:
 760   typedef std::vector< std::vector< Expr > > Triggers;
 761 protected:
 762   typedef std::vector< Expr > VExpr;
 763   VExpr d_vars;
 764   VExpr d_guards;
 765   VExpr d_heads;
 766   Expr d_body;
 767   Triggers d_triggers;
 768   bool d_deduction;
 769 public:
 770   PropagateRuleCommand(const std::vector<Expr>& vars,
 771                        const std::vector<Expr>& guards,
 772                        const std::vector<Expr>& heads,
 773                        Expr body,
 774                        const Triggers& d_triggers,
 775                        /* true if we want a deduction rule */
 776                        bool d_deduction = false) throw();
 777   PropagateRuleCommand(const std::vector<Expr>& vars,
 778                        const std::vector<Expr>& heads,
 779                        Expr body,
 780                        bool d_deduction = false) throw();
 781   ~PropagateRuleCommand() throw() {}
 782   const std::vector<Expr>& getVars() const throw();
 783   const std::vector<Expr>& getGuards() const throw();
 784   const std::vector<Expr>& getHeads() const throw();
 785   Expr getBody() const throw();
 786   const Triggers& getTriggers() const throw();
 787   bool isDeduction() const throw();
 788   void invoke(SmtEngine* smtEngine) throw();
 789   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 790   Command* clone() const;
 791   std::string getCommandName() const throw();
 792 };/* class PropagateRuleCommand */
 793
 794
 795 class CVC4_PUBLIC QuitCommand : public Command {
 796 public:
 797   QuitCommand() throw();
 798   ~QuitCommand() throw() {}
 799   void invoke(SmtEngine* smtEngine) throw();
 800   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 801   Command* clone() const;
 802   std::string getCommandName() const throw();
 803 };/* class QuitCommand */
 804
 805 class CVC4_PUBLIC CommentCommand : public Command {
 806   std::string d_comment;
 807 public:
 808   CommentCommand(std::string comment) throw();
 809   ~CommentCommand() throw() {}
 810   std::string getComment() const throw();
 811   void invoke(SmtEngine* smtEngine) throw();
 812   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 813   Command* clone() const;
 814   std::string getCommandName() const throw();
 815 };/* class CommentCommand */
 816
 817 class CVC4_PUBLIC CommandSequence : public Command {
 818 private:
 819   /** All the commands to be executed (in sequence) */
 820   std::vector<Command*> d_commandSequence;
 821   /** Next command to be executed */
 822   unsigned int d_index;
 823 public:
 824   CommandSequence() throw();
 825   ~CommandSequence() throw();
 826
 827   void addCommand(Command* cmd) throw();
 828   void clear() throw();
 829
 830   void invoke(SmtEngine* smtEngine) throw();
 831   void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
 832
 833   typedef std::vector<Command*>::iterator iterator;
 834   typedef std::vector<Command*>::const_iterator const_iterator;
 835
 836   const_iterator begin() const throw();
 837   const_iterator end() const throw();
 838
 839   iterator begin() throw();
 840   iterator end() throw();
 841
 842   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 843   Command* clone() const;
 844   std::string getCommandName() const throw();
 845 };/* class CommandSequence */
 846
 847 class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
 848 public:
 849   ~DeclarationSequence() throw() {}
 850 };/* class DeclarationSequence */
 851
 852 }/* CVC4 namespace */
 853
 854 #endif /* __CVC4__COMMAND_H */