1 files changed, 206 insertions, 0 deletions
diff --git a/src/expr/result.h b/src/expr/result.h
new file mode 100644
index 000000000..74697eba6
--- /dev/null
+++ b/src/expr/result.h
@@ -0,0 +1,206 @@
+/*********************                                                        */
+/*! \file result.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Encapsulation of the result of a query.
+ **
+ ** Encapsulation of the result of a query.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__RESULT_H
+#define __CVC4__RESULT_H
+
+#include <iostream>
+#include <string>
+
+#include "base/exception.h"
+#include "options/language.h"
+
+namespace CVC4 {
+
+class Result;
+
+std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC;
+
+/**
+ * Three-valued SMT result, with optional explanation.
+ */
+class CVC4_PUBLIC Result {
+public:
+  enum Sat {
+    UNSAT = 0,
+    SAT = 1,
+    SAT_UNKNOWN = 2
+  };
+
+  enum Validity {
+    INVALID = 0,
+    VALID = 1,
+    VALIDITY_UNKNOWN = 2
+  };
+
+  enum Type {
+    TYPE_SAT,
+    TYPE_VALIDITY,
+    TYPE_NONE
+  };
+
+  enum UnknownExplanation {
+    REQUIRES_FULL_CHECK,
+    INCOMPLETE,
+    TIMEOUT,
+    RESOURCEOUT,
+    MEMOUT,
+    INTERRUPTED,
+    NO_STATUS,
+    UNSUPPORTED,
+    OTHER,
+    UNKNOWN_REASON
+  };
+
+private:
+  enum Sat d_sat;
+  enum Validity d_validity;
+  enum Type d_which;
+  enum UnknownExplanation d_unknownExplanation;
+  std::string d_inputName;
+
+public:
+  Result() :
+    d_sat(SAT_UNKNOWN),
+    d_validity(VALIDITY_UNKNOWN),
+    d_which(TYPE_NONE),
+    d_unknownExplanation(UNKNOWN_REASON),
+    d_inputName("") {
+  }
+  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) {
+    CheckArgument(s != SAT_UNKNOWN,
+                  "Must provide a reason for satisfiability being unknown");
+  }
+  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) {
+    CheckArgument(v != VALIDITY_UNKNOWN,
+                  "Must provide a reason for validity being unknown");
+  }
+  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) {
+    CheckArgument(s == SAT_UNKNOWN,
+                  "improper use of unknown-result constructor");
+  }
+  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) {
+    CheckArgument(v == VALIDITY_UNKNOWN,
+                  "improper use of unknown-result constructor");
+  }
+  Result(const std::string& s, std::string inputName = "");
+
+  Result(const Result& r, std::string inputName) {
+    *this = r;
+    d_inputName = inputName;
+  }
+
+  enum Sat isSat() const {
+    return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
+  }
+  enum Validity isValid() const {
+    return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
+  }
+  bool isUnknown() const {
+    return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
+  }
+  Type getType() const {
+    return d_which;
+  }
+  bool isNull() const {
+    return d_which == TYPE_NONE;
+  }
+  enum UnknownExplanation whyUnknown() const {
+    CheckArgument( isUnknown(), this,
+                   "This result is not unknown, so the reason for "
+                   "being unknown cannot be inquired of it" );
+    return d_unknownExplanation;
+  }
+
+  bool operator==(const Result& r) const throw();
+  inline bool operator!=(const Result& r) const throw();
+  Result asSatisfiabilityResult() const throw();
+  Result asValidityResult() const throw();
+
+  std::string toString() const;
+
+  std::string getInputName() const { return d_inputName; }
+
+  /**
+   * Write a Result out to a stream in this language.
+   */
+  void toStream(std::ostream& out, OutputLanguage language) const throw();
+
+  /**
+   * This is mostly the same the default
+   * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN,
+   *
+   */
+  void toStreamSmt2(std::ostream& out) const throw();
+
+  /**
+   * Write a Result out to a stream in the Tptp format
+   */
+  void toStreamTptp(std::ostream& out) const throw();
+
+  /**
+   * Write a Result out to a stream.
+   *
+   * The default implementation writes a reasonable string in lowercase
+   * for sat, unsat, valid, invalid, or unknown results.  This behavior
+   * is overridable by each Printer, since sometimes an output language
+   * has a particular preference for how results should appear.
+   */
+  void toStreamDefault(std::ostream& out) const throw();
+};/* class Result */
+
+inline bool Result::operator!=(const Result& r) const throw() {
+  return !(*this == r);
+}
+
+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;
+
+bool operator==(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC;
+bool operator==(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
+
+bool operator!=(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC;
+bool operator!=(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RESULT_H */