Addressed many of the concerns of bug 10 (build system code review).

Some parts split into other bugs: 19, 20, 21.

Addressed concerns of bug 11 (util package code review).

Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers

Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main().  Silenced MiniSat when
verbosity is not requested.

1 files changed, 181 insertions, 17 deletions

diff --git a/src/util/command.h b/src/util/command.h
index 57edfea01..15104a5ea 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -10,26 +10,30 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Implementation of the command pattern on SmtEngines.  Generated by
- ** the parser.
+ ** Implementation of the command pattern on SmtEngines.  Command
+ ** objects are generated by the parser (typically) to implement the
+ ** commands in parsed input (see Parser::parseNextCommand()), or by
+ ** client code.
  **/
 
 #ifndef __CVC4__COMMAND_H
 #define __CVC4__COMMAND_H
 
 #include <iostream>
+#include <sstream>
+#include <string>
+#include <vector>
 
 #include "cvc4_config.h"
 #include "expr/expr.h"
+#include "util/result.h"
 
 namespace CVC4 {
-  class SmtEngine;
-  class Command;
-}/* CVC4 namespace */
 
-namespace CVC4 {
+class SmtEngine;
+class Command;
 
-std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
 
 class CVC4_PUBLIC Command {
@@ -49,7 +53,6 @@ private:
   std::string d_name;
 };/* class EmptyCommand */
 
-
 class CVC4_PUBLIC AssertCommand : public Command {
 public:
   AssertCommand(const BoolExpr& e);
@@ -59,7 +62,6 @@ protected:
   BoolExpr d_expr;
 };/* class AssertCommand */
 
-
 class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
 public:
   DeclarationCommand(const std::vector<std::string>& ids);
@@ -73,22 +75,24 @@ public:
   CheckSatCommand();
   CheckSatCommand(const BoolExpr& e);
   void invoke(SmtEngine* smt);
+  Result getResult();
   void toStream(std::ostream& out) const;
 protected:
   BoolExpr d_expr;
+  Result d_result;
 };/* class CheckSatCommand */
 
-
 class CVC4_PUBLIC QueryCommand : public Command {
 public:
   QueryCommand(const BoolExpr& e);
   void invoke(SmtEngine* smt);
+  Result getResult();
   void toStream(std::ostream& out) const;
 protected:
   BoolExpr d_expr;
+  Result d_result;
 };/* class QueryCommand */
 
-
 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
 public:
   /** The status an SMT benchmark can have */
@@ -105,7 +109,11 @@ public:
   void toStream(std::ostream& out) const;
 protected:
   BenchmarkStatus d_status;
-};/* class QueryCommand */
+};/* class SetBenchmarkStatusCommand */
+
+inline std::ostream& operator<<(std::ostream& out,
+                                SetBenchmarkStatusCommand::BenchmarkStatus bs)
+  CVC4_PUBLIC;
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
 public:
@@ -114,9 +122,7 @@ public:
   void toStream(std::ostream& out) const;
 protected:
   std::string d_logic;
-};/* class QueryCommand */
-
-
+};/* class SetBenchmarkLogicCommand */
 
 class CVC4_PUBLIC CommandSequence : public Command {
 public:
@@ -125,13 +131,171 @@ public:
   void invoke(SmtEngine* smt);
   void addCommand(Command* cmd);
   void toStream(std::ostream& out) const;
+
+  typedef std::vector<Command*>::iterator iterator;
+  typedef std::vector<Command*>::const_iterator const_iterator;
+
+  const_iterator begin() const { return d_commandSequence.begin(); }
+  const_iterator end() const { return d_commandSequence.end(); }
+
+  iterator begin() { return d_commandSequence.begin(); }
+  iterator end() { return d_commandSequence.end(); }
+
 private:
   /** All the commands to be executed (in sequence) */
-  std::vector<Command*> d_command_sequence;
+  std::vector<Command*> d_commandSequence;
   /** Next command to be executed */
-  unsigned int d_last_index;
+  unsigned int d_index;
 };/* class CommandSequence */
 
 }/* CVC4 namespace */
 
+/* =========== inline function definitions =========== */
+
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+inline std::ostream& operator<<(std::ostream& out, const Command& c) {
+  c.toStream(out);
+  return out;
+}
+
+/* class Command */
+
+inline std::string Command::toString() const {
+  std::stringstream ss;
+  toStream(ss);
+  return ss.str();
+}
+
+/* class EmptyCommand */
+
+inline EmptyCommand::EmptyCommand(std::string name) :
+  d_name(name) {
+}
+
+inline void EmptyCommand::invoke(SmtEngine* smt_engine) {
+}
+
+inline void EmptyCommand::toStream(std::ostream& out) const {
+  out << "EmptyCommand(" << d_name << ")";
+}
+
+/* class AssertCommand */
+
+inline AssertCommand::AssertCommand(const BoolExpr& e) :
+  d_expr(e) {
+}
+
+inline void AssertCommand::invoke(SmtEngine* smt_engine) {
+  smt_engine->assertFormula(d_expr);
+}
+
+inline void AssertCommand::toStream(std::ostream& out) const {
+  out << "Assert(" << d_expr << ")";
+}
+
+/* class CheckSatCommand */
+
+inline CheckSatCommand::CheckSatCommand() {
+}
+
+inline CheckSatCommand::CheckSatCommand(const BoolExpr& e) :
+  d_expr(e) {
+}
+
+inline void CheckSatCommand::invoke(SmtEngine* smt_engine) {
+  d_result = smt_engine->checkSat(d_expr);
+}
+
+inline Result CheckSatCommand::getResult() {
+  return d_result;
+}
+
+/* class QueryCommand */
+
+inline QueryCommand::QueryCommand(const BoolExpr& e) :
+  d_expr(e) {
+}
+
+inline void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) {
+  d_result = smt_engine->query(d_expr);
+}
+
+inline Result QueryCommand::getResult() {
+  return d_result;
+}
+
+inline void QueryCommand::toStream(std::ostream& out) const {
+  out << "Query(";
+  d_expr.printAst(out, 0);
+  out << ")";
+}
+
+/* class CommandSequence */
+
+inline CommandSequence::CommandSequence() :
+  d_index(0) {
+}
+
+inline void CommandSequence::addCommand(Command* cmd) {
+  d_commandSequence.push_back(cmd);
+}
+
+/* class DeclarationCommand */
+
+inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) :
+  d_declaredSymbols(ids) {
+}
+
+/* class SetBenchmarkStatusCommand */
+
+inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus s) :
+  d_status(s) {
+}
+
+inline void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) {
+  // FIXME: TODO: something to be done with the status
+}
+
+inline void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
+  out << "SetBenchmarkStatus(" << d_status << ")";
+}
+
+/* class SetBenchmarkLogicCommand */
+
+inline SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string l) :
+  d_logic(l) {
+}
+
+inline void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) {
+  // FIXME: TODO: something to be done with the logic
+}
+
+inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
+  out << "SetBenchmarkLogic(" << d_logic << ")";
+}
+
+/* output stream insertion operator for benchmark statuses */
+inline std::ostream& operator<<(std::ostream& out,
+                                SetBenchmarkStatusCommand::BenchmarkStatus bs) {
+  switch(bs) {
+
+  case SetBenchmarkStatusCommand::SMT_SATISFIABLE:
+    return out << "sat";
+
+  case SetBenchmarkStatusCommand::SMT_UNSATISFIABLE:
+    return out << "unsat";
+
+  case SetBenchmarkStatusCommand::SMT_UNKNOWN:
+    return out << "unknown";
+
+  default:
+    return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]";
+  }
+}
+
+}/* CVC4 namespace */
+
 #endif /* __CVC4__COMMAND_H */