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

1 files changed, 38 insertions, 6 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);
+}