src/smt/command.h

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