diff options
Diffstat (limited to 'src/expr/command.h')
| -rw-r--r-- | src/expr/command.h | 400 |
1 files changed, 278 insertions, 122 deletions
diff --git a/src/expr/command.h b/src/expr/command.h index b686025fe..cf8c1b615 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -41,9 +41,12 @@ namespace CVC4 { class SmtEngine; class Command; +class CommandStatus; -std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC; /** The status an SMT benchmark can have */ enum BenchmarkStatus { @@ -56,21 +59,156 @@ enum BenchmarkStatus { }; std::ostream& operator<<(std::ostream& out, - BenchmarkStatus status) CVC4_PUBLIC; + BenchmarkStatus status) throw() CVC4_PUBLIC; + +/** + * IOStream manipulator to print success messages or not. + * + * out << Command::printsuccess(false) << CommandSuccess(); + * + * prints nothing, but + * + * out << Command::printsuccess(true) << CommandSuccess(); + * + * prints a success message (in a manner appropriate for the current + * output language). + */ +class CVC4_PUBLIC CommandPrintSuccess { + /** + * The allocated index in ios_base for our depth setting. + */ + static const int s_iosIndex; + + /** + * The default setting, for ostreams that haven't yet had a + * setdepth() applied to them. + */ + static const int s_defaultPrintSuccess = false; + + /** + * When this manipulator is used, the setting is stored here. + */ + bool d_printSuccess; + +public: + /** + * Construct a CommandPrintSuccess with the given setting. + */ + CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {} + + inline void applyPrintSuccess(std::ostream& out) throw() { + out.iword(s_iosIndex) = d_printSuccess; + } + + static inline bool getPrintSuccess(std::ostream& out) throw() { + return out.iword(s_iosIndex); + } + + static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() { + out.iword(s_iosIndex) = printSuccess; + } + + /** + * Set the print-success state on the output stream for the current + * stack scope. This makes sure the old state is reset on the + * stream after normal OR exceptional exit from the scope, using the + * RAII C++ idiom. + */ + class Scope { + std::ostream& d_out; + bool d_oldPrintSuccess; + + public: + + inline Scope(std::ostream& out, bool printSuccess) throw() : + d_out(out), + d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) { + CommandPrintSuccess::setPrintSuccess(out, printSuccess); + } + + inline ~Scope() throw() { + CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess); + } + + };/* class CommandPrintSuccess::Scope */ + +};/* class CommandPrintSuccess */ + +/** + * Sets the default print-success setting when pretty-printing an Expr + * to an ostream. Use like this: + * + * // let out be an ostream, e an Expr + * out << Expr::setdepth(n) << e << endl; + * + * The depth stays permanently (until set again) with the stream. + */ +inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() { + cps.applyPrintSuccess(out); + return out; +} + +class CVC4_PUBLIC CommandStatus { +protected: + // shouldn't construct a CommandStatus (use a derived class) + CommandStatus() throw() {} +public: + virtual ~CommandStatus() throw() {} + void toStream(std::ostream& out, + OutputLanguage language = language::output::LANG_AST) const throw(); +};/* class CommandStatus */ + +class CVC4_PUBLIC CommandSuccess : public CommandStatus { + static const CommandSuccess* s_instance; +public: + static const CommandSuccess* instance() throw() { return s_instance; } +};/* class CommandSuccess */ + +class CVC4_PUBLIC CommandUnsupported : public CommandStatus { +};/* class CommandSuccess */ + +class CVC4_PUBLIC CommandFailure : public CommandStatus { + std::string d_message; +public: + CommandFailure(std::string message) throw() : d_message(message) {} + ~CommandFailure() throw() {} + std::string getMessage() const throw() { return d_message; } +};/* class CommandFailure */ class CVC4_PUBLIC Command { +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. + */ + const CommandStatus* d_commandStatus; + public: - virtual ~Command() {} + typedef CommandPrintSuccess printsuccess; + + Command() throw(); + virtual ~Command() throw(); - virtual void invoke(SmtEngine* smtEngine) = 0; - virtual void invoke(SmtEngine* smtEngine, std::ostream& out); + virtual void invoke(SmtEngine* smtEngine) throw() = 0; + virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, - OutputLanguage language = language::output::LANG_AST) const; + OutputLanguage language = language::output::LANG_AST) const throw(); + + std::string toString() const throw(); + + /** Either the command hasn't run yet, or it completed successfully. */ + bool ok() const throw(); - std::string toString() const; + /** Get the command status (it's NULL if we haven't run yet). */ + const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; } - virtual void printResult(std::ostream& out) const; + virtual void printResult(std::ostream& out) const throw(); };/* class Command */ @@ -82,45 +220,51 @@ class CVC4_PUBLIC EmptyCommand : public Command { protected: std::string d_name; public: - EmptyCommand(std::string name = ""); - std::string getName() const; - void invoke(SmtEngine* smtEngine); + EmptyCommand(std::string name = "") throw(); + ~EmptyCommand() throw() {} + std::string getName() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class EmptyCommand */ class CVC4_PUBLIC AssertCommand : public Command { protected: BoolExpr d_expr; public: - AssertCommand(const BoolExpr& e); - BoolExpr getExpr() const; - void invoke(SmtEngine* smtEngine); + AssertCommand(const BoolExpr& e) throw(); + ~AssertCommand() throw() {} + BoolExpr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class AssertCommand */ class CVC4_PUBLIC PushCommand : public Command { public: - void invoke(SmtEngine* smtEngine); + ~PushCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); };/* class PushCommand */ class CVC4_PUBLIC PopCommand : public Command { public: - void invoke(SmtEngine* smtEngine); + ~PopCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); };/* class PopCommand */ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command { protected: std::string d_symbol; public: - DeclarationDefinitionCommand(const std::string& id); - std::string getSymbol() const; + DeclarationDefinitionCommand(const std::string& id) throw(); + ~DeclarationDefinitionCommand() throw() {} + std::string getSymbol() const throw(); };/* class DeclarationDefinitionCommand */ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { protected: Type d_type; public: - DeclareFunctionCommand(const std::string& id, Type type); - Type getType() const; - void invoke(SmtEngine* smtEngine); + DeclareFunctionCommand(const std::string& id, Type type) throw(); + ~DeclareFunctionCommand() throw() {} + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DeclareFunctionCommand */ class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand { @@ -128,10 +272,11 @@ protected: size_t d_arity; Type d_type; public: - DeclareTypeCommand(const std::string& id, size_t arity, Type t); - size_t getArity() const; - Type getType() const; - void invoke(SmtEngine* smtEngine); + DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw(); + ~DeclareTypeCommand() throw() {} + size_t getArity() const throw(); + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DeclareTypeCommand */ class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand { @@ -139,11 +284,12 @@ protected: std::vector<Type> d_params; Type d_type; public: - DefineTypeCommand(const std::string& id, Type t); - DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t); - const std::vector<Type>& getParameters() const; - Type getType() const; - void invoke(SmtEngine* smtEngine); + DefineTypeCommand(const std::string& id, Type t) throw(); + DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw(); + ~DefineTypeCommand() throw() {} + const std::vector<Type>& getParameters() const throw(); + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DefineTypeCommand */ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { @@ -152,13 +298,14 @@ protected: std::vector<Expr> d_formals; Expr d_formula; public: - DefineFunctionCommand(const std::string& id, Expr func, Expr formula); + DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw(); DefineFunctionCommand(const std::string& id, Expr func, - const std::vector<Expr>& formals, Expr formula); - Expr getFunction() const; - const std::vector<Expr>& getFormals() const; - Expr getFormula() const; - void invoke(SmtEngine* smtEngine); + 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(); };/* class DefineFunctionCommand */ /** @@ -169,8 +316,8 @@ public: class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand { public: DefineNamedFunctionCommand(const std::string& id, Expr func, - const std::vector<Expr>& formals, Expr formula); - void invoke(SmtEngine* smtEngine); + const std::vector<Expr>& formals, Expr formula) throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DefineNamedFunctionCommand */ class CVC4_PUBLIC CheckSatCommand : public Command { @@ -178,12 +325,13 @@ protected: BoolExpr d_expr; Result d_result; public: - CheckSatCommand(); - CheckSatCommand(const BoolExpr& expr); - BoolExpr getExpr() const; - void invoke(SmtEngine* smtEngine); - Result getResult() const; - void printResult(std::ostream& out) const; + CheckSatCommand() throw(); + CheckSatCommand(const BoolExpr& expr) throw(); + ~CheckSatCommand() throw() {} + BoolExpr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Result getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class CheckSatCommand */ class CVC4_PUBLIC QueryCommand : public Command { @@ -191,11 +339,12 @@ protected: BoolExpr d_expr; Result d_result; public: - QueryCommand(const BoolExpr& e); - BoolExpr getExpr() const; - void invoke(SmtEngine* smtEngine); - Result getResult() const; - void printResult(std::ostream& out) const; + QueryCommand(const BoolExpr& e) throw(); + ~QueryCommand() throw() {} + BoolExpr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Result getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class QueryCommand */ // this is TRANSFORM in the CVC presentation language @@ -204,11 +353,12 @@ protected: Expr d_term; Expr d_result; public: - SimplifyCommand(Expr term); - Expr getTerm() const; - void invoke(SmtEngine* smtEngine); - Expr getResult() const; - void printResult(std::ostream& out) const; + SimplifyCommand(Expr term) throw(); + ~SimplifyCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class SimplifyCommand */ class CVC4_PUBLIC GetValueCommand : public Command { @@ -216,75 +366,77 @@ protected: Expr d_term; Expr d_result; public: - GetValueCommand(Expr term); - Expr getTerm() const; - void invoke(SmtEngine* smtEngine); - Expr getResult() const; - void printResult(std::ostream& out) const; + GetValueCommand(Expr term) throw(); + ~GetValueCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetValueCommand */ class CVC4_PUBLIC GetAssignmentCommand : public Command { protected: SExpr d_result; public: - GetAssignmentCommand(); - void invoke(SmtEngine* smtEngine); - SExpr getResult() const; - void printResult(std::ostream& out) const; + GetAssignmentCommand() throw(); + ~GetAssignmentCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + SExpr getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetAssignmentCommand */ class CVC4_PUBLIC GetProofCommand : public Command { protected: Proof* d_result; public: - GetProofCommand(); - void invoke(SmtEngine* smtEngine); - Proof* getResult() const; - void printResult(std::ostream& out) const; + GetProofCommand() throw(); + ~GetProofCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Proof* getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetProofCommand */ class CVC4_PUBLIC GetAssertionsCommand : public Command { protected: std::string d_result; public: - GetAssertionsCommand(); - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + GetAssertionsCommand() throw(); + ~GetAssertionsCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetAssertionsCommand */ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { protected: - std::string d_result; BenchmarkStatus d_status; public: - SetBenchmarkStatusCommand(BenchmarkStatus status); - BenchmarkStatus getStatus() const; - void invoke(SmtEngine* smtEngine); + SetBenchmarkStatusCommand(BenchmarkStatus status) throw(); + ~SetBenchmarkStatusCommand() throw() {} + BenchmarkStatus getStatus() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class SetBenchmarkStatusCommand */ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { protected: - std::string d_result; std::string d_logic; public: - SetBenchmarkLogicCommand(std::string logic); - std::string getLogic() const; - void invoke(SmtEngine* smtEngine); + SetBenchmarkLogicCommand(std::string logic) throw(); + ~SetBenchmarkLogicCommand() throw() {} + std::string getLogic() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class SetBenchmarkLogicCommand */ class CVC4_PUBLIC SetInfoCommand : public Command { protected: std::string d_flag; SExpr d_sexpr; - std::string d_result; public: - SetInfoCommand(std::string flag, const SExpr& sexpr); - std::string getFlag() const; - SExpr getSExpr() const; - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + SetInfoCommand(std::string flag, const SExpr& sexpr) throw(); + ~SetInfoCommand() throw() {} + std::string getFlag() const throw(); + SExpr getSExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class SetInfoCommand */ class CVC4_PUBLIC GetInfoCommand : public Command { @@ -292,25 +444,24 @@ protected: std::string d_flag; std::string d_result; public: - GetInfoCommand(std::string flag); - std::string getFlag() const; - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + GetInfoCommand(std::string flag) throw(); + ~GetInfoCommand() throw() {} + std::string getFlag() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetInfoCommand */ class CVC4_PUBLIC SetOptionCommand : public Command { protected: std::string d_flag; SExpr d_sexpr; - std::string d_result; public: - SetOptionCommand(std::string flag, const SExpr& sexpr); - std::string getFlag() const; - SExpr getSExpr() const; - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + SetOptionCommand(std::string flag, const SExpr& sexpr) throw(); + ~SetOptionCommand() throw() {} + std::string getFlag() const throw(); + SExpr getSExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class SetOptionCommand */ class CVC4_PUBLIC GetOptionCommand : public Command { @@ -318,35 +469,39 @@ protected: std::string d_flag; std::string d_result; public: - GetOptionCommand(std::string flag); - std::string getFlag() const; - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + GetOptionCommand(std::string flag) throw(); + ~GetOptionCommand() throw() {} + std::string getFlag() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetOptionCommand */ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { private: std::vector<DatatypeType> d_datatypes; public: - DatatypeDeclarationCommand(const DatatypeType& datatype); - DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes); - const std::vector<DatatypeType>& getDatatypes() const; - void invoke(SmtEngine* smtEngine); + DatatypeDeclarationCommand(const DatatypeType& datatype) throw(); + ~DatatypeDeclarationCommand() throw() {} + DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw(); + const std::vector<DatatypeType>& getDatatypes() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DatatypeDeclarationCommand */ class CVC4_PUBLIC QuitCommand : public Command { public: - QuitCommand(); - void invoke(SmtEngine* smtEngine); + QuitCommand() throw(); + ~QuitCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); };/* class QuitCommand */ class CVC4_PUBLIC CommentCommand : public Command { std::string d_comment; public: - CommentCommand(std::string comment); - std::string getComment() const; - void invoke(SmtEngine* smtEngine); + CommentCommand(std::string comment) throw(); + ~CommentCommand() throw() {} + std::string getComment() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class CommentCommand */ class CVC4_PUBLIC CommandSequence : public Command { @@ -356,27 +511,28 @@ private: /** Next command to be executed */ unsigned int d_index; public: - CommandSequence(); - ~CommandSequence(); + CommandSequence() throw(); + ~CommandSequence() throw(); - void addCommand(Command* cmd); + void addCommand(Command* cmd) throw(); - void invoke(SmtEngine* smtEngine); - void invoke(SmtEngine* smtEngine, std::ostream& out); + void invoke(SmtEngine* smtEngine) throw(); + void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); typedef std::vector<Command*>::iterator iterator; typedef std::vector<Command*>::const_iterator const_iterator; - const_iterator begin() const; - const_iterator end() const; + const_iterator begin() const throw(); + const_iterator end() const throw(); - iterator begin(); - iterator end(); + iterator begin() throw(); + iterator end() throw(); };/* class CommandSequence */ class CVC4_PUBLIC DeclarationSequence : public CommandSequence { public: + ~DeclarationSequence() throw() {} };/* class DeclarationSequence */ }/* CVC4 namespace */ |