From 3c6398194b01372720964590b2b07d93590e511d Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 8 Jan 2018 22:04:02 -0800 Subject: [PATCH] Removing more miscellaneous throw specifiers. (#1488) Removing more miscellaneous throw specifiers. --- src/main/interactive_shell.cpp | 3 +- src/main/interactive_shell.h | 2 +- src/main/util.cpp | 3 +- src/options/base_handlers.h | 39 +- src/options/options.h | 8 +- src/options/options_handler.cpp | 3 +- src/options/options_handler.h | 2 +- src/options/options_template.cpp | 10 +- src/options/theoryof_mode.cpp | 6 +- src/options/theoryof_mode.h | 2 +- src/theory/arrays/static_fact_manager.h | 1 - src/theory/arrays/union_find.h | 4 +- src/theory/bv/bitblaster_template.h | 2 +- src/theory/bv/lazy_bitblaster.cpp | 3 +- src/theory/bv/type_enumerator.h | 8 +- src/theory/output_channel.h | 6 +- src/theory/quantifiers/ambqi_builder.h | 8 +- src/theory/quantifiers/candidate_generator.h | 63 +-- src/theory/quantifiers/conjecture_generator.h | 2 +- src/theory/quantifiers/first_order_model.cpp | 6 +- src/theory/quantifiers/first_order_model.h | 24 +- src/theory/quantifiers/full_model_check.h | 1 - .../quantifiers/inst_match_generator.cpp | 10 +- src/theory/quantifiers/inst_match_generator.h | 430 +++++++++--------- src/theory/quantifiers/inst_strategy_cbqi.cpp | 5 +- src/theory/quantifiers/inst_strategy_cbqi.h | 16 +- src/theory/quantifiers/model_builder.h | 42 +- src/theory/quantifiers/quant_conflict_find.h | 2 +- .../quantifiers/quant_equality_engine.h | 1 - src/theory/quantifiers/rewrite_engine.h | 1 - src/theory/theory_model.h | 2 +- src/theory/uf/symmetry_breaker.h | 11 +- src/util/abstract_value.cpp | 9 +- src/util/abstract_value.h | 35 +- src/util/cache.h | 20 +- src/util/integer_cln_imp.cpp | 9 +- src/util/integer_cln_imp.h | 16 +- src/util/rational_cln_imp.h | 8 +- src/util/resource_manager.cpp | 7 +- src/util/resource_manager.h | 4 +- src/util/statistics_registry.cpp | 12 +- src/util/statistics_registry.h | 11 +- src/util/tuple.h | 11 +- 43 files changed, 438 insertions(+), 430 deletions(-) diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 325f44769..4761ba07e 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -176,7 +176,8 @@ InteractiveShell::~InteractiveShell() { delete d_parser; } -Command* InteractiveShell::readCommand() throw (UnsafeInterruptException) { +Command* InteractiveShell::readCommand() +{ char* lineBuf = NULL; string line = ""; diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index a3834a1e3..049b0649e 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -57,7 +57,7 @@ public: * Read a command from the interactive shell. This will read as * many lines as necessary to parse a well-formed command. */ - Command* readCommand() throw (UnsafeInterruptException); + Command* readCommand(); /** * Return the internal parser being used. diff --git a/src/main/util.cpp b/src/main/util.cpp index de6b47aa5..7086ea26f 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -345,7 +345,8 @@ void cvc4_init() default_terminator = set_terminate(cvc4terminate); } -void cvc4_shutdown() throw () { +void cvc4_shutdown() noexcept +{ #ifndef __WIN32__ #ifdef HAVE_SIGALTSTACK free(cvc4StackBase); diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h index b036c7e93..874516265 100644 --- a/src/options/base_handlers.h +++ b/src/options/base_handlers.h @@ -35,11 +35,10 @@ class comparator { double d_dbound; bool d_hasLbound; -public: - comparator(int i) throw() : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {} - comparator(long l) throw() : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {} - comparator(double d) throw() : d_lbound(0), d_dbound(d), d_hasLbound(false) {} - + public: + comparator(int i) : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {} + comparator(long l) : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {} + comparator(double d) : d_lbound(0), d_dbound(d), d_hasLbound(false) {} template void operator()(std::string option, const T& value) { if((d_hasLbound && !(Cmp()(value, T(d_lbound)))) || @@ -52,33 +51,33 @@ public: };/* class comparator */ struct greater : public comparator { - greater(int i) throw() : comparator(i) {} - greater(long l) throw() : comparator(l) {} - greater(double d) throw() : comparator(d) {} + greater(int i) : comparator(i) {} + greater(long l) : comparator(l) {} + greater(double d) : comparator(d) {} };/* struct greater */ struct greater_equal : public comparator { - greater_equal(int i) throw() : comparator(i) {} - greater_equal(long l) throw() : comparator(l) {} - greater_equal(double d) throw() : comparator(d) {} + greater_equal(int i) : comparator(i) {} + greater_equal(long l) : comparator(l) {} + greater_equal(double d) : comparator(d) {} };/* struct greater_equal */ struct less : public comparator { - less(int i) throw() : comparator(i) {} - less(long l) throw() : comparator(l) {} - less(double d) throw() : comparator(d) {} + less(int i) : comparator(i) {} + less(long l) : comparator(l) {} + less(double d) : comparator(d) {} };/* struct less */ struct less_equal : public comparator { - less_equal(int i) throw() : comparator(i) {} - less_equal(long l) throw() : comparator(l) {} - less_equal(double d) throw() : comparator(d) {} + less_equal(int i) : comparator(i) {} + less_equal(long l) : comparator(l) {} + less_equal(double d) : comparator(d) {} };/* struct less_equal */ struct not_equal : public comparator { - not_equal(int i) throw() : comparator(i) {} - not_equal(long l) throw() : comparator(l) {} - not_equal(double d) throw() : comparator(d) {} + not_equal(int i) : comparator(i) {} + not_equal(long l) : comparator(l) {} + not_equal(double d) : comparator(d) {} };/* struct not_equal_to */ }/* CVC4::options namespace */ diff --git a/src/options/options.h b/src/options/options.h index 474ef0f96..ce0e3c347 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -302,7 +302,7 @@ public: * to the given name. Returns an empty string if there are no * suggestions. */ - static std::string suggestCommandLineOptions(const std::string& optionName) throw(); + static std::string suggestCommandLineOptions(const std::string& optionName); /** * Look up SMT option names that bear some similarity to @@ -310,7 +310,8 @@ public: * useful in case of typos. Can return an empty vector if there are * no suggestions. */ - static std::vector suggestSmtOptions(const std::string& optionName) throw(); + static std::vector suggestSmtOptions( + const std::string& optionName); /** * Initialize the Options object options based on the given @@ -329,8 +330,7 @@ public: /** * Get the setting for all options. */ - std::vector< std::vector > getOptions() const throw(); - + std::vector > getOptions() const; /** * Registers a listener for the notification, notifyBeforeSearch. diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 4fb6357bd..583f79d2d 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1361,7 +1361,8 @@ SygusSolutionOutMode OptionsHandler::stringToSygusSolutionOutMode( } } -void OptionsHandler::setProduceAssertions(std::string option, bool value) throw() { +void OptionsHandler::setProduceAssertions(std::string option, bool value) +{ options::produceAssertions.set(value); options::interactiveMode.set(value); } diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 9d5f8cc6e..eef4c9b61 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -146,7 +146,7 @@ public: SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException); SygusSolutionOutMode stringToSygusSolutionOutMode( std::string option, std::string optarg) throw(OptionException); - void setProduceAssertions(std::string option, bool value) throw(); + void setProduceAssertions(std::string option, bool value); void proofEnabledBuild(std::string option, bool value) throw(OptionException); void LFSCEnabledBuild(std::string option, bool value); void notifyDumpToFile(std::string option); diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index a48b22625..9de47b388 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -787,7 +787,8 @@ ${all_modules_option_handlers} free(argv); } -std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() { +std::string Options::suggestCommandLineOptions(const std::string& optionName) +{ DidYouMean didYouMean; const char* opt; @@ -804,7 +805,9 @@ static const char* smtOptions[] = { NULL };/* smtOptions[] */ -std::vector Options::suggestSmtOptions(const std::string& optionName) throw() { +std::vector Options::suggestSmtOptions( + const std::string& optionName) +{ std::vector suggestions; const char* opt; @@ -817,7 +820,8 @@ std::vector Options::suggestSmtOptions(const std::string& optionNam return suggestions; } -std::vector< std::vector > Options::getOptions() const throw() { +std::vector > Options::getOptions() const +{ std::vector< std::vector > opts; ${all_modules_get_options} diff --git a/src/options/theoryof_mode.cpp b/src/options/theoryof_mode.cpp index 9eb2be178..3fe7db532 100644 --- a/src/options/theoryof_mode.cpp +++ b/src/options/theoryof_mode.cpp @@ -19,19 +19,17 @@ #include "options/theoryof_mode.h" #include -#include "base/cvc4_assert.h" namespace CVC4 { namespace theory { -std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() { +std::ostream& operator<<(std::ostream& out, TheoryOfMode m) +{ switch(m) { case THEORY_OF_TYPE_BASED: return out << "THEORY_OF_TYPE_BASED"; case THEORY_OF_TERM_BASED: return out << "THEORY_OF_TERM_BASED"; default: return out << "TheoryOfMode!UNKNOWN"; } - - Unreachable(); } }/* CVC4::theory namespace */ diff --git a/src/options/theoryof_mode.h b/src/options/theoryof_mode.h index f999a6081..d1306defd 100644 --- a/src/options/theoryof_mode.h +++ b/src/options/theoryof_mode.h @@ -31,7 +31,7 @@ enum TheoryOfMode { THEORY_OF_TERM_BASED };/* enum TheoryOfMode */ -std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, TheoryOfMode m) CVC4_PUBLIC; }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h index 4a08838fe..deefb02cf 100644 --- a/src/theory/arrays/static_fact_manager.h +++ b/src/theory/arrays/static_fact_manager.h @@ -45,7 +45,6 @@ namespace arrays { public: StaticFactManager() {} - ~StaticFactManager() throw() { } /** * Return a Node's union-find representative, doing path compression. diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h index eb60f339b..3028eaf17 100644 --- a/src/theory/arrays/union_find.h +++ b/src/theory/arrays/union_find.h @@ -56,14 +56,12 @@ class UnionFind : context::ContextNotifyObj { /** Our current offset in the d_trace stack (context-dependent). */ context::CDO d_offset; -public: + public: UnionFind(context::Context* ctxt) : context::ContextNotifyObj(ctxt), d_offset(ctxt, 0) { } - ~UnionFind() throw() { } - /** * Return a Node's union-find representative, doing path compression. */ diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 0e7614221..33dd4387e 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -180,7 +180,7 @@ public: bool hasBBAtom(TNode atom) const; TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false); - ~TLazyBitblaster() throw(); + ~TLazyBitblaster(); /** * Pushes the assumption literal associated with node to the SAT * solver assumption queue. diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 831b767e0..d108a37f0 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -71,7 +71,8 @@ void TLazyBitblaster::setAbstraction(AbstractionModule* abs) { d_abstraction = abs; } -TLazyBitblaster::~TLazyBitblaster() throw() { +TLazyBitblaster::~TLazyBitblaster() +{ delete d_cnfStream; delete d_nullRegistrar; delete d_nullContext; diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h index a27d3a64e..718121499 100644 --- a/src/theory/bv/type_enumerator.h +++ b/src/theory/bv/type_enumerator.h @@ -49,15 +49,13 @@ public: return utils::mkConst(d_size, d_bits); } - BitVectorEnumerator& operator++() throw() { + BitVectorEnumerator& operator++() + { d_bits += 1; return *this; } - bool isFinished() throw() { - return d_bits != d_bits.modByPow2(d_size); - } - + bool isFinished() { return d_bits != d_bits.modByPow2(d_size); } };/* BitVectorEnumerator */ }/* CVC4::theory::bv namespace */ diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index cc8cee481..317795f0d 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -44,15 +44,13 @@ class LemmaStatus { : d_rewrittenLemma(rewrittenLemma), d_level(level) {} /** Get the T-rewritten form of the lemma. */ - TNode getRewrittenLemma() const throw() { return d_rewrittenLemma; } - + TNode getRewrittenLemma() const { return d_rewrittenLemma; } /** * Get the user-level at which the lemma resides. After this user level * is popped, the lemma is un-asserted from the SAT layer. This level * will be 0 if the lemma didn't reach the SAT layer at all. */ - unsigned getLevel() const throw() { return d_level; } - + unsigned getLevel() const { return d_level; } private: Node d_rewrittenLemma; unsigned d_level; diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index 89cd8b6a8..c451f0489 100644 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -89,11 +89,13 @@ private: bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ); public: AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ); - ~AbsMbqiBuilder() throw() {} + //process build model - bool processBuildModel(TheoryModel* m); + bool processBuildModel(TheoryModel* m) override; //do exhaustive instantiation - int doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ); + int doExhaustiveInstantiation(FirstOrderModel* fm, + Node q, + int effort) override; }; } diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index dd71ef56e..4662d7c4c 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -61,25 +61,26 @@ public: /** candidate generator queue (for manual candidate generation) */ class CandidateGeneratorQueue : public CandidateGenerator { -private: + private: std::vector< Node > d_candidates; int d_candidate_index; -public: + + public: CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){} - ~CandidateGeneratorQueue() throw() {} - void addCandidate( Node n ); + void addCandidate(Node n) override; - void resetInstantiationRound(){} - void reset( Node eqc ); - Node getNextCandidate(); + void resetInstantiationRound() override {} + void reset(Node eqc) override; + Node getNextCandidate() override; };/* class CandidateGeneratorQueue */ //the default generator class CandidateGeneratorQE : public CandidateGenerator { friend class CandidateGeneratorQEDisequal; -private: + + private: //operator you are looking for Node d_op; //the equality class iterator @@ -102,56 +103,56 @@ private: bool isLegalOpCandidate( Node n ); Node d_n; std::map< Node, bool > d_exclude_eqc; -public: + + public: CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ); - ~CandidateGeneratorQE() throw() {} - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; void excludeEqc( Node r ) { d_exclude_eqc[r] = true; } bool isExcludedEqc( Node r ) { return d_exclude_eqc.find( r )!=d_exclude_eqc.end(); } }; class CandidateGeneratorQELitEq : public CandidateGenerator { -private: + private: //the equality classes iterator eq::EqClassesIterator d_eq; //equality you are trying to match equalities for Node d_match_pattern; Node d_match_gterm; bool d_do_mgt; -public: + + public: CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ); - ~CandidateGeneratorQELitEq() throw() {} - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; }; class CandidateGeneratorQELitDeq : public CandidateGenerator { -private: + private: //the equality class iterator for false eq::EqClassIterator d_eqc_false; //equality you are trying to match disequalities for Node d_match_pattern; //type of disequality TypeNode d_match_pattern_type; -public: + + public: CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ); - ~CandidateGeneratorQELitDeq() throw() {} - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; }; class CandidateGeneratorQEAll : public CandidateGenerator { -private: + private: //the equality classes iterator eq::EqClassesIterator d_eq; //equality you are trying to match equalities for @@ -162,13 +163,13 @@ private: unsigned d_index; //first time bool d_firstTime; -public: + + public: CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ); - ~CandidateGeneratorQEAll() throw() {} - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; }; }/* CVC4::theory::inst namespace */ diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index fa74795c3..85a7d3eb4 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -399,7 +399,7 @@ private: //information about ground equivalence classes unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ); public: ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ); - ~ConjectureGenerator() throw() {} + /* needs check */ bool needsCheck( Theory::Effort e ); /* reset at a round */ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 6749a8c0d..e7070b469 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -836,7 +836,8 @@ FirstOrderModel(qe, c, name){ } -FirstOrderModelFmc::~FirstOrderModelFmc() throw() { +FirstOrderModelFmc::~FirstOrderModelFmc() +{ for(std::map::iterator i = d_models.begin(); i != d_models.end(); ++i) { delete (*i).second; } @@ -1004,7 +1005,8 @@ FirstOrderModel(qe, c, name) { } -FirstOrderModelAbs::~FirstOrderModelAbs() throw() { +FirstOrderModelAbs::~FirstOrderModelAbs() +{ for(std::map::iterator i = d_models.begin(); i != d_models.end(); ++i) { delete (*i).second; } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 57582a856..0c4b6b7a4 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -93,7 +93,7 @@ class FirstOrderModel : public TheoryModel { public: FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name); - virtual ~FirstOrderModel() throw() {} + virtual FirstOrderModelIG* asFirstOrderModelIG() { return nullptr; } virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; } virtual FirstOrderModelQInt* asFirstOrderModelQInt() { return nullptr; } @@ -214,7 +214,7 @@ private: //the following functions are for evaluating quantifier bodies public: FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name); - ~FirstOrderModelIG() throw() {} + FirstOrderModelIG * asFirstOrderModelIG() { return this; } // initialize the model void processInitialize( bool ispre ); @@ -257,7 +257,7 @@ private: void processInitializeModelForTerm(Node n); public: FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name); - virtual ~FirstOrderModelFmc() throw(); + ~FirstOrderModelFmc() override; FirstOrderModelFmc * asFirstOrderModelFmc() { return this; } // initialize the model void processInitialize( bool ispre ); @@ -277,24 +277,26 @@ class AbsDef; class FirstOrderModelAbs : public FirstOrderModel { -public: + public: std::map< Node, AbsDef * > d_models; std::map< Node, bool > d_models_valid; std::map< TNode, unsigned > d_rep_id; std::map< TypeNode, unsigned > d_domain; std::map< Node, std::vector< int > > d_var_order; std::map< Node, std::map< int, int > > d_var_index; -private: + + private: /** get current model value */ - void processInitializeModelForTerm(Node n); - void processInitializeQuantifier( Node q ); + void processInitializeModelForTerm(Node n) override; + void processInitializeQuantifier(Node q) override; void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars ); TNode getUsedRepresentative( TNode n ); -public: + + public: FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name); - ~FirstOrderModelAbs() throw(); - FirstOrderModelAbs * asFirstOrderModelAbs() { return this; } - void processInitialize( bool ispre ); + ~FirstOrderModelAbs() override; + FirstOrderModelAbs* asFirstOrderModelAbs() override { return this; } + void processInitialize(bool ispre) override; unsigned getRepresentativeId( TNode n ); bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); } Node getFunctionValue(Node op, const char* argPrefix ); diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index c5d005969..f6d16dc03 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -134,7 +134,6 @@ private: Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); public: FullModelChecker( context::Context* c, QuantifiersEngine* qe ); - ~FullModelChecker() throw() {} void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 884ed29f5..46ae8aa84 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -59,7 +59,8 @@ InstMatchGenerator::InstMatchGenerator() { d_independent_gen = false; } -InstMatchGenerator::~InstMatchGenerator() throw() { +InstMatchGenerator::~InstMatchGenerator() +{ for( unsigned i=0; ireset( Node::null(), qe ) ){ @@ -814,7 +811,8 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q, } } -InstMatchGeneratorMulti::~InstMatchGeneratorMulti() throw() { +InstMatchGeneratorMulti::~InstMatchGeneratorMulti() +{ for( unsigned i=0; i& pats, + QuantifiersEngine* qe); + /** mkInstMatchGenerator * - * A match generator is indepndent when this generator fails to produce a - * match in a call to getNextMatch, the overall matching fails. - */ - void setIndependent() { d_independent_gen = true; } - //-------------------------------construction of inst match generators - /** mkInstMatchGenerator for single triggers, calls the method below */ - static InstMatchGenerator* mkInstMatchGenerator(Node q, - Node pat, - QuantifiersEngine* qe); - /** mkInstMatchGenerator for the multi trigger case - * - * This linked list of InstMatchGenerator classes with one - * InstMatchGeneratorMultiLinear at the head and a list of trailing - * InstMatchGenerators corresponding to each unique subterm of pats with - * free variables. - */ - static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q, - std::vector& pats, - QuantifiersEngine* qe); - /** mkInstMatchGenerator - * - * This generates a linked list of InstMatchGenerators for each unique - * subterm of pats with free variables. - * - * q is the quantified formula associated with the generator we are making - * pats is a set of terms we are making InstMatchGenerator nodes for - * qe is a pointer to the quantifiers engine (used for querying necessary - * information during initialization) pat_map_init maps from terms to - * generators we have already made for them. - * - * It calls initialize(...) for all InstMatchGenerators generated by this call. - */ - static InstMatchGenerator* mkInstMatchGenerator( - Node q, - std::vector& pats, - QuantifiersEngine* qe, - std::map& pat_map_init); - //-------------------------------end construction of inst match generators - -protected: - /** constructors + * This generates a linked list of InstMatchGenerators for each unique + * subterm of pats with free variables. * - * These are intentionally private, and are called during linked list - * construction in mkInstMatchGenerator. - */ - InstMatchGenerator(Node pat); - InstMatchGenerator(); - /** The pattern we are producing matches for. + * q is the quantified formula associated with the generator we are making + * pats is a set of terms we are making InstMatchGenerator nodes for + * qe is a pointer to the quantifiers engine (used for querying necessary + * information during initialization) pat_map_init maps from terms to + * generators we have already made for them. * - * This term and d_match_pattern can be different since this - * term may involve information regarding phase and (dis)equality entailment, - * or other special cases of Triggers. - * - * For example, for the trigger for P( x ) = false, which matches P( x ) with - * P( t ) in the equivalence class of false, - * P( x ) = false is d_pattern - * P( x ) is d_match_pattern - * Another example, for pure theory triggers like head( x ), we have - * head( x ) is d_pattern - * x is d_match_pattern - * since head( x ) can match any (List) datatype term x. - * - * If null, this is a multi trigger that is merging matches from d_children, - * which is used in InstMatchGeneratorMulti. - */ - Node d_pattern; - /** The match pattern - * This is the term that is matched against ground terms, - * see examples above. - */ - Node d_match_pattern; - /** The current term we are matching. */ - Node d_curr_matched; - /** do we need to call reset on this generator? */ - bool d_needsReset; - /** candidate generator - * This is the back-end utility for InstMatchGenerator. - * It generates a stream of candidate terms to match against d_match_pattern - * below, dependending upon what kind of term we are matching - * (e.g. a matchable term, a variable, a relation, etc.). + * It calls initialize(...) for all InstMatchGenerators generated by this call. */ - CandidateGenerator* d_cg; - /** children generators - * These match generators correspond to the children of the term - * we are matching with this generator. - * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ] - * in the example (EX1) above. - */ - std::vector d_children; - /** for each child, the index in the term - * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ] - * in the example (EX1) above, indicating it is the 2nd child - * of the term. + static InstMatchGenerator* mkInstMatchGenerator( + Node q, + std::vector& pats, + QuantifiersEngine* qe, + std::map& pat_map_init); + //-------------------------------end construction of inst match generators + + protected: + /** constructors + * + * These are intentionally private, and are called during linked list + * construction in mkInstMatchGenerator. */ - std::vector d_children_index; - /** children types + InstMatchGenerator(Node pat); + InstMatchGenerator(); + /** The pattern we are producing matches for. + * + * This term and d_match_pattern can be different since this + * term may involve information regarding phase and (dis)equality entailment, + * or other special cases of Triggers. * - * If d_match_pattern is an instantiation constant, then this is a singleton - * vector containing the variable number of the d_match_pattern itself. - * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each - * index i, d_children[i] stores the type of node ti is, where: - * >= 0 : variable (indicates its number), - * -1 : ground term, - * -2 : child term. - */ - std::vector d_children_types; - /** The next generator in the linked list - * that this generator is a part of. - */ - InstMatchGenerator* d_next; - /** The equivalence class we are currently matching in. */ - Node d_eq_class; - /** If non-null, then this is a relational trigger of the form x ~ - * d_eq_class_rel. */ - Node d_eq_class_rel; - /** Excluded matches - * Stores the terms we are not allowed to match. - * These can for instance be specified by the smt2 - * extended syntax (! ... :no-pattern). - */ - std::map d_curr_exclude_match; - /** Current first candidate - * Used in a key fail-quickly optimization which generates - * the first candidate term to match during reset(). - */ - Node d_curr_first_candidate; - /** Indepdendent generate - * If this flag is true, failures to match should be cached. - */ - bool d_independent_gen; - /** active add flag, described above. */ - bool d_active_add; - /** cached value of d_match_pattern.getType() */ - TypeNode d_match_pattern_type; - /** the match operator for d_match_pattern + * For example, for the trigger for P( x ) = false, which matches P( x ) with + * P( t ) in the equivalence class of false, + * P( x ) = false is d_pattern + * P( x ) is d_match_pattern + * Another example, for pure theory triggers like head( x ), we have + * head( x ) is d_pattern + * x is d_match_pattern + * since head( x ) can match any (List) datatype term x. * - * See TermDatabase::getMatchOperator for details on match operators. + * If null, this is a multi trigger that is merging matches from d_children, + * which is used in InstMatchGeneratorMulti. */ - Node d_match_pattern_op; - /** get the match against ground term or formula t. - * - * d_match_pattern and t should have the same shape, that is, - * their match operator (see TermDatabase::getMatchOperator) is the same. - * only valid for use where !d_match_pattern.isNull(). + Node d_pattern; + /** The match pattern + * This is the term that is matched against ground terms, + * see examples above. + */ + Node d_match_pattern; + /** The current term we are matching. */ + Node d_curr_matched; + /** do we need to call reset on this generator? */ + bool d_needsReset; + /** candidate generator + * This is the back-end utility for InstMatchGenerator. + * It generates a stream of candidate terms to match against d_match_pattern + * below, dependending upon what kind of term we are matching + * (e.g. a matchable term, a variable, a relation, etc.). + */ + CandidateGenerator* d_cg; + /** children generators + * These match generators correspond to the children of the term + * we are matching with this generator. + * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ] + * in the example (EX1) above. + */ + std::vector d_children; + /** for each child, the index in the term + * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ] + * in the example (EX1) above, indicating it is the 2nd child + * of the term. + */ + std::vector d_children_index; + /** children types + * + * If d_match_pattern is an instantiation constant, then this is a singleton + * vector containing the variable number of the d_match_pattern itself. + * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each + * index i, d_children[i] stores the type of node ti is, where: + * >= 0 : variable (indicates its number), + * -1 : ground term, + * -2 : child term. + */ + std::vector d_children_types; + /** The next generator in the linked list + * that this generator is a part of. + */ + InstMatchGenerator* d_next; + /** The equivalence class we are currently matching in. */ + Node d_eq_class; + /** If non-null, then this is a relational trigger of the form x ~ + * d_eq_class_rel. */ + Node d_eq_class_rel; + /** Excluded matches + * Stores the terms we are not allowed to match. + * These can for instance be specified by the smt2 + * extended syntax (! ... :no-pattern). */ - int getMatch( - Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent); - /** Initialize this generator. - * - * q is the quantified formula associated with this generator. - * - * This constructs the appropriate information about what - * patterns we are matching and children generators. - * - * It may construct new (child) generators needed to implement - * the matching algorithm for this term. For each new generator - * constructed in this way, it adds them to gens. + std::map d_curr_exclude_match; + /** Current first candidate + * Used in a key fail-quickly optimization which generates + * the first candidate term to match during reset(). */ - void initialize(Node q, - QuantifiersEngine* qe, - std::vector& gens); - /** Continue next match - * - * This is called during getNextMatch when the current generator in the linked - * list succesfully satisfies its matching constraint. This function either - * calls getNextMatch of the next element in the linked list, or finalizes the - * match (calling sendInstantiation(...) if active add is true, or returning a - * value >0 if active add is false). Its return value has the same semantics - * as getNextMatch. - */ - int continueNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent); - /** Get inst match generator - * - * Gets the InstMatchGenerator that implements the - * appropriate matching algorithm for n within q - * within a linked list of InstMatchGenerators. + Node d_curr_first_candidate; + /** Indepdendent generate + * If this flag is true, failures to match should be cached. */ - static InstMatchGenerator* getInstMatchGenerator(Node q, Node n); + bool d_independent_gen; + /** active add flag, described above. */ + bool d_active_add; + /** cached value of d_match_pattern.getType() */ + TypeNode d_match_pattern_type; + /** the match operator for d_match_pattern + * + * See TermDatabase::getMatchOperator for details on match operators. + */ + Node d_match_pattern_op; + /** get the match against ground term or formula t. + * + * d_match_pattern and t should have the same shape, that is, + * their match operator (see TermDatabase::getMatchOperator) is the same. + * only valid for use where !d_match_pattern.isNull(). + */ + int getMatch( + Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent); + /** Initialize this generator. + * + * q is the quantified formula associated with this generator. + * + * This constructs the appropriate information about what + * patterns we are matching and children generators. + * + * It may construct new (child) generators needed to implement + * the matching algorithm for this term. For each new generator + * constructed in this way, it adds them to gens. + */ + void initialize(Node q, + QuantifiersEngine* qe, + std::vector& gens); + /** Continue next match + * + * This is called during getNextMatch when the current generator in the linked + * list succesfully satisfies its matching constraint. This function either + * calls getNextMatch of the next element in the linked list, or finalizes the + * match (calling sendInstantiation(...) if active add is true, or returning a + * value >0 if active add is false). Its return value has the same semantics + * as getNextMatch. + */ + int continueNextMatch(Node q, + InstMatch& m, + QuantifiersEngine* qe, + Trigger* tparent); + /** Get inst match generator + * + * Gets the InstMatchGenerator that implements the + * appropriate matching algorithm for n within q + * within a linked list of InstMatchGenerators. + */ + static InstMatchGenerator* getInstMatchGenerator(Node q, Node n); };/* class InstMatchGenerator */ /** match generator for Boolean term ITEs @@ -424,7 +424,7 @@ protected: class VarMatchGeneratorBooleanTerm : public InstMatchGenerator { public: VarMatchGeneratorBooleanTerm( Node var, Node comp ); - virtual ~VarMatchGeneratorBooleanTerm() throw() {} + /** Reset */ bool reset(Node eqc, QuantifiersEngine* qe) override { @@ -451,7 +451,7 @@ public: class VarMatchGeneratorTermSubs : public InstMatchGenerator { public: VarMatchGeneratorTermSubs( Node var, Node subs ); - virtual ~VarMatchGeneratorTermSubs() throw() {} + /** Reset */ bool reset(Node eqc, QuantifiersEngine* qe) override { @@ -515,9 +515,6 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator { friend class InstMatchGenerator; public: - /** destructor */ - virtual ~InstMatchGeneratorMultiLinear() throw(); - /** Reset. */ bool reset(Node eqc, QuantifiersEngine* qe) override; /** Get the next match. */ @@ -552,7 +549,7 @@ class InstMatchGeneratorMulti : public IMGenerator { std::vector& pats, QuantifiersEngine* qe); /** destructor */ - virtual ~InstMatchGeneratorMulti() throw(); + ~InstMatchGeneratorMulti() override; /** Reset instantiation round. */ void resetInstantiationRound(QuantifiersEngine* qe) override; @@ -641,8 +638,7 @@ class InstMatchGeneratorSimple : public IMGenerator { public: /** constructors */ InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe); - /** destructor */ - ~InstMatchGeneratorSimple() throw() {} + /** Reset instantiation round. */ void resetInstantiationRound(QuantifiersEngine* qe) override; /** Add instantiations. */ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index bd2b8e78e..70dc9c4e9 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -48,8 +48,6 @@ d_nested_qe_waitlist_proc( qe->getUserContext() ) d_qid_count = 0; } -InstStrategyCbqi::~InstStrategyCbqi() throw(){} - bool InstStrategyCbqi::needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } @@ -673,7 +671,8 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) d_check_vts_lemma_lc = false; } -InstStrategyCegqi::~InstStrategyCegqi() throw () { +InstStrategyCegqi::~InstStrategyCegqi() +{ delete d_out; for(std::map< Node, CegInstantiator * >::iterator i = d_cinst.begin(), diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 0b23de10d..c2520a973 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -35,7 +35,8 @@ namespace quantifiers { class InstStrategyCbqi : public QuantifiersModule { typedef context::CDHashSet NodeSet; typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; -protected: + + protected: bool d_cbqi_set_quant_inactive; bool d_incomplete_check; /** whether we have added cbqi lemma */ @@ -64,7 +65,8 @@ protected: /** process functions */ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; virtual void process( Node q, Theory::Effort effort, int e ) = 0; -protected: + + protected: //for identification uint64_t d_qid_count; //nested qe map @@ -90,12 +92,14 @@ protected: NodeIntMap d_nested_qe_waitlist_size; NodeIntMap d_nested_qe_waitlist_proc; std::map< Node, std::vector< Node > > d_nested_qe_waitlist; -public: + + public: //do nested quantifier elimination Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ); -public: + + public: InstStrategyCbqi( QuantifiersEngine * qe ); - ~InstStrategyCbqi() throw(); + /** whether to do CBQI for quantifier q */ bool doCbqi( Node q ); /** process functions */ @@ -138,7 +142,7 @@ protected: void registerCounterexampleLemma( Node q, Node lem ); public: InstStrategyCegqi( QuantifiersEngine * qe ); - ~InstStrategyCegqi() throw(); + ~InstStrategyCegqi() override; bool doAddInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 73e2937ab..511aebf3b 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -38,7 +38,7 @@ protected: unsigned d_triedLemmas; public: QModelBuilder( context::Context* c, QuantifiersEngine* qe ); - virtual ~QModelBuilder() throw() {} + //do exhaustive instantiation // 0 : failed, but resorting to true exhaustive instantiation may work // >0 : success @@ -77,7 +77,8 @@ public: class QModelBuilderIG : public QModelBuilder { typedef context::CDHashMap BoolMap; -protected: + + protected: BoolMap d_basisNoMatch; //map from operators to model preference data std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; @@ -87,7 +88,8 @@ protected: bool d_didInstGen; /** process build model */ virtual bool processBuildModel( TheoryModel* m ); -protected: + + protected: //reset virtual void reset( FirstOrderModel* fm ) = 0; //initialize quantifiers, return number of lemmas produced @@ -100,20 +102,23 @@ protected: virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0; //theory-specific build models virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0; -protected: + + protected: //map from quantifiers to if are SAT //std::map< Node, bool > d_quant_sat; //which quantifiers have been initialized std::map< Node, bool > d_quant_basis_match_added; //map from quantifiers to model basis match std::map< Node, InstMatch > d_quant_basis_match; -protected: //helper functions + + protected: // helper functions /** term has constant definition */ bool hasConstantDefinition( Node n ); -public: + + public: QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); - virtual ~QModelBuilderIG() throw() {} -public: + + public: /** statistics class */ class Statistics { public: @@ -152,8 +157,8 @@ public: class QModelBuilderDefault : public QModelBuilderIG { -private: ///information for (old) InstGen - //map from quantifiers to their selection literals + private: /// information for (old) InstGen + // map from quantifiers to their selection literals std::map< Node, Node > d_quant_selection_lit; std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates; //map from quantifiers to their selection literal terms @@ -164,20 +169,23 @@ private: ///information for (old) InstGen std::map< Node, std::vector< Node > > d_op_selection_terms; //get selection score int getSelectionScore( std::vector< Node >& uf_terms ); -protected: + + protected: //reset - void reset( FirstOrderModel* fm ); + void reset(FirstOrderModel* fm) override; //analyze quantifier - void analyzeQuantifier( FirstOrderModel* fm, Node f ); + void analyzeQuantifier(FirstOrderModel* fm, Node f) override; //do InstGen techniques for quantifier, return number of lemmas produced - int doInstGen( FirstOrderModel* fm, Node f ); + int doInstGen(FirstOrderModel* fm, Node f) override; //theory-specific build models void constructModelUf( FirstOrderModel* fm, Node op ); -protected: + + protected: std::map< Node, QuantPhaseReq > d_phase_reqs; -public: + + public: QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} - ~QModelBuilderDefault() throw() {} + //options bool optReconsiderFuncConstants() { return true; } //has inst gen diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index f4d0e8e43..3448e967b 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -236,7 +236,7 @@ private: //for equivalence classes bool areMatchDisequal( TNode n1, TNode n2 ); public: QuantConflictFind( QuantifiersEngine * qe, context::Context* c ); - ~QuantConflictFind() throw() {} + /** register quantifier */ void registerQuantifier( Node q ); public: diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h index d2e9ec77b..47adddd9e 100644 --- a/src/theory/quantifiers/quant_equality_engine.h +++ b/src/theory/quantifiers/quant_equality_engine.h @@ -73,7 +73,6 @@ private: TNode getUnivRepresentativeInternal( TNode n ); public: QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c ); - virtual ~QuantEqualityEngine() throw (){} /* whether this module needs to check this round */ bool needsCheck( Theory::Effort e ); diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index d56e7c730..cfca96259 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -49,7 +49,6 @@ private: int checkRewriteRule( Node f, Theory::Effort e ); public: RewriteEngine( context::Context* c, QuantifiersEngine* qe ); - ~RewriteEngine() throw() {} bool needsCheck( Theory::Effort e ); void check(Theory::Effort e, QEffort quant_e); diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index ab844c6ec..934a09a8e 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -80,7 +80,7 @@ class TheoryModel : public Model friend class TheoryEngineModelBuilder; public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); - virtual ~TheoryModel() throw(); + ~TheoryModel() override; /** reset the model */ virtual void reset(); diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index 64ca41df2..bc729bcbf 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -154,17 +154,16 @@ private: Statistics d_stats; -protected: - - void contextNotifyPop() { + protected: + void contextNotifyPop() override + { Debug("ufsymm") << "UFSYMM: clearing state due to pop" << std::endl; clear(); } -public: - + public: SymmetryBreaker(context::Context* context, std::string name = ""); - ~SymmetryBreaker() throw() {} + void assertFormula(TNode phi); void apply(std::vector& newClauses); diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp index 123d568cb..a957d6809 100644 --- a/src/util/abstract_value.cpp +++ b/src/util/abstract_value.cpp @@ -30,9 +30,12 @@ std::ostream& operator<<(std::ostream& out, const AbstractValue& val) { return out << "@" << val.getIndex(); } -AbstractValue::AbstractValue(Integer index) throw(IllegalArgumentException) : - d_index(index) { - PrettyCheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str()); +AbstractValue::AbstractValue(Integer index) : d_index(index) +{ + PrettyCheckArgument(index >= 1, + index, + "index >= 1 required for abstract value, not `%s'", + index.toString().c_str()); } }/* CVC4 namespace */ diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h index 9c8e1cb37..2fbc26bec 100644 --- a/src/util/abstract_value.h +++ b/src/util/abstract_value.h @@ -27,36 +27,25 @@ namespace CVC4 { class CVC4_PUBLIC AbstractValue { const Integer d_index; -public: + public: + AbstractValue(Integer index); - AbstractValue(Integer index) throw(IllegalArgumentException); - - ~AbstractValue() throw() {} - - const Integer& getIndex() const throw() { - return d_index; - } - - bool operator==(const AbstractValue& val) const throw() { + const Integer& getIndex() const { return d_index; } + bool operator==(const AbstractValue& val) const + { return d_index == val.d_index; } - bool operator!=(const AbstractValue& val) const throw() { - return !(*this == val); - } - - bool operator<(const AbstractValue& val) const throw() { + bool operator!=(const AbstractValue& val) const { return !(*this == val); } + bool operator<(const AbstractValue& val) const + { return d_index < val.d_index; } - bool operator<=(const AbstractValue& val) const throw() { + bool operator<=(const AbstractValue& val) const + { return d_index <= val.d_index; } - bool operator>(const AbstractValue& val) const throw() { - return !(*this <= val); - } - bool operator>=(const AbstractValue& val) const throw() { - return !(*this < val); - } - + bool operator>(const AbstractValue& val) const { return !(*this <= val); } + bool operator>=(const AbstractValue& val) const { return !(*this < val); } };/* class AbstractValue */ std::ostream& operator<<(std::ostream& out, const AbstractValue& val) CVC4_PUBLIC; diff --git a/src/util/cache.h b/src/util/cache.h index 38dc0fc99..4f9af98a6 100644 --- a/src/util/cache.h +++ b/src/util/cache.h @@ -58,9 +58,9 @@ public: bool d_fired; public: - Scope(Cache& cache, const T& elt) throw(AssertionException) : - d_cache(cache), - d_fired(d_cache.computing(elt)) { + Scope(Cache& cache, const T& elt) + : d_cache(cache), d_fired(d_cache.computing(elt)) + { } ~Scope() { @@ -69,21 +69,21 @@ public: } } - operator bool() throw() { - return d_fired; - } - - const U& get() throw(AssertionException) { + operator bool() const { return d_fired; } + const U& get() const + { Assert(d_fired, "nothing in cache"); return d_cache.get(); } - U& operator()(U& computed) throw(AssertionException) { + U& operator()(U& computed) + { Assert(!d_fired, "can only cache a computation once"); d_fired = true; return d_cache(computed); } - const U& operator()(const U& computed) throw(AssertionException) { + const U& operator()(const U& computed) + { Assert(!d_fired, "can only cache a computation once"); d_fired = true; return d_cache(computed); diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index 8f98d908f..c67277ad0 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -59,8 +59,8 @@ Integer Integer::exactQuotient(const Integer& y) const { return Integer( cln::exquo(d_value, y.d_value) ); } - -void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) { +void Integer::parseInt(const std::string& s, unsigned base) +{ cln::cl_read_flags flags; flags.syntax = cln::syntax_integer; flags.lsyntax = cln::lsyntax_standard; @@ -86,7 +86,10 @@ void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_a readInt(flags, s, base); } -void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) { +void Integer::readInt(const cln::cl_read_flags& flags, + const std::string& s, + unsigned base) +{ try { // Removing leading zeroes, CLN has a bug for these inputs up to and // including CLN v1.3.2. diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 0433494cc..542333b1f 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -52,11 +52,13 @@ private: * Constructs an Integer by copying a CLN C++ primitive. */ Integer(const cln::cl_I& val) : d_value(val) {} + // Throws a std::invalid_argument on invalid input `s` for the given base. + void readInt(const cln::cl_read_flags& flags, + const std::string& s, + unsigned base); - void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument); - - void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument); - + // Throws a std::invalid_argument on invalid inputs. + void parseInt(const std::string& s, unsigned base); // These constants are to help with CLN conversion in 32 bit. // See http://www.ginac.de/CLN/cln.html#Conversions @@ -81,11 +83,13 @@ public: * For more information about what is a valid rational string, * see GMP's documentation for mpq_set_str(). */ - explicit Integer(const char* sp, unsigned base = 10) throw (std::invalid_argument) { + explicit Integer(const char* sp, unsigned base = 10) + { parseInt(std::string(sp), base); } - explicit Integer(const std::string& s, unsigned base = 10) throw (std::invalid_argument) { + explicit Integer(const std::string& s, unsigned base = 10) + { parseInt(s, base); } diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 0b09bf1fd..2752971d2 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -84,14 +84,15 @@ public: /** Constructs a rational with the value 0/1. */ Rational() : d_value(0){ } - /** * Constructs a Rational from a C string in a given base (defaults to 10). + * * Throws std::invalid_argument if the string is not a valid rational. * For more information about what is a valid rational string, * see GMP's documentation for mpq_set_str(). */ - explicit Rational(const char* s, unsigned base = 10) throw (std::invalid_argument){ + explicit Rational(const char* s, unsigned base = 10) + { cln::cl_read_flags flags; flags.syntax = cln::syntax_rational; @@ -105,7 +106,8 @@ public: throw std::invalid_argument(ss.str()); } } - Rational(const std::string& s, unsigned base = 10) throw (std::invalid_argument){ + Rational(const std::string& s, unsigned base = 10) + { cln::cl_read_flags flags; flags.syntax = cln::syntax_rational; diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index b2adb4aba..9bcdcd96b 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -173,13 +173,14 @@ uint64_t ResourceManager::getTimeRemaining() const { return d_thisCallTimeBudget - time_passed; } -void ResourceManager::spendResource(unsigned ammount) throw (UnsafeInterruptException) { +void ResourceManager::spendResource(unsigned amount) +{ ++d_spendResourceCalls; - d_cumulativeResourceUsed += ammount; + d_cumulativeResourceUsed += amount; if (!d_on) return; Debug("limit") << "ResourceManager::spendResource()" << std::endl; - d_thisCallResourceUsed += ammount; + d_thisCallResourceUsed += amount; if(out()) { Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl; Trace("limit") << " on call " << d_spendResourceCalls << std::endl; diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 35315559f..e49b27286 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -151,8 +151,8 @@ public: uint64_t getResourceBudgetForThisCall() { return d_thisCallResourceBudget; } - - void spendResource(unsigned ammount) throw(UnsafeInterruptException); + // Throws an UnsafeInterruptException if there are no remaining resources. + void spendResource(unsigned amount); void setHardLimit(bool value); void setResourceLimit(uint64_t units, bool cumulative = false); diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 016bd2184..11afb99ed 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -140,10 +140,8 @@ std::ostream& operator<<(std::ostream& os, const timespec& t) { /** Construct a statistics registry */ -StatisticsRegistry::StatisticsRegistry(const std::string& name) - throw(CVC4::IllegalArgumentException) : - Stat(name) { - +StatisticsRegistry::StatisticsRegistry(const std::string& name) : Stat(name) +{ d_prefix = name; if(__CVC4_USE_STATISTICS) { PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name, @@ -152,7 +150,8 @@ StatisticsRegistry::StatisticsRegistry(const std::string& name) } } -void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) { +void StatisticsRegistry::registerStat(Stat* s) +{ #ifdef CVC4_STATISTICS_ON PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s, "Statistic `%s' was not registered with this registry.", @@ -161,7 +160,8 @@ void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentExcept #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat_() */ -void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) { +void StatisticsRegistry::unregisterStat(Stat* s) +{ #ifdef CVC4_STATISTICS_ON PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s, "Statistic `%s' was not registered with this registry.", diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 3de001e32..73a545185 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -91,8 +91,8 @@ public: * will throw an assertion exception if the given name contains the * statistic delimiter string. */ - Stat(const std::string& name) throw(CVC4::IllegalArgumentException) : - d_name(name) { + Stat(const std::string& name) : d_name(name) + { if(__CVC4_USE_STATISTICS) { CheckArgument(d_name.find(", ") == std::string::npos, name, "Statistics names cannot include a comma (',')"); @@ -659,8 +659,7 @@ public: StatisticsRegistry() {} /** Construct a statistics registry */ - StatisticsRegistry(const std::string& name) - throw(CVC4::IllegalArgumentException); + StatisticsRegistry(const std::string& name); /** * Set the name of this statistic registry, used as prefix during @@ -689,10 +688,10 @@ public: } /** Register a new statistic */ - void registerStat(Stat* s) throw(CVC4::IllegalArgumentException); + void registerStat(Stat* s); /** Unregister a new statistic */ - void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException); + void unregisterStat(Stat* s); };/* class StatisticsRegistry */ diff --git a/src/util/tuple.h b/src/util/tuple.h index e2440cc39..10da466de 100644 --- a/src/util/tuple.h +++ b/src/util/tuple.h @@ -28,11 +28,12 @@ namespace CVC4 { class CVC4_PUBLIC TupleUpdate { unsigned d_index; -public: - TupleUpdate(unsigned index) throw() : d_index(index) { } - unsigned getIndex() const throw() { return d_index; } - bool operator==(const TupleUpdate& t) const throw() { return d_index == t.d_index; } - bool operator!=(const TupleUpdate& t) const throw() { return d_index != t.d_index; } + + public: + TupleUpdate(unsigned index) : d_index(index) {} + unsigned getIndex() const { return d_index; } + bool operator==(const TupleUpdate& t) const { return d_index == t.d_index; } + bool operator!=(const TupleUpdate& t) const { return d_index != t.d_index; } };/* class TupleUpdate */ struct CVC4_PUBLIC TupleUpdateHashFunction { -- 2.30.2