cvc4-1.3
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_AST) 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_AST) 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 
309 class CVC4_PUBLIC AssertCommand : public Command {
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 
322 class CVC4_PUBLIC PushCommand : public Command {
323 public:
324  ~PushCommand() throw() {}
325  void invoke(SmtEngine* smtEngine) throw();
326  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
327  Command* clone() const;
328  std::string getCommandName() const throw();
329 };/* class PushCommand */
330 
331 class CVC4_PUBLIC PopCommand : public Command {
332 public:
333  ~PopCommand() throw() {}
334  void invoke(SmtEngine* smtEngine) throw();
335  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
336  Command* clone() const;
337  std::string getCommandName() const throw();
338 };/* class PopCommand */
339 
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:
354 public:
355  DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw();
357  Expr getFunction() const throw();
358  Type getType() const throw();
359  void invoke(SmtEngine* smtEngine) throw();
360  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
361  Command* clone() const;
362  std::string getCommandName() const throw();
363 };/* class DeclareFunctionCommand */
364 
365 class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
366 protected:
367  size_t d_arity;
369 public:
370  DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw();
371  ~DeclareTypeCommand() throw() {}
372  size_t getArity() const throw();
373  Type getType() const throw();
374  void invoke(SmtEngine* smtEngine) throw();
375  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
376  Command* clone() const;
377  std::string getCommandName() const throw();
378 };/* class DeclareTypeCommand */
379 
380 class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
381 protected:
382  std::vector<Type> d_params;
384 public:
385  DefineTypeCommand(const std::string& id, Type t) throw();
386  DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw();
387  ~DefineTypeCommand() throw() {}
388  const std::vector<Type>& getParameters() const throw();
389  Type getType() const throw();
390  void invoke(SmtEngine* smtEngine) throw();
391  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
392  Command* clone() const;
393  std::string getCommandName() const throw();
394 };/* class DefineTypeCommand */
395 
396 class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
397 protected:
399  std::vector<Expr> d_formals;
401 public:
402  DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw();
403  DefineFunctionCommand(const std::string& id, Expr func,
404  const std::vector<Expr>& formals, Expr formula) throw();
406  Expr getFunction() const throw();
407  const std::vector<Expr>& getFormals() const throw();
408  Expr getFormula() const throw();
409  void invoke(SmtEngine* smtEngine) throw();
410  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
411  Command* clone() const;
412  std::string getCommandName() const throw();
413 };/* class DefineFunctionCommand */
414 
421 public:
422  DefineNamedFunctionCommand(const std::string& id, Expr func,
423  const std::vector<Expr>& formals, Expr formula) throw();
424  void invoke(SmtEngine* smtEngine) throw();
425  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
426  Command* clone() const;
427 };/* class DefineNamedFunctionCommand */
428 
433 class CVC4_PUBLIC SetUserAttributeCommand : public Command {
434 protected:
435  std::string d_attr;
437  //std::vector<Expr> d_expr_values;
438  //std::string d_str_value;
439 public:
440  SetUserAttributeCommand( const std::string& attr, Expr expr ) throw();
441  //SetUserAttributeCommand( const std::string& id, Expr expr, std::vector<Expr>& values ) throw();
442  //SetUserAttributeCommand( const std::string& id, Expr expr, std::string& value ) throw();
444  void invoke(SmtEngine* smtEngine) throw();
445  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
446  Command* clone() const;
447  std::string getCommandName() const throw();
448 };/* class SetUserAttributeCommand */
449 
450 
451 class CVC4_PUBLIC CheckSatCommand : public Command {
452 protected:
455 public:
456  CheckSatCommand() throw();
457  CheckSatCommand(const Expr& expr) throw();
458  ~CheckSatCommand() throw() {}
459  Expr getExpr() const throw();
460  void invoke(SmtEngine* smtEngine) throw();
461  Result getResult() const throw();
462  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
463  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
464  Command* clone() const;
465  std::string getCommandName() const throw();
466 };/* class CheckSatCommand */
467 
468 class CVC4_PUBLIC QueryCommand : public Command {
469 protected:
472 public:
473  QueryCommand(const Expr& e) throw();
474  ~QueryCommand() throw() {}
475  Expr getExpr() const throw();
476  void invoke(SmtEngine* smtEngine) throw();
477  Result getResult() const throw();
478  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
479  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
480  Command* clone() const;
481  std::string getCommandName() const throw();
482 };/* class QueryCommand */
483 
484 // this is TRANSFORM in the CVC presentation language
485 class CVC4_PUBLIC SimplifyCommand : public Command {
486 protected:
489 public:
490  SimplifyCommand(Expr term) throw();
491  ~SimplifyCommand() throw() {}
492  Expr getTerm() const throw();
493  void invoke(SmtEngine* smtEngine) throw();
494  Expr getResult() const throw();
495  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
496  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
497  Command* clone() const;
498  std::string getCommandName() const throw();
499 };/* class SimplifyCommand */
500 
501 class CVC4_PUBLIC ExpandDefinitionsCommand : public Command {
502 protected:
505 public:
506  ExpandDefinitionsCommand(Expr term) throw();
508  Expr getTerm() const throw();
509  void invoke(SmtEngine* smtEngine) throw();
510  Expr getResult() const throw();
511  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
512  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
513  Command* clone() const;
514  std::string getCommandName() const throw();
515 };/* class ExpandDefinitionsCommand */
516 
517 class CVC4_PUBLIC GetValueCommand : public Command {
518 protected:
519  std::vector<Expr> d_terms;
521 public:
522  GetValueCommand(Expr term) throw();
523  GetValueCommand(const std::vector<Expr>& terms) throw();
524  ~GetValueCommand() throw() {}
525  const std::vector<Expr>& getTerms() const throw();
526  void invoke(SmtEngine* smtEngine) throw();
527  Expr getResult() const throw();
528  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
529  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
530  Command* clone() const;
531  std::string getCommandName() const throw();
532 };/* class GetValueCommand */
533 
534 class CVC4_PUBLIC GetAssignmentCommand : public Command {
535 protected:
537 public:
538  GetAssignmentCommand() throw();
539  ~GetAssignmentCommand() throw() {}
540  void invoke(SmtEngine* smtEngine) throw();
541  SExpr getResult() const throw();
542  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
543  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
544  Command* clone() const;
545  std::string getCommandName() const throw();
546 };/* class GetAssignmentCommand */
547 
548 class CVC4_PUBLIC GetModelCommand : public Command {
549 protected:
550  Model* d_result;
552 public:
553  GetModelCommand() throw();
554  ~GetModelCommand() throw() {}
555  void invoke(SmtEngine* smtEngine) throw();
556  // Model is private to the library -- for now
557  //Model* getResult() const throw();
558  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
559  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
560  Command* clone() const;
561  std::string getCommandName() const throw();
562 };/* class GetModelCommand */
563 
564 class CVC4_PUBLIC GetProofCommand : public Command {
565 protected:
567 public:
568  GetProofCommand() throw();
569  ~GetProofCommand() throw() {}
570  void invoke(SmtEngine* smtEngine) throw();
571  Proof* getResult() const throw();
572  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
573  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
574  Command* clone() const;
575  std::string getCommandName() const throw();
576 };/* class GetProofCommand */
577 
578 class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
579 protected:
580  //UnsatCore* d_result;
581 public:
582  GetUnsatCoreCommand() throw();
583  ~GetUnsatCoreCommand() throw() {}
584  void invoke(SmtEngine* smtEngine) throw();
585  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
586  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
587  Command* clone() const;
588  std::string getCommandName() const throw();
589 };/* class GetUnsatCoreCommand */
590 
591 class CVC4_PUBLIC GetAssertionsCommand : public Command {
592 protected:
593  std::string d_result;
594 public:
595  GetAssertionsCommand() throw();
596  ~GetAssertionsCommand() throw() {}
597  void invoke(SmtEngine* smtEngine) throw();
598  std::string getResult() const throw();
599  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
600  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
601  Command* clone() const;
602  std::string getCommandName() const throw();
603 };/* class GetAssertionsCommand */
604 
605 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
606 protected:
608 public:
611  BenchmarkStatus getStatus() const throw();
612  void invoke(SmtEngine* smtEngine) throw();
613  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
614  Command* clone() const;
615  std::string getCommandName() const throw();
616 };/* class SetBenchmarkStatusCommand */
617 
618 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
619 protected:
620  std::string d_logic;
621 public:
622  SetBenchmarkLogicCommand(std::string logic) throw();
624  std::string getLogic() const throw();
625  void invoke(SmtEngine* smtEngine) throw();
626  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
627  Command* clone() const;
628  std::string getCommandName() const throw();
629 };/* class SetBenchmarkLogicCommand */
630 
631 class CVC4_PUBLIC SetInfoCommand : public Command {
632 protected:
633  std::string d_flag;
635 public:
636  SetInfoCommand(std::string flag, const SExpr& sexpr) throw();
637  ~SetInfoCommand() throw() {}
638  std::string getFlag() const throw();
639  SExpr getSExpr() const throw();
640  void invoke(SmtEngine* smtEngine) throw();
641  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
642  Command* clone() const;
643  std::string getCommandName() const throw();
644 };/* class SetInfoCommand */
645 
646 class CVC4_PUBLIC GetInfoCommand : public Command {
647 protected:
648  std::string d_flag;
649  std::string d_result;
650 public:
651  GetInfoCommand(std::string flag) throw();
652  ~GetInfoCommand() throw() {}
653  std::string getFlag() const throw();
654  void invoke(SmtEngine* smtEngine) throw();
655  std::string getResult() const throw();
656  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
657  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
658  Command* clone() const;
659  std::string getCommandName() const throw();
660 };/* class GetInfoCommand */
661 
662 class CVC4_PUBLIC SetOptionCommand : public Command {
663 protected:
664  std::string d_flag;
666 public:
667  SetOptionCommand(std::string flag, const SExpr& sexpr) throw();
668  ~SetOptionCommand() throw() {}
669  std::string getFlag() const throw();
670  SExpr getSExpr() const throw();
671  void invoke(SmtEngine* smtEngine) throw();
672  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
673  Command* clone() const;
674  std::string getCommandName() const throw();
675 };/* class SetOptionCommand */
676 
677 class CVC4_PUBLIC GetOptionCommand : public Command {
678 protected:
679  std::string d_flag;
680  std::string d_result;
681 public:
682  GetOptionCommand(std::string flag) throw();
683  ~GetOptionCommand() throw() {}
684  std::string getFlag() const throw();
685  void invoke(SmtEngine* smtEngine) throw();
686  std::string getResult() const throw();
687  void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
688  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
689  Command* clone() const;
690  std::string getCommandName() const throw();
691 };/* class GetOptionCommand */
692 
693 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
694 private:
695  std::vector<DatatypeType> d_datatypes;
696 public:
697  DatatypeDeclarationCommand(const DatatypeType& datatype) throw();
699  DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
700  const std::vector<DatatypeType>& getDatatypes() const throw();
701  void invoke(SmtEngine* smtEngine) throw();
702  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
703  Command* clone() const;
704  std::string getCommandName() const throw();
705 };/* class DatatypeDeclarationCommand */
706 
707 class CVC4_PUBLIC RewriteRuleCommand : public Command {
708 public:
709  typedef std::vector< std::vector< Expr > > Triggers;
710 protected:
711  typedef std::vector< Expr > VExpr;
712  VExpr d_vars;
713  VExpr d_guards;
716  Triggers d_triggers;
717 public:
718  RewriteRuleCommand(const std::vector<Expr>& vars,
719  const std::vector<Expr>& guards,
720  Expr head,
721  Expr body,
722  const Triggers& d_triggers) throw();
723  RewriteRuleCommand(const std::vector<Expr>& vars,
724  Expr head,
725  Expr body) throw();
726  ~RewriteRuleCommand() throw() {}
727  const std::vector<Expr>& getVars() const throw();
728  const std::vector<Expr>& getGuards() const throw();
729  Expr getHead() const throw();
730  Expr getBody() const throw();
731  const Triggers& getTriggers() const throw();
732  void invoke(SmtEngine* smtEngine) throw();
733  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
734  Command* clone() const;
735  std::string getCommandName() const throw();
736 };/* class RewriteRuleCommand */
737 
738 class CVC4_PUBLIC PropagateRuleCommand : public Command {
739 public:
740  typedef std::vector< std::vector< Expr > > Triggers;
741 protected:
742  typedef std::vector< Expr > VExpr;
743  VExpr d_vars;
744  VExpr d_guards;
745  VExpr d_heads;
747  Triggers d_triggers;
749 public:
750  PropagateRuleCommand(const std::vector<Expr>& vars,
751  const std::vector<Expr>& guards,
752  const std::vector<Expr>& heads,
753  Expr body,
754  const Triggers& d_triggers,
755  /* true if we want a deduction rule */
756  bool d_deduction = false) throw();
757  PropagateRuleCommand(const std::vector<Expr>& vars,
758  const std::vector<Expr>& heads,
759  Expr body,
760  bool d_deduction = false) throw();
761  ~PropagateRuleCommand() throw() {}
762  const std::vector<Expr>& getVars() const throw();
763  const std::vector<Expr>& getGuards() const throw();
764  const std::vector<Expr>& getHeads() const throw();
765  Expr getBody() const throw();
766  const Triggers& getTriggers() const throw();
767  bool isDeduction() const throw();
768  void invoke(SmtEngine* smtEngine) throw();
769  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
770  Command* clone() const;
771  std::string getCommandName() const throw();
772 };/* class PropagateRuleCommand */
773 
774 
775 class CVC4_PUBLIC QuitCommand : public Command {
776 public:
777  QuitCommand() throw();
778  ~QuitCommand() throw() {}
779  void invoke(SmtEngine* smtEngine) throw();
780  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
781  Command* clone() const;
782  std::string getCommandName() const throw();
783 };/* class QuitCommand */
784 
785 class CVC4_PUBLIC CommentCommand : public Command {
786  std::string d_comment;
787 public:
788  CommentCommand(std::string comment) throw();
789  ~CommentCommand() throw() {}
790  std::string getComment() const throw();
791  void invoke(SmtEngine* smtEngine) throw();
792  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
793  Command* clone() const;
794  std::string getCommandName() const throw();
795 };/* class CommentCommand */
796 
797 class CVC4_PUBLIC CommandSequence : public Command {
798 private:
800  std::vector<Command*> d_commandSequence;
802  unsigned int d_index;
803 public:
804  CommandSequence() throw();
805  ~CommandSequence() throw();
806 
807  void addCommand(Command* cmd) throw();
808  void clear() throw();
809 
810  void invoke(SmtEngine* smtEngine) throw();
811  void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
812 
813  typedef std::vector<Command*>::iterator iterator;
814  typedef std::vector<Command*>::const_iterator const_iterator;
815 
816  const_iterator begin() const throw();
817  const_iterator end() const throw();
818 
819  iterator begin() throw();
820  iterator end() throw();
821 
822  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
823  Command* clone() const;
824  std::string getCommandName() const throw();
825 };/* class CommandSequence */
826 
828 public:
829  ~DeclarationSequence() throw() {}
830 };/* class DeclarationSequence */
831 
832 }/* CVC4 namespace */
833 
834 #endif /* __CVC4__COMMAND_H */
std::vector< Expr > VExpr
Definition: command.h:742
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:226
std::vector< Expr > d_formals
Definition: command.h:399
[[ Add one-line brief description here ]]
struct CVC4::options::printSuccess__option_t printSuccess
std::vector< Expr > d_terms
Definition: command.h:519
bool isMuted()
Determine whether this Command will print a success message.
Definition: command.h:228
std::vector< Expr > VExpr
Definition: command.h:711
std::string d_result
Definition: command.h:649
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:433
Class encapsulating CVC4 expression types.
Definition: type.h:88
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:740
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:679
static const CommandSuccess * instance()
Definition: command.h:166
std::vector< Command * >::iterator iterator
Definition: command.h:813
static bool getPrintSuccess(std::ostream &out)
Definition: command.h:103
Encapsulation of the result of a query.
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
The AST output language.
Definition: language.h:115
bool d_muted
True if this command is "muted"—i.e., don't print "success" on successful execution.
Definition: command.h:200
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:633
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Definition: kind.h:508
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:420
virtual ~CommandStatus()
Definition: command.h:157
Class encapsulating the datatype type.
Definition: type.h:594
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:551
EmptyCommands are the residue of a command after the parser handles them (and there'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:382
CommandStatus & clone() const
Definition: command.h:167
std::vector< std::vector< Expr > > Triggers
Definition: command.h:709
static void setPrintSuccess(std::ostream &out, bool printSuccess)
Definition: command.h:107
std::string d_result
Definition: command.h:680
std::string d_flag
Definition: command.h:664
std::string d_flag
Definition: command.h:648
BenchmarkStatus d_status
Definition: command.h:607
Interface for expression types.
ExportTransformer(ExprManager *exprManager, ExprManagerMapCollection &variableMap)
Definition: command.h:265
std::vector< Command * >::const_iterator const_iterator
Definition: command.h:814