additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command

1 files changed, 72 insertions, 89 deletions

diff --git a/src/util/result.h b/src/util/result.h
index f1f6ae1c2..fc2fa4522 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -21,20 +21,29 @@
 #ifndef __CVC4__RESULT_H
 #define __CVC4__RESULT_H
 
+#include <iostream>
+#include <string>
+
+#include "util/Assert.h"
+
 namespace CVC4 {
 
-// TODO: perhaps best to templatize Result on its Kind (SAT/Validity),
-// but this requires doing the same for Prover and needs discussion.
+// TODO: either templatize Result on its Kind (Sat/Validity) or subclass.
+// TODO: INVALID/SAT provide models, etc?---perhaps just by linking back
+// into the SmtEngine that produced the Result?
+// TODO: make unconstructible except by SmtEngine?  That would ensure that
+// any Result in the system is bona fide.
 
-// TODO: subclass to provide models, etc.  This is really just
-// intended as a three-valued response code.
+class Result;
+
+std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC;
 
 /**
- * Three-valued, immutable SMT result, with optional explanation.
+ * Three-valued SMT result, with optional explanation.
  */
 class CVC4_PUBLIC Result {
 public:
-  enum SAT {
+  enum Sat {
     UNSAT = 0,
     SAT = 1,
     SAT_UNKNOWN = 2
@@ -50,121 +59,95 @@ public:
     REQUIRES_FULL_CHECK,
     INCOMPLETE,
     TIMEOUT,
-    BAIL,
-    OTHER
+    MEMOUT,
+    OTHER,
+    UNKNOWN_REASON
   };
 
 private:
-  enum SAT      d_sat;
+  enum Sat d_sat;
   enum Validity d_validity;
   enum { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE } d_which;
+  enum UnknownExplanation d_unknownExplanation;
 
-  friend std::ostream& CVC4::operator<<(std::ostream& out, Result r);
+  friend std::ostream& CVC4::operator<<(std::ostream& out, const Result& r);
 
 public:
   Result() :
     d_sat(SAT_UNKNOWN),
     d_validity(VALIDITY_UNKNOWN),
-    d_which(TYPE_NONE) {
+    d_which(TYPE_NONE),
+    d_unknownExplanation(UNKNOWN_REASON) {
   }
-  Result(enum SAT s) :
+  Result(enum Sat s) :
     d_sat(s),
     d_validity(VALIDITY_UNKNOWN),
-    d_which(TYPE_SAT) {
+    d_which(TYPE_SAT),
+    d_unknownExplanation(UNKNOWN_REASON) {
+    CheckArgument(s != SAT_UNKNOWN,
+                  "Must provide a reason for satisfiability being unknown");
   }
   Result(enum Validity v) :
     d_sat(SAT_UNKNOWN),
     d_validity(v),
-    d_which(TYPE_VALIDITY) {
+    d_which(TYPE_VALIDITY),
+    d_unknownExplanation(UNKNOWN_REASON) {
+    CheckArgument(v != VALIDITY_UNKNOWN,
+                  "Must provide a reason for validity being unknown");
+  }
+  Result(enum Sat s, enum UnknownExplanation unknownExplanation) :
+    d_sat(s),
+    d_validity(VALIDITY_UNKNOWN),
+    d_which(TYPE_SAT),
+    d_unknownExplanation(unknownExplanation) {
+    CheckArgument(s == SAT_UNKNOWN,
+                  "improper use of unknown-result constructor");
+  }
+  Result(enum Validity v, enum UnknownExplanation unknownExplanation) :
+    d_sat(SAT_UNKNOWN),
+    d_validity(v),
+    d_which(TYPE_VALIDITY),
+    d_unknownExplanation(unknownExplanation) {
+    CheckArgument(v == VALIDITY_UNKNOWN,
+                  "improper use of unknown-result constructor");
   }
+  Result(const std::string& s);
 
-  enum SAT isSAT() {
+  enum Sat isSat() const {
     return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
   }
-  enum Validity isValid() {
+  enum Validity isValid() const {
     return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
   }
-  enum UnknownExplanation whyUnknown();
-
-  inline bool operator==(Result r) {
-    if(d_which != r.d_which) {
-      return false;
-    }
-    if(d_which == TYPE_SAT) {
-      return d_sat == r.d_sat;
-    }
-    if(d_which == TYPE_VALIDITY) {
-      return d_validity == r.d_validity;
-    }
-    return false;
-  }
-  inline bool operator!=(Result r) {
-    return !(*this == r);
-  }
-  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);
+  bool isUnknown() const {
+    return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
   }
-}
-
-inline Result Result::asValidityResult() const {
-  if(d_which == TYPE_VALIDITY) {
-    return *this;
+  enum UnknownExplanation whyUnknown() const {
+    AlwaysAssert( isUnknown(),
+                  "This result is not unknown, so the reason for "
+                  "being unknown cannot be inquired of it" );
+    return d_unknownExplanation;
   }
 
-  switch(d_sat) {
-
-  case SAT:
-    return Result(INVALID);
+  bool operator==(const Result& r) const;
+  inline bool operator!=(const Result& r) const;
+  Result asSatisfiabilityResult() const;
+  Result asValidityResult() const;
 
-  case UNSAT:
-    return Result(VALID);
+  std::string toString() const;
 
-  case SAT_UNKNOWN:
-    return Result(VALIDITY_UNKNOWN);
+};/* class Result */
 
-  default:
-    Unhandled(d_sat);
-  }
+inline bool Result::operator!=(const Result& r) const {
+  return !(*this == r);
 }
 
-inline std::ostream& operator<<(std::ostream& out, Result r) {
-  if(r.d_which == Result::TYPE_SAT) {
-    switch(r.d_sat) {
-    case Result::UNSAT: out << "UNSAT"; break;
-    case Result::SAT: out << "SAT"; break;
-    case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break;
-    }
-  } else {
-    switch(r.d_validity) {
-    case Result::INVALID: out << "INVALID"; break;
-    case Result::VALID: out << "VALID"; break;
-    case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break;
-    }
-  }
-
-  return out;
-}
+std::ostream& operator<<(std::ostream& out,
+                         enum Result::Sat s) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out,
+                         enum Result::Validity v) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out,
+                         enum Result::UnknownExplanation e) CVC4_PUBLIC;
 
 }/* CVC4 namespace */