from meeting

1 files changed, 65 insertions, 0 deletions

diff --git a/src/util/result.h b/src/util/result.h
new file mode 100644
index 000000000..50f488682
--- /dev/null
+++ b/src/util/result.h
@@ -0,0 +1,65 @@
+/*********************                                           -*- C++ -*-  */
+/** result.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ **/
+
+#ifndef __CVC4_RESULT_H
+#define __CVC4_RESULT_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: subclass to provide models, etc.  This is really just
+// intended as a three-valued response code.
+
+/**
+ * Three-valued, immutable SMT result, with optional explanation.
+ */
+class Result {
+public:
+  enum SAT {
+    UNSAT = 0,
+    SAT = 1,
+    SAT_UNKNOWN = 2
+  };
+
+  enum Validity {
+    INVALID = 0,
+    VALID = 1,
+    VALIDITY_UNKNOWN = 2
+  };
+
+  enum UnknownExplanation {
+    REQUIRES_FULL_CHECK,
+    INCOMPLETE,
+    TIMEOUT,
+    BAIL,
+    OTHER
+  };
+
+private:
+  enum SAT      d_sat;
+  enum Validity d_validity;
+  enum { TYPE_SAT, TYPE_VALIDITY } d_which;
+
+public:
+  Result(enum SAT);
+  Result(enum Validity);
+
+  enum SAT isSAT();
+  enum Validity isValid();
+  enum UnknownExplanation whyUnknown();
+
+};/* class Result */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_RESULT_H */