cvc4-1.4
|
#include <command.h>
Data Structures | |
class | ExportTransformer |
Public Types | |
typedef CommandPrintSuccess | printsuccess |
Public Member Functions | |
Command () throw () | |
Command (const Command &cmd) | |
virtual | ~Command () throw () |
virtual void | invoke (SmtEngine *smtEngine)=0 throw () |
virtual void | invoke (SmtEngine *smtEngine, std::ostream &out) 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 () |
virtual std::string | getCommandName () const =0 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 () |
virtual Command * | exportTo (ExprManager *exprManager, ExprManagerMapCollection &variableMap)=0 |
Maps this Command into one for a different ExprManager, using variableMap for the translation and extending it with any new mappings. More... | |
virtual Command * | clone () const =0 |
Clone this Command (make a shallow copy). More... | |
Protected Attributes | |
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... | |
CVC4::Command::Command | ( | ) | ||
throw | ( | |||
) |
CVC4::Command::Command | ( | const Command & | cmd | ) |
|
virtual |
|
pure virtual |
Clone this Command (make a shallow copy).
Implemented in CVC4::CommandSequence, CVC4::CommentCommand, CVC4::QuitCommand, CVC4::PropagateRuleCommand, CVC4::RewriteRuleCommand, CVC4::DatatypeDeclarationCommand, CVC4::GetOptionCommand, CVC4::SetOptionCommand, CVC4::GetInfoCommand, CVC4::SetInfoCommand, CVC4::SetBenchmarkLogicCommand, CVC4::SetBenchmarkStatusCommand, CVC4::GetAssertionsCommand, CVC4::GetUnsatCoreCommand, CVC4::GetInstantiationsCommand, CVC4::GetProofCommand, CVC4::GetModelCommand, CVC4::GetAssignmentCommand, CVC4::GetValueCommand, CVC4::ExpandDefinitionsCommand, CVC4::SimplifyCommand, CVC4::QueryCommand, CVC4::CheckSatCommand, CVC4::SetUserAttributeCommand, CVC4::DefineNamedFunctionCommand, CVC4::DefineFunctionCommand, CVC4::DefineTypeCommand, CVC4::DeclareTypeCommand, CVC4::DeclareFunctionCommand, CVC4::PopCommand, CVC4::PushCommand, CVC4::AssertCommand, CVC4::EchoCommand, and CVC4::EmptyCommand.
|
pure virtual |
Maps this Command into one for a different ExprManager, using variableMap for the translation and extending it with any new mappings.
Implemented in CVC4::CommandSequence, CVC4::CommentCommand, CVC4::QuitCommand, CVC4::PropagateRuleCommand, CVC4::RewriteRuleCommand, CVC4::DatatypeDeclarationCommand, CVC4::GetOptionCommand, CVC4::SetOptionCommand, CVC4::GetInfoCommand, CVC4::SetInfoCommand, CVC4::SetBenchmarkLogicCommand, CVC4::SetBenchmarkStatusCommand, CVC4::GetAssertionsCommand, CVC4::GetUnsatCoreCommand, CVC4::GetInstantiationsCommand, CVC4::GetProofCommand, CVC4::GetModelCommand, CVC4::GetAssignmentCommand, CVC4::GetValueCommand, CVC4::ExpandDefinitionsCommand, CVC4::SimplifyCommand, CVC4::QueryCommand, CVC4::CheckSatCommand, CVC4::SetUserAttributeCommand, CVC4::DefineNamedFunctionCommand, CVC4::DefineFunctionCommand, CVC4::DefineTypeCommand, CVC4::DeclareTypeCommand, CVC4::DeclareFunctionCommand, CVC4::PopCommand, CVC4::PushCommand, CVC4::AssertCommand, CVC4::EchoCommand, and CVC4::EmptyCommand.
bool CVC4::Command::fail | ( | ) | const | |
throw | ( | |||
) |
The command completed in a failure state (CommandFailure, not CommandSuccess or CommandUnsupported).
|
pure virtual |
Implemented in CVC4::CommandSequence, CVC4::CommentCommand, CVC4::QuitCommand, CVC4::PropagateRuleCommand, CVC4::RewriteRuleCommand, CVC4::DatatypeDeclarationCommand, CVC4::GetOptionCommand, CVC4::SetOptionCommand, CVC4::GetInfoCommand, CVC4::SetInfoCommand, CVC4::SetBenchmarkLogicCommand, CVC4::SetBenchmarkStatusCommand, CVC4::GetAssertionsCommand, CVC4::GetUnsatCoreCommand, CVC4::GetInstantiationsCommand, CVC4::GetProofCommand, CVC4::GetModelCommand, CVC4::GetAssignmentCommand, CVC4::GetValueCommand, CVC4::ExpandDefinitionsCommand, CVC4::SimplifyCommand, CVC4::QueryCommand, CVC4::CheckSatCommand, CVC4::SetUserAttributeCommand, CVC4::DefineFunctionCommand, CVC4::DefineTypeCommand, CVC4::DeclareTypeCommand, CVC4::DeclareFunctionCommand, CVC4::PopCommand, CVC4::PushCommand, CVC4::AssertCommand, CVC4::EchoCommand, and CVC4::EmptyCommand.
|
inline |
|
pure virtual |
Implemented in CVC4::CommandSequence, CVC4::CommentCommand, CVC4::QuitCommand, CVC4::PropagateRuleCommand, CVC4::RewriteRuleCommand, CVC4::DatatypeDeclarationCommand, CVC4::GetOptionCommand, CVC4::SetOptionCommand, CVC4::GetInfoCommand, CVC4::SetInfoCommand, CVC4::SetBenchmarkLogicCommand, CVC4::SetBenchmarkStatusCommand, CVC4::GetAssertionsCommand, CVC4::GetUnsatCoreCommand, CVC4::GetInstantiationsCommand, CVC4::GetProofCommand, CVC4::GetModelCommand, CVC4::GetAssignmentCommand, CVC4::GetValueCommand, CVC4::ExpandDefinitionsCommand, CVC4::SimplifyCommand, CVC4::QueryCommand, CVC4::CheckSatCommand, CVC4::SetUserAttributeCommand, CVC4::DefineNamedFunctionCommand, CVC4::DefineFunctionCommand, CVC4::DefineTypeCommand, CVC4::DeclareTypeCommand, CVC4::DeclareFunctionCommand, CVC4::DeclarationDefinitionCommand, CVC4::PopCommand, CVC4::PushCommand, CVC4::AssertCommand, CVC4::EchoCommand, and CVC4::EmptyCommand.
|
virtual |
Reimplemented in CVC4::CommandSequence, and CVC4::EchoCommand.
|
inline |
bool CVC4::Command::ok | ( | ) | const | |
throw | ( | |||
) |
Either the command hasn't run yet, or it completed successfully (CommandSuccess, not CommandUnsupported or CommandFailure).
|
virtual |
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.
|
inline |
|
virtual |
std::string CVC4::Command::toString | ( | ) | const | |
throw | ( | |||
) |
|
protected |
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 |