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.

1 files changed, 63 insertions, 3 deletions

diff --git a/src/util/result.h b/src/util/result.h
index 87686d59c..d4980c776 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -16,6 +16,8 @@
 #ifndef __CVC4__RESULT_H
 #define __CVC4__RESULT_H
 
+#include "util/Assert.h"
+
 namespace CVC4 {
 
 // TODO: perhaps best to templatize Result on its Kind (SAT/Validity),
@@ -52,20 +54,78 @@ public:
 private:
   enum SAT      d_sat;
   enum Validity d_validity;
-  enum { TYPE_SAT, TYPE_VALIDITY } d_which;
+  enum { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE } d_which;
 
   friend std::ostream& CVC4::operator<<(std::ostream& out, Result r);
 
 public:
-  Result(enum SAT s) : d_sat(s), d_validity(VALIDITY_UNKNOWN), d_which(TYPE_SAT) {}
-  Result(enum Validity v) : d_sat(SAT_UNKNOWN), d_validity(v), d_which(TYPE_VALIDITY) {}
+  Result() :
+    d_sat(SAT_UNKNOWN),
+    d_validity(VALIDITY_UNKNOWN),
+    d_which(TYPE_NONE) {
+  }
+  Result(enum SAT s) :
+    d_sat(s),
+    d_validity(VALIDITY_UNKNOWN),
+    d_which(TYPE_SAT) {
+  }
+  Result(enum Validity v) :
+    d_sat(SAT_UNKNOWN),
+    d_validity(v),
+    d_which(TYPE_VALIDITY) {
+  }
 
   enum SAT isSAT();
   enum Validity isValid();
   enum UnknownExplanation whyUnknown();
 
+  inline Result asSatisfiabilityResult() const;
+  inline Result asValidityResult() const;
+
 };/* class Result */
 
+inline Result Result::asSatisfiabilityResult() const {
+  if(d_which == TYPE_SAT) {
+    return *this;
+  }
+
+  switch(d_validity) {
+
+  case INVALID:
+    return Result(SAT);
+
+  case VALID:
+    return Result(UNSAT);
+
+  case VALIDITY_UNKNOWN:
+    return Result(SAT_UNKNOWN);
+
+  default:
+    Unhandled(d_validity);
+  }
+}
+
+inline Result Result::asValidityResult() const {
+  if(d_which == TYPE_VALIDITY) {
+    return *this;
+  }
+
+  switch(d_sat) {
+
+  case SAT:
+    return Result(INVALID);
+
+  case UNSAT:
+    return Result(VALID);
+
+  case SAT_UNKNOWN:
+    return Result(VALIDITY_UNKNOWN);
+
+  default:
+    Unhandled(d_sat);
+  }
+}
+
 inline std::ostream& operator<<(std::ostream& out, Result r) {
   if(r.d_which == Result::TYPE_SAT) {
     switch(r.d_sat) {