2 files changed, 18 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f6b81465b..f9ebc713d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -10,8 +10,17 @@
  **/
 
 #include "smt/smt_engine.h"
+#include "util/exception.h"
+#include "util/command.h"
 
 namespace CVC4 {
 
+void doCommand(Command* c) {
+  if(c->getSmtEngine() != this)
+    throw new IllegalArgumentException("SmtEngine does not match Command");
+
+  c->invoke();
+}
+
 
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 149de058e..af2f45c23 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -15,7 +15,6 @@
 #include <vector>
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
-#include "util/command.h"
 #include "util/result.h"
 #include "util/model.h"
 #include "util/options.h"
@@ -26,6 +25,8 @@
 
 namespace CVC4 {
 
+class Command;
+
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
 // SmtEngine and override check()?
@@ -84,7 +85,7 @@ public:
   /*
    * Construct an SmtEngine with the given expression manager and user options.
    */
-  SmtEngine(ExprManager* em, Options* opts) : d_em(em), d_opts(opts) {}
+  SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts) {}
 
   /**
    * Execute a command.
@@ -106,6 +107,12 @@ public:
   Result query(Expr);
 
   /**
+   * Add a formula to the current context and call check().  Returns
+   * true iff consistent.
+   */
+  Result checkSat(Expr);
+
+  /**
    * Simplify a formula without doing "much" work.  Requires assist
    * from the SAT Engine.
    */