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.

1 files changed, 8 insertions, 9 deletions

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