parsing/expr/command/result/various other fixes

4 files changed, 159 insertions, 102 deletions

diff --git a/src/util/command.cpp b/src/util/command.cpp
index 35db79a0d..9e541574a 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -5,73 +5,73 @@
  *      Author: dejan
  */
 
-#include "command.h"
+#include "util/command.h"
+#include "smt/smt_engine.h"
+#include "util/result.h"
 
-using namespace CVC4;
+namespace CVC4 {
 
-void EmptyCommand::invoke(SmtEngine* smt_engine) { }
+EmptyCommand::EmptyCommand() {
+}
+
+Result EmptyCommand::invoke(SmtEngine* smt_engine) {
+  return Result::VALIDITY_UNKNOWN;
+}
 
 AssertCommand::AssertCommand(const Expr& e) :
-  d_expr(e)
-{
+  d_expr(e) {
 }
 
-void AssertCommand::invoke(SmtEngine* smt_engine)
-{
-  smt_engine->assert(d_expr);
+Result AssertCommand::invoke(SmtEngine* smt_engine) {
+  return smt_engine->assert(d_expr);
 }
 
-CheckSatCommand::CheckSatCommand()
-{
+CheckSatCommand::CheckSatCommand() :
+  d_expr(Expr::null()) {
 }
 
 CheckSatCommand::CheckSatCommand(const Expr& e) :
-  d_expr(e)
-{
+  d_expr(e) {
 }
 
-void CheckSatCommand::invoke(SmtEngine* smt_engine)
-{
-  smt_engine->checkSat(d_expr);
+Result CheckSatCommand::invoke(SmtEngine* smt_engine) {
+  return smt_engine->checkSat(d_expr);
 }
 
 QueryCommand::QueryCommand(const Expr& e) :
-  d_expr(e)
-{
+  d_expr(e) {
 }
 
-void QueryCommand::invoke(CVC4::SmtEngine* smt_engine)
-{
-  smt_engine->query(d_expr);
+Result QueryCommand::invoke(CVC4::SmtEngine* smt_engine) {
+  return smt_engine->query(d_expr);
 }
 
 CommandSequence::CommandSequence() :
-  d_last_index(0)
-{
+  d_last_index(0) {
 }
 
 CommandSequence::CommandSequence(Command* cmd) :
-  d_last_index(0)
-{
+  d_last_index(0) {
   addCommand(cmd);
 }
 
 
-CommandSequence::~CommandSequence()
-{
-  for (unsigned i = d_last_index; i < d_command_sequence.size(); i++)
+CommandSequence::~CommandSequence() {
+  for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i)
     delete d_command_sequence[i];
 }
 
-void CommandSequence::invoke(SmtEngine* smt_engine)
-{
-  for (; d_last_index < d_command_sequence.size(); d_last_index++) {
-    d_command_sequence[d_last_index]->invoke(smt_engine);
+Result CommandSequence::invoke(SmtEngine* smt_engine) {
+  Result r = Result::VALIDITY_UNKNOWN;
+  for(; d_last_index < d_command_sequence.size(); ++d_last_index) {
+    r = d_command_sequence[d_last_index]->invoke(smt_engine);
     delete d_command_sequence[d_last_index];
   }
+  return r;
 }
 
-void CommandSequence::addCommand(Command* cmd)
-{
+void CommandSequence::addCommand(Command* cmd) {
   d_command_sequence.push_back(cmd);
 }
+
+}/* CVC4 namespace */
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 */
diff --git a/src/util/output.h b/src/util/output.h
index 4d3752849..21b7b6e4c 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -20,7 +20,6 @@
 
 namespace CVC4 {
 
-
 class Debug {
   std::set<std::string> d_tags;
   std::ostream &d_out;
@@ -30,19 +29,23 @@ public:
   static void operator()(const char* tag, std::string);
   static void operator()(string tag, const char*);
   static void operator()(string tag, std::string);
+  static void operator()(const char*);// Yeting option
+  static void operator()(std::string);// Yeting option
 
   static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
   static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
   static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
   static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3)));
+  // Yeting option not possible here
 
   static std::ostream& operator()(const char* tag);
   static std::ostream& operator()(std::string tag);
+  static std::ostream& operator()();// Yeting option
 
-  static void on (const char* tag) { d_tags.insert(std::string(tag)); };
-  static void on (std::string tag) { d_tags.insert(tag);              };
-  static void off(const char* tag) { d_tags.erase (std::string(tag)); };
-  static void off(std::string tag) { d_tags.erase (tag);              };
+  static void on (const char* tag) { d_tags.insert(std::string(tag)); }
+  static void on (std::string tag) { d_tags.insert(tag);              }
+  static void off(const char* tag) { d_tags.erase (std::string(tag)); }
+  static void off(std::string tag) { d_tags.erase (tag);              }
 
   static void setStream(std::ostream& os) { d_out = os; }
 };/* class Debug */
diff --git a/src/util/result.h b/src/util/result.h
index 1e2b61738..8d9b93a1e 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -50,9 +50,11 @@ private:
   enum Validity d_validity;
   enum { TYPE_SAT, TYPE_VALIDITY } d_which;
 
+  friend std::ostream& CVC4::operator<<(std::ostream& out, Result r);
+
 public:
-  Result(enum SAT);
-  Result(enum Validity);
+  Result(enum SAT s) : d_sat(s), d_validity(VALIDITY_UNKNOWN), d_which(TYPE_SAT) {}
+  Result(enum Validity v) : d_sat(SAT_UNKNOWN), d_validity(v), d_which(TYPE_VALIDITY) {}
 
   enum SAT isSAT();
   enum Validity isValid();
@@ -60,6 +62,24 @@ public:
 
 };/* class Result */
 
+inline std::ostream& operator<<(std::ostream& out, Result r) {
+  if(r.d_which == Result::TYPE_SAT) {
+    switch(r.d_sat) {
+    case Result::UNSAT: out << "UNSAT"; break;
+    case Result::SAT: out << "SAT"; break;
+    case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break;
+    }
+  } else {
+    switch(r.d_validity) {
+    case Result::INVALID: out << "INVALID"; break;
+    case Result::VALID: out << "VALID"; break;
+    case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break;
+    }
+  }
+
+  return out;
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__RESULT_H */