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  public:
 472   SetUserAttributeCommand(const std::string& attr, Expr expr) throw();
 473   SetUserAttributeCommand(const std::string& attr, Expr expr,
 474                           const std::vector<Expr>& values) throw();
 475   SetUserAttributeCommand(const std::string& attr, Expr expr,
 476                           const std::string& value) throw();
 477   ~SetUserAttributeCommand() throw() override {}
 478
 479   void invoke(SmtEngine* smtEngine) override;
 480   Command* exportTo(ExprManager* exprManager,
 481                     ExprManagerMapCollection& variableMap) override;
 482   Command* clone() const override;
 483   std::string getCommandName() const throw() override;
 484
 485  private:
 486   SetUserAttributeCommand(const std::string& attr, Expr expr,
 487                           const std::vector<Expr>& expr_values,
 488                           const std::string& str_value) throw();
 489
 490   const std::string d_attr;
 491   const Expr d_expr;
 492   const std::vector<Expr> d_expr_values;
 493   const std::string d_str_value;
 494 }; /* class SetUserAttributeCommand */
 495
 496 class CVC4_PUBLIC CheckSatCommand : public Command {
 497 protected:
 498   Expr d_expr;
 499   Result d_result;
 500   bool d_inUnsatCore;
 501 public:
 502   CheckSatCommand() throw();
 503   CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw();
 504   ~CheckSatCommand() throw() {}
 505   Expr getExpr() const throw();
 506   void invoke(SmtEngine* smtEngine);
 507   Result getResult() const throw();
 508   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 509   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 510   Command* clone() const;
 511   std::string getCommandName() const throw();
 512 };/* class CheckSatCommand */
 513
 514 class CVC4_PUBLIC QueryCommand : public Command {
 515 protected:
 516   Expr d_expr;
 517   Result d_result;
 518   bool d_inUnsatCore;
 519 public:
 520   QueryCommand(const Expr& e, bool inUnsatCore = true) throw();
 521   ~QueryCommand() throw() {}
 522   Expr getExpr() const throw();
 523   void invoke(SmtEngine* smtEngine);
 524   Result getResult() const throw();
 525   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 526   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 527   Command* clone() const;
 528   std::string getCommandName() const throw();
 529 };/* class QueryCommand */
 530
 531 class CVC4_PUBLIC CheckSynthCommand : public Command {
 532 public:
 533   CheckSynthCommand() throw();
 534   CheckSynthCommand(const Expr& expr) throw();
 535   ~CheckSynthCommand() throw() {}
 536   Expr getExpr() const throw();
 537   void invoke(SmtEngine* smtEngine);
 538   Result getResult() const throw();
 539   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 540   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 541   Command* clone() const;
 542   std::string getCommandName() const throw();
 543
 544  protected:
 545   /** the assertion of check-synth */
 546   Expr d_expr;
 547   /** result of the check-synth call */
 548   Result d_result;
 549   /** string stream that stores the output of the solution */
 550   std::stringstream d_solution;
 551 };/* class CheckSynthCommand */
 552
 553 // this is TRANSFORM in the CVC presentation language
 554 class CVC4_PUBLIC SimplifyCommand : public Command {
 555 protected:
 556   Expr d_term;
 557   Expr d_result;
 558 public:
 559   SimplifyCommand(Expr term) throw();
 560   ~SimplifyCommand() throw() {}
 561   Expr getTerm() const throw();
 562   void invoke(SmtEngine* smtEngine);
 563   Expr getResult() const throw();
 564   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 565   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 566   Command* clone() const;
 567   std::string getCommandName() const throw();
 568 };/* class SimplifyCommand */
 569
 570 class CVC4_PUBLIC ExpandDefinitionsCommand : public Command {
 571 protected:
 572   Expr d_term;
 573   Expr d_result;
 574 public:
 575   ExpandDefinitionsCommand(Expr term) throw();
 576   ~ExpandDefinitionsCommand() throw() {}
 577   Expr getTerm() const throw();
 578   void invoke(SmtEngine* smtEngine);
 579   Expr getResult() const throw();
 580   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 581   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 582   Command* clone() const;
 583   std::string getCommandName() const throw();
 584 };/* class ExpandDefinitionsCommand */
 585
 586 class CVC4_PUBLIC GetValueCommand : public Command {
 587 protected:
 588   std::vector<Expr> d_terms;
 589   Expr d_result;
 590 public:
 591   GetValueCommand(Expr term) throw();
 592   GetValueCommand(const std::vector<Expr>& terms) throw();
 593   ~GetValueCommand() throw() {}
 594   const std::vector<Expr>& getTerms() const throw();
 595   void invoke(SmtEngine* smtEngine);
 596   Expr getResult() const throw();
 597   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 598   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 599   Command* clone() const;
 600   std::string getCommandName() const throw();
 601 };/* class GetValueCommand */
 602
 603 class CVC4_PUBLIC GetAssignmentCommand : public Command {
 604 protected:
 605   SExpr d_result;
 606 public:
 607   GetAssignmentCommand() throw();
 608   ~GetAssignmentCommand() throw() {}
 609   void invoke(SmtEngine* smtEngine);
 610   SExpr getResult() const throw();
 611   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 612   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 613   Command* clone() const;
 614   std::string getCommandName() const throw();
 615 };/* class GetAssignmentCommand */
 616
 617 class CVC4_PUBLIC GetModelCommand : public Command {
 618  public:
 619   GetModelCommand() throw();
 620   ~GetModelCommand() throw() {}
 621   void invoke(SmtEngine* smtEngine);
 622   // Model is private to the library -- for now
 623   // Model* getResult() const throw();
 624   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 625   Command* exportTo(ExprManager* exprManager,
 626                     ExprManagerMapCollection& variableMap);
 627   Command* clone() const;
 628   std::string getCommandName() const throw();
 629
 630  protected:
 631   Model* d_result;
 632   SmtEngine* d_smtEngine;
 633 }; /* class GetModelCommand */
 634
 635 class CVC4_PUBLIC GetProofCommand : public Command {
 636  public:
 637   GetProofCommand() throw();
 638   ~GetProofCommand() throw() {}
 639   void invoke(SmtEngine* smtEngine);
 640   const Proof& getResult() const throw();
 641   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 642   Command* exportTo(ExprManager* exprManager,
 643                     ExprManagerMapCollection& variableMap);
 644   Command* clone() const;
 645   std::string getCommandName() const throw();
 646
 647  protected:
 648   SmtEngine* d_smtEngine;
 649   // d_result is owned by d_smtEngine.
 650   const Proof* d_result;
 651 }; /* class GetProofCommand */
 652
 653 class CVC4_PUBLIC GetInstantiationsCommand : public Command {
 654  public:
 655   GetInstantiationsCommand() throw();
 656   ~GetInstantiationsCommand() throw() {}
 657   void invoke(SmtEngine* smtEngine);
 658   // Instantiations* getResult() const throw();
 659   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 660   Command* exportTo(ExprManager* exprManager,
 661                     ExprManagerMapCollection& variableMap);
 662   Command* clone() const;
 663   std::string getCommandName() const throw();
 664
 665  protected:
 666   SmtEngine* d_smtEngine;
 667 }; /* class GetInstantiationsCommand */
 668
 669 class CVC4_PUBLIC GetSynthSolutionCommand : public Command {
 670  public:
 671   GetSynthSolutionCommand() throw();
 672   ~GetSynthSolutionCommand() throw() {}
 673   void invoke(SmtEngine* smtEngine);
 674   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 675   Command* exportTo(ExprManager* exprManager,
 676                     ExprManagerMapCollection& variableMap);
 677   Command* clone() const;
 678   std::string getCommandName() const throw();
 679
 680  protected:
 681   SmtEngine* d_smtEngine;
 682 }; /* class GetSynthSolutionCommand */
 683
 684 class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command {
 685 protected:
 686   Expr d_expr;
 687   bool d_doFull;
 688   Expr d_result;
 689 public:
 690   GetQuantifierEliminationCommand() throw();
 691   GetQuantifierEliminationCommand(const Expr& expr, bool doFull) throw();
 692   ~GetQuantifierEliminationCommand() throw() {}
 693   Expr getExpr() const throw();
 694   bool getDoFull() const throw();
 695   void invoke(SmtEngine* smtEngine);
 696   Expr getResult() const throw();
 697   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 698   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 699   Command* clone() const;
 700   std::string getCommandName() const throw();
 701 };/* class GetQuantifierEliminationCommand */
 702
 703 class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
 704 public:
 705   GetUnsatCoreCommand() throw();
 706   ~GetUnsatCoreCommand() throw() {}
 707   void invoke(SmtEngine* smtEngine);
 708   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 709   const UnsatCore& getUnsatCore() const throw();
 710   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 711   Command* clone() const;
 712   std::string getCommandName() const throw();
 713
 714 protected:
 715   // the result of the unsat core call
 716   UnsatCore d_result;
 717 };/* class GetUnsatCoreCommand */
 718
 719 class CVC4_PUBLIC GetAssertionsCommand : public Command {
 720 protected:
 721   std::string d_result;
 722 public:
 723   GetAssertionsCommand() throw();
 724   ~GetAssertionsCommand() throw() {}
 725   void invoke(SmtEngine* smtEngine);
 726   std::string getResult() const throw();
 727   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 728   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 729   Command* clone() const;
 730   std::string getCommandName() const throw();
 731 };/* class GetAssertionsCommand */
 732
 733 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
 734 protected:
 735   BenchmarkStatus d_status;
 736 public:
 737   SetBenchmarkStatusCommand(BenchmarkStatus status) throw();
 738   ~SetBenchmarkStatusCommand() throw() {}
 739   BenchmarkStatus getStatus() const throw();
 740   void invoke(SmtEngine* smtEngine);
 741   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 742   Command* clone() const;
 743   std::string getCommandName() const throw();
 744 };/* class SetBenchmarkStatusCommand */
 745
 746 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
 747 protected:
 748   std::string d_logic;
 749 public:
 750   SetBenchmarkLogicCommand(std::string logic) throw();
 751   ~SetBenchmarkLogicCommand() throw() {}
 752   std::string getLogic() const throw();
 753   void invoke(SmtEngine* smtEngine);
 754   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 755   Command* clone() const;
 756   std::string getCommandName() const throw();
 757 };/* class SetBenchmarkLogicCommand */
 758
 759 class CVC4_PUBLIC SetInfoCommand : public Command {
 760 protected:
 761   std::string d_flag;
 762   SExpr d_sexpr;
 763 public:
 764   SetInfoCommand(std::string flag, const SExpr& sexpr) throw();
 765   ~SetInfoCommand() throw() {}
 766   std::string getFlag() const throw();
 767   SExpr getSExpr() const throw();
 768   void invoke(SmtEngine* smtEngine);
 769   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 770   Command* clone() const;
 771   std::string getCommandName() const throw();
 772 };/* class SetInfoCommand */
 773
 774 class CVC4_PUBLIC GetInfoCommand : public Command {
 775 protected:
 776   std::string d_flag;
 777   std::string d_result;
 778 public:
 779   GetInfoCommand(std::string flag) throw();
 780   ~GetInfoCommand() throw() {}
 781   std::string getFlag() const throw();
 782   void invoke(SmtEngine* smtEngine);
 783   std::string getResult() const throw();
 784   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 785   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 786   Command* clone() const;
 787   std::string getCommandName() const throw();
 788 };/* class GetInfoCommand */
 789
 790 class CVC4_PUBLIC SetOptionCommand : public Command {
 791 protected:
 792   std::string d_flag;
 793   SExpr d_sexpr;
 794 public:
 795   SetOptionCommand(std::string flag, const SExpr& sexpr) throw();
 796   ~SetOptionCommand() throw() {}
 797   std::string getFlag() const throw();
 798   SExpr getSExpr() const throw();
 799   void invoke(SmtEngine* smtEngine);
 800   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 801   Command* clone() const;
 802   std::string getCommandName() const throw();
 803 };/* class SetOptionCommand */
 804
 805 class CVC4_PUBLIC GetOptionCommand : public Command {
 806 protected:
 807   std::string d_flag;
 808   std::string d_result;
 809 public:
 810   GetOptionCommand(std::string flag) throw();
 811   ~GetOptionCommand() throw() {}
 812   std::string getFlag() const throw();
 813   void invoke(SmtEngine* smtEngine);
 814   std::string getResult() const throw();
 815   void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 816   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 817   Command* clone() const;
 818   std::string getCommandName() const throw();
 819 };/* class GetOptionCommand */
 820
 821 // Set expression name command
 822 // Note this is not an official smt2 command
 823 // Conceptually:
 824 //   (assert (! expr :named name))
 825 // is converted to
 826 //   (assert expr)
 827 //   (set-expr-name expr name)
 828 class CVC4_PUBLIC SetExpressionNameCommand : public Command {
 829 protected:
 830   Expr d_expr;
 831   std::string d_name;
 832 public:
 833   SetExpressionNameCommand(Expr expr, std::string name) throw();
 834   ~SetExpressionNameCommand() throw() {}
 835   void invoke(SmtEngine* smtEngine);
 836   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 837   Command* clone() const;
 838   std::string getCommandName() const throw();
 839 };/* class SetExpressionNameCommand */
 840
 841
 842 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
 843 private:
 844   std::vector<DatatypeType> d_datatypes;
 845 public:
 846   DatatypeDeclarationCommand(const DatatypeType& datatype) throw();
 847   ~DatatypeDeclarationCommand() throw() {}
 848   DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
 849   const std::vector<DatatypeType>& getDatatypes() const throw();
 850   void invoke(SmtEngine* smtEngine);
 851   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 852   Command* clone() const;
 853   std::string getCommandName() const throw();
 854 };/* class DatatypeDeclarationCommand */
 855
 856 class CVC4_PUBLIC RewriteRuleCommand : public Command {
 857 public:
 858   typedef std::vector< std::vector< Expr > > Triggers;
 859 protected:
 860   typedef std::vector< Expr > VExpr;
 861   VExpr d_vars;
 862   VExpr d_guards;
 863   Expr d_head;
 864   Expr d_body;
 865   Triggers d_triggers;
 866 public:
 867   RewriteRuleCommand(const std::vector<Expr>& vars,
 868                      const std::vector<Expr>& guards,
 869                      Expr head,
 870                      Expr body,
 871                      const Triggers& d_triggers) throw();
 872   RewriteRuleCommand(const std::vector<Expr>& vars,
 873                      Expr head,
 874                      Expr body) throw();
 875   ~RewriteRuleCommand() throw() {}
 876   const std::vector<Expr>& getVars() const throw();
 877   const std::vector<Expr>& getGuards() const throw();
 878   Expr getHead() const throw();
 879   Expr getBody() const throw();
 880   const Triggers& getTriggers() const throw();
 881   void invoke(SmtEngine* smtEngine);
 882   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 883   Command* clone() const;
 884   std::string getCommandName() const throw();
 885 };/* class RewriteRuleCommand */
 886
 887 class CVC4_PUBLIC PropagateRuleCommand : public Command {
 888 public:
 889   typedef std::vector< std::vector< Expr > > Triggers;
 890 protected:
 891   typedef std::vector< Expr > VExpr;
 892   VExpr d_vars;
 893   VExpr d_guards;
 894   VExpr d_heads;
 895   Expr d_body;
 896   Triggers d_triggers;
 897   bool d_deduction;
 898 public:
 899   PropagateRuleCommand(const std::vector<Expr>& vars,
 900                        const std::vector<Expr>& guards,
 901                        const std::vector<Expr>& heads,
 902                        Expr body,
 903                        const Triggers& d_triggers,
 904                        /* true if we want a deduction rule */
 905                        bool d_deduction = false) throw();
 906   PropagateRuleCommand(const std::vector<Expr>& vars,
 907                        const std::vector<Expr>& heads,
 908                        Expr body,
 909                        bool d_deduction = false) throw();
 910   ~PropagateRuleCommand() throw() {}
 911   const std::vector<Expr>& getVars() const throw();
 912   const std::vector<Expr>& getGuards() const throw();
 913   const std::vector<Expr>& getHeads() const throw();
 914   Expr getBody() const throw();
 915   const Triggers& getTriggers() const throw();
 916   bool isDeduction() 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 PropagateRuleCommand */
 922
 923 class CVC4_PUBLIC ResetCommand : public Command {
 924 public:
 925   ResetCommand() throw() {}
 926   ~ResetCommand() throw() {}
 927   void invoke(SmtEngine* smtEngine);
 928   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 929   Command* clone() const;
 930   std::string getCommandName() const throw();
 931 };/* class ResetCommand */
 932
 933 class CVC4_PUBLIC ResetAssertionsCommand : public Command {
 934 public:
 935   ResetAssertionsCommand() throw() {}
 936   ~ResetAssertionsCommand() throw() {}
 937   void invoke(SmtEngine* smtEngine);
 938   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 939   Command* clone() const;
 940   std::string getCommandName() const throw();
 941 };/* class ResetAssertionsCommand */
 942
 943 class CVC4_PUBLIC QuitCommand : public Command {
 944 public:
 945   QuitCommand() throw() {}
 946   ~QuitCommand() throw() {}
 947   void invoke(SmtEngine* smtEngine);
 948   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 949   Command* clone() const;
 950   std::string getCommandName() const throw();
 951 };/* class QuitCommand */
 952
 953 class CVC4_PUBLIC CommentCommand : public Command {
 954   std::string d_comment;
 955 public:
 956   CommentCommand(std::string comment) throw();
 957   ~CommentCommand() throw() {}
 958   std::string getComment() const throw();
 959   void invoke(SmtEngine* smtEngine);
 960   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 961   Command* clone() const;
 962   std::string getCommandName() const throw();
 963 };/* class CommentCommand */
 964
 965 class CVC4_PUBLIC CommandSequence : public Command {
 966 private:
 967   /** All the commands to be executed (in sequence) */
 968   std::vector<Command*> d_commandSequence;
 969   /** Next command to be executed */
 970   unsigned int d_index;
 971 public:
 972   CommandSequence() throw();
 973   ~CommandSequence() throw();
 974
 975   void addCommand(Command* cmd) throw();
 976   void clear() throw();
 977
 978   void invoke(SmtEngine* smtEngine);
 979   void invoke(SmtEngine* smtEngine, std::ostream& out);
 980
 981   typedef std::vector<Command*>::iterator iterator;
 982   typedef std::vector<Command*>::const_iterator const_iterator;
 983
 984   const_iterator begin() const throw();
 985   const_iterator end() const throw();
 986
 987   iterator begin() throw();
 988   iterator end() throw();
 989
 990   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 991   Command* clone() const;
 992   std::string getCommandName() const throw();
 993 };/* class CommandSequence */
 994
 995 class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
 996 public:
 997   ~DeclarationSequence() throw() {}
 998 };/* class DeclarationSequence */
 999
1000 }/* CVC4 namespace */
1001
1002 #endif /* __CVC4__COMMAND_H */