From 3ecadd3bf0575a9502ce0a6af63ac936cadf4291 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 1 Oct 2016 14:06:20 -0700 Subject: Removing the throw specifiers from SExpr. --- src/util/sexpr.h | 60 +++++++++++++++++++++++++++----------------------------- 1 file changed, 29 insertions(+), 31 deletions(-) (limited to 'src/util/sexpr.h') diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 9c80a1b1f..2948cba4b 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -40,18 +40,18 @@ namespace CVC4 { class CVC4_PUBLIC SExprKeyword { std::string d_str; -public: + + public: SExprKeyword(const std::string& s) : d_str(s) {} const std::string& getString() const { return d_str; } -};/* class SExpr::Keyword */ +}; /* class SExpr::Keyword */ /** * A simple S-expression. An S-expression is either an atom with a * string value, or a list of other S-expressions. */ class CVC4_PUBLIC SExpr { -public: - + public: typedef SExprKeyword Keyword; SExpr(); @@ -138,7 +138,6 @@ public: /** Is this S-expression different from another? */ bool operator!=(const SExpr& s) const; - /** * This returns the best match in the following order: * match atom with @@ -157,21 +156,23 @@ public: /** * Parses a list of list of atoms. */ - static SExpr parseListOfListOfAtoms(const std::vector< std::vector >& atoms_lists); - + static SExpr parseListOfListOfAtoms( + const std::vector >& atoms_lists); /** * Outputs the SExpr onto the ostream out. This version reads defaults to the - * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level is + * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level + * is * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise. */ - static void toStream(std::ostream& out, const SExpr& sexpr) throw(); + static void toStream(std::ostream& out, const SExpr& sexpr); /** * Outputs the SExpr onto the ostream out. This version sets the indent level * to 2 if PrettySExprs::getPrettySExprs() is on. */ - static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw(); + static void toStream(std::ostream& out, const SExpr& sexpr, + OutputLanguage language); /** * Outputs the SExpr onto the ostream out. @@ -181,19 +182,20 @@ public: * Otherwise this prints using toStreamRec(). * * TIM: Keywords that are children are not currently quoted. This seems - * incorrect but I am just reproduicing the old behavior even if it does not make + * incorrect but I am just reproduicing the old behavior even if it does not + * make * sense. */ - static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw(); - -private: + static void toStream(std::ostream& out, const SExpr& sexpr, + OutputLanguage language, int indent); + private: /** * Simple printer for SExpr to an ostream. * The current implementation is language independent. */ - static void toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw(); - + static void toStreamRec(std::ostream& out, const SExpr& sexpr, + OutputLanguage language, int indent); /** Returns true if this language quotes Keywords when printing. */ static bool languageQuotesKeywords(OutputLanguage language); @@ -222,11 +224,12 @@ private: * Whenever the SExpr isAtom() holds, this points at NULL. * * This should be a pointer in case the implementation of vector ever - * directly contained or allocated an SExpr. If this happened this would trigger, + * directly contained or allocated an SExpr. If this happened this would + * trigger, * either the size being infinite or SExpr() being an infinite loop. */ SExprVector* d_children; -};/* class SExpr */ +}; /* class SExpr */ /** Prints an SExpr. */ std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC; @@ -245,7 +248,7 @@ class CVC4_PUBLIC PrettySExprs { */ bool d_prettySExprs; -public: + public: /** * Construct a PrettySExprs with the given setting. */ @@ -273,21 +276,17 @@ public: std::ostream& d_out; bool d_oldPrettySExprs; - public: - - inline Scope(std::ostream& out, bool prettySExprs) : - d_out(out), - d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) { + public: + inline Scope(std::ostream& out, bool prettySExprs) + : d_out(out), d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) { PrettySExprs::setPrettySExprs(out, prettySExprs); } - inline ~Scope() { - PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs); - } + inline ~Scope() { PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs); } - };/* class PrettySExprs::Scope */ + }; /* class PrettySExprs::Scope */ -};/* class PrettySExprs */ +}; /* class PrettySExprs */ /** * Sets the default pretty-sexprs setting for an ostream. Use like this: @@ -299,7 +298,6 @@ public: */ std::ostream& operator<<(std::ostream& out, PrettySExprs ps); - -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__SEXPR_H */ -- cgit v1.2.3 From f95488791b2d14e0710fea09202bb5638e66e93d Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 1 Oct 2016 15:40:30 -0700 Subject: Removing the throw specifiers from Result. --- src/util/result.cpp | 383 +++++++++++++++++++++++++++------------------------- src/util/result.h | 75 ++++------ src/util/sexpr.h | 5 +- 3 files changed, 229 insertions(+), 234 deletions(-) (limited to 'src/util/sexpr.h') diff --git a/src/util/result.cpp b/src/util/result.cpp index 51b1a8de1..af28269f1 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -28,167 +28,152 @@ 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("") -{ } - + : 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) -{ + : 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) -{ + : 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) -{ + : 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) -{ + : 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) { +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") { + if (s == "sat" || s == "satisfiable") { d_which = TYPE_SAT; d_sat = SAT; - } else if(s == "unsat" || s == "unsatisfiable") { + } else if (s == "unsat" || s == "unsatisfiable") { d_which = TYPE_SAT; d_sat = UNSAT; - } else if(s == "valid") { + } else if (s == "valid") { d_which = TYPE_VALIDITY; d_validity = VALID; - } else if(s == "invalid") { + } else if (s == "invalid") { d_which = TYPE_VALIDITY; d_validity = INVALID; - } else if(s == "incomplete") { + } else if (s == "incomplete") { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = INCOMPLETE; - } else if(s == "timeout") { + } else if (s == "timeout") { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = TIMEOUT; - } else if(s == "resourceout") { + } else if (s == "resourceout") { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = RESOURCEOUT; - } else if(s == "memout") { + } else if (s == "memout") { d_which = TYPE_SAT; d_sat = SAT_UNKNOWN; d_unknownExplanation = MEMOUT; - } else if(s == "interrupted") { + } 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) { + } 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()); + 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" ); + 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) { +bool Result::operator==(const Result& r) const { + 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_SAT) { + return d_sat == r.d_sat && (d_sat != SAT_UNKNOWN || + d_unknownExplanation == r.d_unknownExplanation); } - if(d_which == TYPE_VALIDITY) { + if (d_which == TYPE_VALIDITY) { return d_validity == r.d_validity && - ( d_validity != VALIDITY_UNKNOWN || - d_unknownExplanation == r.d_unknownExplanation ); + (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::Sat sr, const Result& r) { 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); -} +bool operator==(enum Result::Validity vr, const Result& r) { return r == vr; } +bool operator!=(enum Result::Sat s, const Result& r) { return !(s == r); } +bool operator!=(enum Result::Validity v, const Result& r) { return !(v == r); } -Result Result::asSatisfiabilityResult() const throw() { - if(d_which == TYPE_SAT) { +Result Result::asSatisfiabilityResult() const { + if (d_which == TYPE_SAT) { return *this; } - if(d_which == TYPE_VALIDITY) { - switch(d_validity) { - - case INVALID: - return Result(SAT, d_inputName); + if (d_which == TYPE_VALIDITY) { + switch (d_validity) { + case INVALID: + return Result(SAT, d_inputName); - case VALID: - return Result(UNSAT, d_inputName); + case VALID: + return Result(UNSAT, d_inputName); - case VALIDITY_UNKNOWN: - return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName); + case VALIDITY_UNKNOWN: + return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName); - default: - Unhandled(d_validity); + default: + Unhandled(d_validity); } } @@ -196,25 +181,24 @@ Result Result::asSatisfiabilityResult() const throw() { return Result(SAT_UNKNOWN, NO_STATUS, d_inputName); } -Result Result::asValidityResult() const throw() { - if(d_which == TYPE_VALIDITY) { +Result Result::asValidityResult() const { + if (d_which == TYPE_VALIDITY) { return *this; } - if(d_which == TYPE_SAT) { - switch(d_sat) { - - case SAT: - return Result(INVALID, d_inputName); + if (d_which == TYPE_SAT) { + switch (d_sat) { + case SAT: + return Result(INVALID, d_inputName); - case UNSAT: - return Result(VALID, d_inputName); + case UNSAT: + return Result(VALID, d_inputName); - case SAT_UNKNOWN: - return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName); + case SAT_UNKNOWN: + return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName); - default: - Unhandled(d_sat); + default: + Unhandled(d_sat); } } @@ -229,38 +213,73 @@ string Result::toString() const { } 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); + 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); + 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); + 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; } @@ -268,61 +287,59 @@ ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) { 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; +} /* operator<<(ostream&, const Result&) */ + +void Result::toStreamDefault(std::ostream& out) const { + 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; + 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() */ +} /* Result::toStreamDefault() */ - -void Result::toStreamSmt2(ostream& out) const throw(){ - if(getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) { +void Result::toStreamSmt2(ostream& out) const { + if (getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) { out << "unknown"; } else { toStreamDefault(out); } } -void Result::toStreamTptp(std::ostream& out) const throw() { +void Result::toStreamTptp(std::ostream& out) const { out << "% SZS status "; - if(isSat() == Result::SAT) { + if (isSat() == Result::SAT) { out << "Satisfiable"; - } else if(isSat() == Result::UNSAT) { + } else if (isSat() == Result::UNSAT) { out << "Unsatisfiable"; - } else if(isValid() == Result::VALID) { + } else if (isValid() == Result::VALID) { out << "Theorem"; - } else if(isValid() == Result::INVALID) { + } else if (isValid() == Result::INVALID) { out << "CounterSatisfiable"; } else { out << "GaveUp"; @@ -330,27 +347,27 @@ void Result::toStreamTptp(std::ostream& out) const throw() { 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; +void Result::toStream(std::ostream& out, OutputLanguage language) const { + 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 */ +} /* CVC4 namespace */ diff --git a/src/util/result.h b/src/util/result.h index 8303ad0e8..80fbc0cf7 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -35,24 +35,12 @@ 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 - }; + public: + enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 }; - enum Validity { - INVALID = 0, - VALID = 1, - VALIDITY_UNKNOWN = 2 - }; + enum Validity { INVALID = 0, VALID = 1, VALIDITY_UNKNOWN = 2 }; - enum Type { - TYPE_SAT, - TYPE_VALIDITY, - TYPE_NONE - }; + enum Type { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE }; enum UnknownExplanation { REQUIRES_FULL_CHECK, @@ -67,23 +55,21 @@ public: UNKNOWN_REASON }; -private: + private: enum Sat d_sat; enum Validity d_validity; enum Type d_which; enum UnknownExplanation d_unknownExplanation; std::string d_inputName; -public: - + public: Result(); Result(enum Sat s, std::string inputName = ""); Result(enum Validity v, std::string inputName = ""); - Result(enum Sat s, - enum UnknownExplanation unknownExplanation, + Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = ""); Result(enum Validity v, enum UnknownExplanation unknownExplanation, @@ -96,9 +82,7 @@ public: d_inputName = inputName; } - enum Sat isSat() const { - return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; - } + 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; @@ -108,20 +92,16 @@ public: return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; } - Type getType() const { - return d_which; - } + Type getType() const { return d_which; } - bool isNull() const { - return d_which == TYPE_NONE; - } + 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(); + bool operator==(const Result& r) const; + inline bool operator!=(const Result& r) const; + Result asSatisfiabilityResult() const; + Result asValidityResult() const; std::string toString() const; @@ -130,19 +110,19 @@ public: /** * Write a Result out to a stream in this language. */ - void toStream(std::ostream& out, OutputLanguage language) const throw(); + void toStream(std::ostream& out, OutputLanguage language) const; /** * This is mostly the same the default * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN, * */ - void toStreamSmt2(std::ostream& out) const throw(); + void toStreamSmt2(std::ostream& out) const; /** * Write a Result out to a stream in the Tptp format */ - void toStreamTptp(std::ostream& out) const throw(); + void toStreamTptp(std::ostream& out) const; /** * Write a Result out to a stream. @@ -152,26 +132,23 @@ public: * 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 */ + void toStreamDefault(std::ostream& out) const; +}; /* class Result */ -inline bool Result::operator!=(const Result& r) const throw() { - return !(*this == r); -} +inline bool Result::operator!=(const Result& r) const { return !(*this == r); } -std::ostream& operator<<(std::ostream& out, - enum Result::Sat s) CVC4_PUBLIC; +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) CVC4_PUBLIC; +bool operator==(enum Result::Validity v, const Result& r) 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) CVC4_PUBLIC; +bool operator!=(enum Result::Validity v, const Result& r) CVC4_PUBLIC; -}/* CVC4 namespace */ +} /* CVC4 namespace */ #endif /* __CVC4__RESULT_H */ diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 2948cba4b..0b517570e 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -39,11 +39,12 @@ namespace CVC4 { class CVC4_PUBLIC SExprKeyword { - std::string d_str; - public: SExprKeyword(const std::string& s) : d_str(s) {} const std::string& getString() const { return d_str; } + + private: + std::string d_str; }; /* class SExpr::Keyword */ /** -- cgit v1.2.3