diff options
Diffstat (limited to 'src/expr/result.h')
| -rw-r--r-- | src/expr/result.h | 177 |
1 files changed, 0 insertions, 177 deletions
diff --git a/src/expr/result.h b/src/expr/result.h deleted file mode 100644 index 8069f7ef9..000000000 --- a/src/expr/result.h +++ /dev/null @@ -1,177 +0,0 @@ -/********************* */ -/*! \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(); - - Result(enum Sat s, std::string inputName = ""); - - Result(enum Validity v, std::string inputName = ""); - - Result(enum Sat s, - enum UnknownExplanation unknownExplanation, - std::string inputName = ""); - - Result(enum Validity v, enum UnknownExplanation unknownExplanation, - std::string inputName = ""); - - 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; - - 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 */ |