From 256d4093ab6ac3b792c6f1f11131124d1ae6b069 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 4 Jan 2018 13:09:39 -0800 Subject: [PATCH] Removing miscellaneous throw specifiers. (#1474) --- src/cvc4.i | 1 + src/decision/justification_heuristic.cpp | 3 +- src/decision/justification_heuristic.h | 2 +- src/expr/array_store_all.cpp | 22 ++++++++----- src/expr/array_store_all.h | 18 +++++------ src/expr/expr_manager_template.cpp | 6 ++-- src/expr/expr_manager_template.h | 25 ++------------- src/expr/node_manager.h | 5 +-- src/main/main.h | 9 +++--- src/main/portfolio_util.h | 4 +-- src/main/util.cpp | 3 +- src/smt_util/boolean_simplification.cpp | 7 ++--- src/smt_util/boolean_simplification.h | 39 ++++++++++++++---------- src/smt_util/lemma_input_channel.h | 6 ++-- src/smt_util/lemma_output_channel.h | 12 ++++---- 15 files changed, 80 insertions(+), 82 deletions(-) diff --git a/src/cvc4.i b/src/cvc4.i index 58dceb6b1..2f7205b19 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -3,6 +3,7 @@ #if SWIG_VERSION < 0x030000 %define final %enddef %define override %enddef +%define noexcept %enddef #endif %import "bindings/swig.h" diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index a60f2c365..aae802490 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -55,7 +55,8 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, Trace("decision") << "Justification heuristic enabled" << std::endl; } -JustificationHeuristic::~JustificationHeuristic() throw() { +JustificationHeuristic::~JustificationHeuristic() +{ smtStatisticsRegistry()->unregisterStat(&d_helfulness); smtStatisticsRegistry()->unregisterStat(&d_giveup); smtStatisticsRegistry()->unregisterStat(&d_timestat); diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 70fecb871..210ab4d5c 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -115,7 +115,7 @@ public: context::UserContext *uc, context::Context *c); - ~JustificationHeuristic() throw(); + ~JustificationHeuristic(); prop::SatLiteral getNext(bool &stopSearch); diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp index ff026057c..65d16d9cc 100644 --- a/src/expr/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -65,33 +65,39 @@ ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other) { return *this; } -const ArrayType& ArrayStoreAll::getType() const throw() { return *d_type; } +const ArrayType& ArrayStoreAll::getType() const { return *d_type; } -const Expr& ArrayStoreAll::getExpr() const throw() { return *d_expr; } +const Expr& ArrayStoreAll::getExpr() const { return *d_expr; } -bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const throw() { +bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const +{ return getType() == asa.getType() && getExpr() == asa.getExpr(); } -bool ArrayStoreAll::operator!=(const ArrayStoreAll& asa) const throw() { +bool ArrayStoreAll::operator!=(const ArrayStoreAll& asa) const +{ return !(*this == asa); } -bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const throw() { +bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const +{ return (getType() < asa.getType()) || (getType() == asa.getType() && getExpr() < asa.getExpr()); } -bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const throw() { +bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const +{ return (getType() < asa.getType()) || (getType() == asa.getType() && getExpr() <= asa.getExpr()); } -bool ArrayStoreAll::operator>(const ArrayStoreAll& asa) const throw() { +bool ArrayStoreAll::operator>(const ArrayStoreAll& asa) const +{ return !(*this <= asa); } -bool ArrayStoreAll::operator>=(const ArrayStoreAll& asa) const throw() { +bool ArrayStoreAll::operator>=(const ArrayStoreAll& asa) const +{ return !(*this < asa); } diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h index 308794f48..6b265d740 100644 --- a/src/expr/array_store_all.h +++ b/src/expr/array_store_all.h @@ -40,20 +40,20 @@ class CVC4_PUBLIC ArrayStoreAll { * not a constant of type `type`. */ ArrayStoreAll(const ArrayType& type, const Expr& expr); - ~ArrayStoreAll() throw(); + ~ArrayStoreAll(); ArrayStoreAll(const ArrayStoreAll& other); ArrayStoreAll& operator=(const ArrayStoreAll& other); - const ArrayType& getType() const throw(); - const Expr& getExpr() const throw(); + const ArrayType& getType() const; + const Expr& getExpr() const; - bool operator==(const ArrayStoreAll& asa) const throw(); - bool operator!=(const ArrayStoreAll& asa) const throw(); - bool operator<(const ArrayStoreAll& asa) const throw(); - bool operator<=(const ArrayStoreAll& asa) const throw(); - bool operator>(const ArrayStoreAll& asa) const throw(); - bool operator>=(const ArrayStoreAll& asa) const throw(); + bool operator==(const ArrayStoreAll& asa) const; + bool operator!=(const ArrayStoreAll& asa) const; + bool operator<(const ArrayStoreAll& asa) const; + bool operator<=(const ArrayStoreAll& asa) const; + bool operator>(const ArrayStoreAll& asa) const; + bool operator>=(const ArrayStoreAll& asa) const; private: std::unique_ptr d_type; diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index d6249d6fd..bc4205217 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -93,7 +93,8 @@ ExprManager::ExprManager(const Options& options) : #endif } -ExprManager::~ExprManager() throw() { +ExprManager::~ExprManager() +{ NodeManagerScope nms(d_nodeManager); try { @@ -128,7 +129,8 @@ const Options& ExprManager::getOptions() const { return d_nodeManager->getOptions(); } -ResourceManager* ExprManager::getResourceManager() throw() { +ResourceManager* ExprManager::getResourceManager() +{ return d_nodeManager->getResourceManager(); } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index a12c68791..35a3b6a6e 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -109,13 +109,13 @@ public: * any expression references that used to be managed by this expression * manager and are left-over are bad. */ - ~ExprManager() throw(); + ~ExprManager(); /** Get this expr manager's options */ const Options& getOptions() const; /** Get this expr manager's resource manager */ - ResourceManager* getResourceManager() throw(); + ResourceManager* getResourceManager(); /** Get the type for booleans */ BooleanType booleanType() const; @@ -436,27 +436,6 @@ public: SortConstructorType mkSortConstructor(const std::string& name, size_t arity) const; - /** - * Make a predicate subtype type defined by the given LAMBDA - * expression. A TypeCheckingException can be thrown if lambda is - * not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that - * the resulting predicate subtype is inhabited. - */ - // not in release 1.0 - //Type mkPredicateSubtype(Expr lambda) - // throw(TypeCheckingException); - - /** - * Make a predicate subtype type defined by the given LAMBDA - * expression and whose non-emptiness is witnessed by the given - * witness. A TypeCheckingException can be thrown if lambda is not - * a LAMBDA, or is ill-typed, or if the witness is not a witness or - * ill-typed. - */ - // not in release 1.0 - //Type mkPredicateSubtype(Expr lambda, Expr witness) - // throw(TypeCheckingException); - /** Get the type of an expression */ Type getType(Expr e, bool check = false) throw(TypeCheckingException); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 0b1773114..d9345a5f5 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -391,10 +391,11 @@ public: } /** Get this node manager's resource manager */ - ResourceManager* getResourceManager() throw() { return d_resourceManager; } + ResourceManager* getResourceManager() { return d_resourceManager; } /** Get this node manager's statistics registry */ - StatisticsRegistry* getStatisticsRegistry() const throw() { + StatisticsRegistry* getStatisticsRegistry() const + { return d_statisticsRegistry; } diff --git a/src/main/main.h b/src/main/main.h index 8a5d0971e..0a5139c59 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -56,12 +56,13 @@ extern bool segvSpin; /** A pointer to the options in play */ extern CVC4_THREAD_LOCAL Options* pOptions; -/** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ -void cvc4_init() throw(Exception); +/** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. + * This can throw a CVC4::Exception. + */ +void cvc4_init(); /** Shutdown the driver. Frees memory for the signal handlers. */ -void cvc4_shutdown() throw(); - +void cvc4_shutdown() noexcept; }/* CVC4::main namespace */ }/* CVC4 namespace */ diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index 5ed9a36fd..4f80f24ef 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -47,7 +47,7 @@ public: cnt(0) {} - ~PortfolioLemmaOutputChannel() throw() { } + ~PortfolioLemmaOutputChannel() {} void notifyNewLemma(Expr lemma); };/* class PortfolioLemmaOutputChannel */ @@ -65,7 +65,7 @@ public: VarMap& to, VarMap& from); - ~PortfolioLemmaInputChannel() throw() { } + ~PortfolioLemmaInputChannel() {} bool hasNewLemma(); Expr getNewLemma(); diff --git a/src/main/util.cpp b/src/main/util.cpp index 43c880a7f..de6b47aa5 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -261,7 +261,8 @@ void cvc4terminate() { } /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ -void cvc4_init() throw(Exception) { +void cvc4_init() +{ #ifdef CVC4_DEBUG LastExceptionBuffer::setCurrent(new LastExceptionBuffer()); #endif diff --git a/src/smt_util/boolean_simplification.cpp b/src/smt_util/boolean_simplification.cpp index 40f96a47c..13ae93dc3 100644 --- a/src/smt_util/boolean_simplification.cpp +++ b/src/smt_util/boolean_simplification.cpp @@ -18,10 +18,9 @@ namespace CVC4 { -bool -BooleanSimplification::push_back_associative_commute_recursive - (Node n, std::vector& buffer, Kind k, Kind notK, bool negateNode) - throw(AssertionException) { +bool BooleanSimplification::push_back_associative_commute_recursive( + Node n, std::vector& buffer, Kind k, Kind notK, bool negateNode) +{ Node::iterator i = n.begin(), end = n.end(); for(; i != end; ++i){ Node child = *i; diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h index 2d350c9d9..4a6764b0e 100644 --- a/src/smt_util/boolean_simplification.h +++ b/src/smt_util/boolean_simplification.h @@ -38,12 +38,11 @@ class BooleanSimplification { BooleanSimplification() CVC4_UNDEFINED; BooleanSimplification(const BooleanSimplification&) CVC4_UNDEFINED; - static bool push_back_associative_commute_recursive - (Node n, std::vector& buffer, Kind k, Kind notK, bool negateNode) - throw(AssertionException) CVC4_WARN_UNUSED_RESULT; - -public: + static bool push_back_associative_commute_recursive( + Node n, std::vector& buffer, Kind k, Kind notK, bool negateNode) + CVC4_WARN_UNUSED_RESULT; + public: /** * The threshold for removing duplicates. (See removeDuplicates().) */ @@ -55,7 +54,7 @@ public: * function is a no-op. */ static void removeDuplicates(std::vector& buffer) - throw(AssertionException) { + { if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) { std::sort(buffer.begin(), buffer.end()); std::vector::iterator new_end = @@ -70,7 +69,8 @@ public: * push_back_associative_commute()), removes duplicates, and returns * the resulting Node. */ - static Node simplifyConflict(Node andNode) throw(AssertionException) { + static Node simplifyConflict(Node andNode) + { AssertArgument(!andNode.isNull(), andNode); AssertArgument(andNode.getKind() == kind::AND, andNode); @@ -94,7 +94,8 @@ public: * push_back_associative_commute()), removes duplicates, and returns * the resulting Node. */ - static Node simplifyClause(Node orNode) throw(AssertionException) { + static Node simplifyClause(Node orNode) + { AssertArgument(!orNode.isNull(), orNode); AssertArgument(orNode.getKind() == kind::OR, orNode); @@ -120,7 +121,8 @@ public: * The input doesn't actually have to be Horn, it seems, but that's * the common case(?), hence the name. */ - static Node simplifyHornClause(Node implication) throw(AssertionException) { + static Node simplifyHornClause(Node implication) + { AssertArgument(implication.getKind() == kind::IMPLIES, implication); TNode left = implication[0]; @@ -151,10 +153,12 @@ public: * this if e.g. you're simplifying the (OR...) in (NOT (OR...)), * intending to make the result an AND. */ - static inline void - push_back_associative_commute(Node n, std::vector& buffer, - Kind k, Kind notK, bool negateChildren = false) - throw(AssertionException) { + static inline void push_back_associative_commute(Node n, + std::vector& buffer, + Kind k, + Kind notK, + bool negateChildren = false) + { AssertArgument(buffer.empty(), buffer); AssertArgument(!n.isNull(), n); AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, k); @@ -177,7 +181,8 @@ public: * * @param n the node to negate (cannot be the null node) */ - static Node negate(TNode n) throw(AssertionException) { + static Node negate(TNode n) + { AssertArgument(!n.isNull(), n); bool polarity = true; @@ -202,7 +207,8 @@ public: * * @param e the Expr to negate (cannot be the null Expr) */ - static Expr negate(Expr e) throw(AssertionException) { + static Expr negate(Expr e) + { ExprManagerScope ems(e); return negate(Node::fromExpr(e)).toExpr(); } @@ -211,7 +217,8 @@ public: * Simplify an OR, AND, or IMPLIES. This function is the identity * for all other kinds. */ - inline static Node simplify(TNode n) throw(AssertionException) { + inline static Node simplify(TNode n) + { switch(n.getKind()) { case kind::AND: return simplifyConflict(n); diff --git a/src/smt_util/lemma_input_channel.h b/src/smt_util/lemma_input_channel.h index af2ac6442..f141111b1 100644 --- a/src/smt_util/lemma_input_channel.h +++ b/src/smt_util/lemma_input_channel.h @@ -26,10 +26,10 @@ namespace CVC4 { class CVC4_PUBLIC LemmaInputChannel { public: - virtual ~LemmaInputChannel() throw() { } + virtual ~LemmaInputChannel() {} - virtual bool hasNewLemma() = 0; - virtual Expr getNewLemma() = 0; + virtual bool hasNewLemma() = 0; + virtual Expr getNewLemma() = 0; };/* class LemmaOutputChannel */ diff --git a/src/smt_util/lemma_output_channel.h b/src/smt_util/lemma_output_channel.h index 0e49e99cb..c03aa0d18 100644 --- a/src/smt_util/lemma_output_channel.h +++ b/src/smt_util/lemma_output_channel.h @@ -32,13 +32,13 @@ namespace CVC4 { */ class CVC4_PUBLIC LemmaOutputChannel { public: - virtual ~LemmaOutputChannel() throw() { } + virtual ~LemmaOutputChannel() {} - /** - * Notifies this output channel that there's a new lemma. - * The lemma may or may not be in CNF. - */ - virtual void notifyNewLemma(Expr lemma) = 0; + /** + * Notifies this output channel that there's a new lemma. + * The lemma may or may not be in CNF. + */ + virtual void notifyNewLemma(Expr lemma) = 0; };/* class LemmaOutputChannel */ }/* CVC4 namespace */ -- 2.30.2