1 files changed, 43 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f9ebc713d..05ee12462 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -15,12 +15,51 @@
 
 namespace CVC4 {
 
-void doCommand(Command* c) {
-  if(c->getSmtEngine() != this)
-    throw new IllegalArgumentException("SmtEngine does not match Command");
+void SmtEngine::doCommand(Command* c) {
+  c->invoke(this);
+}
+
+Expr SmtEngine::preprocess(Expr e) {
+  return e;
+}
+
+void SmtEngine::processAssertionList() {
+  for(std::vector<Expr>::iterator i = d_assertions.begin();
+      i != d_assertions.end();
+      ++i)
+    ;//d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i);
+}
+
+Result SmtEngine::check() {
+  processAssertionList();
+  return Result(Result::VALIDITY_UNKNOWN);
+}
 
-  c->invoke();
+Result SmtEngine::quickCheck() {
+  processAssertionList();
+  return Result(Result::VALIDITY_UNKNOWN);
 }
 
+void SmtEngine::addFormula(Expr e) {
+  d_assertions.push_back(e);
+}
+
+Result SmtEngine::checkSat(Expr e) {
+  e = preprocess(e);
+  addFormula(e);
+  return check();
+}
+
+Result SmtEngine::query(Expr e) {
+  e = preprocess(e);
+  addFormula(e);
+  return check();
+}
+
+Result SmtEngine::assert(Expr e) {
+  e = preprocess(e);
+  addFormula(e);
+  return quickCheck();
+}
 
 }/* CVC4 namespace */