diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-03 03:07:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-03 03:07:58 +0000 |
commit | 541379b3d361e255cd664207f8b2e278a5b5e3eb (patch) | |
tree | c6f563d69bc563116836a6d2ed85e34ba51bc31e /src/include/result.h | |
parent | a101d3298691265ee4cf72bed1ca59cd60318839 (diff) |
additional headers
Diffstat (limited to 'src/include/result.h')
-rw-r--r-- | src/include/result.h | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/src/include/result.h b/src/include/result.h new file mode 100644 index 000000000..1cecc5301 --- /dev/null +++ b/src/include/result.h @@ -0,0 +1,61 @@ +/********************* -*- C++ -*- */ +/** result.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#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 { + UNSAT = 0, + SAT = 1, + UNKNOWN = 2 + } SAT; + + enum { + INVALID = 0, + VALID = 1, + UNKNOWN = 2 + } Validity; + + enum { + REQUIRES_FULL_CHECK, + INCOMPLETE, + TIMEOUT, + BAIL, + OTHER + } UnknownExplanation; + +private: + SAT d_sat; + Validity d_validity; + enum { SAT, VALIDITY } d_which; + +public: + Result(SAT); + Result(Validity); + + SAT isSAT(); + Validity isValid(); + UnknownExplanation whyUnknown(); + +};/* class Result */ + +}/* CVC4 namespace */ |