cvc4-1.4
command.h
Go to the documentation of this file.
1 /********************* */
20 #include "cvc4_public.h"
21 
22 #ifndef __CVC4__COMMAND_H
23 #define __CVC4__COMMAND_H
24 
25 #include <iostream>
26 #include <sstream>
27 #include <string>
28 #include <vector>
29 #include <map>
30 
31 #include "expr/expr.h"
32 #include "expr/type.h"
33 #include "expr/variable_type_map.h"
34 #include "util/result.h"
35 #include "util/sexpr.h"
36 #include "util/datatype.h"
37 #include "util/proof.h"
38 
39 namespace CVC4 {
40 
41 class SmtEngine;
42 class Command;
43 class CommandStatus;
44 class Model;
45 
46 std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC;
47 std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
48 std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
49 std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC;
50 
59 };/* enum BenchmarkStatus */
60 
61 std::ostream& operator<<(std::ostream& out,
62  BenchmarkStatus status) throw() CVC4_PUBLIC;
63 
80  static const int s_iosIndex;
81 
86  static const int s_defaultPrintSuccess = false;
87 
91  bool d_printSuccess;
92 
93 public:
97  CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {}
98 
99  inline void applyPrintSuccess(std::ostream& out) throw() {
100  out.iword(s_iosIndex) = d_printSuccess;
101  }
102 
103  static inline bool getPrintSuccess(std::ostream& out) throw() {
104  return out.iword(s_iosIndex);
105  }
106 
107  static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() {
108  out.iword(s_iosIndex) = printSuccess;
109  }
110 
117  class Scope {
118  std::ostream& d_out;
119  bool d_oldPrintSuccess;
120 
121  public:
122 
123  inline Scope(std::ostream& out, bool printSuccess) throw() :
124  d_out(out),
125  d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) {
127  }
128 
129  inline ~Scope() throw() {
130  CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess);
131  }
132 
133  };/* class CommandPrintSuccess::Scope */
134 
135 };/* class CommandPrintSuccess */
136 
146 inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC;
147 inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() {
148  cps.applyPrintSuccess(out);
149  return out;
150 }
151 
153 protected:
154  // shouldn't construct a CommandStatus (use a derived class)
155  CommandStatus() throw() {}
156 public:
157  virtual ~CommandStatus() throw() {}
158  void toStream(std::ostream& out,
159  OutputLanguage language = language::output::LANG_AUTO) const throw();
160  virtual CommandStatus& clone() const = 0;
161 };/* class CommandStatus */
162 
164  static const CommandSuccess* s_instance;
165 public:
166  static const CommandSuccess* instance() throw() { return s_instance; }
167  CommandStatus& clone() const { return const_cast<CommandSuccess&>(*this); }
168 };/* class CommandSuccess */
169 
171 public:
172  CommandStatus& clone() const { return *new CommandUnsupported(*this); }
173 };/* class CommandSuccess */
174 
176  std::string d_message;
177 public:
178  CommandFailure(std::string message) throw() : d_message(message) {}
179  CommandFailure& clone() const { return *new CommandFailure(*this); }
180  ~CommandFailure() throw() {}
181  std::string getMessage() const throw() { return d_message; }
182 };/* class CommandFailure */
183 
185 protected:
195 
200  bool d_muted;
201 
202 public:
204 
205  Command() throw();
206  Command(const Command& cmd);
207 
208  virtual ~Command() throw();
209 
210  virtual void invoke(SmtEngine* smtEngine) throw() = 0;
211  virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
212 
213  virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
214  OutputLanguage language = language::output::LANG_AUTO) const throw();
215 
216  std::string toString() const throw();
217 
218  virtual std::string getCommandName() const throw() = 0;
219 
223  void setMuted(bool muted) throw() { d_muted = muted; }
224 
228  bool isMuted() throw() { return d_muted; }
229 
234  bool ok() const throw();
235 
240  bool fail() const throw();
241 
243  const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
244 
245  virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
246 
252  virtual Command* exportTo(ExprManager* exprManager,
253  ExprManagerMapCollection& variableMap) = 0;
254 
258  virtual Command* clone() const = 0;
259 
260 protected:
262  ExprManager* d_exprManager;
263  ExprManagerMapCollection& d_variableMap;
264  public:
266  d_exprManager(exprManager),
267  d_variableMap(variableMap) {
268  }
270  return e.exportTo(d_exprManager, d_variableMap);
271  }
273  return t.exportTo(d_exprManager, d_variableMap);
274  }
275  };/* class Command::ExportTransformer */
276 };/* class Command */
277 
283 protected:
284  std::string d_name;
285 public:
286  EmptyCommand(std::string name = "") throw();
287  ~EmptyCommand() throw() {}
288  std::string getName() const throw();
289  void invoke(SmtEngine* smtEngine) throw();
290  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
291  Command* clone() const;
292  std::string getCommandName() const throw();
293 };/* class EmptyCommand */
294 
296 protected:
297  std::string d_output;
298 public:
299  EchoCommand(std::string output = "") throw();
300  ~EchoCommand() throw() {}
301  std::string getOutput() const throw();
302  void invoke(SmtEngine* smtEngine) throw();
303  void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
304  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
305  Command* clone() const;
306  std::string getCommandName() const throw();
307 };/* class EchoCommand */
308 
310 protected:
312 public:
313  AssertCommand(const Expr& e) throw();
314  ~AssertCommand() throw() {}
315  Expr getExpr() const throw();
316  void invoke(SmtEngine* smtEngine) throw();
317  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
318  Command* clone() const;
319  std::string getCommandName() const throw();
320 };/* class AssertCommand */
321 
323 public:
324  ~PushCommand() throw() {}
325  void invoke(SmtEngine* smtEngine) throw();
326  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
327  Command* clone() const;
328  std::string getCommandName() const throw();
329 };/* class PushCommand */
330 
332 public:
333  ~PopCommand() throw() {}
334  void invoke(SmtEngine* smtEngine) throw();
335  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
336  Command* clone() const;
337  std::string getCommandName() const throw();
338 };/* class PopCommand */
339 
341 protected:
342  std::string d_symbol;
343 public:
344  DeclarationDefinitionCommand(const std::string& id) throw();
346  virtual void invoke(SmtEngine* smtEngine) throw() = 0;
347  std::string getSymbol() const throw();
348 };/* class DeclarationDefinitionCommand */
349 
351 protected:
356 public:
357  DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw();
359  Expr getFunction() const throw();
360  Type getType() const throw();
361  bool getPrintInModel() const throw();
362  bool getPrintInModelSetByUser() const throw();
363  void setPrintInModel( bool p );
364  void invoke(SmtEngine* smtEngine) throw();
365  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
366  Command* clone() const;
367  std::string getCommandName() const throw();
368 };/* class DeclareFunctionCommand */
369 
371 protected:
372  size_t d_arity;
374 public:
375  DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw();
376  ~DeclareTypeCommand() throw() {}
377  size_t getArity() const throw();
378  Type getType() const throw();
379  void invoke(SmtEngine* smtEngine) throw();
380  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
381  Command* clone() const;
382  std::string getCommandName() const throw();
383 };/* class DeclareTypeCommand */
384 
386 protected:
387  std::vector<Type> d_params;
389 public:
390  DefineTypeCommand(const std::string& id, Type t) throw();
391  DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw();
392  ~DefineTypeCommand() throw() {}
393  const std::vector<Type>& getParameters() const throw();
394  Type getType() const throw();
395  void invoke(SmtEngine* smtEngine) throw();
396  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
397  Command* clone() const;
398  std::string getCommandName() const throw();
399 };/* class DefineTypeCommand */
400 
402 protected:
404  std::vector<Expr> d_formals;
406 public:
407  DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw();
408  DefineFunctionCommand(const std::string& id, Expr func,
409  const std::vector<Expr>& formals, Expr formula) throw();
411  Expr getFunction() const throw();
412  const std::vector<Expr>& getFormals() const throw();
413  Expr getFormula() const throw();
414  void invoke(SmtEngine* smtEngine) throw();
415  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
416  Command* clone() const;
417  std::string getCommandName() const throw();
418 };/* class DefineFunctionCommand */
419 
426 public:
427  DefineNamedFunctionCommand(const std::string& id, Expr func,
428  const std::vector<Expr>& formals, Expr formula) throw();
429  void invoke(SmtEngine* smtEngine) throw();
430  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
431  Command* clone() const;
432 };/* class DefineNamedFunctionCommand */
433 
439 protected:
440  std::string d_attr;
442  //std::vector<Expr> d_expr_values;
443  //std::string d_str_value;
444 public:
445  SetUserAttributeCommand( const std::string& attr, Expr expr ) throw();
446  //SetUserAttributeCommand( const std::string& id, Expr expr, std::vector<Expr>& values ) throw();
447  //SetUserAttributeCommand( const std::string& id, Expr expr, std::string& value ) throw();
449  void invoke(SmtEngine* smtEngine) throw();
450  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
451  Command* clone() const;
452  std::string getCommandName() const throw();
453 };/* class SetUserAttributeCommand */
454 
455 
457 protected:
460 public:
461  CheckSatCommand() throw();
462  CheckSatCommand(const Expr& expr) throw();
463  ~CheckSatCommand() throw() {}
464  Expr getExpr() const throw();
465  void invoke(SmtEngine* smtEngine) throw();
466  Result getResult() const throw();
467  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
468  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
469  Command* clone() const;
470  std::string getCommandName() const throw();
471 };/* class CheckSatCommand */
472 
474 protected:
477 public:
478  QueryCommand(const Expr& e) throw();
479  ~QueryCommand() throw() {}
480  Expr getExpr() const throw();
481  void invoke(SmtEngine* smtEngine) throw();
482  Result getResult() const throw();
483  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
484  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
485  Command* clone() const;
486  std::string getCommandName() const throw();
487 };/* class QueryCommand */
488 
489 // this is TRANSFORM in the CVC presentation language
491 protected:
494 public:
495  SimplifyCommand(Expr term) throw();
496  ~SimplifyCommand() throw() {}
497  Expr getTerm() const throw();
498  void invoke(SmtEngine* smtEngine) throw();
499  Expr getResult() const throw();
500  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
501  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
502  Command* clone() const;
503  std::string getCommandName() const throw();
504 };/* class SimplifyCommand */
505 
507 protected:
510 public:
511  ExpandDefinitionsCommand(Expr term) throw();
513  Expr getTerm() const throw();
514  void invoke(SmtEngine* smtEngine) throw();
515  Expr getResult() const throw();
516  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
517  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
518  Command* clone() const;
519  std::string getCommandName() const throw();
520 };/* class ExpandDefinitionsCommand */
521 
523 protected:
524  std::vector<Expr> d_terms;
526 public:
527  GetValueCommand(Expr term) throw();
528  GetValueCommand(const std::vector<Expr>& terms) throw();
529  ~GetValueCommand() throw() {}
530  const std::vector<Expr>& getTerms() const throw();
531  void invoke(SmtEngine* smtEngine) throw();
532  Expr getResult() const throw();
533  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
534  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
535  Command* clone() const;
536  std::string getCommandName() const throw();
537 };/* class GetValueCommand */
538 
540 protected:
542 public:
543  GetAssignmentCommand() throw();
544  ~GetAssignmentCommand() throw() {}
545  void invoke(SmtEngine* smtEngine) throw();
546  SExpr getResult() const throw();
547  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
548  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
549  Command* clone() const;
550  std::string getCommandName() const throw();
551 };/* class GetAssignmentCommand */
552 
554 protected:
555  Model* d_result;
557 public:
558  GetModelCommand() throw();
559  ~GetModelCommand() throw() {}
560  void invoke(SmtEngine* smtEngine) throw();
561  // Model is private to the library -- for now
562  //Model* getResult() const throw();
563  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
564  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
565  Command* clone() const;
566  std::string getCommandName() const throw();
567 };/* class GetModelCommand */
568 
570 protected:
572 public:
573  GetProofCommand() throw();
574  ~GetProofCommand() throw() {}
575  void invoke(SmtEngine* smtEngine) throw();
576  Proof* getResult() const throw();
577  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
578  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
579  Command* clone() const;
580  std::string getCommandName() const throw();
581 };/* class GetProofCommand */
582 
584 protected:
585  //Instantiations* d_result;
587 public:
588  GetInstantiationsCommand() throw();
590  void invoke(SmtEngine* smtEngine) throw();
591  //Instantiations* getResult() const throw();
592  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
593  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
594  Command* clone() const;
595  std::string getCommandName() const throw();
596 };/* class GetInstantiationsCommand */
597 
599 protected:
600  //UnsatCore* d_result;
601 public:
602  GetUnsatCoreCommand() throw();
603  ~GetUnsatCoreCommand() throw() {}
604  void invoke(SmtEngine* smtEngine) throw();
605  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
606  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
607  Command* clone() const;
608  std::string getCommandName() const throw();
609 };/* class GetUnsatCoreCommand */
610 
612 protected:
613  std::string d_result;
614 public:
615  GetAssertionsCommand() throw();
616  ~GetAssertionsCommand() throw() {}
617  void invoke(SmtEngine* smtEngine) throw();
618  std::string getResult() const throw();
619  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
620  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
621  Command* clone() const;
622  std::string getCommandName() const throw();
623 };/* class GetAssertionsCommand */
624 
626 protected:
628 public:
631  BenchmarkStatus getStatus() const throw();
632  void invoke(SmtEngine* smtEngine) throw();
633  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
634  Command* clone() const;
635  std::string getCommandName() const throw();
636 };/* class SetBenchmarkStatusCommand */
637 
639 protected:
640  std::string d_logic;
641 public:
642  SetBenchmarkLogicCommand(std::string logic) throw();
644  std::string getLogic() const throw();
645  void invoke(SmtEngine* smtEngine) throw();
646  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
647  Command* clone() const;
648  std::string getCommandName() const throw();
649 };/* class SetBenchmarkLogicCommand */
650 
652 protected:
653  std::string d_flag;
655 public:
656  SetInfoCommand(std::string flag, const SExpr& sexpr) throw();
657  ~SetInfoCommand() throw() {}
658  std::string getFlag() const throw();
659  SExpr getSExpr() const throw();
660  void invoke(SmtEngine* smtEngine) throw();
661  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
662  Command* clone() const;
663  std::string getCommandName() const throw();
664 };/* class SetInfoCommand */
665 
667 protected:
668  std::string d_flag;
669  std::string d_result;
670 public:
671  GetInfoCommand(std::string flag) throw();
672  ~GetInfoCommand() throw() {}
673  std::string getFlag() const throw();
674  void invoke(SmtEngine* smtEngine) throw();
675  std::string getResult() const throw();
676  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
677  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
678  Command* clone() const;
679  std::string getCommandName() const throw();
680 };/* class GetInfoCommand */
681 
683 protected:
684  std::string d_flag;
686 public:
687  SetOptionCommand(std::string flag, const SExpr& sexpr) throw();
688  ~SetOptionCommand() throw() {}
689  std::string getFlag() const throw();
690  SExpr getSExpr() const throw();
691  void invoke(SmtEngine* smtEngine) throw();
692  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
693  Command* clone() const;
694  std::string getCommandName() const throw();
695 };/* class SetOptionCommand */
696 
698 protected:
699  std::string d_flag;
700  std::string d_result;
701 public:
702  GetOptionCommand(std::string flag) throw();
703  ~GetOptionCommand() throw() {}
704  std::string getFlag() const throw();
705  void invoke(SmtEngine* smtEngine) throw();
706  std::string getResult() const throw();
707  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
708  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
709  Command* clone() const;
710  std::string getCommandName() const throw();
711 };/* class GetOptionCommand */
712 
714 private:
715  std::vector<DatatypeType> d_datatypes;
716 public:
717  DatatypeDeclarationCommand(const DatatypeType& datatype) throw();
719  DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
720  const std::vector<DatatypeType>& getDatatypes() const throw();
721  void invoke(SmtEngine* smtEngine) throw();
722  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
723  Command* clone() const;
724  std::string getCommandName() const throw();
725 };/* class DatatypeDeclarationCommand */
726 
728 public:
729  typedef std::vector< std::vector< Expr > > Triggers;
730 protected:
731  typedef std::vector< Expr > VExpr;
732  VExpr d_vars;
733  VExpr d_guards;
736  Triggers d_triggers;
737 public:
738  RewriteRuleCommand(const std::vector<Expr>& vars,
739  const std::vector<Expr>& guards,
740  Expr head,
741  Expr body,
742  const Triggers& d_triggers) throw();
743  RewriteRuleCommand(const std::vector<Expr>& vars,
744  Expr head,
745  Expr body) throw();
746  ~RewriteRuleCommand() throw() {}
747  const std::vector<Expr>& getVars() const throw();
748  const std::vector<Expr>& getGuards() const throw();
749  Expr getHead() const throw();
750  Expr getBody() const throw();
751  const Triggers& getTriggers() const throw();
752  void invoke(SmtEngine* smtEngine) throw();
753  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
754  Command* clone() const;
755  std::string getCommandName() const throw();
756 };/* class RewriteRuleCommand */
757 
759 public:
760  typedef std::vector< std::vector< Expr > > Triggers;
761 protected:
762  typedef std::vector< Expr > VExpr;
763  VExpr d_vars;
764  VExpr d_guards;
765  VExpr d_heads;
767  Triggers d_triggers;
769 public:
770  PropagateRuleCommand(const std::vector<Expr>& vars,
771  const std::vector<Expr>& guards,
772  const std::vector<Expr>& heads,
773  Expr body,
774  const Triggers& d_triggers,
775  /* true if we want a deduction rule */
776  bool d_deduction = false) throw();
777  PropagateRuleCommand(const std::vector<Expr>& vars,
778  const std::vector<Expr>& heads,
779  Expr body,
780  bool d_deduction = false) throw();
781  ~PropagateRuleCommand() throw() {}
782  const std::vector<Expr>& getVars() const throw();
783  const std::vector<Expr>& getGuards() const throw();
784  const std::vector<Expr>& getHeads() const throw();
785  Expr getBody() const throw();
786  const Triggers& getTriggers() const throw();
787  bool isDeduction() const throw();
788  void invoke(SmtEngine* smtEngine) throw();
789  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
790  Command* clone() const;
791  std::string getCommandName() const throw();
792 };/* class PropagateRuleCommand */
793 
794 
796 public:
797  QuitCommand() throw();
798  ~QuitCommand() throw() {}
799  void invoke(SmtEngine* smtEngine) throw();
800  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
801  Command* clone() const;
802  std::string getCommandName() const throw();
803 };/* class QuitCommand */
804 
806  std::string d_comment;
807 public:
808  CommentCommand(std::string comment) throw();
809  ~CommentCommand() throw() {}
810  std::string getComment() const throw();
811  void invoke(SmtEngine* smtEngine) throw();
812  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
813  Command* clone() const;
814  std::string getCommandName() const throw();
815 };/* class CommentCommand */
816 
818 private:
820  std::vector<Command*> d_commandSequence;
822  unsigned int d_index;
823 public:
824  CommandSequence() throw();
825  ~CommandSequence() throw();
826 
827  void addCommand(Command* cmd) throw();
828  void clear() throw();
829 
830  void invoke(SmtEngine* smtEngine) throw();
831  void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
832 
833  typedef std::vector<Command*>::iterator iterator;
834  typedef std::vector<Command*>::const_iterator const_iterator;
835 
836  const_iterator begin() const throw();
837  const_iterator end() const throw();
838 
839  iterator begin() throw();
840  iterator end() throw();
841 
842  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
843  Command* clone() const;
844  std::string getCommandName() const throw();
845 };/* class CommandSequence */
846 
848 public:
849  ~DeclarationSequence() throw() {}
850 };/* class DeclarationSequence */
851 
852 }/* CVC4 namespace */
853 
854 #endif /* __CVC4__COMMAND_H */
std::vector< Expr > VExpr
Definition: command.h:762
A class representing a Datatype definition.
Expr exportTo(ExprManager *exprManager, ExprManagerMapCollection &variableMap, uint32_t flags=0) const
Maps this Expr into one for a different ExprManager, using variableMap for the translation and extend...
CommandStatus & clone() const
Definition: command.h:172
Scope(std::ostream &out, bool printSuccess)
Definition: command.h:123
Set the print-success state on the output stream for the current stack scope.
Definition: command.h:117
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
std::vector< Expr > d_formals
Definition: command.h:404
[[ Add one-line brief description here ]]
struct CVC4::options::printSuccess__option_t printSuccess
std::vector< Expr > d_terms
Definition: command.h:524
bool isMuted()
Determine whether this Command will print a success message.
Definition: command.h:228
std::vector< Expr > VExpr
Definition: command.h:731
std::string d_result
Definition: command.h:669
std::string d_output
Definition: command.h:297
Benchmark is satisfiable.
Definition: command.h:54
void applyPrintSuccess(std::ostream &out)
Definition: command.h:99
The command when an attribute is set by a user.
Definition: command.h:438
Class encapsulating CVC4 expression types.
Definition: type.h:89
STL namespace.
Simple representation of S-expressions.
const CommandStatus * d_commandStatus
This field contains a command status if the command has been invoked, or NULL if it has not...
Definition: command.h:194
std::vector< std::vector< Expr > > Triggers
Definition: command.h:760
struct CVC4::options::verbosity__option_t verbosity
std::string d_name
Definition: command.h:284
Type exportTo(ExprManager *exprManager, ExprManagerMapCollection &vmap) const
Exports this type into a different ExprManager.
std::string d_flag
Definition: command.h:699
static const CommandSuccess * instance()
Definition: command.h:166
std::vector< Command * >::iterator iterator
Definition: command.h:833
static bool getPrintSuccess(std::ostream &out)
Definition: command.h:103
Encapsulation of the result of a query.
Match the output language to the input language.
Definition: language.h:99
Auto-detect the language.
Definition: language.h:37
bool d_muted
True if this command is "muted"—i.e., don&#39;t print "success" on successful execution.
Definition: command.h:200
const CommandStatus * getCommandStatus() const
Get the command status (it&#39;s NULL if we haven&#39;t run yet).
Definition: command.h:243
CommandPrintSuccess printsuccess
Definition: command.h:203
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
IOStream manipulator to print success messages or not.
Definition: command.h:76
std::string d_flag
Definition: command.h:653
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Definition: kind.h:568
The status of the benchmark is unknown.
Definition: command.h:58
This differs from DefineFunctionCommand only in that it instructs the SmtEngine to "remember" this fu...
Definition: command.h:425
virtual ~CommandStatus()
Definition: command.h:157
Class encapsulating the datatype type.
Definition: type.h:615
CommandPrintSuccess(bool printSuccess)
Construct a CommandPrintSuccess with the given setting.
Definition: command.h:97
Macros that should be defined everywhere during the building of the libraries and driver binary...
Three-valued SMT result, with optional explanation.
Definition: result.h:36
SmtEngine * d_smtEngine
Definition: command.h:556
EmptyCommands are the residue of a command after the parser handles them (and there&#39;s nothing left to...
Definition: command.h:282
std::string getMessage() const
Definition: command.h:181
BenchmarkStatus
The status an SMT benchmark can have.
Definition: command.h:52
Benchmark is unsatisfiable.
Definition: command.h:56
struct CVC4::options::out__option_t out
[[ Add one-line brief description here ]]
expr.h
CommandFailure & clone() const
Definition: command.h:179
CommandFailure(std::string message)
Definition: command.h:178
A simple S-expression.
Definition: sexpr.h:51
std::vector< Type > d_params
Definition: command.h:387
CommandStatus & clone() const
Definition: command.h:167
std::vector< std::vector< Expr > > Triggers
Definition: command.h:729
static void setPrintSuccess(std::ostream &out, bool printSuccess)
Definition: command.h:107
std::string d_result
Definition: command.h:700
std::string d_flag
Definition: command.h:684
std::string d_flag
Definition: command.h:668
BenchmarkStatus d_status
Definition: command.h:627
Interface for expression types.
ExportTransformer(ExprManager *exprManager, ExprManagerMapCollection &variableMap)
Definition: command.h:265
std::vector< Command * >::const_iterator const_iterator
Definition: command.h:834