From 2163539a8b839acf98bda0e1a65f1fcca5232fb2 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 8 Dec 2009 10:10:20 +0000
Subject: work on propositional layer, expression builder support for large
 expressions, output classes, and minisat

---
 src/smt/smt_engine.cpp |  5 +++--
 src/smt/smt_engine.h   | 22 ++++++++++++++++++++--
 2 files changed, 23 insertions(+), 4 deletions(-)

(limited to 'src/smt')

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 05ee12462..412c0f3af 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -27,11 +27,12 @@ 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);
+    d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i);
 }
 
 Result SmtEngine::check() {
   processAssertionList();
+  d_prop.solve(d_expr);
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
@@ -56,7 +57,7 @@ Result SmtEngine::query(Expr e) {
   return check();
 }
 
-Result SmtEngine::assert(Expr e) {
+Result SmtEngine::assertFormula(Expr e) {
   e = preprocess(e);
   addFormula(e);
   return quickCheck();
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index ab3fc816a..30786511e 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -20,6 +20,8 @@
 #include "util/result.h"
 #include "util/model.h"
 #include "util/options.h"
+#include "prop/prop_engine.h"
+#include "util/decision_engine.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -54,6 +56,15 @@ class SmtEngine {
   /** Expression built-up for handing off to the propagation engine */
   Expr d_expr;
 
+  /** The decision engine */
+  DecisionEngine d_de;
+
+  /** The decision engine */
+  TheoryEngine d_te;
+
+  /** The propositional engine */
+  PropEngine d_prop;
+
   /**
    * Pre-process an Expr.  This is expected to be highly-variable,
    * with a lot of "source-level configurability" to add multiple
@@ -90,7 +101,14 @@ public:
   /*
    * Construct an SmtEngine with the given expression manager and user options.
    */
-  SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts), d_expr(Expr::null()) {}
+  SmtEngine(ExprManager* em, Options* opts) throw() :
+    d_em(em),
+    d_opts(opts),
+    d_expr(Expr::null()),
+    d_de(),
+    d_te(),
+    d_prop(d_de, d_te) {
+  }
 
   /**
    * Execute a command.
@@ -103,7 +121,7 @@ public:
    * literals and conjunction of literals.  Returns false iff
    * inconsistent.
    */
-  Result assert(Expr);
+  Result assertFormula(Expr);
 
   /**
    * Add a formula to the current context and call check().  Returns
-- 
cgit v1.2.3