1 files changed, 96 insertions, 62 deletions
diff --git a/src/util/command.h b/src/util/command.h
index c6778f34a..c65429fdb 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -12,69 +12,103 @@
 #ifndef __CVC4__COMMAND_H
 #define __CVC4__COMMAND_H
 
-#include "cvc4.h"
-
-namespace CVC4
-{
-
-class SmtEngine;
-
-class Command
-{
-  public:
-    virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
-    virtual ~Command() {};
-};
-
-class EmptyCommand : public Command
-{
-  public:
-    virtual void invoke(CVC4::SmtEngine* smt_engine);
-};
-
-class AssertCommand: public Command
-{
-  public:
-    AssertCommand(const Expr& e);
-    void invoke(CVC4::SmtEngine* smt_engine);
-  protected:
-    Expr d_expr;
-};
-
-class CheckSatCommand: public Command
-{
-  public:
-    CheckSatCommand();
-    CheckSatCommand(const Expr& e);
-    void invoke(CVC4::SmtEngine* smt);
-  protected:
-    Expr d_expr;
-};
-
-class QueryCommand: public Command
-{
-  public:
-    QueryCommand(const Expr& e);
-    void invoke(CVC4::SmtEngine* smt);
-  protected:
-    Expr d_expr;
-};
-
-class CommandSequence: public Command
-{
-  public:
-    CommandSequence();
-    CommandSequence(Command* cmd);
-    ~CommandSequence();
-    void invoke(CVC4::SmtEngine* smt);
-    void addCommand(Command* cmd);
-  private:
-    /** All the commands to be executed (in sequence) */
-    std::vector<Command*> d_command_sequence;
-    /** Next command to be executed */
-    unsigned int d_last_index;
-};
+#include <iostream>
+
+#include "cvc4_config.h"
+#include "expr/expr.h"
+#include "util/result.h"
+
+namespace CVC4 {
+  class SmtEngine;
+  class Command;
+  class Expr;
+}/* 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;
+}
+
+namespace CVC4 {
+
+class CVC4_PUBLIC Command {
+public:
+  virtual Result invoke(CVC4::SmtEngine* smt_engine) = 0;
+  virtual ~Command() {};
+  virtual void toString(std::ostream&) const = 0;
+};/* class Command */
+
+class CVC4_PUBLIC EmptyCommand : public Command {
+public:
+  EmptyCommand();
+  Result invoke(CVC4::SmtEngine* smt_engine);
+  void toString(std::ostream& out) const { out << "EmptyCommand"; }
+};/* class EmptyCommand */
+
+
+class CVC4_PUBLIC AssertCommand : public Command {
+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 << ")"; }
+};/* class AssertCommand */
+
+
+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 << ")"; }
+protected:
+  Expr d_expr;
+};/* class CheckSatCommand */
+
+
+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 << ")"; }
+protected:
+  Expr d_expr;
+};/* class QueryCommand */
+
+
+class CVC4_PUBLIC CommandSequence : public Command {
+public:
+  CommandSequence();
+  CommandSequence(Command* cmd);
+  ~CommandSequence();
+  Result 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 << ")";
+  }
+private:
+  /** All the commands to be executed (in sequence) */
+  std::vector<Command*> d_command_sequence;
+  /** Next command to be executed */
+  unsigned int d_last_index;
+};/* class CommandSequence */
 
 }/* 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 */