diff options
Diffstat (limited to 'src/util/command.h')
-rw-r--r-- | src/util/command.h | 44 |
1 files changed, 12 insertions, 32 deletions
diff --git a/src/util/command.h b/src/util/command.h index c65429fdb..ce137896a 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -16,7 +16,6 @@ #include "cvc4_config.h" #include "expr/expr.h" -#include "util/result.h" namespace CVC4 { class SmtEngine; @@ -25,15 +24,14 @@ namespace CVC4 { }/* CVC4 namespace */ namespace std { -inline std::ostream& operator<<(std::ostream&, const CVC4::Command*) CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC; + std::ostream& operator<<(std::ostream&, const CVC4::Command&) CVC4_PUBLIC; } namespace CVC4 { class CVC4_PUBLIC Command { public: - virtual Result invoke(CVC4::SmtEngine* smt_engine) = 0; + virtual void invoke(CVC4::SmtEngine* smt_engine) = 0; virtual ~Command() {}; virtual void toString(std::ostream&) const = 0; };/* class Command */ @@ -41,8 +39,8 @@ public: class CVC4_PUBLIC EmptyCommand : public Command { public: EmptyCommand(); - Result invoke(CVC4::SmtEngine* smt_engine); - void toString(std::ostream& out) const { out << "EmptyCommand"; } + void invoke(CVC4::SmtEngine* smt_engine); + void toString(std::ostream& out) const; };/* class EmptyCommand */ @@ -51,8 +49,8 @@ protected: Expr d_expr; public: AssertCommand(const Expr& e); - Result invoke(CVC4::SmtEngine* smt_engine); - void toString(std::ostream& out) const { out << "Assert(" << d_expr << ")"; } + void invoke(CVC4::SmtEngine* smt_engine); + void toString(std::ostream& out) const; };/* class AssertCommand */ @@ -60,8 +58,8 @@ class CVC4_PUBLIC CheckSatCommand : public Command { public: CheckSatCommand(); CheckSatCommand(const Expr& e); - Result invoke(SmtEngine* smt); - void toString(std::ostream& out) const { out << "CheckSat(" << d_expr << ")"; } + void invoke(SmtEngine* smt); + void toString(std::ostream& out) const; protected: Expr d_expr; };/* class CheckSatCommand */ @@ -70,8 +68,8 @@ protected: class CVC4_PUBLIC QueryCommand : public Command { public: QueryCommand(const Expr& e); - Result invoke(SmtEngine* smt); - void toString(std::ostream& out) const { out << "Query(" << d_expr << ")"; } + void invoke(SmtEngine* smt); + void toString(std::ostream& out) const; protected: Expr d_expr; };/* class QueryCommand */ @@ -80,21 +78,10 @@ protected: class CVC4_PUBLIC CommandSequence : public Command { public: CommandSequence(); - CommandSequence(Command* cmd); ~CommandSequence(); - Result invoke(SmtEngine* smt); + void invoke(SmtEngine* smt); void addCommand(Command* cmd); - void toString(std::ostream& out) const { - out << "CommandSequence("; - for(std::vector<Command*>::const_iterator i = d_command_sequence.begin(); - i != d_command_sequence.end(); - ++i) { - out << *i; - if(i != d_command_sequence.end()) - out << " ; "; - } - out << ")"; - } + void toString(std::ostream& out) const; private: /** All the commands to be executed (in sequence) */ std::vector<Command*> d_command_sequence; @@ -104,11 +91,4 @@ private: }/* CVC4 namespace */ -inline std::ostream& std::operator<<(std::ostream& out, const CVC4::Command* c) { - if(c) - c->toString(out); - else out << "(null)"; - return out; -} - #endif /* __CVC4__COMMAND_H */ |