cvc4-1.4
CVC4::RewriteRuleCommand Class Reference

#include <command.h>

Inheritance diagram for CVC4::RewriteRuleCommand:
CVC4::Command

Public Types

typedef std::vector< std::vector< Expr > > Triggers
 
typedef CommandPrintSuccess printsuccess
 

Public Member Functions

 RewriteRuleCommand (const std::vector< Expr > &vars, const std::vector< Expr > &guards, Expr head, Expr body, const Triggers &d_triggers) throw ()
 
 RewriteRuleCommand (const std::vector< Expr > &vars, Expr head, Expr body) throw ()
 
 ~RewriteRuleCommand () throw ()
 
const std::vector< Expr > & getVars () const throw ()
 
const std::vector< Expr > & getGuards () const throw ()
 
Expr getHead () const throw ()
 
Expr getBody () const throw ()
 
const TriggersgetTriggers () const throw ()
 
void invoke (SmtEngine *smtEngine) throw ()
 
CommandexportTo (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...
 
Commandclone () 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 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 ()
 

Protected Types

typedef std::vector< ExprVExpr
 

Protected Attributes

VExpr d_vars
 
VExpr d_guards
 
Expr d_head
 
Expr d_body
 
Triggers d_triggers
 
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 727 of file command.h.

Member Typedef Documentation

Definition at line 203 of file command.h.

typedef std::vector< std::vector< Expr > > CVC4::RewriteRuleCommand::Triggers

Definition at line 729 of file command.h.

typedef std::vector< Expr > CVC4::RewriteRuleCommand::VExpr
protected

Definition at line 731 of file command.h.

Constructor & Destructor Documentation

CVC4::RewriteRuleCommand::RewriteRuleCommand ( const std::vector< Expr > &  vars,
const std::vector< Expr > &  guards,
Expr  head,
Expr  body,
const Triggers d_triggers 
)
throw (
)
CVC4::RewriteRuleCommand::RewriteRuleCommand ( const std::vector< Expr > &  vars,
Expr  head,
Expr  body 
)
throw (
)
CVC4::RewriteRuleCommand::~RewriteRuleCommand ( )
throw (
)
inline

Definition at line 746 of file command.h.

Member Function Documentation

Command* CVC4::RewriteRuleCommand::clone ( ) const
virtual

Clone this Command (make a shallow copy).

Implements CVC4::Command.

Command* CVC4::RewriteRuleCommand::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).

Expr CVC4::RewriteRuleCommand::getBody ( ) const
throw (
)
std::string CVC4::RewriteRuleCommand::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.

const std::vector<Expr>& CVC4::RewriteRuleCommand::getGuards ( ) const
throw (
)
Expr CVC4::RewriteRuleCommand::getHead ( ) const
throw (
)
const Triggers& CVC4::RewriteRuleCommand::getTriggers ( ) const
throw (
)
const std::vector<Expr>& CVC4::RewriteRuleCommand::getVars ( ) const
throw (
)
virtual void CVC4::Command::invoke ( SmtEngine smtEngine,
std::ostream &  out 
)
throw (
)
virtualinherited

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

void CVC4::RewriteRuleCommand::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).

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

Expr CVC4::RewriteRuleCommand::d_body
protected

Definition at line 735 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.

VExpr CVC4::RewriteRuleCommand::d_guards
protected

Definition at line 733 of file command.h.

Expr CVC4::RewriteRuleCommand::d_head
protected

Definition at line 734 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.

Triggers CVC4::RewriteRuleCommand::d_triggers
protected

Definition at line 736 of file command.h.

VExpr CVC4::RewriteRuleCommand::d_vars
protected

Definition at line 732 of file command.h.


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