1 files changed, 33 insertions, 33 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 */