Added an EmptyCommand and a CommandSequence commands and changed the parser a bit.

2 files changed, 61 insertions, 8 deletions

diff --git a/src/util/command.cpp b/src/util/command.cpp
index b728a2228..35db79a0d 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -9,12 +9,14 @@
 
 using namespace CVC4;
 
+void EmptyCommand::invoke(SmtEngine* smt_engine) { }
+
 AssertCommand::AssertCommand(const Expr& e) :
   d_expr(e)
 {
 }
 
-void AssertCommand::invoke(CVC4::SmtEngine* smt_engine)
+void AssertCommand::invoke(SmtEngine* smt_engine)
 {
   smt_engine->assert(d_expr);
 }
@@ -23,18 +25,18 @@ CheckSatCommand::CheckSatCommand()
 {
 }
 
-CheckSatCommand::CheckSatCommand(const Expr& e):
-    d_expr(e)
+CheckSatCommand::CheckSatCommand(const Expr& e) :
+  d_expr(e)
 {
 }
 
-void CheckSatCommand::invoke(CVC4::SmtEngine* smt_engine)
+void CheckSatCommand::invoke(SmtEngine* smt_engine)
 {
   smt_engine->checkSat(d_expr);
 }
 
-QueryCommand::QueryCommand(const Expr& e):
-    d_expr(e)
+QueryCommand::QueryCommand(const Expr& e) :
+  d_expr(e)
 {
 }
 
@@ -43,3 +45,33 @@ void QueryCommand::invoke(CVC4::SmtEngine* smt_engine)
   smt_engine->query(d_expr);
 }
 
+CommandSequence::CommandSequence() :
+  d_last_index(0)
+{
+}
+
+CommandSequence::CommandSequence(Command* cmd) :
+  d_last_index(0)
+{
+  addCommand(cmd);
+}
+
+
+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);
+    delete d_command_sequence[d_last_index];
+  }
+}
+
+void CommandSequence::addCommand(Command* cmd)
+{
+  d_command_sequence.push_back(cmd);
+}
diff --git a/src/util/command.h b/src/util/command.h
index 745f6f5e2..c6778f34a 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -12,7 +12,7 @@
 #ifndef __CVC4__COMMAND_H
 #define __CVC4__COMMAND_H
 
-#include "expr/expr.h"
+#include "cvc4.h"
 
 namespace CVC4
 {
@@ -23,7 +23,13 @@ class Command
 {
   public:
     virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
-    virtual ~Command() {}
+    virtual ~Command() {};
+};
+
+class EmptyCommand : public Command
+{
+  public:
+    virtual void invoke(CVC4::SmtEngine* smt_engine);
 };
 
 class AssertCommand: public Command
@@ -54,6 +60,21 @@ class QueryCommand: public Command
     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;
+};
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__COMMAND_H */