Small changes to the smt-engine, removed the assertions list.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 24795111fab091f0c12389bf67a996b1e41d82ae..36954ace46fc3e3a7be848da26cc2d5df965761e 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -25,7 +25,6 @@ using namespace CVC4::prop;
 namespace CVC4 {
 
 SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
-  d_assertions(),
   d_exprManager(em),
   d_nodeManager(em->getNodeManager()),
   d_options(opts)
@@ -50,35 +49,25 @@ Node SmtEngine::preprocess(const Node& e) {
   return e;
 }
 
-void SmtEngine::processAssertionList() {
-  for(unsigned i = 0; i < d_assertions.size(); ++i) {
-    d_propEngine->assertFormula(d_assertions[i]);
-  }
-  d_assertions.clear();
-}
-
 Result SmtEngine::check() {
   Debug("smt") << "SMT check()" << std::endl;
-  processAssertionList();
   return d_propEngine->checkSat();
 }
 
 Result SmtEngine::quickCheck() {
   Debug("smt") << "SMT quickCheck()" << std::endl;
-  processAssertionList();
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
 void SmtEngine::addFormula(const Node& e) {
   Debug("smt") << "push_back assertion " << e << std::endl;
-  d_assertions.push_back(e);
+  d_propEngine->assertFormula(preprocess(e));
 }
 
 Result SmtEngine::checkSat(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT checkSat(" << e << ")" << std::endl;
-  Node node_e = preprocess(e.getNode());
-  addFormula(node_e);
+  addFormula(e.getNode());
   Result r = check().asSatisfiabilityResult();
   Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << std::endl;
   return r;
@@ -87,8 +76,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 Result SmtEngine::query(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT query(" << e << ")" << std::endl;
-  Node node_e = preprocess(d_nodeManager->mkNode(NOT, e.getNode()));
-  addFormula(node_e);
+  addFormula(e.getNode().notExpr());
   Result r = check().asValidityResult();
   Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl;
   return r;
@@ -97,8 +85,7 @@ Result SmtEngine::query(const BoolExpr& e) {
 Result SmtEngine::assertFormula(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl;
-  Node node_e = preprocess(e.getNode());
-  addFormula(node_e);
+  addFormula(e.getNode());
   return quickCheck().asValidityResult();
 }
 

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index d796959a92be82a49da79a0ca2797469575cd50e..0e7e951f8fda31d5f1399f72c74f03873b02e049 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -112,10 +112,6 @@ public:
 
 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_exprManager;
 
@@ -160,12 +156,6 @@ private:
    */
   Result quickCheck();
 
-  /**
-   * Process the assertion list: for literals and conjunctions of
-   * literals, assert to T-solver.
-   */
-  void processAssertionList();
-
 };/* class SmtEngine */
 
 }/* CVC4 namespace */