diff options
author | Tim King <taking@google.com> | 2016-01-05 16:29:44 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-05 16:29:44 -0800 |
commit | 5eabda0f55cee3be81aa7ae126269c32e818322f (patch) | |
tree | b873e4cb8e5d37ff3bb70596494bc5964aaef135 /src/util | |
parent | b717513e2a1d956c4456d13e0625957fc84c2449 (diff) |
Add SmtGlobals Class
- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 3 | ||||
-rw-r--r-- | src/util/result.cpp | 356 | ||||
-rw-r--r-- | src/util/result.h | 177 | ||||
-rw-r--r-- | src/util/result.i | 20 |
4 files changed, 556 insertions, 0 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 55f1a14da..b06666ae3 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -43,6 +43,8 @@ libutil_la_SOURCES = \ proof.h \ regexp.cpp \ regexp.h \ + result.cpp \ + result.h \ smt2_quote_string.cpp \ smt2_quote_string.h \ subrange_bound.cpp \ @@ -89,6 +91,7 @@ EXTRA_DIST = \ rational_gmp_imp.cpp \ rational_gmp_imp.h \ regexp.i \ + result.i \ subrange_bound.i \ tuple.i \ unsafe_interrupt_exception.i diff --git a/src/util/result.cpp b/src/util/result.cpp new file mode 100644 index 000000000..b981164a4 --- /dev/null +++ b/src/util/result.cpp @@ -0,0 +1,356 @@ +/********************* */ +/*! \file result.cpp + ** \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 "util/result.h" + +#include <algorithm> +#include <cctype> +#include <iostream> +#include <string> + +#include "base/cvc4_assert.h" +#include "options/set_language.h" + +using namespace std; + +namespace CVC4 { + +Result::Result() + : d_sat(SAT_UNKNOWN) + , d_validity(VALIDITY_UNKNOWN) + , d_which(TYPE_NONE) + , d_unknownExplanation(UNKNOWN_REASON) + , d_inputName("") +{ } + + +Result::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) +{ + PrettyCheckArgument(s != SAT_UNKNOWN, + "Must provide a reason for satisfiability being unknown"); +} + +Result::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) +{ + PrettyCheckArgument(v != VALIDITY_UNKNOWN, + "Must provide a reason for validity being unknown"); +} + + +Result::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) +{ + PrettyCheckArgument(s == SAT_UNKNOWN, + "improper use of unknown-result constructor"); +} + +Result::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) +{ + PrettyCheckArgument(v == VALIDITY_UNKNOWN, + "improper use of unknown-result constructor"); +} + +Result::Result(const std::string& instr, std::string inputName) : + d_sat(SAT_UNKNOWN), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_NONE), + d_unknownExplanation(UNKNOWN_REASON), + d_inputName(inputName) { + string s = instr; + transform(s.begin(), s.end(), s.begin(), ::tolower); + if(s == "sat" || s == "satisfiable") { + d_which = TYPE_SAT; + d_sat = SAT; + } else if(s == "unsat" || s == "unsatisfiable") { + d_which = TYPE_SAT; + d_sat = UNSAT; + } else if(s == "valid") { + d_which = TYPE_VALIDITY; + d_validity = VALID; + } else if(s == "invalid") { + d_which = TYPE_VALIDITY; + d_validity = INVALID; + } else if(s == "incomplete") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = INCOMPLETE; + } else if(s == "timeout") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = TIMEOUT; + } else if(s == "resourceout") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = RESOURCEOUT; + } else if(s == "memout") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = MEMOUT; + } else if(s == "interrupted") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = INTERRUPTED; + } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + } else { + IllegalArgument(s, "expected satisfiability/validity result, " + "instead got `%s'", s.c_str()); + } +} + +Result::UnknownExplanation Result::whyUnknown() const { + PrettyCheckArgument( isUnknown(), this, + "This result is not unknown, so the reason for " + "being unknown cannot be inquired of it" ); + return d_unknownExplanation; +} + +bool Result::operator==(const Result& r) const throw() { + if(d_which != r.d_which) { + return false; + } + if(d_which == TYPE_SAT) { + return d_sat == r.d_sat && + ( d_sat != SAT_UNKNOWN || + d_unknownExplanation == r.d_unknownExplanation ); + } + if(d_which == TYPE_VALIDITY) { + return d_validity == r.d_validity && + ( d_validity != VALIDITY_UNKNOWN || + d_unknownExplanation == r.d_unknownExplanation ); + } + return false; +} + +bool operator==(enum Result::Sat sr, const Result& r) throw() { + return r == sr; +} + +bool operator==(enum Result::Validity vr, const Result& r) throw() { + return r == vr; +} +bool operator!=(enum Result::Sat s, const Result& r) throw(){ + return !(s == r); +} +bool operator!=(enum Result::Validity v, const Result& r) throw(){ + return !(v == r); +} + +Result Result::asSatisfiabilityResult() const throw() { + if(d_which == TYPE_SAT) { + return *this; + } + + if(d_which == TYPE_VALIDITY) { + switch(d_validity) { + + case INVALID: + return Result(SAT, d_inputName); + + case VALID: + return Result(UNSAT, d_inputName); + + case VALIDITY_UNKNOWN: + return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName); + + default: + Unhandled(d_validity); + } + } + + // TYPE_NONE + return Result(SAT_UNKNOWN, NO_STATUS, d_inputName); +} + +Result Result::asValidityResult() const throw() { + if(d_which == TYPE_VALIDITY) { + return *this; + } + + if(d_which == TYPE_SAT) { + switch(d_sat) { + + case SAT: + return Result(INVALID, d_inputName); + + case UNSAT: + return Result(VALID, d_inputName); + + case SAT_UNKNOWN: + return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName); + + default: + Unhandled(d_sat); + } + } + + // TYPE_NONE + return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName); +} + +string Result::toString() const { + stringstream ss; + ss << *this; + return ss.str(); +} + +ostream& operator<<(ostream& out, enum Result::Sat s) { + switch(s) { + case Result::UNSAT: out << "UNSAT"; break; + case Result::SAT: out << "SAT"; break; + case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break; + default: Unhandled(s); + } + return out; +} + +ostream& operator<<(ostream& out, enum Result::Validity v) { + switch(v) { + case Result::INVALID: out << "INVALID"; break; + case Result::VALID: out << "VALID"; break; + case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break; + default: Unhandled(v); + } + return out; +} + +ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) { + switch(e) { + case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break; + case Result::INCOMPLETE: out << "INCOMPLETE"; break; + case Result::TIMEOUT: out << "TIMEOUT"; break; + case Result::RESOURCEOUT: out << "RESOURCEOUT"; break; + case Result::MEMOUT: out << "MEMOUT"; break; + case Result::INTERRUPTED: out << "INTERRUPTED"; break; + case Result::NO_STATUS: out << "NO_STATUS"; break; + case Result::UNSUPPORTED: out << "UNSUPPORTED"; break; + case Result::OTHER: out << "OTHER"; break; + case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break; + default: Unhandled(e); + } + return out; +} + +ostream& operator<<(ostream& out, const Result& r) { + r.toStream(out, language::SetLanguage::getLanguage(out)); + return out; +}/* operator<<(ostream&, const Result&) */ + + +void Result::toStreamDefault(std::ostream& out) const throw() { + if(getType() == Result::TYPE_SAT) { + switch(isSat()) { + case Result::UNSAT: + out << "unsat"; + break; + case Result::SAT: + out << "sat"; + break; + case Result::SAT_UNKNOWN: + out << "unknown"; + if(whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << whyUnknown() << ")"; + } + break; + } + } else { + switch(isValid()) { + case Result::INVALID: + out << "invalid"; + break; + case Result::VALID: + out << "valid"; + break; + case Result::VALIDITY_UNKNOWN: + out << "unknown"; + if(whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << whyUnknown() << ")"; + } + break; + } + } +}/* Result::toStreamDefault() */ + + +void Result::toStreamSmt2(ostream& out) const throw(){ + if(getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) { + out << "unknown"; + } else { + toStreamDefault(out); + } +} + +void Result::toStreamTptp(std::ostream& out) const throw() { + out << "% SZS status "; + if(isSat() == Result::SAT) { + out << "Satisfiable"; + } else if(isSat() == Result::UNSAT) { + out << "Unsatisfiable"; + } else if(isValid() == Result::VALID) { + out << "Theorem"; + } else if(isValid() == Result::INVALID) { + out << "CounterSatisfiable"; + } else { + out << "GaveUp"; + } + out << " for " << getInputName(); +} + +void Result::toStream(std::ostream& out, OutputLanguage language) const throw() { + switch(language) { + case language::output::LANG_SMTLIB_V2_0: + case language::output::LANG_SMTLIB_V2_5: + case language::output::LANG_SYGUS: + case language::output::LANG_Z3STR: + toStreamSmt2(out); + break; + case language::output::LANG_TPTP: + toStreamTptp(out); + break; + case language::output::LANG_AST: + case language::output::LANG_AUTO: + case language::output::LANG_CVC3: + case language::output::LANG_CVC4: + case language::output::LANG_MAX: + case language::output::LANG_SMTLIB_V1: + default: + toStreamDefault(out); + break; + }; +} + +}/* CVC4 namespace */ diff --git a/src/util/result.h b/src/util/result.h new file mode 100644 index 000000000..8069f7ef9 --- /dev/null +++ b/src/util/result.h @@ -0,0 +1,177 @@ +/********************* */ +/*! \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 */ diff --git a/src/util/result.i b/src/util/result.i new file mode 100644 index 000000000..b77bfd881 --- /dev/null +++ b/src/util/result.i @@ -0,0 +1,20 @@ +%{ +#include "util/result.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const Result& r); + +%rename(equals) CVC4::Result::operator==(const Result& r) const; +%ignore CVC4::Result::operator!=(const Result& r) const; + +%ignore CVC4::operator<<(std::ostream&, enum Result::Sat); +%ignore CVC4::operator<<(std::ostream&, enum Result::Validity); +%ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation); + +%ignore CVC4::operator==(enum Result::Sat, const Result&); +%ignore CVC4::operator!=(enum Result::Sat, const Result&); + +%ignore CVC4::operator==(enum Result::Validity, const Result&); +%ignore CVC4::operator!=(enum Result::Validity, const Result&); + +%include "util/result.h" |