22 #ifndef __CVC4__COMMAND_H
23 #define __CVC4__COMMAND_H
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;
80 static const int s_iosIndex;
86 static const int s_defaultPrintSuccess =
false;
100 out.iword(s_iosIndex) = d_printSuccess;
104 return out.iword(s_iosIndex);
119 bool d_oldPrintSuccess;
148 cps.applyPrintSuccess(
out);
158 void toStream(std::ostream&
out,
176 std::string d_message;
210 virtual
void invoke(
SmtEngine* smtEngine) throw() = 0;
213 virtual
void toStream(
std::ostream&
out,
int toDepth = -1,
bool types = false,
size_t dag = 1,
216 std::
string toString() const throw();
218 virtual
std::
string getCommandName() const throw() = 0;
223 void setMuted(
bool muted) throw() { d_muted = muted; }
234 bool ok()
const throw();
240 bool fail() const throw();
243 const
CommandStatus* getCommandStatus() const throw() {
return d_commandStatus; }
245 virtual void printResult(std::ostream&
out, uint32_t
verbosity = 2)
const throw();
258 virtual
Command* clone() const = 0;
266 d_exprManager(exprManager),
267 d_variableMap(variableMap) {
270 return e.
exportTo(d_exprManager, d_variableMap);
273 return t.
exportTo(d_exprManager, d_variableMap);
288 std::string getName()
const throw();
289 void invoke(
SmtEngine* smtEngine) throw();
292 std::
string getCommandName() const throw();
301 std::string getOutput()
const throw();
302 void invoke(
SmtEngine* smtEngine) throw();
305 Command* clone() const;
306 std::
string getCommandName() const throw();
315 Expr getExpr()
const throw();
316 void invoke(
SmtEngine* smtEngine) throw();
318 Command* clone() const;
319 std::
string getCommandName() const throw();
325 void invoke(
SmtEngine* smtEngine)
throw();
327 Command* clone()
const;
328 std::string getCommandName()
const throw();
334 void invoke(
SmtEngine* smtEngine)
throw();
336 Command* clone()
const;
337 std::string getCommandName()
const throw();
346 virtual void invoke(
SmtEngine* smtEngine)
throw() = 0;
347 std::string getSymbol()
const 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();
366 Command* clone() const;
367 std::
string getCommandName() const throw();
377 size_t getArity()
const throw();
378 Type getType() const throw();
379 void invoke(
SmtEngine* smtEngine) throw();
381 Command* clone() const;
382 std::
string getCommandName() const throw();
393 const std::vector<Type>& getParameters()
const throw();
394 Type getType() const throw();
395 void invoke(
SmtEngine* smtEngine) throw();
397 Command* clone() const;
398 std::
string getCommandName() const throw();
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();
416 Command* clone() const;
417 std::
string getCommandName() const throw();
428 const std::vector<Expr>& formals,
Expr formula)
throw();
429 void invoke(
SmtEngine* smtEngine)
throw();
431 Command* clone()
const;
449 void invoke(
SmtEngine* smtEngine)
throw();
451 Command* clone()
const;
452 std::string getCommandName()
const 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();
469 Command* clone() const;
470 std::
string getCommandName() const 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();
485 Command* clone() const;
486 std::
string getCommandName() const 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();
502 Command* clone() const;
503 std::
string getCommandName() const 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();
518 Command* clone() const;
519 std::
string getCommandName() const 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();
535 Command* clone() const;
536 std::
string getCommandName() const throw();
545 void invoke(
SmtEngine* smtEngine)
throw();
546 SExpr getResult()
const throw();
547 void printResult(
std::ostream& out, uint32_t
verbosity = 2) const throw();
549 Command* clone() const;
550 std::
string getCommandName() const throw();
560 void invoke(
SmtEngine* smtEngine)
throw();
563 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
565 Command* clone() const;
566 std::
string getCommandName() const throw();
575 void invoke(
SmtEngine* smtEngine)
throw();
576 Proof* getResult()
const throw();
577 void printResult(
std::ostream& out, uint32_t
verbosity = 2) const throw();
579 Command* clone() const;
580 std::
string getCommandName() const throw();
590 void invoke(
SmtEngine* smtEngine)
throw();
592 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
594 Command* clone() const;
595 std::
string getCommandName() const throw();
604 void invoke(
SmtEngine* smtEngine)
throw();
605 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
607 Command* clone() const;
608 std::
string getCommandName() const 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();
621 Command* clone() const;
622 std::
string getCommandName() const throw();
632 void invoke(
SmtEngine* smtEngine) throw();
634 Command* clone() const;
635 std::
string getCommandName() const throw();
644 std::string getLogic()
const throw();
645 void invoke(
SmtEngine* smtEngine) throw();
647 Command* clone() const;
648 std::
string getCommandName() const throw();
658 std::string getFlag()
const throw();
659 SExpr getSExpr() const throw();
660 void invoke(
SmtEngine* smtEngine) throw();
662 Command* clone() const;
663 std::
string getCommandName() const 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();
678 Command* clone() const;
679 std::
string getCommandName() const throw();
689 std::string getFlag()
const throw();
690 SExpr getSExpr() const throw();
691 void invoke(
SmtEngine* smtEngine) throw();
693 Command* clone() const;
694 std::
string getCommandName() const 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();
709 Command* clone() const;
710 std::
string getCommandName() const throw();
715 std::vector<DatatypeType> d_datatypes;
720 const std::vector<DatatypeType>& getDatatypes()
const throw();
721 void invoke(
SmtEngine* smtEngine) throw();
723 Command* clone() const;
724 std::
string getCommandName() const throw();
729 typedef std::vector< std::vector< Expr > >
Triggers;
739 const std::vector<Expr>& guards,
742 const Triggers& d_triggers)
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();
754 Command* clone() const;
755 std::
string getCommandName() const throw();
760 typedef std::vector< std::vector< Expr > >
Triggers;
771 const std::vector<Expr>& guards,
772 const std::vector<Expr>& heads,
774 const Triggers& d_triggers,
776 bool d_deduction =
false) throw();
778 const
std::vector<
Expr>& heads,
780 bool d_deduction = false) 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();
790 Command* clone() const;
791 std::
string getCommandName() const throw();
799 void invoke(
SmtEngine* smtEngine)
throw();
801 Command* clone()
const;
802 std::string getCommandName()
const throw();
806 std::string d_comment;
810 std::string getComment()
const throw();
811 void invoke(
SmtEngine* smtEngine) throw();
813 Command* clone() const;
814 std::
string getCommandName() const throw();
820 std::vector<Command*> d_commandSequence;
822 unsigned int d_index;
827 void addCommand(Command* cmd)
throw();
828 void clear()
throw();
830 void invoke(
SmtEngine* smtEngine)
throw();
831 void invoke(
SmtEngine* smtEngine, std::ostream& out)
throw();
836 const_iterator begin()
const throw();
837 const_iterator end() const throw();
839 iterator begin() throw();
840 iterator end() throw();
843 Command* clone() const;
844 std::
string getCommandName() const throw();
std::vector< Expr > VExpr
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
Scope(std::ostream &out, bool printSuccess)
Set the print-success state on the output stream for the current stack scope.
Class encapsulating CVC4 expressions and methods for constructing new expressions.
std::vector< Expr > d_formals
[[ Add one-line brief description here ]]
struct CVC4::options::printSuccess__option_t printSuccess
std::vector< Expr > d_terms
bool isMuted()
Determine whether this Command will print a success message.
~SetUserAttributeCommand()
std::vector< Expr > VExpr
~DeclarationDefinitionCommand()
Benchmark is satisfiable.
void applyPrintSuccess(std::ostream &out)
~DeclareFunctionCommand()
The command when an attribute is set by a user.
Class encapsulating CVC4 expression types.
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...
~SetBenchmarkLogicCommand()
std::vector< std::vector< Expr > > Triggers
struct CVC4::options::verbosity__option_t verbosity
Type exportTo(ExprManager *exprManager, ExprManagerMapCollection &vmap) const
Exports this type into a different ExprManager.
static const CommandSuccess * instance()
~SetBenchmarkStatusCommand()
std::vector< Command * >::iterator iterator
bool d_printInModelSetByUser
static bool getPrintSuccess(std::ostream &out)
Encapsulation of the result of a query.
Match the output language to the input language.
bool d_muted
True if this command is "muted"—i.e., don't print "success" on successful execution.
~ExpandDefinitionsCommand()
CommandPrintSuccess printsuccess
IOStream manipulator to print success messages or not.
std::ostream & operator<<(std::ostream &out, const TypeCheckingException &e)
The status of the benchmark is unknown.
This differs from DefineFunctionCommand only in that it instructs the SmtEngine to "remember" this fu...
Class encapsulating the datatype type.
CommandPrintSuccess(bool printSuccess)
Construct a CommandPrintSuccess with the given setting.
Macros that should be defined everywhere during the building of the libraries and driver binary...
Three-valued SMT result, with optional explanation.
~DatatypeDeclarationCommand()
EmptyCommands are the residue of a command after the parser handles them (and there's nothing left to...
std::string getMessage() const
BenchmarkStatus
The status an SMT benchmark can have.
Benchmark is unsatisfiable.
struct CVC4::options::out__option_t out
[[ Add one-line brief description here ]]
CommandFailure & clone() const
CommandFailure(std::string message)
std::vector< Type > d_params
CommandStatus & clone() const
std::vector< std::vector< Expr > > Triggers
static void setPrintSuccess(std::ostream &out, bool printSuccess)
Interface for expression types.
std::vector< Command * >::const_iterator const_iterator