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

2 files changed, 100 insertions, 79 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();
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index c4addc7dd..edcbdcca3 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -16,7 +16,9 @@
 
 #include "cvc4_config.h"
 #include "expr/node.h"
+#include "expr/expr.h"
 #include "expr/node_manager.h"
+#include "expr/expr_manager.h"
 #include "util/result.h"
 #include "util/model.h"
 #include "util/options.h"
@@ -42,73 +44,19 @@ class Command;
 //
 // The CNF conversion can go on in PropEngine.
 
-class SmtEngine {
-  /** Current set of assertions. */
-  // TODO: make context-aware to handle user-level push/pop.
-  std::vector<Node> d_assertions;
-
-  /** Our expression manager */
-  NodeManager *d_em;
-
-  /** User-level options */
-  Options *d_opts;
-
-  /** Expression built-up for handing off to the propagation engine */
-  Node d_expr;
-
-  /** The decision engine */
-  DecisionEngine d_de;
-
-  /** The decision engine */
-  TheoryEngine d_te;
-
-  /** The propositional engine */
-  PropEngine d_prop;
-
-  /**
-   * Pre-process an Node.  This is expected to be highly-variable,
-   * with a lot of "source-level configurability" to add multiple
-   * passes over the Node.  TODO: may need to specify a LEVEL of
-   * preprocessing (certain contexts need more/less ?).
-   */
-  Node preprocess(Node);
+class CVC4_PUBLIC SmtEngine {
 
-  /**
-   * Adds a formula to the current context.
-   */
-  void addFormula(Node);
-
-  /**
-   * Full check of consistency in current context.  Returns true iff
-   * consistent.
-   */
-  Result check();
+public:
 
   /**
-   * Quick check of consistency in current context: calls
-   * processAssertionList() then look for inconsistency (based only on
-   * that).
+   * Construct an SmtEngine with the given expression manager and user options.
    */
-  Result quickCheck();
+  SmtEngine(ExprManager* em, Options* opts) throw();
 
   /**
-   * Process the assertion list: for literals and conjunctions of
-   * literals, assert to T-solver.
-   */
-  void processAssertionList();
-
-public:
-  /*
-   * Construct an SmtEngine with the given expression manager and user options.
+   * Destruct the smt engine.
    */
-  SmtEngine(NodeManager* em, Options* opts) throw() :
-    d_em(em),
-    d_opts(opts),
-    d_expr(Node::null()),
-    d_de(),
-    d_te(),
-    d_prop(d_de, d_te) {
-  }
+  ~SmtEngine();
 
   /**
    * Execute a command.
@@ -121,25 +69,25 @@ public:
    * literals and conjunction of literals.  Returns false iff
    * inconsistent.
    */
-  Result assertFormula(Node);
+  Result assertFormula(const BoolExpr& e);
 
   /**
    * Add a formula to the current context and call check().  Returns
    * true iff consistent.
    */
-  Result query(Node);
+  Result query(const BoolExpr& e);
 
   /**
    * Add a formula to the current context and call check().  Returns
    * true iff consistent.
    */
-  Result checkSat(Node);
+  Result checkSat(const BoolExpr& e);
 
   /**
    * Simplify a formula without doing "much" work.  Requires assist
    * from the SAT Engine.
    */
-  Node simplify(Node);
+  Expr simplify(const Expr& e);
 
   /**
    * Get a (counter)model (only if preceded by a SAT or INVALID query.
@@ -155,6 +103,64 @@ public:
    * Pop a user-level context.  Throws an exception if nothing to pop.
    */
   void pop();
+
+private:
+
+  /** Current set of assertions. */
+  // TODO: make context-aware to handle user-level push/pop.
+  std::vector<Node> d_assertions;
+
+  /** Our expression manager */
+  ExprManager *d_public_em;
+
+  /** Out internal expression/node manager */
+  NodeManager *d_em;
+
+  /** User-level options */
+  Options *d_opts;
+
+  /** The decision engine */
+  DecisionEngine d_de;
+
+  /** The decision engine */
+  TheoryEngine d_te;
+
+  /** The propositional engine */
+  PropEngine d_prop;
+
+  /**
+   * Pre-process an Node.  This is expected to be highly-variable,
+   * with a lot of "source-level configurability" to add multiple
+   * passes over the Node.  TODO: may need to specify a LEVEL of
+   * preprocessing (certain contexts need more/less ?).
+   */
+  Node preprocess(const Node& e);
+
+  /**
+   * Adds a formula to the current context.
+   */
+  void addFormula(const Node& e);
+
+  /**
+   * Full check of consistency in current context.  Returns true iff
+   * consistent.
+   */
+  Result check();
+
+  /**
+   * Quick check of consistency in current context: calls
+   * processAssertionList() then look for inconsistency (based only on
+   * that).
+   */
+  Result quickCheck();
+
+  /**
+   * Process the assertion list: for literals and conjunctions of
+   * literals, assert to T-solver.
+   */
+  Node processAssertionList();
+
+
 };/* class SmtEngine */
 
 }/* CVC4 namespace */