From d4f60e0c8d21b5ec84fa2f93d11fc3f0f4d53ab3 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Tue, 3 Oct 2017 18:22:04 +0200 Subject: [PATCH] fixing some clang warnings --- Indexing/ResultSubstitution.hpp | 2 +- Indexing/SubstitutionTree.hpp | 3 +-- Inferences/CTFwSubsAndRes.hpp | 4 ++-- Inferences/ForwardDemodulation.hpp | 4 ++-- Inferences/ForwardLiteralRewriting.hpp | 4 ++-- Inferences/ForwardSubsumptionAndResolution.hpp | 4 ++-- Inferences/GlobalSubsumption.hpp | 4 ++-- Inferences/HyperSuperposition.hpp | 4 ++-- Kernel/ELiteralSelector.hpp | 2 +- Kernel/SpassLiteralSelector.hpp | 2 +- Shell/SimplifyProver.cpp | 2 +- 11 files changed, 17 insertions(+), 18 deletions(-) diff --git a/Indexing/ResultSubstitution.hpp b/Indexing/ResultSubstitution.hpp index e1a0590bee..3484953964 100644 --- 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 index d088c590f3..651c393c17 100644 --- 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 _nodeIterators; - bool tag; }; typedef pair,UnificationConstraintStackSP> QueryResult; diff --git a/Inferences/CTFwSubsAndRes.hpp b/Inferences/CTFwSubsAndRes.hpp index 03ac06e73f..f6abbdfccb 100644 --- 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 index c3f5eef1c1..fdc2bd965d 100644 --- 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 index 9e32f842e6..a71378a70c 100644 --- 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 index 43969f1e3a..a74d9ec5ce 100644 --- 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 index e049696527..64fbfed979 100644 --- 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& prems); diff --git a/Inferences/HyperSuperposition.hpp b/Inferences/HyperSuperposition.hpp index d2d7afe877..d6fbb9be1f 100644 --- 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 index afaabb1e9d..8a88966887 100644 --- 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 index bdd1e808a4..edecd4eaff 100644 --- 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 index 7c75c591b2..d05299298c 100644 --- 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) {