Extracted the public Expr and ExprManager interface to encapsulate the optimized expressions and the internal expression manager.

1 files changed, 30 insertions, 15 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4ccdd07d0..723263177 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -15,24 +15,39 @@
 
 namespace CVC4 {
 
+SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() :
+    d_public_em(em),
+    d_em(em->getNodeManager()),
+    d_opts(opts),
+    d_de(),
+    d_te(),
+    d_prop(d_de, d_te) {
+  }
+
+SmtEngine::~SmtEngine() {
+
+}
+
 void SmtEngine::doCommand(Command* c) {
   c->invoke(this);
 }
 
-Node SmtEngine::preprocess(Node e) {
+Node SmtEngine::preprocess(const Node& e) {
   return e;
 }
 
-void SmtEngine::processAssertionList() {
+Node SmtEngine::processAssertionList() {
+  Node asserts;
   for(std::vector<Node>::iterator i = d_assertions.begin();
       i != d_assertions.end();
       ++i)
-    d_expr = d_expr.isNull() ? *i : d_em->mkExpr(AND, d_expr, *i);
+    asserts = asserts.isNull() ? *i : d_em->mkExpr(AND, asserts, *i);
+  return asserts;
 }
 
 Result SmtEngine::check() {
-  processAssertionList();
-  d_prop.solve(d_expr);
+  Node asserts = processAssertionList();
+  d_prop.solve(asserts);
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
@@ -41,25 +56,25 @@ Result SmtEngine::quickCheck() {
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
-void SmtEngine::addFormula(Node e) {
+void SmtEngine::addFormula(const Node& e) {
   d_assertions.push_back(e);
 }
 
-Result SmtEngine::checkSat(Node e) {
-  e = preprocess(e);
-  addFormula(e);
+Result SmtEngine::checkSat(const BoolExpr& e) {
+  Node node_e = preprocess(e.getNode());
+  addFormula(node_e);
   return check();
 }
 
-Result SmtEngine::query(Node e) {
-  e = preprocess(e);
-  addFormula(e);
+Result SmtEngine::query(const BoolExpr& e) {
+  Node node_e = preprocess(e.getNode());
+  addFormula(node_e);
   return check();
 }
 
-Result SmtEngine::assertFormula(Node e) {
-  e = preprocess(e);
-  addFormula(e);
+Result SmtEngine::assertFormula(const BoolExpr& e) {
+  Node node_e = preprocess(e.getNode());
+  addFormula(node_e);
   return quickCheck();
 }