Addressed many of the concerns of bug 10 (build system code review).

Some parts split into other bugs: 19, 20, 21.

Addressed concerns of bug 11 (util package code review).

Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers

Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main().  Silenced MiniSat when
verbosity is not requested.

2 files changed, 16 insertions, 12 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7e2b6e24c..e4a54b694 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -17,17 +17,18 @@
 #include "util/command.h"
 #include "util/output.h"
 #include "expr/node_builder.h"
+#include "util/options.h"
 
 namespace CVC4 {
 
-SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() :
+SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
   d_assertions(),
   d_publicEm(em),
   d_nm(em->getNodeManager()),
   d_opts(opts),
   d_de(),
   d_te(),
-  d_prop(d_de, d_te){
+  d_prop(opts, d_de, d_te) {
 }
 
 SmtEngine::~SmtEngine() {
@@ -53,8 +54,7 @@ void SmtEngine::processAssertionList() {
 Result SmtEngine::check() {
   Debug("smt") << "SMT check()" << std::endl;
   processAssertionList();
-  d_prop.solve();
-  return Result(Result::VALIDITY_UNKNOWN);
+  return d_prop.solve();
 }
 
 Result SmtEngine::quickCheck() {
@@ -73,7 +73,9 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
   NodeManagerScope nms(d_nm);
   Node node_e = preprocess(e.getNode());
   addFormula(node_e);
-  return check();
+  Result r = check().asSatisfiabilityResult();
+  Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << std::endl;
+  return r;
 }
 
 Result SmtEngine::query(const BoolExpr& e) {
@@ -81,7 +83,9 @@ Result SmtEngine::query(const BoolExpr& e) {
   NodeManagerScope nms(d_nm);
   Node node_e = preprocess(d_nm->mkNode(NOT, e.getNode()));
   addFormula(node_e);
-  return check();
+  Result r = check().asValidityResult();
+  Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl;
+  return r;
 }
 
 Result SmtEngine::assertFormula(const BoolExpr& e) {
@@ -89,7 +93,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) {
   NodeManagerScope nms(d_nm);
   Node node_e = preprocess(e.getNode());
   addFormula(node_e);
-  return quickCheck();
+  return quickCheck().asValidityResult();
 }
 
 Expr SmtEngine::simplify(const Expr& e) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 59eddccf0..48365e129 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -26,7 +26,6 @@
 #include "expr/expr_manager.h"
 #include "util/result.h"
 #include "util/model.h"
-#include "util/options.h"
 #include "prop/prop_engine.h"
 #include "util/decision_engine.h"
 
@@ -37,6 +36,7 @@
 namespace CVC4 {
 
 class Command;
+class Options;
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
 // hood): use a type parameter and have check() delegate, or subclass
@@ -56,7 +56,7 @@ public:
   /**
    * Construct an SmtEngine with the given expression manager and user options.
    */
-  SmtEngine(ExprManager* em, Options* opts) throw();
+  SmtEngine(ExprManager* em, const Options* opts) throw();
 
   /**
    * Destruct the SMT engine.
@@ -116,13 +116,13 @@ private:
   std::vector<Node> d_assertions;
 
   /** Our expression manager */
-  ExprManager *d_publicEm;
+  ExprManager* d_publicEm;
 
   /** Out internal expression/node manager */
-  NodeManager *d_nm;
+  NodeManager* d_nm;
 
   /** User-level options */
-  Options *d_opts;
+  const Options* d_opts;
 
   /** The decision engine */
   DecisionEngine d_de;