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

Adds missing override keywords.

8 files changed, 33 insertions, 27 deletions

diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h
index 73798f94c..fa65214e7 100644
--- a/src/theory/arith/attempt_solution_simplex.h
+++ b/src/theory/arith/attempt_solution_simplex.h
@@ -67,11 +67,9 @@ public:
 
   Result::Sat attempt(const ApproximateSimplex::Solution& sol);
 
-  Result::Sat findModel(bool exactResult){
-    Unreachable();
-  }
+  Result::Sat findModel(bool exactResult) override { Unreachable(); }
 
-private:
+ private:
   bool matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const;
 
   bool processSignals(){
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 3710ac5c0..f84550dcc 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -73,7 +73,7 @@ private:
   TheoryArithPrivate& d_arith;
 public:
   SetupLiteralCallBack(TheoryArithPrivate& ta);
-  void operator()(TNode lit);
+  void operator()(TNode lit) override;
 };
 
 class DeltaComputeCallback : public RationalCallBack {
@@ -81,7 +81,7 @@ private:
   const TheoryArithPrivate& d_ta;
 public:
   DeltaComputeCallback(const TheoryArithPrivate& ta);
-  Rational operator()() const;
+  Rational operator()() const override;
 };
 
 class BasicVarModelUpdateCallBack : public ArithVarCallBack{
@@ -89,7 +89,7 @@ private:
   TheoryArithPrivate& d_ta;
 public:
   BasicVarModelUpdateCallBack(TheoryArithPrivate& ta);
-  void operator()(ArithVar x);
+  void operator()(ArithVar x) override;
 };
 
 class TempVarMalloc : public ArithVarMalloc {
@@ -97,8 +97,8 @@ private:
   TheoryArithPrivate& d_ta;
 public:
   TempVarMalloc(TheoryArithPrivate& ta);
-  ArithVar request();
-  void release(ArithVar v);
+  ArithVar request() override;
+  void release(ArithVar v) override;
 };
 
 class RaiseConflict {
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 228f29838..5085dc841 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -61,17 +61,20 @@ private:
   public:
     ArithCongruenceNotify(ArithCongruenceManager& acm);
 
-    bool eqNotifyTriggerEquality(TNode equality, bool value);
+    bool eqNotifyTriggerEquality(TNode equality, bool value) override;
 
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
 
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
+    bool eqNotifyTriggerTermEquality(TheoryId tag,
+                                     TNode t1,
+                                     TNode t2,
+                                     bool value) override;
 
-    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
-    void eqNotifyNewClass(TNode t);
-    void eqNotifyPreMerge(TNode t1, TNode t2);
-    void eqNotifyPostMerge(TNode t1, TNode t2);
-    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
+    void eqNotifyNewClass(TNode t) override;
+    void eqNotifyPreMerge(TNode t1, TNode t2) override;
+    void eqNotifyPostMerge(TNode t1, TNode t2) override;
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
   };
   ArithCongruenceNotify d_notify;
   
diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h
index 2911592c7..10d18170e 100644
--- a/src/theory/arith/dual_simplex.h
+++ b/src/theory/arith/dual_simplex.h
@@ -63,7 +63,8 @@ class DualSimplexDecisionProcedure : public SimplexDecisionProcedure{
 public:
   DualSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
 
-  Result::Sat findModel(bool exactResult) {
+  Result::Sat findModel(bool exactResult) override
+  {
     return dualFindModel(exactResult);
   }
 
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index c4f996f9f..a93fa88e8 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -66,7 +66,7 @@ class FCSimplexDecisionProcedure : public SimplexDecisionProcedure{
 public:
   FCSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
 
-  Result::Sat findModel(bool exactResult);
+  Result::Sat findModel(bool exactResult) override;
 
   // other error variables are dropping
   WitnessImprovement dualLikeImproveError(ArithVar evar);
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index c2fa99e31..0f2862a72 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -588,13 +588,16 @@ private:
     LinearEqualityModule* d_linEq;
   public:
     TrackingCallback(LinearEqualityModule* le) : d_linEq(le) {}
-    void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){
+    void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override
+    {
       d_linEq->trackingCoefficientChange(ridx, nb, oldSgn, currSgn);
     }
-    void multiplyRow(RowIndex ridx, int sgn){
+    void multiplyRow(RowIndex ridx, int sgn) override
+    {
       d_linEq->trackingMultiplyRow(ridx, sgn);
     }
-    bool canUseRow(RowIndex ridx) const {
+    bool canUseRow(RowIndex ridx) const override
+    {
       ArithVar basic = d_linEq->getTableau().rowIndexToBasic(ridx);
       return d_linEq->basicIsTracked(basic);
     }
@@ -746,7 +749,8 @@ private:
   LinearEqualityModule* d_mod;
 public:
   UpdateTrackingCallback(LinearEqualityModule* mod): d_mod(mod){}
-  void operator()(ArithVar v, const BoundsInfo& bi){
+  void operator()(ArithVar v, const BoundsInfo& bi) override
+  {
     d_mod->includeBoundUpdate(v, bi);
   }
 };
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h
index 2e0a1ebb2..eda5b9dac 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -48,9 +48,9 @@ public:
 
 class NoEffectCCCB : public CoefficientChangeCallback {
 public:
-  void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn);
-  void multiplyRow(RowIndex ridx, int Sgn);
-  bool canUseRow(RowIndex ridx) const;
+ void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override;
+ void multiplyRow(RowIndex ridx, int Sgn) override;
+ bool canUseRow(RowIndex ridx) const override;
 };
 
 template<class T>
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index 5f2233b3f..54a47ac4d 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -66,7 +66,7 @@ class SumOfInfeasibilitiesSPD : public SimplexDecisionProcedure {
 public:
   SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
 
-  Result::Sat findModel(bool exactResult);
+  Result::Sat findModel(bool exactResult) override;
 
   // other error variables are dropping
   WitnessImprovement dualLikeImproveError(ArithVar evar);