parsing/expr/command/result/various other fixes

2 files changed, 51 insertions, 7 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 */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index af2f45c23..3e33cc8af 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -13,6 +13,8 @@
 #define __CVC4__SMT_ENGINE_H
 
 #include <vector>
+
+#include "cvc4_config.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "util/result.h"
@@ -41,7 +43,7 @@ class Command;
 class SmtEngine {
   /** Current set of assertions. */
   // TODO: make context-aware to handle user-level push/pop.
-  std::vector<Expr> d_assertList;
+  std::vector<Expr> d_assertions;
 
   /** Our expression manager */
   ExprManager *d_em;
@@ -49,13 +51,16 @@ class SmtEngine {
   /** User-level options */
   Options *d_opts;
 
+  /** Expression built-up for handing off to the propagation engine */
+  Expr d_expr;
+
   /**
    * Pre-process an Expr.  This is expected to be highly-variable,
    * with a lot of "source-level configurability" to add multiple
    * passes over the Expr.  TODO: may need to specify a LEVEL of
    * preprocessing (certain contexts need more/less ?).
    */
-  void preprocess(Expr);
+  Expr preprocess(Expr);
 
   /**
    * Adds a formula to the current context.
@@ -85,7 +90,7 @@ public:
   /*
    * Construct an SmtEngine with the given expression manager and user options.
    */
-  SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts) {}
+  SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts), d_expr(Expr::null()) {}
 
   /**
    * Execute a command.