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/expr | |
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/expr')
-rw-r--r-- | src/expr/Makefile.am | 3 | ||||
-rw-r--r-- | src/expr/result.cpp | 358 | ||||
-rw-r--r-- | src/expr/result.h | 177 | ||||
-rw-r--r-- | src/expr/result.i | 20 |
4 files changed, 0 insertions, 558 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 63f31ed67..d4964f56a 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -70,8 +70,6 @@ libexpr_la_SOURCES = \ predicate.cpp \ record.cpp \ record.h \ - result.cpp \ - result.h \ uninterpreted_constant.cpp \ uninterpreted_constant.h @@ -113,7 +111,6 @@ EXTRA_DIST = \ resource_manager.i \ sexpr.i \ record.i \ - result.i \ predicate.i \ variable_type_map.i \ uninterpreted_constant.i diff --git a/src/expr/result.cpp b/src/expr/result.cpp deleted file mode 100644 index aeb62b0c3..000000000 --- a/src/expr/result.cpp +++ /dev/null @@ -1,358 +0,0 @@ -/********************* */ -/*! \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 "expr/result.h" - -#include <algorithm> -#include <cctype> -#include <iostream> -#include <string> - -#include "base/cvc4_assert.h" -#include "expr/node.h" - -using namespace std; - -#warning "TODO: Move Node::setLanguage out of Node and into util/. Then move Result back into util/." - -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, Node::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/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 */ diff --git a/src/expr/result.i b/src/expr/result.i deleted file mode 100644 index becbe9aa9..000000000 --- a/src/expr/result.i +++ /dev/null @@ -1,20 +0,0 @@ -%{ -#include "expr/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 "expr/result.h" |