Enable -Wsuggest-override by default. (#1643)

Adds missing override keywords.

3 files changed, 68 insertions, 54 deletions

diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h
index 3114821b3..f2566d35c 100644
--- a/src/smt/managed_ostreams.h
+++ b/src/smt/managed_ostreams.h
@@ -79,7 +79,8 @@ class SetToDefaultSourceListener : public Listener {
   SetToDefaultSourceListener(ManagedOstream* managedOstream)
       : d_managedOstream(managedOstream){}
 
-  virtual void notify() {
+  void notify() override
+  {
     d_managedOstream->set(d_managedOstream->defaultSource());
   }
 
@@ -97,15 +98,15 @@ class ManagedDumpOStream : public ManagedOstream {
   ManagedDumpOStream(){}
   ~ManagedDumpOStream();
 
-  virtual const char* getName() const { return "dump-to"; }
-  virtual std::string defaultSource() const;
+  const char* getName() const override { return "dump-to"; }
+  std::string defaultSource() const override;
 
  protected:
   /** Initializes an output stream. Not necessarily managed. */
-  virtual void initialize(std::ostream* outStream);
+  void initialize(std::ostream* outStream) override;
 
   /** Adds special cases to an ostreamopener. */
-  virtual void addSpecialCases(OstreamOpener* opener) const;
+  void addSpecialCases(OstreamOpener* opener) const override;
 };/* class ManagedDumpOStream */
 
 /**
@@ -120,15 +121,15 @@ class ManagedRegularOutputChannel : public ManagedOstream {
   /** Assumes Options are in scope. */
   ~ManagedRegularOutputChannel();
 
-  virtual const char* getName() const { return "regular-output-channel"; }
-  virtual std::string defaultSource() const;
+  const char* getName() const override { return "regular-output-channel"; }
+  std::string defaultSource() const override;
 
  protected:
   /** Initializes an output stream. Not necessarily managed. */
-  virtual void initialize(std::ostream* outStream);
+  void initialize(std::ostream* outStream) override;
 
   /** Adds special cases to an ostreamopener. */
-  virtual void addSpecialCases(OstreamOpener* opener) const;
+  void addSpecialCases(OstreamOpener* opener) const override;
 };/* class ManagedRegularOutputChannel */
 
 
@@ -144,15 +145,15 @@ class ManagedDiagnosticOutputChannel : public ManagedOstream {
   /** Assumes Options are in scope. */
   ~ManagedDiagnosticOutputChannel();
 
-  virtual const char* getName() const { return "diagnostic-output-channel"; }
-  virtual std::string defaultSource() const;
+  const char* getName() const override { return "diagnostic-output-channel"; }
+  std::string defaultSource() const override;
 
  protected:
   /** Initializes an output stream. Not necessarily managed. */
-  virtual void initialize(std::ostream* outStream);
+  void initialize(std::ostream* outStream) override;
 
   /** Adds special cases to an ostreamopener. */
-  virtual void addSpecialCases(OstreamOpener* opener) const;
+  void addSpecialCases(OstreamOpener* opener) const override;
 };/* class ManagedRegularOutputChannel */
 
 /** This controls the memory associated with replay-log. */
@@ -162,15 +163,15 @@ class ManagedReplayLogOstream : public ManagedOstream {
   ~ManagedReplayLogOstream();
 
   std::ostream* getReplayLog() const { return d_replayLog; }
-  virtual const char* getName() const { return "replay-log"; }
-  virtual std::string defaultSource() const;
+  const char* getName() const override { return "replay-log"; }
+  std::string defaultSource() const override;
 
  protected:
   /** Initializes an output stream. Not necessarily managed. */
-  virtual void initialize(std::ostream* outStream);
+  void initialize(std::ostream* outStream) override;
 
   /** Adds special cases to an ostreamopener. */
-  virtual void addSpecialCases(OstreamOpener* opener) const;
+  void addSpecialCases(OstreamOpener* opener) const override;
 
  private:
   std::ostream* d_replayLog;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6e90ab152..74d6c1b10 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -298,7 +298,8 @@ struct SmtEngineStatistics {
 class SoftResourceOutListener : public Listener {
  public:
   SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
-  virtual void notify() {
+  void notify() override
+  {
     SmtScope scope(d_smt);
     Assert(smt::smtEngineInScope());
     d_smt->interrupt();
@@ -311,7 +312,8 @@ class SoftResourceOutListener : public Listener {
 class HardResourceOutListener : public Listener {
  public:
   HardResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
-  virtual void notify() {
+  void notify() override
+  {
     SmtScope scope(d_smt);
     theory::Rewriter::clearCaches();
   }
@@ -322,7 +324,8 @@ class HardResourceOutListener : public Listener {
 class SetLogicListener : public Listener {
  public:
   SetLogicListener(SmtEngine& smt) : d_smt(&smt) {}
-  virtual void notify() {
+  void notify() override
+  {
     LogicInfo inOptions(options::forceLogicString());
     d_smt->setLogic(inOptions);
   }
@@ -333,9 +336,8 @@ class SetLogicListener : public Listener {
 class BeforeSearchListener : public Listener {
  public:
   BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {}
-  virtual void notify() {
-    d_smt->beforeSearch();
-  }
+  void notify() override { d_smt->beforeSearch(); }
+
  private:
   SmtEngine* d_smt;
 }; /* class BeforeSearchListener */
@@ -346,7 +348,8 @@ class UseTheoryListListener : public Listener {
       : d_theoryEngine(theoryEngine)
   {}
 
-  void notify() {
+  void notify() override
+  {
     std::stringstream commaList(options::useTheoryList());
     std::string token;
 
@@ -375,7 +378,8 @@ class UseTheoryListListener : public Listener {
 
 class SetDefaultExprDepthListener : public Listener {
  public:
-  virtual void notify() {
+  void notify() override
+  {
     int depth = options::defaultExprDepth();
     Debug.getStream() << expr::ExprSetDepth(depth);
     Trace.getStream() << expr::ExprSetDepth(depth);
@@ -389,7 +393,8 @@ class SetDefaultExprDepthListener : public Listener {
 
 class SetDefaultExprDagListener : public Listener {
  public:
-  virtual void notify() {
+  void notify() override
+  {
     int dag = options::defaultDagThresh();
     Debug.getStream() << expr::ExprDag(dag);
     Trace.getStream() << expr::ExprDag(dag);
@@ -403,7 +408,8 @@ class SetDefaultExprDagListener : public Listener {
 
 class SetPrintExprTypesListener : public Listener {
  public:
-  virtual void notify() {
+  void notify() override
+  {
     bool value = options::printExprTypes();
     Debug.getStream() << expr::ExprPrintTypes(value);
     Trace.getStream() << expr::ExprPrintTypes(value);
@@ -417,7 +423,8 @@ class SetPrintExprTypesListener : public Listener {
 
 class DumpModeListener : public Listener {
  public:
-  virtual void notify() {
+  void notify() override
+  {
     const std::string& value = options::dumpModeString();
     Dump.setDumpFromString(value);
   }
@@ -425,7 +432,8 @@ class DumpModeListener : public Listener {
 
 class PrintSuccessListener : public Listener {
  public:
-  virtual void notify() {
+  void notify() override
+  {
     bool value = options::printSuccess();
     Debug.getStream() << Command::printsuccess(value);
     Trace.getStream() << Command::printsuccess(value);
@@ -748,7 +756,8 @@ public:
     d_resourceManager->spendResource(amount);
   }
 
-  void nmNotifyNewSort(TypeNode tn, uint32_t flags) {
+  void nmNotifyNewSort(TypeNode tn, uint32_t flags) override
+  {
     DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
                          0,
                          tn.toType());
@@ -757,19 +766,22 @@ public:
     }
   }
 
-  void nmNotifyNewSortConstructor(TypeNode tn) {
+  void nmNotifyNewSortConstructor(TypeNode tn) override
+  {
     DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
                          tn.getAttribute(expr::SortArityAttr()),
                          tn.toType());
     d_smt.addToModelCommandAndDump(c);
   }
 
-  void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) {
+  void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) override
+  {
     DatatypeDeclarationCommand c(dtts);
     d_smt.addToModelCommandAndDump(c);
   }
 
-  void nmNotifyNewVar(TNode n, uint32_t flags) {
+  void nmNotifyNewVar(TNode n, uint32_t flags) override
+  {
     DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()),
                              n.toExpr(),
                              n.getType().toType());
@@ -781,11 +793,12 @@ public:
     }
   }
 
-  void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) {
+  void nmNotifyNewSkolem(TNode n,
+                         const std::string& comment,
+                         uint32_t flags) override
+  {
     string id = n.getAttribute(expr::VarNameAttr());
-    DeclareFunctionCommand c(id,
-                             n.toExpr(),
-                             n.getType().toType());
+    DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType());
     if(Dump.isOn("skolems") && comment != "") {
       Dump("skolems") << CommentCommand(id + " is " + comment);
     }
@@ -797,7 +810,7 @@ public:
     }
   }
 
-  void nmNotifyDeleteNode(TNode n) {}
+  void nmNotifyDeleteNode(TNode n) override {}
 
   Node applySubstitutions(TNode node) const {
     return Rewriter::rewrite(d_topLevelSubstitutions.apply(node));
diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h
index ce4504279..a161985de 100644
--- a/src/smt/update_ostream.h
+++ b/src/smt/update_ostream.h
@@ -73,50 +73,50 @@ public:
 
 class OptionsErrOstreamUpdate : public OstreamUpdate {
  public:
-  virtual std::ostream& get() { return *(options::err()); }
-  virtual void set(std::ostream* setTo) { return options::err.set(setTo); }
+  std::ostream& get() override { return *(options::err()); }
+  void set(std::ostream* setTo) override { return options::err.set(setTo); }
 };  /* class OptionsErrOstreamUpdate */
 
 class DumpOstreamUpdate : public OstreamUpdate {
  public:
-  virtual std::ostream& get() { return Dump.getStream(); }
-  virtual void set(std::ostream* setTo) { Dump.setStream(setTo); }
+  std::ostream& get() override { return Dump.getStream(); }
+  void set(std::ostream* setTo) override { Dump.setStream(setTo); }
 };  /* class DumpOstreamUpdate */
 
 class DebugOstreamUpdate : public OstreamUpdate {
  public:
-  virtual std::ostream& get() { return Debug.getStream(); }
-  virtual void set(std::ostream* setTo) { Debug.setStream(setTo); }
+  std::ostream& get() override { return Debug.getStream(); }
+  void set(std::ostream* setTo) override { Debug.setStream(setTo); }
 };  /* class DebugOstreamUpdate */
 
 class WarningOstreamUpdate : public OstreamUpdate {
  public:
-  virtual std::ostream& get() { return Warning.getStream(); }
-  virtual void set(std::ostream* setTo) { Warning.setStream(setTo); }
+  std::ostream& get() override { return Warning.getStream(); }
+  void set(std::ostream* setTo) override { Warning.setStream(setTo); }
 };  /* class WarningOstreamUpdate */
 
 class MessageOstreamUpdate : public OstreamUpdate {
  public:
-  virtual std::ostream& get() { return Message.getStream(); }
-  virtual void set(std::ostream* setTo) { Message.setStream(setTo); }
+  std::ostream& get() override { return Message.getStream(); }
+  void set(std::ostream* setTo) override { Message.setStream(setTo); }
 };  /* class MessageOstreamUpdate */
 
 class NoticeOstreamUpdate : public OstreamUpdate {
  public:
-  virtual std::ostream& get() { return Notice.getStream(); }
-  virtual void set(std::ostream* setTo) { Notice.setStream(setTo); }
+  std::ostream& get() override { return Notice.getStream(); }
+  void set(std::ostream* setTo) override { Notice.setStream(setTo); }
 };  /* class NoticeOstreamUpdate */
 
 class ChatOstreamUpdate : public OstreamUpdate {
  public:
-  virtual std::ostream& get() { return Chat.getStream(); }
-  virtual void set(std::ostream* setTo) { Chat.setStream(setTo); }
+  std::ostream& get() override { return Chat.getStream(); }
+  void set(std::ostream* setTo) override { Chat.setStream(setTo); }
 };  /* class ChatOstreamUpdate */
 
 class TraceOstreamUpdate : public OstreamUpdate {
  public:
-  virtual std::ostream& get() { return Trace.getStream(); }
-  virtual void set(std::ostream* setTo) { Trace.setStream(setTo); }
+  std::ostream& get() override { return Trace.getStream(); }
+  void set(std::ostream* setTo) override { Trace.setStream(setTo); }
 };  /* class TraceOstreamUpdate */
 
 }/* CVC4 namespace */