src/smt/command.h

   1 /*********************                                                        */
   2 /*! \file command.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Morgan Deters, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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&) CVC4_PUBLIC;
  48 std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
  49 std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC4_PUBLIC;
  50 std::ostream& operator<<(std::ostream&, const CommandStatus*) CVC4_PUBLIC;
  51
  52 /** The status an SMT benchmark can have */
  53 enum BenchmarkStatus
  54 {
  55   /** Benchmark is satisfiable */
  56   SMT_SATISFIABLE,
  57   /** Benchmark is unsatisfiable */
  58   SMT_UNSATISFIABLE,
  59   /** The status of the benchmark is unknown */
  60   SMT_UNKNOWN
  61 }; /* enum BenchmarkStatus */
  62
  63 std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) 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  public:
  80   /** Construct a CommandPrintSuccess with the given setting. */
  81   CommandPrintSuccess(bool printSuccess) : d_printSuccess(printSuccess) {}
  82   void applyPrintSuccess(std::ostream& out);
  83   static bool getPrintSuccess(std::ostream& out);
  84   static void setPrintSuccess(std::ostream& out, bool printSuccess);
  85
  86  private:
  87   /** The allocated index in ios_base for our depth setting. */
  88   static const int s_iosIndex;
  89
  90   /**
  91    * The default setting, for ostreams that haven't yet had a setdepth()
  92    * applied to them.
  93    */
  94   static const int s_defaultPrintSuccess = false;
  95
  96   /** When this manipulator is used, the setting is stored here. */
  97   bool d_printSuccess;
  98
  99 }; /* class CommandPrintSuccess */
 100
 101 /**
 102  * Sets the default print-success setting when pretty-printing an Expr
 103  * to an ostream.  Use like this:
 104  *
 105  *   // let out be an ostream, e an Expr
 106  *   out << Expr::setdepth(n) << e << endl;
 107  *
 108  * The depth stays permanently (until set again) with the stream.
 109  */
 110 std::ostream& operator<<(std::ostream& out,
 111                          CommandPrintSuccess cps) CVC4_PUBLIC;
 112
 113 class CVC4_PUBLIC CommandStatus
 114 {
 115  protected:
 116   // shouldn't construct a CommandStatus (use a derived class)
 117   CommandStatus() {}
 118  public:
 119   virtual ~CommandStatus() {}
 120   void toStream(std::ostream& out,
 121                 OutputLanguage language = language::output::LANG_AUTO) const;
 122   virtual CommandStatus& clone() const = 0;
 123 }; /* class CommandStatus */
 124
 125 class CVC4_PUBLIC CommandSuccess : public CommandStatus
 126 {
 127   static const CommandSuccess* s_instance;
 128
 129  public:
 130   static const CommandSuccess* instance() { return s_instance; }
 131   CommandStatus& clone() const override
 132   {
 133     return const_cast<CommandSuccess&>(*this);
 134   }
 135 }; /* class CommandSuccess */
 136
 137 class CVC4_PUBLIC CommandInterrupted : public CommandStatus
 138 {
 139   static const CommandInterrupted* s_instance;
 140
 141  public:
 142   static const CommandInterrupted* instance() { return s_instance; }
 143   CommandStatus& clone() const override
 144   {
 145     return const_cast<CommandInterrupted&>(*this);
 146   }
 147 }; /* class CommandInterrupted */
 148
 149 class CVC4_PUBLIC CommandUnsupported : public CommandStatus
 150 {
 151  public:
 152   CommandStatus& clone() const override
 153   {
 154     return *new CommandUnsupported(*this);
 155   }
 156 }; /* class CommandSuccess */
 157
 158 class CVC4_PUBLIC CommandFailure : public CommandStatus
 159 {
 160   std::string d_message;
 161
 162  public:
 163   CommandFailure(std::string message) : d_message(message) {}
 164   CommandFailure& clone() const override { return *new CommandFailure(*this); }
 165   std::string getMessage() const { return d_message; }
 166 }; /* class CommandFailure */
 167
 168 /**
 169  * The execution of the command resulted in a non-fatal error and further
 170  * commands can be processed. This status is for example used when a user asks
 171  * for an unsat core in a place that is not immediately preceded by an
 172  * unsat/valid response.
 173  */
 174 class CVC4_PUBLIC CommandRecoverableFailure : public CommandStatus
 175 {
 176   std::string d_message;
 177
 178  public:
 179   CommandRecoverableFailure(std::string message) : d_message(message) {}
 180   CommandRecoverableFailure& clone() const override
 181   {
 182     return *new CommandRecoverableFailure(*this);
 183   }
 184   std::string getMessage() const { return d_message; }
 185 }; /* class CommandRecoverableFailure */
 186
 187 class CVC4_PUBLIC Command
 188 {
 189  protected:
 190   /**
 191    * This field contains a command status if the command has been
 192    * invoked, or NULL if it has not.  This field is either a
 193    * dynamically-allocated pointer, or it's a pointer to the singleton
 194    * CommandSuccess instance.  Doing so is somewhat asymmetric, but
 195    * it avoids the need to dynamically allocate memory in the common
 196    * case of a successful command.
 197    */
 198   const CommandStatus* d_commandStatus;
 199
 200   /**
 201    * True if this command is "muted"---i.e., don't print "success" on
 202    * successful execution.
 203    */
 204   bool d_muted;
 205
 206  public:
 207   typedef CommandPrintSuccess printsuccess;
 208
 209   Command();
 210   Command(const Command& cmd);
 211
 212   virtual ~Command();
 213
 214   virtual void invoke(SmtEngine* smtEngine) = 0;
 215   virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
 216
 217   void toStream(std::ostream& out,
 218                 int toDepth = -1,
 219                 bool types = false,
 220                 size_t dag = 1,
 221                 OutputLanguage language = language::output::LANG_AUTO) const;
 222
 223   std::string toString() const;
 224
 225   virtual std::string getCommandName() const = 0;
 226
 227   /**
 228    * If false, instruct this Command not to print a success message.
 229    */
 230   void setMuted(bool muted) { d_muted = muted; }
 231   /**
 232    * Determine whether this Command will print a success message.
 233    */
 234   bool isMuted() { return d_muted; }
 235   /**
 236    * Either the command hasn't run yet, or it completed successfully
 237    * (CommandSuccess, not CommandUnsupported or CommandFailure).
 238    */
 239   bool ok() const;
 240
 241   /**
 242    * The command completed in a failure state (CommandFailure, not
 243    * CommandSuccess or CommandUnsupported).
 244    */
 245   bool fail() const;
 246
 247   /**
 248    * The command was ran but was interrupted due to resource limiting.
 249    */
 250   bool interrupted() const;
 251
 252   /** Get the command status (it's NULL if we haven't run yet). */
 253   const CommandStatus* getCommandStatus() const { return d_commandStatus; }
 254   virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const;
 255
 256   /**
 257    * Maps this Command into one for a different ExprManager, using
 258    * variableMap for the translation and extending it with any new
 259    * mappings.
 260    */
 261   virtual Command* exportTo(ExprManager* exprManager,
 262                             ExprManagerMapCollection& variableMap) = 0;
 263
 264   /**
 265    * Clone this Command (make a shallow copy).
 266    */
 267   virtual Command* clone() const = 0;
 268
 269  protected:
 270   class ExportTransformer
 271   {
 272     ExprManager* d_exprManager;
 273     ExprManagerMapCollection& d_variableMap;
 274
 275    public:
 276     ExportTransformer(ExprManager* exprManager,
 277                       ExprManagerMapCollection& variableMap)
 278         : d_exprManager(exprManager), d_variableMap(variableMap)
 279     {
 280     }
 281     Expr operator()(Expr e) { return e.exportTo(d_exprManager, d_variableMap); }
 282     Type operator()(Type t) { return t.exportTo(d_exprManager, d_variableMap); }
 283   }; /* class Command::ExportTransformer */
 284 };   /* class Command */
 285
 286 /**
 287  * EmptyCommands are the residue of a command after the parser handles
 288  * them (and there's nothing left to do).
 289  */
 290 class CVC4_PUBLIC EmptyCommand : public Command
 291 {
 292  public:
 293   EmptyCommand(std::string name = "");
 294   std::string getName() const;
 295   void invoke(SmtEngine* smtEngine) override;
 296   Command* exportTo(ExprManager* exprManager,
 297                     ExprManagerMapCollection& variableMap) override;
 298   Command* clone() const override;
 299   std::string getCommandName() const override;
 300
 301  protected:
 302   std::string d_name;
 303 }; /* class EmptyCommand */
 304
 305 class CVC4_PUBLIC EchoCommand : public Command
 306 {
 307  public:
 308   EchoCommand(std::string output = "");
 309
 310   std::string getOutput() const;
 311
 312   void invoke(SmtEngine* smtEngine) override;
 313   void invoke(SmtEngine* smtEngine, std::ostream& out) override;
 314   Command* exportTo(ExprManager* exprManager,
 315                     ExprManagerMapCollection& variableMap) override;
 316   Command* clone() const override;
 317   std::string getCommandName() const override;
 318
 319  protected:
 320   std::string d_output;
 321 }; /* class EchoCommand */
 322
 323 class CVC4_PUBLIC AssertCommand : public Command
 324 {
 325  protected:
 326   Expr d_expr;
 327   bool d_inUnsatCore;
 328
 329  public:
 330   AssertCommand(const Expr& e, bool inUnsatCore = true);
 331
 332   Expr getExpr() const;
 333
 334   void invoke(SmtEngine* smtEngine) override;
 335   Command* exportTo(ExprManager* exprManager,
 336                     ExprManagerMapCollection& variableMap) override;
 337   Command* clone() const override;
 338   std::string getCommandName() const override;
 339 }; /* class AssertCommand */
 340
 341 class CVC4_PUBLIC PushCommand : public Command
 342 {
 343  public:
 344   void invoke(SmtEngine* smtEngine) override;
 345   Command* exportTo(ExprManager* exprManager,
 346                     ExprManagerMapCollection& variableMap) override;
 347   Command* clone() const override;
 348   std::string getCommandName() const override;
 349 }; /* class PushCommand */
 350
 351 class CVC4_PUBLIC PopCommand : public Command
 352 {
 353  public:
 354   void invoke(SmtEngine* smtEngine) override;
 355   Command* exportTo(ExprManager* exprManager,
 356                     ExprManagerMapCollection& variableMap) override;
 357   Command* clone() const override;
 358   std::string getCommandName() const override;
 359 }; /* class PopCommand */
 360
 361 class CVC4_PUBLIC DeclarationDefinitionCommand : public Command
 362 {
 363  protected:
 364   std::string d_symbol;
 365
 366  public:
 367   DeclarationDefinitionCommand(const std::string& id);
 368
 369   void invoke(SmtEngine* smtEngine) override = 0;
 370   std::string getSymbol() const;
 371 }; /* class DeclarationDefinitionCommand */
 372
 373 class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand
 374 {
 375  protected:
 376   Expr d_func;
 377   Type d_type;
 378   bool d_printInModel;
 379   bool d_printInModelSetByUser;
 380
 381  public:
 382   DeclareFunctionCommand(const std::string& id, Expr func, Type type);
 383   Expr getFunction() const;
 384   Type getType() const;
 385   bool getPrintInModel() const;
 386   bool getPrintInModelSetByUser() const;
 387   void setPrintInModel(bool p);
 388
 389   void invoke(SmtEngine* smtEngine) override;
 390   Command* exportTo(ExprManager* exprManager,
 391                     ExprManagerMapCollection& variableMap) override;
 392   Command* clone() const override;
 393   std::string getCommandName() const override;
 394 }; /* class DeclareFunctionCommand */
 395
 396 class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand
 397 {
 398  protected:
 399   size_t d_arity;
 400   Type d_type;
 401
 402  public:
 403   DeclareTypeCommand(const std::string& id, size_t arity, Type t);
 404
 405   size_t getArity() const;
 406   Type getType() const;
 407
 408   void invoke(SmtEngine* smtEngine) override;
 409   Command* exportTo(ExprManager* exprManager,
 410                     ExprManagerMapCollection& variableMap) override;
 411   Command* clone() const override;
 412   std::string getCommandName() const override;
 413 }; /* class DeclareTypeCommand */
 414
 415 class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand
 416 {
 417  protected:
 418   std::vector<Type> d_params;
 419   Type d_type;
 420
 421  public:
 422   DefineTypeCommand(const std::string& id, Type t);
 423   DefineTypeCommand(const std::string& id,
 424                     const std::vector<Type>& params,
 425                     Type t);
 426
 427   const std::vector<Type>& getParameters() const;
 428   Type getType() const;
 429
 430   void invoke(SmtEngine* smtEngine) override;
 431   Command* exportTo(ExprManager* exprManager,
 432                     ExprManagerMapCollection& variableMap) override;
 433   Command* clone() const override;
 434   std::string getCommandName() const override;
 435 }; /* class DefineTypeCommand */
 436
 437 class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand
 438 {
 439  protected:
 440   Expr d_func;
 441   std::vector<Expr> d_formals;
 442   Expr d_formula;
 443
 444  public:
 445   DefineFunctionCommand(const std::string& id, Expr func, Expr formula);
 446   DefineFunctionCommand(const std::string& id,
 447                         Expr func,
 448                         const std::vector<Expr>& formals,
 449                         Expr formula);
 450
 451   Expr getFunction() const;
 452   const std::vector<Expr>& getFormals() const;
 453   Expr getFormula() const;
 454
 455   void invoke(SmtEngine* smtEngine) override;
 456   Command* exportTo(ExprManager* exprManager,
 457                     ExprManagerMapCollection& variableMap) override;
 458   Command* clone() const override;
 459   std::string getCommandName() const override;
 460 }; /* class DefineFunctionCommand */
 461
 462 /**
 463  * This differs from DefineFunctionCommand only in that it instructs
 464  * the SmtEngine to "remember" this function for later retrieval with
 465  * getAssignment().  Used for :named attributes in SMT-LIBv2.
 466  */
 467 class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand
 468 {
 469  public:
 470   DefineNamedFunctionCommand(const std::string& id,
 471                              Expr func,
 472                              const std::vector<Expr>& formals,
 473                              Expr formula);
 474   void invoke(SmtEngine* smtEngine) override;
 475   Command* exportTo(ExprManager* exprManager,
 476                     ExprManagerMapCollection& variableMap) override;
 477   Command* clone() const override;
 478 }; /* class DefineNamedFunctionCommand */
 479
 480 /**
 481  * The command when parsing define-fun-rec or define-funs-rec.
 482  * This command will assert a set of quantified formulas that specify
 483  * the (mutually recursive) function definitions provided to it.
 484  */
 485 class CVC4_PUBLIC DefineFunctionRecCommand : public Command
 486 {
 487  public:
 488   DefineFunctionRecCommand(Expr func,
 489                            const std::vector<Expr>& formals,
 490                            Expr formula);
 491   DefineFunctionRecCommand(const std::vector<Expr>& funcs,
 492                            const std::vector<std::vector<Expr> >& formals,
 493                            const std::vector<Expr>& formula);
 494
 495   const std::vector<Expr>& getFunctions() const;
 496   const std::vector<std::vector<Expr> >& getFormals() const;
 497   const std::vector<Expr>& getFormulas() const;
 498
 499   void invoke(SmtEngine* smtEngine) override;
 500   Command* exportTo(ExprManager* exprManager,
 501                     ExprManagerMapCollection& variableMap) override;
 502   Command* clone() const override;
 503   std::string getCommandName() const override;
 504
 505  protected:
 506   /** functions we are defining */
 507   std::vector<Expr> d_funcs;
 508   /** formal arguments for each of the functions we are defining */
 509   std::vector<std::vector<Expr> > d_formals;
 510   /** formulas corresponding to the bodies of the functions we are defining */
 511   std::vector<Expr> d_formulas;
 512 }; /* class DefineFunctionRecCommand */
 513
 514 /**
 515  * The command when an attribute is set by a user.  In SMT-LIBv2 this is done
 516  *  via the syntax (! expr :attr)
 517  */
 518 class CVC4_PUBLIC SetUserAttributeCommand : public Command
 519 {
 520  public:
 521   SetUserAttributeCommand(const std::string& attr, Expr expr);
 522   SetUserAttributeCommand(const std::string& attr,
 523                           Expr expr,
 524                           const std::vector<Expr>& values);
 525   SetUserAttributeCommand(const std::string& attr,
 526                           Expr expr,
 527                           const std::string& value);
 528
 529   void invoke(SmtEngine* smtEngine) override;
 530   Command* exportTo(ExprManager* exprManager,
 531                     ExprManagerMapCollection& variableMap) override;
 532   Command* clone() const override;
 533   std::string getCommandName() const override;
 534
 535  private:
 536   SetUserAttributeCommand(const std::string& attr,
 537                           Expr expr,
 538                           const std::vector<Expr>& expr_values,
 539                           const std::string& str_value);
 540
 541   const std::string d_attr;
 542   const Expr d_expr;
 543   const std::vector<Expr> d_expr_values;
 544   const std::string d_str_value;
 545 }; /* class SetUserAttributeCommand */
 546
 547 /**
 548  * The command when parsing check-sat.
 549  * This command will check satisfiability of the input formula.
 550  */
 551 class CVC4_PUBLIC CheckSatCommand : public Command
 552 {
 553  public:
 554   CheckSatCommand();
 555   CheckSatCommand(const Expr& expr, bool inUnsatCore = true);
 556
 557   Expr getExpr() const;
 558   Result getResult() const;
 559   void invoke(SmtEngine* smtEngine) override;
 560   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 561   Command* exportTo(ExprManager* exprManager,
 562                     ExprManagerMapCollection& variableMap) override;
 563   Command* clone() const override;
 564   std::string getCommandName() const override;
 565
 566  private:
 567   Expr d_expr;
 568   Result d_result;
 569   bool d_inUnsatCore;
 570 }; /* class CheckSatCommand */
 571
 572 /**
 573  * The command when parsing check-sat-assuming.
 574  * This command will assume a set of formulas and check satisfiability of the
 575  * input formula under these assumptions.
 576  */
 577 class CVC4_PUBLIC CheckSatAssumingCommand : public Command
 578 {
 579  public:
 580   CheckSatAssumingCommand(Expr term);
 581   CheckSatAssumingCommand(const std::vector<Expr>& terms,
 582                           bool inUnsatCore = true);
 583
 584   const std::vector<Expr>& getTerms() const;
 585   Result getResult() const;
 586   void invoke(SmtEngine* smtEngine) override;
 587   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 588   Command* exportTo(ExprManager* exprManager,
 589                     ExprManagerMapCollection& variableMap) override;
 590   Command* clone() const override;
 591   std::string getCommandName() const override;
 592
 593  private:
 594   std::vector<Expr> d_terms;
 595   Result d_result;
 596   bool d_inUnsatCore;
 597 }; /* class CheckSatAssumingCommand */
 598
 599 class CVC4_PUBLIC QueryCommand : public Command
 600 {
 601  protected:
 602   Expr d_expr;
 603   Result d_result;
 604   bool d_inUnsatCore;
 605
 606  public:
 607   QueryCommand(const Expr& e, bool inUnsatCore = true);
 608
 609   Expr getExpr() const;
 610   Result getResult() const;
 611   void invoke(SmtEngine* smtEngine) override;
 612   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 613   Command* exportTo(ExprManager* exprManager,
 614                     ExprManagerMapCollection& variableMap) override;
 615   Command* clone() const override;
 616   std::string getCommandName() const override;
 617 }; /* class QueryCommand */
 618
 619 class CVC4_PUBLIC CheckSynthCommand : public Command
 620 {
 621  public:
 622   CheckSynthCommand();
 623   CheckSynthCommand(const Expr& expr);
 624
 625   Expr getExpr() const;
 626   Result getResult() const;
 627   void invoke(SmtEngine* smtEngine) override;
 628   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 629   Command* exportTo(ExprManager* exprManager,
 630                     ExprManagerMapCollection& variableMap) override;
 631   Command* clone() const override;
 632   std::string getCommandName() const override;
 633
 634  protected:
 635   /** the assertion of check-synth */
 636   Expr d_expr;
 637   /** result of the check-synth call */
 638   Result d_result;
 639   /** string stream that stores the output of the solution */
 640   std::stringstream d_solution;
 641 }; /* class CheckSynthCommand */
 642
 643 // this is TRANSFORM in the CVC presentation language
 644 class CVC4_PUBLIC SimplifyCommand : public Command
 645 {
 646  protected:
 647   Expr d_term;
 648   Expr d_result;
 649
 650  public:
 651   SimplifyCommand(Expr term);
 652
 653   Expr getTerm() const;
 654   Expr getResult() const;
 655   void invoke(SmtEngine* smtEngine) override;
 656   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 657   Command* exportTo(ExprManager* exprManager,
 658                     ExprManagerMapCollection& variableMap) override;
 659   Command* clone() const override;
 660   std::string getCommandName() const override;
 661 }; /* class SimplifyCommand */
 662
 663 class CVC4_PUBLIC ExpandDefinitionsCommand : public Command
 664 {
 665  protected:
 666   Expr d_term;
 667   Expr d_result;
 668
 669  public:
 670   ExpandDefinitionsCommand(Expr term);
 671
 672   Expr getTerm() const;
 673   Expr getResult() const;
 674   void invoke(SmtEngine* smtEngine) override;
 675   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 676   Command* exportTo(ExprManager* exprManager,
 677                     ExprManagerMapCollection& variableMap) override;
 678   Command* clone() const override;
 679   std::string getCommandName() const override;
 680 }; /* class ExpandDefinitionsCommand */
 681
 682 class CVC4_PUBLIC GetValueCommand : public Command
 683 {
 684  protected:
 685   std::vector<Expr> d_terms;
 686   Expr d_result;
 687
 688  public:
 689   GetValueCommand(Expr term);
 690   GetValueCommand(const std::vector<Expr>& terms);
 691
 692   const std::vector<Expr>& getTerms() const;
 693   Expr getResult() const;
 694   void invoke(SmtEngine* smtEngine) override;
 695   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 696   Command* exportTo(ExprManager* exprManager,
 697                     ExprManagerMapCollection& variableMap) override;
 698   Command* clone() const override;
 699   std::string getCommandName() const override;
 700 }; /* class GetValueCommand */
 701
 702 class CVC4_PUBLIC GetAssignmentCommand : public Command
 703 {
 704  protected:
 705   SExpr d_result;
 706
 707  public:
 708   GetAssignmentCommand();
 709
 710   SExpr getResult() const;
 711   void invoke(SmtEngine* smtEngine) override;
 712   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 713   Command* exportTo(ExprManager* exprManager,
 714                     ExprManagerMapCollection& variableMap) override;
 715   Command* clone() const override;
 716   std::string getCommandName() const override;
 717 }; /* class GetAssignmentCommand */
 718
 719 class CVC4_PUBLIC GetModelCommand : public Command
 720 {
 721  public:
 722   GetModelCommand();
 723
 724   // Model is private to the library -- for now
 725   // Model* getResult() const ;
 726   void invoke(SmtEngine* smtEngine) override;
 727   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 728   Command* exportTo(ExprManager* exprManager,
 729                     ExprManagerMapCollection& variableMap) override;
 730   Command* clone() const override;
 731   std::string getCommandName() const override;
 732
 733  protected:
 734   Model* d_result;
 735   SmtEngine* d_smtEngine;
 736 }; /* class GetModelCommand */
 737
 738 class CVC4_PUBLIC GetProofCommand : public Command
 739 {
 740  public:
 741   GetProofCommand();
 742
 743   const Proof& getResult() const;
 744   void invoke(SmtEngine* smtEngine) override;
 745   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 746   Command* exportTo(ExprManager* exprManager,
 747                     ExprManagerMapCollection& variableMap) override;
 748   Command* clone() const override;
 749   std::string getCommandName() const override;
 750
 751  protected:
 752   SmtEngine* d_smtEngine;
 753   // d_result is owned by d_smtEngine.
 754   const Proof* d_result;
 755 }; /* class GetProofCommand */
 756
 757 class CVC4_PUBLIC GetInstantiationsCommand : public Command
 758 {
 759  public:
 760   GetInstantiationsCommand();
 761
 762   void invoke(SmtEngine* smtEngine) override;
 763   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 764   Command* exportTo(ExprManager* exprManager,
 765                     ExprManagerMapCollection& variableMap) override;
 766   Command* clone() const override;
 767   std::string getCommandName() const override;
 768
 769  protected:
 770   SmtEngine* d_smtEngine;
 771 }; /* class GetInstantiationsCommand */
 772
 773 class CVC4_PUBLIC GetSynthSolutionCommand : public Command
 774 {
 775  public:
 776   GetSynthSolutionCommand();
 777
 778   void invoke(SmtEngine* smtEngine) override;
 779   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 780   Command* exportTo(ExprManager* exprManager,
 781                     ExprManagerMapCollection& variableMap) override;
 782   Command* clone() const override;
 783   std::string getCommandName() const override;
 784
 785  protected:
 786   SmtEngine* d_smtEngine;
 787 }; /* class GetSynthSolutionCommand */
 788
 789 class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
 790 {
 791  protected:
 792   Expr d_expr;
 793   bool d_doFull;
 794   Expr d_result;
 795
 796  public:
 797   GetQuantifierEliminationCommand();
 798   GetQuantifierEliminationCommand(const Expr& expr, bool doFull);
 799
 800   Expr getExpr() const;
 801   bool getDoFull() const;
 802   void invoke(SmtEngine* smtEngine) override;
 803   Expr getResult() const;
 804   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 805
 806   Command* exportTo(ExprManager* exprManager,
 807                     ExprManagerMapCollection& variableMap) override;
 808   Command* clone() const override;
 809   std::string getCommandName() const override;
 810 }; /* class GetQuantifierEliminationCommand */
 811
 812 class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
 813 {
 814  public:
 815   GetUnsatAssumptionsCommand();
 816   void invoke(SmtEngine* smtEngine) override;
 817   std::vector<Expr> getResult() const;
 818   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 819   Command* exportTo(ExprManager* exprManager,
 820                     ExprManagerMapCollection& variableMap) override;
 821   Command* clone() const override;
 822   std::string getCommandName() const override;
 823  protected:
 824   std::vector<Expr> d_result;
 825 }; /* class GetUnsatAssumptionsCommand */
 826
 827 class CVC4_PUBLIC GetUnsatCoreCommand : public Command
 828 {
 829  public:
 830   GetUnsatCoreCommand();
 831   const UnsatCore& getUnsatCore() const;
 832
 833   void invoke(SmtEngine* smtEngine) override;
 834   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 835
 836   Command* exportTo(ExprManager* exprManager,
 837                     ExprManagerMapCollection& variableMap) override;
 838   Command* clone() const override;
 839   std::string getCommandName() const override;
 840
 841  protected:
 842   // the result of the unsat core call
 843   UnsatCore d_result;
 844 }; /* class GetUnsatCoreCommand */
 845
 846 class CVC4_PUBLIC GetAssertionsCommand : public Command
 847 {
 848  protected:
 849   std::string d_result;
 850
 851  public:
 852   GetAssertionsCommand();
 853
 854   void invoke(SmtEngine* smtEngine) override;
 855   std::string getResult() const;
 856   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 857   Command* exportTo(ExprManager* exprManager,
 858                     ExprManagerMapCollection& variableMap) override;
 859   Command* clone() const override;
 860   std::string getCommandName() const override;
 861 }; /* class GetAssertionsCommand */
 862
 863 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command
 864 {
 865  protected:
 866   BenchmarkStatus d_status;
 867
 868  public:
 869   SetBenchmarkStatusCommand(BenchmarkStatus status);
 870
 871   BenchmarkStatus getStatus() const;
 872
 873   void invoke(SmtEngine* smtEngine) override;
 874   Command* exportTo(ExprManager* exprManager,
 875                     ExprManagerMapCollection& variableMap) override;
 876   Command* clone() const override;
 877   std::string getCommandName() const override;
 878 }; /* class SetBenchmarkStatusCommand */
 879
 880 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command
 881 {
 882  protected:
 883   std::string d_logic;
 884
 885  public:
 886   SetBenchmarkLogicCommand(std::string logic);
 887
 888   std::string getLogic() const;
 889   void invoke(SmtEngine* smtEngine) override;
 890   Command* exportTo(ExprManager* exprManager,
 891                     ExprManagerMapCollection& variableMap) override;
 892   Command* clone() const override;
 893   std::string getCommandName() const override;
 894 }; /* class SetBenchmarkLogicCommand */
 895
 896 class CVC4_PUBLIC SetInfoCommand : public Command
 897 {
 898  protected:
 899   std::string d_flag;
 900   SExpr d_sexpr;
 901
 902  public:
 903   SetInfoCommand(std::string flag, const SExpr& sexpr);
 904
 905   std::string getFlag() const;
 906   SExpr getSExpr() const;
 907
 908   void invoke(SmtEngine* smtEngine) override;
 909   Command* exportTo(ExprManager* exprManager,
 910                     ExprManagerMapCollection& variableMap) override;
 911   Command* clone() const override;
 912   std::string getCommandName() const override;
 913 }; /* class SetInfoCommand */
 914
 915 class CVC4_PUBLIC GetInfoCommand : public Command
 916 {
 917  protected:
 918   std::string d_flag;
 919   std::string d_result;
 920
 921  public:
 922   GetInfoCommand(std::string flag);
 923
 924   std::string getFlag() const;
 925   std::string getResult() const;
 926
 927   void invoke(SmtEngine* smtEngine) override;
 928   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 929   Command* exportTo(ExprManager* exprManager,
 930                     ExprManagerMapCollection& variableMap) override;
 931   Command* clone() const override;
 932   std::string getCommandName() const override;
 933 }; /* class GetInfoCommand */
 934
 935 class CVC4_PUBLIC SetOptionCommand : public Command
 936 {
 937  protected:
 938   std::string d_flag;
 939   SExpr d_sexpr;
 940
 941  public:
 942   SetOptionCommand(std::string flag, const SExpr& sexpr);
 943
 944   std::string getFlag() const;
 945   SExpr getSExpr() const;
 946
 947   void invoke(SmtEngine* smtEngine) override;
 948   Command* exportTo(ExprManager* exprManager,
 949                     ExprManagerMapCollection& variableMap) override;
 950   Command* clone() const override;
 951   std::string getCommandName() const override;
 952 }; /* class SetOptionCommand */
 953
 954 class CVC4_PUBLIC GetOptionCommand : public Command
 955 {
 956  protected:
 957   std::string d_flag;
 958   std::string d_result;
 959
 960  public:
 961   GetOptionCommand(std::string flag);
 962
 963   std::string getFlag() const;
 964   std::string getResult() const;
 965
 966   void invoke(SmtEngine* smtEngine) override;
 967   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 968   Command* exportTo(ExprManager* exprManager,
 969                     ExprManagerMapCollection& variableMap) override;
 970   Command* clone() const override;
 971   std::string getCommandName() const override;
 972 }; /* class GetOptionCommand */
 973
 974 // Set expression name command
 975 // Note this is not an official smt2 command
 976 // Conceptually:
 977 //   (assert (! expr :named name))
 978 // is converted to
 979 //   (assert expr)
 980 //   (set-expr-name expr name)
 981 class CVC4_PUBLIC SetExpressionNameCommand : public Command
 982 {
 983  protected:
 984   Expr d_expr;
 985   std::string d_name;
 986
 987  public:
 988   SetExpressionNameCommand(Expr expr, std::string name);
 989
 990   void invoke(SmtEngine* smtEngine) override;
 991   Command* exportTo(ExprManager* exprManager,
 992                     ExprManagerMapCollection& variableMap) override;
 993   Command* clone() const override;
 994   std::string getCommandName() const override;
 995 }; /* class SetExpressionNameCommand */
 996
 997 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
 998 {
 999  private:
1000   std::vector<DatatypeType> d_datatypes;
1001
1002  public:
1003   DatatypeDeclarationCommand(const DatatypeType& datatype);
1004
1005   DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes);
1006   const std::vector<DatatypeType>& getDatatypes() const;
1007   void invoke(SmtEngine* smtEngine) override;
1008   Command* exportTo(ExprManager* exprManager,
1009                     ExprManagerMapCollection& variableMap) override;
1010   Command* clone() const override;
1011   std::string getCommandName() const override;
1012 }; /* class DatatypeDeclarationCommand */
1013
1014 class CVC4_PUBLIC RewriteRuleCommand : public Command
1015 {
1016  public:
1017   typedef std::vector<std::vector<Expr> > Triggers;
1018
1019  protected:
1020   typedef std::vector<Expr> VExpr;
1021   VExpr d_vars;
1022   VExpr d_guards;
1023   Expr d_head;
1024   Expr d_body;
1025   Triggers d_triggers;
1026
1027  public:
1028   RewriteRuleCommand(const std::vector<Expr>& vars,
1029                      const std::vector<Expr>& guards,
1030                      Expr head,
1031                      Expr body,
1032                      const Triggers& d_triggers);
1033   RewriteRuleCommand(const std::vector<Expr>& vars, Expr head, Expr body);
1034
1035   const std::vector<Expr>& getVars() const;
1036   const std::vector<Expr>& getGuards() const;
1037   Expr getHead() const;
1038   Expr getBody() const;
1039   const Triggers& getTriggers() const;
1040
1041   void invoke(SmtEngine* smtEngine) override;
1042   Command* exportTo(ExprManager* exprManager,
1043                     ExprManagerMapCollection& variableMap) override;
1044   Command* clone() const override;
1045   std::string getCommandName() const override;
1046 }; /* class RewriteRuleCommand */
1047
1048 class CVC4_PUBLIC PropagateRuleCommand : public Command
1049 {
1050  public:
1051   typedef std::vector<std::vector<Expr> > Triggers;
1052
1053  protected:
1054   typedef std::vector<Expr> VExpr;
1055   VExpr d_vars;
1056   VExpr d_guards;
1057   VExpr d_heads;
1058   Expr d_body;
1059   Triggers d_triggers;
1060   bool d_deduction;
1061
1062  public:
1063   PropagateRuleCommand(const std::vector<Expr>& vars,
1064                        const std::vector<Expr>& guards,
1065                        const std::vector<Expr>& heads,
1066                        Expr body,
1067                        const Triggers& d_triggers,
1068                        /* true if we want a deduction rule */
1069                        bool d_deduction = false);
1070   PropagateRuleCommand(const std::vector<Expr>& vars,
1071                        const std::vector<Expr>& heads,
1072                        Expr body,
1073                        bool d_deduction = false);
1074
1075   const std::vector<Expr>& getVars() const;
1076   const std::vector<Expr>& getGuards() const;
1077   const std::vector<Expr>& getHeads() const;
1078   Expr getBody() const;
1079   const Triggers& getTriggers() const;
1080   bool isDeduction() const;
1081   void invoke(SmtEngine* smtEngine) override;
1082   Command* exportTo(ExprManager* exprManager,
1083                     ExprManagerMapCollection& variableMap) override;
1084   Command* clone() const override;
1085   std::string getCommandName() const override;
1086 }; /* class PropagateRuleCommand */
1087
1088 class CVC4_PUBLIC ResetCommand : public Command
1089 {
1090  public:
1091   ResetCommand() {}
1092   void invoke(SmtEngine* smtEngine) override;
1093   Command* exportTo(ExprManager* exprManager,
1094                     ExprManagerMapCollection& variableMap) override;
1095   Command* clone() const override;
1096   std::string getCommandName() const override;
1097 }; /* class ResetCommand */
1098
1099 class CVC4_PUBLIC ResetAssertionsCommand : public Command
1100 {
1101  public:
1102   ResetAssertionsCommand() {}
1103   void invoke(SmtEngine* smtEngine) override;
1104   Command* exportTo(ExprManager* exprManager,
1105                     ExprManagerMapCollection& variableMap) override;
1106   Command* clone() const override;
1107   std::string getCommandName() const override;
1108 }; /* class ResetAssertionsCommand */
1109
1110 class CVC4_PUBLIC QuitCommand : public Command
1111 {
1112  public:
1113   QuitCommand() {}
1114   void invoke(SmtEngine* smtEngine) override;
1115   Command* exportTo(ExprManager* exprManager,
1116                     ExprManagerMapCollection& variableMap) override;
1117   Command* clone() const override;
1118   std::string getCommandName() const override;
1119 }; /* class QuitCommand */
1120
1121 class CVC4_PUBLIC CommentCommand : public Command
1122 {
1123   std::string d_comment;
1124
1125  public:
1126   CommentCommand(std::string comment);
1127
1128   std::string getComment() const;
1129
1130   void invoke(SmtEngine* smtEngine) override;
1131   Command* exportTo(ExprManager* exprManager,
1132                     ExprManagerMapCollection& variableMap) override;
1133   Command* clone() const override;
1134   std::string getCommandName() const override;
1135 }; /* class CommentCommand */
1136
1137 class CVC4_PUBLIC CommandSequence : public Command
1138 {
1139  private:
1140   /** All the commands to be executed (in sequence) */
1141   std::vector<Command*> d_commandSequence;
1142   /** Next command to be executed */
1143   unsigned int d_index;
1144
1145  public:
1146   CommandSequence();
1147   ~CommandSequence();
1148
1149   void addCommand(Command* cmd);
1150   void clear();
1151
1152   void invoke(SmtEngine* smtEngine) override;
1153   void invoke(SmtEngine* smtEngine, std::ostream& out) override;
1154
1155   typedef std::vector<Command*>::iterator iterator;
1156   typedef std::vector<Command*>::const_iterator const_iterator;
1157
1158   const_iterator begin() const;
1159   const_iterator end() const;
1160
1161   iterator begin();
1162   iterator end();
1163
1164   Command* exportTo(ExprManager* exprManager,
1165                     ExprManagerMapCollection& variableMap) override;
1166   Command* clone() const override;
1167   std::string getCommandName() const override;
1168 }; /* class CommandSequence */
1169
1170 class CVC4_PUBLIC DeclarationSequence : public CommandSequence
1171 {
1172 };
1173
1174 } /* CVC4 namespace */
1175
1176 #endif /* __CVC4__COMMAND_H */