Changes to the CNF conversion and the SAT solver. All regression pass now, and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser.

2 files changed, 27 insertions, 27 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d30255e4f..8bca39df4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -24,25 +24,25 @@ using namespace CVC4::prop;
 
 namespace CVC4 {
 
-SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
+SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
   d_assertions(),
-  d_publicEm(em),
-  d_nm(em->getNodeManager()),
-  d_opts(opts)
+  d_exprManager(em),
+  d_nodeManager(em->getNodeManager()),
+  d_options(opts)
 {
-  d_de = new DecisionEngine();
-  d_te = new TheoryEngine(this);
-  d_prop = new PropEngine(opts, d_de, d_te);
+  d_decisionEngine = new DecisionEngine();
+  d_theoryEngine = new TheoryEngine(this);
+  d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine);
 }
 
 SmtEngine::~SmtEngine() {
-   delete d_prop;
-   delete d_te;
-   delete d_de;
+  delete d_propEngine;
+  delete d_theoryEngine;
+  delete d_decisionEngine;
 }
 
 void SmtEngine::doCommand(Command* c) {
-  NodeManagerScope nms(d_nm);
+  NodeManagerScope nms(d_nodeManager);
   c->invoke(this);
 }
 
@@ -52,16 +52,15 @@ 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_propEngine->assertFormula(d_assertions[i]);
   }
   d_assertions.clear();
 }
 
-
 Result SmtEngine::check() {
   Debug("smt") << "SMT check()" << std::endl;
   processAssertionList();
-  return d_prop->solve();
+  return d_propEngine->checkSat();
 }
 
 Result SmtEngine::quickCheck() {
@@ -77,7 +76,7 @@ void SmtEngine::addFormula(const Node& e) {
 
 Result SmtEngine::checkSat(const BoolExpr& e) {
   Debug("smt") << "SMT checkSat(" << e << ")" << std::endl;
-  NodeManagerScope nms(d_nm);
+  NodeManagerScope nms(d_nodeManager);
   Node node_e = preprocess(e.getNode());
   addFormula(node_e);
   Result r = check().asSatisfiabilityResult();
@@ -87,8 +86,8 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 
 Result SmtEngine::query(const BoolExpr& e) {
   Debug("smt") << "SMT query(" << e << ")" << std::endl;
-  NodeManagerScope nms(d_nm);
-  Node node_e = preprocess(d_nm->mkNode(NOT, e.getNode()));
+  NodeManagerScope nms(d_nodeManager);
+  Node node_e = preprocess(d_nodeManager->mkNode(NOT, e.getNode()));
   addFormula(node_e);
   Result r = check().asValidityResult();
   Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl;
@@ -97,7 +96,7 @@ Result SmtEngine::query(const BoolExpr& e) {
 
 Result SmtEngine::assertFormula(const BoolExpr& e) {
   Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl;
-  NodeManagerScope nms(d_nm);
+  NodeManagerScope nms(d_nodeManager);
   Node node_e = preprocess(e.getNode());
   addFormula(node_e);
   return quickCheck().asValidityResult();
@@ -110,9 +109,11 @@ Expr SmtEngine::simplify(const Expr& e) {
 }
 
 void SmtEngine::push() {
+  Debug("smt") << "SMT push()" << std::endl;
 }
 
 void SmtEngine::pop() {
+  Debug("smt") << "SMT pop()" << std::endl;
 }
 
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index eb9384ca5..d796959a9 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -117,23 +117,22 @@ private:
   std::vector<Node> d_assertions;
 
   /** Our expression manager */
-  ExprManager* d_publicEm;
+  ExprManager* d_exprManager;
 
   /** Out internal expression/node manager */
-  NodeManager* d_nm;
+  NodeManager* d_nodeManager;
 
   /** User-level options */
-  const Options* d_opts;
+  const Options* d_options;
 
   /** The decision engine */
-  DecisionEngine* d_de;
+  DecisionEngine* d_decisionEngine;
 
   /** The decision engine */
-  TheoryEngine* d_te;
+  TheoryEngine* d_theoryEngine;
 
   /** The propositional engine */
-  prop::PropEngine* d_prop;
-
+  prop::PropEngine* d_propEngine;
 
   /**
    * Pre-process an Node.  This is expected to be highly-variable,
@@ -141,12 +140,12 @@ private:
    * passes over the Node.  TODO: may need to specify a LEVEL of
    * preprocessing (certain contexts need more/less ?).
    */
-  Node preprocess(const Node& e);
+  Node preprocess(const Node& node);
 
   /**
    * Adds a formula to the current context.
    */
-  void addFormula(const Node& e);
+  void addFormula(const Node& node);
 
   /**
    * Full check of consistency in current context.  Returns true iff