cvc4-1.4
CVC4::Command Class Referenceabstract

#include <command.h>

Inheritance diagram for CVC4::Command:
CVC4::AssertCommand CVC4::CheckSatCommand CVC4::CommandSequence CVC4::CommentCommand CVC4::DatatypeDeclarationCommand CVC4::DeclarationDefinitionCommand CVC4::EchoCommand CVC4::EmptyCommand CVC4::ExpandDefinitionsCommand CVC4::GetAssertionsCommand CVC4::GetAssignmentCommand CVC4::GetInfoCommand CVC4::GetInstantiationsCommand CVC4::GetModelCommand CVC4::GetOptionCommand CVC4::GetProofCommand CVC4::GetUnsatCoreCommand CVC4::GetValueCommand CVC4::PopCommand CVC4::PropagateRuleCommand CVC4::PushCommand CVC4::QueryCommand CVC4::QuitCommand CVC4::RewriteRuleCommand CVC4::SetBenchmarkLogicCommand CVC4::SetBenchmarkStatusCommand CVC4::SetInfoCommand CVC4::SetOptionCommand CVC4::SetUserAttributeCommand CVC4::SimplifyCommand

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 CommandStatusgetCommandStatus () 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 CommandexportTo (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 Commandclone () const =0
 Clone this Command (make a shallow copy). More...
 

Protected Attributes

const CommandStatusd_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...
 

Detailed Description

Definition at line 184 of file command.h.

Member Typedef Documentation

Definition at line 203 of file command.h.

Constructor & Destructor Documentation

CVC4::Command::Command ( )
throw (
)
CVC4::Command::Command ( const Command cmd)
virtual CVC4::Command::~Command ( )
throw (
)
virtual

Member Function Documentation

bool CVC4::Command::fail ( ) const
throw (
)

The command completed in a failure state (CommandFailure, not CommandSuccess or CommandUnsupported).

const CommandStatus* CVC4::Command::getCommandStatus ( ) const
throw (
)
inline

Get the command status (it's NULL if we haven't run yet).

Definition at line 243 of file command.h.

virtual void CVC4::Command::invoke ( SmtEngine smtEngine,
std::ostream &  out 
)
throw (
)
virtual

Reimplemented in CVC4::CommandSequence, and CVC4::EchoCommand.

bool CVC4::Command::isMuted ( )
throw (
)
inline

Determine whether this Command will print a success message.

Definition at line 228 of file command.h.

bool CVC4::Command::ok ( ) const
throw (
)

Either the command hasn't run yet, or it completed successfully (CommandSuccess, not CommandUnsupported or CommandFailure).

void CVC4::Command::setMuted ( bool  muted)
throw (
)
inline

If false, instruct this Command not to print a success message.

Definition at line 223 of file command.h.

virtual void CVC4::Command::toStream ( std::ostream &  out,
int  toDepth = -1,
bool  types = false,
size_t  dag = 1,
OutputLanguage  language = language::output::LANG_AUTO 
) const
throw (
)
virtual
std::string CVC4::Command::toString ( ) const
throw (
)

Field Documentation

const CommandStatus* CVC4::Command::d_commandStatus
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.

Definition at line 194 of file command.h.

bool CVC4::Command::d_muted
protected

True if this command is "muted"—i.e., don't print "success" on successful execution.

Definition at line 200 of file command.h.


The documentation for this class was generated from the following file: