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;
158 void toStream(std::ostream& out,
176 std::string d_message;
210 virtual
void invoke(
SmtEngine* smtEngine) throw() = 0;
211 virtual
void invoke(
SmtEngine* smtEngine,
std::ostream& out) throw();
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();
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();
303 void invoke(
SmtEngine* smtEngine, std::ostream& out)
throw();
306 std::string getCommandName()
const throw();
315 Expr getExpr()
const throw();
316 void invoke(
SmtEngine* smtEngine)
throw();
319 std::string getCommandName()
const throw();
325 void invoke(
SmtEngine* smtEngine)
throw();
328 std::string getCommandName()
const throw();
334 void invoke(
SmtEngine* smtEngine)
throw();
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();
367 std::string getCommandName()
const throw();
377 size_t getArity()
const throw();
378 Type getType()
const throw();
379 void invoke(
SmtEngine* smtEngine)
throw();
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();
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();
417 std::string getCommandName()
const throw();
428 const std::vector<Expr>& formals,
Expr formula)
throw();
429 void invoke(
SmtEngine* smtEngine)
throw();
449 void invoke(
SmtEngine* smtEngine)
throw();
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();
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();
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();
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();
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();
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();
550 std::string getCommandName()
const throw();
560 void invoke(
SmtEngine* smtEngine)
throw();
563 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
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();
580 std::string getCommandName()
const throw();
590 void invoke(
SmtEngine* smtEngine)
throw();
592 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
595 std::string getCommandName()
const throw();
604 void invoke(
SmtEngine* smtEngine)
throw();
605 void printResult(std::ostream& out, uint32_t
verbosity = 2)
const throw();
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();
622 std::string getCommandName()
const throw();
632 void invoke(
SmtEngine* smtEngine)
throw();
635 std::string getCommandName()
const throw();
644 std::string getLogic()
const throw();
645 void invoke(
SmtEngine* smtEngine)
throw();
648 std::string getCommandName()
const throw();
658 std::string getFlag()
const throw();
659 SExpr getSExpr()
const throw();
660 void invoke(
SmtEngine* smtEngine)
throw();
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();
679 std::string getCommandName()
const throw();
689 std::string getFlag()
const throw();
690 SExpr getSExpr()
const throw();
691 void invoke(
SmtEngine* smtEngine)
throw();
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();
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();
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();
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();
791 std::string getCommandName()
const throw();
799 void invoke(
SmtEngine* smtEngine)
throw();
802 std::string getCommandName()
const throw();
806 std::string d_comment;
810 std::string getComment()
const throw();
811 void invoke(
SmtEngine* smtEngine)
throw();
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();
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()
const CommandStatus * getCommandStatus() const
Get the command status (it's NULL if we haven't run yet).
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