diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-05 15:36:50 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-05 15:36:50 -0800 |
commit | 3d31caa30e094d337a4919b3d1e6ba9259e461b8 (patch) | |
tree | e99bc99c2ce450f7d0c4fa8c0938b24e886af996 /src/theory/quantifiers/ematching | |
parent | a2e78ec8dd5e935b6ef166154be7ee35bffc6d32 (diff) |
Enable -Wsuggest-override by default. (#1643)
Adds missing override keywords.
Diffstat (limited to 'src/theory/quantifiers/ematching')
-rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching.h | 34 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/instantiation_engine.h | 16 |
3 files changed, 28 insertions, 24 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index 41fec5e5f..85bb09086 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -122,7 +122,7 @@ class HigherOrderTrigger : public Trigger * Extends Trigger::addInstantiations to also send * lemmas based on addHoTypeMatchPredicateLemmas. */ - virtual int addInstantiations() override; + int addInstantiations() override; protected: /** diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index 8f11dfedf..eba49fa9a 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -40,9 +40,10 @@ private: /** counter for quantifiers */ std::map< Node, int > d_counter; /** process functions */ - void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e ); -public: + void processResetInstantiationRound(Theory::Effort effort) override; + int process(Node f, Theory::Effort effort, int e) override; + + public: InstStrategyUserPatterns( QuantifiersEngine* ie ) : InstStrategy( ie ){} ~InstStrategyUserPatterns(){} @@ -54,7 +55,7 @@ public: /** get user pattern */ inst::Trigger* getUserGenerator( Node q, int i ) { return d_user_gen[q][ i ]; } /** identify */ - std::string identify() const { return std::string("UserPatterns"); } + std::string identify() const override { return std::string("UserPatterns"); } };/* class InstStrategyUserPatterns */ class InstStrategyAutoGenTriggers : public InstStrategy { @@ -89,16 +90,16 @@ private: std::map< Node, Node > d_pat_to_mpat; private: /** process functions */ - void processResetInstantiationRound( Theory::Effort effort ); - int process( Node q, Theory::Effort effort, int e ); - /** generate triggers */ - void generateTriggers( Node q ); - void addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat ); - void addTrigger( inst::Trigger * tr, Node f ); - /** has user patterns */ - bool hasUserPatterns( Node q ); - /** has user patterns */ - std::map< Node, bool > d_hasUserPatterns; + void processResetInstantiationRound(Theory::Effort effort) override; + int process(Node q, Theory::Effort effort, int e) override; + /** generate triggers */ + void generateTriggers(Node q); + void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat); + void addTrigger(inst::Trigger* tr, Node f); + /** has user patterns */ + bool hasUserPatterns(Node q); + /** has user patterns */ + std::map<Node, bool> d_hasUserPatterns; public: InstStrategyAutoGenTriggers( QuantifiersEngine* qe ); ~InstStrategyAutoGenTriggers(){} @@ -106,7 +107,10 @@ public: /** get auto-generated trigger */ inst::Trigger* getAutoGenTrigger( Node q ); /** identify */ - std::string identify() const { return std::string("AutoGenTriggers"); } + std::string identify() const override + { + return std::string("AutoGenTriggers"); + } /** add pattern */ void addUserNoPattern( Node q, Node pat ); };/* class InstStrategyAutoGenTriggers */ diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index 18b5ea19c..32ddb19ed 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -76,19 +76,19 @@ class InstantiationEngine : public QuantifiersModule { public: InstantiationEngine(QuantifiersEngine* qe); ~InstantiationEngine(); - void presolve(); - bool needsCheck(Theory::Effort e); - void reset_round(Theory::Effort e); - void check(Theory::Effort e, QEffort quant_e); - bool checkCompleteFor(Node q); - void preRegisterQuantifier(Node q); - void registerQuantifier(Node q); + void presolve() override; + bool needsCheck(Theory::Effort e) override; + void reset_round(Theory::Effort e) override; + void check(Theory::Effort e, QEffort quant_e) override; + bool checkCompleteFor(Node q) override; + void preRegisterQuantifier(Node q) override; + void registerQuantifier(Node q) override; Node explain(TNode n) { return Node::null(); } /** add user pattern */ void addUserPattern(Node q, Node pat); void addUserNoPattern(Node q, Node pat); /** Identify this module */ - std::string identify() const { return "InstEngine"; } + std::string identify() const override { return "InstEngine"; } }; /* class InstantiationEngine */ }/* CVC4::theory::quantifiers namespace */ |