CVC4::SetUserAttributeCommand Class Reference

The command when an attribute is set by a user. More...

#include <command.h>

Inheritance diagram for CVC4::SetUserAttributeCommand:

Public Types
typedef CommandPrintSuccess	printsuccess

Public Member Functions
	SetUserAttributeCommand (const std::string &attr, Expr expr) throw ()
	~SetUserAttributeCommand () 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 ()
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
std::string	d_attr
Expr	d_expr
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...

Detailed Description

The command when an attribute is set by a user.

In SMT-LIBv2 this is done via the syntax (! expr :attr)

Definition at line 438 of file command.h.

Member Typedef Documentation

typedef CommandPrintSuccess CVC4::Command::printsuccess

inherited

Definition at line 203 of file command.h.

Constructor & Destructor Documentation

CVC4::SetUserAttributeCommand::SetUserAttributeCommand	(	const std::string &	attr,
		Expr	expr
	)
throw	(
	)

CVC4::SetUserAttributeCommand::~SetUserAttributeCommand ( ) throw ( )

inline

Definition at line 448 of file command.h.

Member Function Documentation

Command* CVC4::SetUserAttributeCommand::clone ( ) const

virtual

Clone this Command (make a shallow copy).

Implements CVC4::Command.

Command* CVC4::SetUserAttributeCommand::exportTo ( ExprManager *  exprManager, ExprManagerMapCollection &  variableMap  )

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.

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

inherited

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

std::string CVC4::SetUserAttributeCommand::getCommandName ( ) const throw ( )

virtual

Implements CVC4::Command.

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

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.

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

virtualinherited

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

void CVC4::SetUserAttributeCommand::invoke ( SmtEngine *  smtEngine ) throw ( )

virtual

Implements CVC4::Command.

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

inlineinherited

Determine whether this Command will print a success message.

Definition at line 228 of file command.h.

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

inherited

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

virtual void CVC4::Command::printResult ( std::ostream &  out, uint32_t  verbosity = 2  ) const throw ( )

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.

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

inlineinherited

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 ( )

virtualinherited

std::string CVC4::Command::toString ( ) const throw ( )

inherited

Field Documentation

std::string CVC4::SetUserAttributeCommand::d_attr

protected

Definition at line 440 of file command.h.

const CommandStatus* CVC4::Command::d_commandStatus

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.

Definition at line 194 of file command.h.

Expr CVC4::SetUserAttributeCommand::d_expr

protected

Definition at line 441 of file command.h.

bool CVC4::Command::d_muted

protectedinherited

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:

• src/expr/command.h