1 files changed, 63 insertions, 0 deletions
diff --git a/src/expr/result.cpp b/src/expr/result.cpp
index 95e382b98..aeb62b0c3 100644
--- a/src/expr/result.cpp
+++ b/src/expr/result.cpp
@@ -29,6 +29,62 @@ using namespace std;
 
 namespace CVC4 {
 
+Result::Result()
+    : d_sat(SAT_UNKNOWN)
+    , d_validity(VALIDITY_UNKNOWN)
+    , d_which(TYPE_NONE)
+    , d_unknownExplanation(UNKNOWN_REASON)
+    , d_inputName("")
+{ }
+
+
+Result::Result(enum Sat s, std::string inputName)
+    : d_sat(s)
+    , d_validity(VALIDITY_UNKNOWN)
+    , d_which(TYPE_SAT)
+    , d_unknownExplanation(UNKNOWN_REASON)
+    , d_inputName(inputName)
+{
+  PrettyCheckArgument(s != SAT_UNKNOWN,
+                      "Must provide a reason for satisfiability being unknown");
+}
+
+Result::Result(enum Validity v, std::string inputName)
+    : d_sat(SAT_UNKNOWN)
+    , d_validity(v)
+    , d_which(TYPE_VALIDITY)
+    , d_unknownExplanation(UNKNOWN_REASON)
+    , d_inputName(inputName)
+{
+  PrettyCheckArgument(v != VALIDITY_UNKNOWN,
+                      "Must provide a reason for validity being unknown");
+}
+
+
+Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation,
+               std::string inputName)
+    : d_sat(s)
+    , d_validity(VALIDITY_UNKNOWN)
+    , d_which(TYPE_SAT)
+    , d_unknownExplanation(unknownExplanation)
+    , d_inputName(inputName)
+{
+  PrettyCheckArgument(s == SAT_UNKNOWN,
+                      "improper use of unknown-result constructor");
+}
+
+Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation,
+               std::string inputName)
+    : d_sat(SAT_UNKNOWN)
+    , d_validity(v)
+    , d_which(TYPE_VALIDITY)
+    , d_unknownExplanation(unknownExplanation)
+    , d_inputName(inputName)
+{
+  PrettyCheckArgument(v == VALIDITY_UNKNOWN,
+                      "improper use of unknown-result constructor");
+}
+
 Result::Result(const std::string& instr, std::string inputName) :
   d_sat(SAT_UNKNOWN),
   d_validity(VALIDITY_UNKNOWN),
@@ -78,6 +134,13 @@ Result::Result(const std::string& instr, std::string inputName) :
   }
 }
 
+Result::UnknownExplanation Result::whyUnknown() const {
+  PrettyCheckArgument( isUnknown(), this,
+                       "This result is not unknown, so the reason for "
+                       "being unknown cannot be inquired of it" );
+  return d_unknownExplanation;
+}
+
 bool Result::operator==(const Result& r) const throw() {
   if(d_which != r.d_which) {
     return false;