Commands and the eclipse C++ project settings.

2 files changed, 71 insertions, 45 deletions

diff --git a/src/util/command.cpp b/src/util/command.cpp
index db03a9189..b728a2228 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -1,18 +1,45 @@
-/*********************                                           -*- C++ -*-  */
-/** command.cpp
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- **/
+/*
+ * command.cpp
+ *
+ *  Created on: Nov 25, 2009
+ *      Author: dejan
+ */
 
-#include "util/command.h"
-#include "smt/smt_engine.h"
+#include "command.h"
 
-namespace CVC4 {
+using namespace CVC4;
 
+AssertCommand::AssertCommand(const Expr& e) :
+  d_expr(e)
+{
+}
+
+void AssertCommand::invoke(CVC4::SmtEngine* smt_engine)
+{
+  smt_engine->assert(d_expr);
+}
+
+CheckSatCommand::CheckSatCommand()
+{
+}
+
+CheckSatCommand::CheckSatCommand(const Expr& e):
+    d_expr(e)
+{
+}
+
+void CheckSatCommand::invoke(CVC4::SmtEngine* smt_engine)
+{
+  smt_engine->checkSat(d_expr);
+}
+
+QueryCommand::QueryCommand(const Expr& e):
+    d_expr(e)
+{
+}
+
+void QueryCommand::invoke(CVC4::SmtEngine* smt_engine)
+{
+  smt_engine->query(d_expr);
+}
 
-}/* CVC4 namespace */
diff --git a/src/util/command.h b/src/util/command.h
index 6de87c9f2..745f6f5e2 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -13,46 +13,45 @@
 #define __CVC4__COMMAND_H
 
 #include "expr/expr.h"
-#include "smt/smt_engine.h"
 
-namespace CVC4 {
+namespace CVC4
+{
 
-class Command {
-protected:
-  SmtEngine* d_smt;
+class SmtEngine;
 
-public:
-  Command(CVC4::SmtEngine* smt) : d_smt(smt) {}
-  SmtEngine* getSmtEngine() { return d_smt; }
-  virtual void invoke() = 0;
+class Command
+{
+  public:
+    virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
+    virtual ~Command() {}
 };
 
-class AssertCommand : public Command {
-protected:
-  Expr d_expr;
-
-public:
-  AssertCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {}
-  void invoke() { d_smt->assert(d_expr); }
+class AssertCommand: public Command
+{
+  public:
+    AssertCommand(const Expr& e);
+    void invoke(CVC4::SmtEngine* smt_engine);
+  protected:
+    Expr d_expr;
 };
 
-class CheckSatCommand : public Command {
-protected:
-  Expr d_expr;
-
-public:
-  CheckSatCommand(CVC4::SmtEngine* smt) : Command(smt), d_expr(Expr::null()) {}
-  CheckSatCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {}
-  void invoke() { d_smt->checkSat(d_expr); }
+class CheckSatCommand: public Command
+{
+  public:
+    CheckSatCommand();
+    CheckSatCommand(const Expr& e);
+    void invoke(CVC4::SmtEngine* smt);
+  protected:
+    Expr d_expr;
 };
 
-class QueryCommand : public Command {
-protected:
-  Expr d_expr;
-
-public:
-  QueryCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {}
-  void invoke() { d_smt->query(d_expr); }
+class QueryCommand: public Command
+{
+  public:
+    QueryCommand(const Expr& e);
+    void invoke(CVC4::SmtEngine* smt);
+  protected:
+    Expr d_expr;
 };
 
 }/* CVC4 namespace */