cvc4-1.4
|
#include <command.h>
Public Types | |
typedef CommandPrintSuccess | printsuccess |
Public Member Functions | |
DefineFunctionCommand (const std::string &id, Expr func, Expr formula) throw () | |
DefineFunctionCommand (const std::string &id, Expr func, const std::vector< Expr > &formals, Expr formula) throw () | |
~DefineFunctionCommand () throw () | |
Expr | getFunction () const throw () |
const std::vector< Expr > & | getFormals () const throw () |
Expr | getFormula () const throw () |
void | invoke (SmtEngine *smtEngine) throw () |
Command * | exportTo (ExprManager *exprManager, ExprManagerMapCollection &variableMap) |
Maps this Command into one for a different ExprManager, using variableMap for the translation and extending it with any new mappings. More... | |
Command * | clone () const |
Clone this Command (make a shallow copy). More... | |
std::string | getCommandName () const throw () |
virtual void | invoke (SmtEngine *smtEngine, std::ostream &out) throw () |
std::string | getSymbol () const throw () |
virtual void | toStream (std::ostream &out, int toDepth=-1, bool types=false, size_t dag=1, OutputLanguage language=language::output::LANG_AUTO) const throw () |
std::string | toString () const throw () |
void | setMuted (bool muted) throw () |
If false, instruct this Command not to print a success message. More... | |
bool | isMuted () throw () |
Determine whether this Command will print a success message. More... | |
bool | ok () const throw () |
Either the command hasn't run yet, or it completed successfully (CommandSuccess, not CommandUnsupported or CommandFailure). More... | |
bool | fail () const throw () |
The command completed in a failure state (CommandFailure, not CommandSuccess or CommandUnsupported). More... | |
const CommandStatus * | getCommandStatus () const throw () |
Get the command status (it's NULL if we haven't run yet). More... | |
virtual void | printResult (std::ostream &out, uint32_t verbosity=2) const throw () |
Protected Attributes | |
Expr | d_func |
std::vector< Expr > | d_formals |
Expr | d_formula |
std::string | d_symbol |
const CommandStatus * | d_commandStatus |
This field contains a command status if the command has been invoked, or NULL if it has not. More... | |
bool | d_muted |
True if this command is "muted"—i.e., don't print "success" on successful execution. More... | |
|
inherited |
CVC4::DefineFunctionCommand::DefineFunctionCommand | ( | const std::string & | id, |
Expr | func, | ||
Expr | formula | ||
) | |||
throw | ( | ||
) |
CVC4::DefineFunctionCommand::DefineFunctionCommand | ( | const std::string & | id, |
Expr | func, | ||
const std::vector< Expr > & | formals, | ||
Expr | formula | ||
) | |||
throw | ( | ||
) |
|
inline |
|
virtual |
Clone this Command (make a shallow copy).
Implements CVC4::Command.
Reimplemented in CVC4::DefineNamedFunctionCommand.
|
virtual |
Maps this Command into one for a different ExprManager, using variableMap for the translation and extending it with any new mappings.
Implements CVC4::Command.
Reimplemented in CVC4::DefineNamedFunctionCommand.
|
inherited |
The command completed in a failure state (CommandFailure, not CommandSuccess or CommandUnsupported).
|
virtual |
Implements CVC4::Command.
|
inlineinherited |
Get the command status (it's NULL if we haven't run yet).
Definition at line 243 of file command.h.
References CVC4::options::verbosity.
const std::vector<Expr>& CVC4::DefineFunctionCommand::getFormals | ( | ) | const | |
throw | ( | |||
) |
Expr CVC4::DefineFunctionCommand::getFormula | ( | ) | const | |
throw | ( | |||
) |
Expr CVC4::DefineFunctionCommand::getFunction | ( | ) | const | |
throw | ( | |||
) |
|
inherited |
|
virtualinherited |
Reimplemented in CVC4::CommandSequence, and CVC4::EchoCommand.
|
virtual |
Implements CVC4::DeclarationDefinitionCommand.
Reimplemented in CVC4::DefineNamedFunctionCommand.
|
inlineinherited |
|
inherited |
Either the command hasn't run yet, or it completed successfully (CommandSuccess, not CommandUnsupported or CommandFailure).
|
virtualinherited |
Reimplemented in CVC4::GetOptionCommand, CVC4::GetInfoCommand, CVC4::GetAssertionsCommand, CVC4::GetUnsatCoreCommand, CVC4::GetInstantiationsCommand, CVC4::GetProofCommand, CVC4::GetModelCommand, CVC4::GetAssignmentCommand, CVC4::GetValueCommand, CVC4::ExpandDefinitionsCommand, CVC4::SimplifyCommand, CVC4::QueryCommand, and CVC4::CheckSatCommand.
|
inlineinherited |
|
virtualinherited |
|
inherited |
|
protectedinherited |
This field contains a command status if the command has been invoked, or NULL if it has not.
This field is either a dynamically-allocated pointer, or it's a pointer to the singleton CommandSuccess instance. Doing so is somewhat asymmetric, but it avoids the need to dynamically allocate memory in the common case of a successful command.
|
protected |
|
protectedinherited |
|
protectedinherited |