merge from symmetry branch

2 files changed, 35 insertions, 143 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 8d6748e54..2783e8eaa 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -27,21 +27,26 @@
 #include "smt/bad_option_exception.h"
 #include "util/output.h"
 #include "util/sexpr.h"
+#include "expr/node.h"
+#include "printer/printer.h"
 
 using namespace std;
 
 namespace CVC4 {
 
 std::ostream& operator<<(std::ostream& out, const Command& c) {
-  c.toStream(out);
+  c.toStream(out,
+             Node::setdepth::getDepth(out),
+             Node::printtypes::getPrintTypes(out),
+             Node::setlanguage::getLanguage(out));
   return out;
 }
 
-ostream& operator<<(ostream& out, const Command* command) {
-  if(command == NULL) {
+ostream& operator<<(ostream& out, const Command* c) {
+  if(c == NULL) {
     out << "null";
   } else {
-    command->toStream(out);
+    out << *c;
   }
   return out;
 }
@@ -59,6 +64,11 @@ std::string Command::toString() const {
   return ss.str();
 }
 
+void Command::toStream(std::ostream& out, int toDepth, bool types,
+                       OutputLanguage language) const {
+  Printer::getPrinter(language)->toStream(out, this, toDepth, types);
+}
+
 void Command::printResult(std::ostream& out) const {
 }
 
@@ -72,10 +82,6 @@ void EmptyCommand::invoke(SmtEngine* smtEngine) {
   /* empty commands have no implementation */
 }
 
-void EmptyCommand::toStream(std::ostream& out) const {
-  out << "EmptyCommand(" << d_name << ")";
-}
-
 /* class AssertCommand */
 
 AssertCommand::AssertCommand(const BoolExpr& e) :
@@ -86,30 +92,18 @@ void AssertCommand::invoke(SmtEngine* smtEngine) {
   smtEngine->assertFormula(d_expr);
 }
 
-void AssertCommand::toStream(std::ostream& out) const {
-  out << "Assert(" << d_expr << ")";
-}
-
 /* class PushCommand */
 
 void PushCommand::invoke(SmtEngine* smtEngine) {
   smtEngine->push();
 }
 
-void PushCommand::toStream(std::ostream& out) const {
-  out << "Push()";
-}
-
 /* class PopCommand */
 
 void PopCommand::invoke(SmtEngine* smtEngine) {
   smtEngine->pop();
 }
 
-void PopCommand::toStream(std::ostream& out) const {
-  out << "Pop()";
-}
-
 /* class CheckSatCommand */
 
 CheckSatCommand::CheckSatCommand(const BoolExpr& expr) :
@@ -120,14 +114,6 @@ void CheckSatCommand::invoke(SmtEngine* smtEngine) {
   d_result = smtEngine->checkSat(d_expr);
 }
 
-void CheckSatCommand::toStream(std::ostream& out) const {
-  if(d_expr.isNull()) {
-    out << "CheckSat()";
-  } else {
-    out << "CheckSat(" << d_expr << ")";
-  }
-}
-
 Result CheckSatCommand::getResult() const {
   return d_result;
 }
@@ -154,19 +140,11 @@ void QueryCommand::printResult(std::ostream& out) const {
   out << d_result << endl;
 }
 
-void QueryCommand::toStream(std::ostream& out) const {
-  out << "Query(" << d_expr << ')';
-}
-
 /* class QuitCommand */
 
 QuitCommand::QuitCommand() {
 }
 
-void QuitCommand::toStream(std::ostream& out) const {
-  out << "Quit()" << endl;
-}
-
 /* class CommandSequence */
 
 CommandSequence::CommandSequence() :
@@ -197,14 +175,6 @@ void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) {
   }
 }
 
-void CommandSequence::toStream(std::ostream& out) const {
-  out << "CommandSequence[" << endl;
-  for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
-    out << *d_commandSequence[i] << endl;
-  }
-  out << "]";
-}
-
 /* class DeclarationCommand */
 
 DeclarationCommand::DeclarationCommand(const std::string& id, Type t) :
@@ -225,14 +195,6 @@ Type DeclarationCommand::getDeclaredType() const {
   return d_type;
 }
 
-void DeclarationCommand::toStream(std::ostream& out) const {
-  out << "Declare([";
-  copy( d_declaredSymbols.begin(), d_declaredSymbols.end() - 1,
-        ostream_iterator<string>(out, ", ") );
-  out << d_declaredSymbols.back();
-  out << "])";
-}
-
 /* class DefineFunctionCommand */
 
 DefineFunctionCommand::DefineFunctionCommand(Expr func,
@@ -247,16 +209,6 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
   smtEngine->defineFunction(d_func, d_formals, d_formula);
 }
 
-void DefineFunctionCommand::toStream(std::ostream& out) const {
-  out << "DefineFunction( \"" << d_func << "\", [";
-  if(d_formals.size() > 0) {
-    copy( d_formals.begin(), d_formals.end() - 1,
-          ostream_iterator<Expr>(out, ", ") );
-    out << d_formals.back();
-  }
-  out << "], << " << d_formula << " >> )";
-}
-
 /* class DefineFunctionCommand */
 
 DefineNamedFunctionCommand::DefineNamedFunctionCommand(Expr func,
@@ -273,12 +225,6 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) {
   }
 }
 
-void DefineNamedFunctionCommand::toStream(std::ostream& out) const {
-  out << "DefineNamedFunction( ";
-  this->DefineFunctionCommand::toStream(out);
-  out << " )";
-}
-
 /* class Simplify */
 
 SimplifyCommand::SimplifyCommand(Expr term) :
@@ -286,7 +232,7 @@ SimplifyCommand::SimplifyCommand(Expr term) :
 }
 
 void SimplifyCommand::invoke(SmtEngine* smtEngine) {
-#warning TODO: what is this
+  d_result = smtEngine->simplify(d_term);
 }
 
 Expr SimplifyCommand::getResult() const {
@@ -297,10 +243,6 @@ void SimplifyCommand::printResult(std::ostream& out) const {
   out << d_result << endl;
 }
 
-void SimplifyCommand::toStream(std::ostream& out) const {
-  out << "Simplify( << " << d_term << " >> )";
-}
-
 /* class GetValueCommand */
 
 GetValueCommand::GetValueCommand(Expr term) :
@@ -320,10 +262,6 @@ void GetValueCommand::printResult(std::ostream& out) const {
   out << d_result << endl;
 }
 
-void GetValueCommand::toStream(std::ostream& out) const {
-  out << "GetValue( << " << d_term << " >> )";
-}
-
 /* class GetAssignmentCommand */
 
 GetAssignmentCommand::GetAssignmentCommand() {
@@ -341,10 +279,6 @@ void GetAssignmentCommand::printResult(std::ostream& out) const {
   out << d_result << endl;
 }
 
-void GetAssignmentCommand::toStream(std::ostream& out) const {
-  out << "GetAssignment()";
-}
-
 /* class GetAssertionsCommand */
 
 GetAssertionsCommand::GetAssertionsCommand() {
@@ -365,10 +299,6 @@ void GetAssertionsCommand::printResult(std::ostream& out) const {
   out << d_result;
 }
 
-void GetAssertionsCommand::toStream(std::ostream& out) const {
-  out << "GetAssertions()";
-}
-
 /* class SetBenchmarkStatusCommand */
 
 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
@@ -390,10 +320,6 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
   }
 }
 
-void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
-  out << "SetBenchmarkStatus(" << d_status << ")";
-}
-
 /* class SetBenchmarkLogicCommand */
 
 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) :
@@ -409,10 +335,6 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
   }
 }
 
-void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
-  out << "SetBenchmarkLogic(" << d_logic << ")";
-}
-
 /* class SetInfoCommand */
 
 SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) :
@@ -441,10 +363,6 @@ void SetInfoCommand::printResult(std::ostream& out) const {
   }
 }
 
-void SetInfoCommand::toStream(std::ostream& out) const {
-  out << "SetInfo(" << d_flag << ", " << d_sexpr << ")";
-}
-
 /* class GetInfoCommand */
 
 GetInfoCommand::GetInfoCommand(std::string flag) :
@@ -471,10 +389,6 @@ void GetInfoCommand::printResult(std::ostream& out) const {
   }
 }
 
-void GetInfoCommand::toStream(std::ostream& out) const {
-  out << "GetInfo(" << d_flag << ")";
-}
-
 /* class SetOptionCommand */
 
 SetOptionCommand::SetOptionCommand(std::string flag, SExpr& sexpr) :
@@ -503,10 +417,6 @@ void SetOptionCommand::printResult(std::ostream& out) const {
   }
 }
 
-void SetOptionCommand::toStream(std::ostream& out) const {
-  out << "SetOption(" << d_flag << ", " << d_sexpr << ")";
-}
-
 /* class GetOptionCommand */
 
 GetOptionCommand::GetOptionCommand(std::string flag) :
@@ -531,10 +441,6 @@ void GetOptionCommand::printResult(std::ostream& out) const {
   }
 }
 
-void GetOptionCommand::toStream(std::ostream& out) const {
-  out << "GetOption(" << d_flag << ")";
-}
-
 /* class DatatypeDeclarationCommand */
 
 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) :
@@ -553,17 +459,6 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
   //smtEngine->addDatatypeDefinitions(d_datatype);
 }
 
-void DatatypeDeclarationCommand::toStream(std::ostream& out) const {
-  out << "DatatypeDeclarationCommand([";
-  for(vector<DatatypeType>::const_iterator i = d_datatypes.begin(),
-        i_end = d_datatypes.end();
-      i != i_end;
-      ++i) {
-    out << *i << ";" << endl;
-  }
-  out << "])";
-}
-
 /* output stream insertion operator for benchmark statuses */
 std::ostream& operator<<(std::ostream& out,
                          BenchmarkStatus status) {
diff --git a/src/expr/command.h b/src/expr/command.h
index d0b72c3dd..50d382038 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -62,7 +62,8 @@ public:
   virtual void invoke(SmtEngine* smtEngine) = 0;
   virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
   virtual ~Command() {};
-  virtual void toStream(std::ostream&) const = 0;
+  virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+                        OutputLanguage language = language::output::LANG_AST) const;
   std::string toString() const;
   virtual void printResult(std::ostream& out) const;
 };/* class Command */
@@ -77,7 +78,7 @@ protected:
 public:
   EmptyCommand(std::string name = "");
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  std::string getName() const { return d_name; }
 };/* class EmptyCommand */
 
 class CVC4_PUBLIC AssertCommand : public Command {
@@ -86,19 +87,17 @@ protected:
 public:
   AssertCommand(const BoolExpr& e);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  BoolExpr getExpr() const { return d_expr; }
 };/* class AssertCommand */
 
 class CVC4_PUBLIC PushCommand : public Command {
 public:
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
 };/* class PushCommand */
 
 class CVC4_PUBLIC PopCommand : public Command {
 public:
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
 };/* class PopCommand */
 
 class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
@@ -110,7 +109,6 @@ public:
   DeclarationCommand(const std::vector<std::string>& ids, Type t);
   const std::vector<std::string>& getDeclaredSymbols() const;
   Type getDeclaredType() const;
-  void toStream(std::ostream& out) const;
 };/* class DeclarationCommand */
 
 class CVC4_PUBLIC DefineFunctionCommand : public Command {
@@ -123,7 +121,9 @@ public:
                         const std::vector<Expr>& formals,
                         Expr formula);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  Expr getFunction() const { return d_func; }
+  const std::vector<Expr>& getFormals() const { return d_formals; }
+  Expr getFormula() const { return d_formula; }
 };/* class DefineFunctionCommand */
 
 /**
@@ -137,7 +137,6 @@ public:
                              const std::vector<Expr>& formals,
                              Expr formula);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
 };/* class DefineNamedFunctionCommand */
 
 class CVC4_PUBLIC CheckSatCommand : public Command {
@@ -147,9 +146,9 @@ protected:
 public:
   CheckSatCommand(const BoolExpr& expr);
   void invoke(SmtEngine* smtEngine);
+  BoolExpr getExpr() const { return d_expr; }
   Result getResult() const;
   void printResult(std::ostream& out) const;
-  void toStream(std::ostream& out) const;
 };/* class CheckSatCommand */
 
 class CVC4_PUBLIC QueryCommand : public Command {
@@ -159,9 +158,9 @@ protected:
 public:
   QueryCommand(const BoolExpr& e);
   void invoke(SmtEngine* smtEngine);
+  BoolExpr getExpr() const { return d_expr; }
   Result getResult() const;
   void printResult(std::ostream& out) const;
-  void toStream(std::ostream& out) const;
 };/* class QueryCommand */
 
 // this is TRANSFORM in the CVC presentation language
@@ -172,9 +171,9 @@ protected:
 public:
   SimplifyCommand(Expr term);
   void invoke(SmtEngine* smtEngine);
+  Expr getTerm() const { return d_term; }
   Expr getResult() const;
   void printResult(std::ostream& out) const;
-  void toStream(std::ostream& out) const;
 };/* class SimplifyCommand */
 
 class CVC4_PUBLIC GetValueCommand : public Command {
@@ -184,9 +183,9 @@ protected:
 public:
   GetValueCommand(Expr term);
   void invoke(SmtEngine* smtEngine);
+  Expr getTerm() const { return d_term; }
   Expr getResult() const;
   void printResult(std::ostream& out) const;
-  void toStream(std::ostream& out) const;
 };/* class GetValueCommand */
 
 class CVC4_PUBLIC GetAssignmentCommand : public Command {
@@ -197,7 +196,6 @@ public:
   void invoke(SmtEngine* smtEngine);
   SExpr getResult() const;
   void printResult(std::ostream& out) const;
-  void toStream(std::ostream& out) const;
 };/* class GetAssignmentCommand */
 
 class CVC4_PUBLIC GetAssertionsCommand : public Command {
@@ -208,7 +206,6 @@ public:
   void invoke(SmtEngine* smtEngine);
   std::string getResult() const;
   void printResult(std::ostream& out) const;
-  void toStream(std::ostream& out) const;
 };/* class GetAssertionsCommand */
 
 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
@@ -218,7 +215,7 @@ protected:
 public:
   SetBenchmarkStatusCommand(BenchmarkStatus status);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  BenchmarkStatus getStatus() const { return d_status; }
 };/* class SetBenchmarkStatusCommand */
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
@@ -228,7 +225,7 @@ protected:
 public:
   SetBenchmarkLogicCommand(std::string logic);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  std::string getLogic() const { return d_logic; }
 };/* class SetBenchmarkLogicCommand */
 
 class CVC4_PUBLIC SetInfoCommand : public Command {
@@ -239,7 +236,8 @@ protected:
 public:
   SetInfoCommand(std::string flag, SExpr& sexpr);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  std::string getFlag() const { return d_flag; }
+  SExpr getSExpr() const { return d_sexpr; }
   std::string getResult() const;
   void printResult(std::ostream& out) const;
 };/* class SetInfoCommand */
@@ -251,7 +249,7 @@ protected:
 public:
   GetInfoCommand(std::string flag);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  std::string getFlag() const { return d_flag; }
   std::string getResult() const;
   void printResult(std::ostream& out) const;
 };/* class GetInfoCommand */
@@ -264,7 +262,8 @@ protected:
 public:
   SetOptionCommand(std::string flag, SExpr& sexpr);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  std::string getFlag() const { return d_flag; }
+  SExpr getSExpr() const { return d_sexpr; }
   std::string getResult() const;
   void printResult(std::ostream& out) const;
 };/* class SetOptionCommand */
@@ -276,7 +275,7 @@ protected:
 public:
   GetOptionCommand(std::string flag);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  std::string getFlag() const { return d_flag; }
   std::string getResult() const;
   void printResult(std::ostream& out) const;
 };/* class GetOptionCommand */
@@ -288,13 +287,12 @@ public:
   DatatypeDeclarationCommand(const DatatypeType& datatype);
   DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes);
   void invoke(SmtEngine* smtEngine);
-  void toStream(std::ostream& out) const;
+  const std::vector<DatatypeType>& getDatatypes() const { return d_datatypes; }
 };/* class DatatypeDeclarationCommand */
 
 class CVC4_PUBLIC QuitCommand : public EmptyCommand {
 public:
   QuitCommand();
-  void toStream(std::ostream& out) const;
 };/* class QuitCommand */
 
 class CVC4_PUBLIC CommandSequence : public Command {
@@ -309,7 +307,6 @@ public:
   void invoke(SmtEngine* smtEngine);
   void invoke(SmtEngine* smtEngine, std::ostream& out);
   void addCommand(Command* cmd);
-  void toStream(std::ostream& out) const;
 
   typedef std::vector<Command*>::iterator iterator;
   typedef std::vector<Command*>::const_iterator const_iterator;