beautification of the prop engine

2 files changed, 23 insertions, 15 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1555acb7d..a04d16d06 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -13,11 +13,14 @@
  **/
 
 #include "smt/smt_engine.h"
-#include "util/exception.h"
 #include "expr/command.h"
-#include "util/output.h"
 #include "expr/node_builder.h"
+#include "util/output.h"
+#include "util/exception.h"
 #include "util/options.h"
+#include "prop/prop_engine.h"
+
+using namespace CVC4::prop;
 
 namespace CVC4 {
 
@@ -25,13 +28,17 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
   d_assertions(),
   d_publicEm(em),
   d_nm(em->getNodeManager()),
-  d_opts(opts),
-  d_de(),
-  d_te(),
-  d_prop(opts, d_de, d_te) {
+  d_opts(opts)
+{
+  d_de = new DecisionEngine();
+  d_te = new TheoryEngine();
+  d_prop = new PropEngine(opts, d_de, d_te);
 }
 
 SmtEngine::~SmtEngine() {
+   delete d_prop;
+   delete d_te;
+   delete d_de;
 }
 
 void SmtEngine::doCommand(Command* c) {
@@ -45,7 +52,7 @@ Node SmtEngine::preprocess(const Node& e) {
 
 void SmtEngine::processAssertionList() {
   for(unsigned i = 0; i < d_assertions.size(); ++i) {
-    d_prop.assertFormula(d_assertions[i]);
+    d_prop->assertFormula(d_assertions[i]);
   }
   d_assertions.clear();
 }
@@ -54,7 +61,7 @@ void SmtEngine::processAssertionList() {
 Result SmtEngine::check() {
   Debug("smt") << "SMT check()" << std::endl;
   processAssertionList();
-  return d_prop.solve();
+  return d_prop->solve();
 }
 
 Result SmtEngine::quickCheck() {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 79a35a6a1..eb9384ca5 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -19,14 +19,10 @@
 #include <vector>
 
 #include "cvc4_config.h"
-#include "expr/node.h"
 #include "expr/expr.h"
-#include "expr/node_manager.h"
-#include "expr/node_builder.h"
 #include "expr/expr_manager.h"
 #include "util/result.h"
 #include "util/model.h"
-#include "prop/prop_engine.h"
 #include "util/decision_engine.h"
 
 // In terms of abstraction, this is below (and provides services to)
@@ -37,6 +33,11 @@ namespace CVC4 {
 
 class Command;
 class Options;
+class TheoryEngine;
+
+namespace prop {
+  class PropEngine;
+}
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
@@ -125,13 +126,13 @@ private:
   const Options* d_opts;
 
   /** The decision engine */
-  DecisionEngine d_de;
+  DecisionEngine* d_de;
 
   /** The decision engine */
-  TheoryEngine d_te;
+  TheoryEngine* d_te;
 
   /** The propositional engine */
-  PropEngine d_prop;
+  prop::PropEngine* d_prop;
 
 
   /**