fixing some clang warnings

ModelWriter · Oct 3, 2017 · d4f60e0 · d4f60e0
1 parent 5ef6fc4
commit d4f60e0
Show file tree

Hide file tree

Showing 11 changed files with 17 additions and 18 deletions.
diff --git a/Indexing/ResultSubstitution.hpp b/Indexing/ResultSubstitution.hpp
@@ -125,7 +125,7 @@ class ResultSubstitution
 //  static ResultSubstitutionSP fromSubstitution(EGSubstitution* s,
 //	  int queryBank, int resultBank);
 #if VDEBUG
-  virtual vstring toString(bool deref=false){ NOT_IMPLEMENTED; }
+  virtual vstring toString(){ NOT_IMPLEMENTED; }
 #endif
 };
 

diff --git a/Indexing/SubstitutionTree.hpp b/Indexing/SubstitutionTree.hpp
@@ -638,7 +638,7 @@ class SubstitutionTree
   public:
     LeafIterator(SubstitutionTree* st)
     : _nextRootPtr(st->_nodes.begin()), _afterLastRootPtr(st->_nodes.end()),
-    _nodeIterators(8), tag(st->tag) {}
+    _nodeIterators(8) {}
     bool hasNext();
     Leaf* next()
     {
@@ -650,7 +650,6 @@ class SubstitutionTree
     Node** _afterLastRootPtr;
     Node* _curr;
     Stack<NodeIterator> _nodeIterators;
-    bool tag;
   };
 
   typedef pair<pair<LeafData*, ResultSubstitutionSP>,UnificationConstraintStackSP> QueryResult;

diff --git a/Inferences/CTFwSubsAndRes.hpp b/Inferences/CTFwSubsAndRes.hpp
@@ -26,8 +26,8 @@ class CTFwSubsAndRes
   CTFwSubsAndRes(bool subsumptionResolution)
   : _subsumptionResolution(subsumptionResolution) {}
 
-  void attach(SaturationAlgorithm* salg);
-  void detach();
+  void attach(SaturationAlgorithm* salg) override;
+  void detach() override;
   bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override;
 private:
   Clause* buildSResClause(Clause* cl, unsigned resolvedIndex, Clause* premise);

diff --git a/Inferences/ForwardDemodulation.hpp b/Inferences/ForwardDemodulation.hpp
@@ -26,8 +26,8 @@ class ForwardDemodulation
   CLASS_NAME(ForwardDemodulation);
   USE_ALLOCATOR(ForwardDemodulation);
 
-  void attach(SaturationAlgorithm* salg);
-  void detach();
+  void attach(SaturationAlgorithm* salg) override;
+  void detach() override;
   bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override;
 private:
   bool _preorderedOnly;

diff --git a/Inferences/ForwardLiteralRewriting.hpp b/Inferences/ForwardLiteralRewriting.hpp
@@ -25,8 +25,8 @@ class ForwardLiteralRewriting
   CLASS_NAME(ForwardLiteralRewriting);
   USE_ALLOCATOR(ForwardLiteralRewriting);
 
-  void attach(SaturationAlgorithm* salg);
-  void detach();
+  void attach(SaturationAlgorithm* salg) override;
+  void detach() override;
   bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override;
 private:
   RewriteRuleIndex* _index;

diff --git a/Inferences/ForwardSubsumptionAndResolution.hpp b/Inferences/ForwardSubsumptionAndResolution.hpp
@@ -27,8 +27,8 @@ class ForwardSubsumptionAndResolution
   ForwardSubsumptionAndResolution(bool subsumptionResolution=true)
   : _subsumptionResolution(subsumptionResolution) {}
 
-  void attach(SaturationAlgorithm* salg);
-  void detach();
+  void attach(SaturationAlgorithm* salg) override;
+  void detach() override;
   bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override;
 
   static Clause* generateSubsumptionResolutionClause(Clause* cl, Literal* lit, Clause* baseClause);

diff --git a/Inferences/GlobalSubsumption.hpp b/Inferences/GlobalSubsumption.hpp
@@ -39,8 +39,8 @@ class GlobalSubsumption
    */
   GlobalSubsumption(const Options& opts, GroundingIndex* idx) : GlobalSubsumption(opts) { _index = idx; }
 
-  void attach(SaturationAlgorithm* salg);
-  void detach();
+  void attach(SaturationAlgorithm* salg) override;
+  void detach() override;
   bool perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) override;
 
   Clause* perform(Clause* cl, Stack<Unit*>& prems);

diff --git a/Inferences/HyperSuperposition.hpp b/Inferences/HyperSuperposition.hpp
@@ -27,8 +27,8 @@ class HyperSuperposition
 
   HyperSuperposition() : _index(0) {}
 
-  void attach(SaturationAlgorithm* salg);
-  void detach();
+  void attach(SaturationAlgorithm* salg) override;
+  void detach() override;
 
   Clause* generateClause(Clause* queryCl, Literal* queryLit, SLQueryResult res, Limits* limits=0);
   ClauseIterator generateClauses(Clause* premise);

diff --git a/Kernel/ELiteralSelector.hpp b/Kernel/ELiteralSelector.hpp
@@ -44,7 +44,7 @@ class ELiteralSelector
 
   bool isBGComplete() const override { return true; }
 protected:
-  void doSelection(Clause* c, unsigned eligible);
+  void doSelection(Clause* c, unsigned eligible) override;
 
 private:
   LiteralList* getMaximalsInOrder(Clause* c, unsigned eligible);

diff --git a/Kernel/SpassLiteralSelector.hpp b/Kernel/SpassLiteralSelector.hpp
@@ -37,7 +37,7 @@ class SpassLiteralSelector
 
   bool isBGComplete() const override { return true; }
 protected:
-  void doSelection(Clause* c, unsigned eligible);
+  void doSelection(Clause* c, unsigned eligible) override;
 
 private:
   LiteralList* getMaximalsInOrder(Clause* c, unsigned eligible);

diff --git a/Shell/SimplifyProver.cpp b/Shell/SimplifyProver.cpp
@@ -1516,7 +1516,7 @@ void SimplifyProver::buildDistinct()
   Context context = (Context)_isaved.pop();
   unsigned length = (unsigned)_isaved.pop();
   args.ensure(length);
-  for (unsigned i = length-1;i >= 0;i--) {
+  for (int i = length-1;i >= 0;i--) {
     args[i] = _tsaved.pop();
   }
   if (length == 2) {