summaryrefslogtreecommitdiff
path: root/src/include/result.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/include/result.h')
-rw-r--r--src/include/result.h34
1 files changed, 18 insertions, 16 deletions
diff --git a/src/include/result.h b/src/include/result.h
index 1cecc5301..cfabd3be2 100644
--- a/src/include/result.h
+++ b/src/include/result.h
@@ -23,39 +23,41 @@ namespace CVC4 {
*/
class Result {
public:
- enum {
+ enum SAT {
UNSAT = 0,
SAT = 1,
- UNKNOWN = 2
- } SAT;
+ SAT_UNKNOWN = 2
+ };
- enum {
+ enum Validity {
INVALID = 0,
VALID = 1,
- UNKNOWN = 2
- } Validity;
+ VALIDITY_UNKNOWN = 2
+ };
- enum {
+ enum UnknownExplanation {
REQUIRES_FULL_CHECK,
INCOMPLETE,
TIMEOUT,
BAIL,
OTHER
- } UnknownExplanation;
+ };
private:
- SAT d_sat;
- Validity d_validity;
- enum { SAT, VALIDITY } d_which;
+ enum SAT d_sat;
+ enum Validity d_validity;
+ enum { TYPE_SAT, TYPE_VALIDITY } d_which;
public:
- Result(SAT);
- Result(Validity);
+ Result(enum SAT);
+ Result(enum Validity);
- SAT isSAT();
- Validity isValid();
- UnknownExplanation whyUnknown();
+ enum SAT isSAT();
+ enum Validity isValid();
+ enum UnknownExplanation whyUnknown();
};/* class Result */
}/* CVC4 namespace */
+
+#endif /* __CVC4_RESULT_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback