Merge branch 'master' into cleanup_outputcleanup_output

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 */