new gcc warning hygiene

vprover · Jul 13, 2020 · e2be959 · e2be959
1 parent 7dc86cb
commit e2be959
Show file tree

Hide file tree

Showing 6 changed files with 50 additions and 44 deletions.
diff --git a/Debug/Tracer.hpp b/Debug/Tracer.hpp
@@ -108,7 +108,7 @@ template<class A, class... As> struct _printDbg<A, As...>{
 
 template<class... A> void Tracer::printDbg(A... msg)
 {
-  for (int i = 0; i< _depth; i++) {
+  for (unsigned i = 0; i< _depth; i++) {
     cout << "  ";
   }
   // cout << _lastControlPoint << ": ";

diff --git a/Inferences/BackwardSubsumptionDemodulation.cpp b/Inferences/BackwardSubsumptionDemodulation.cpp
@@ -201,7 +201,7 @@ void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Litera
 #endif
 
   bool mustPredInit = false;
-  bool mustPredActive = false;
+  // bool mustPredActive = false;
   unsigned mustPred;
 
   SLQueryResultIterator rit = _index->getInstances(candidateQueryLit, false, false);
@@ -268,12 +268,14 @@ void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Litera
           mustPred = pred;
         }
       }
+      /*
       if (mustPred == 0) {
         // for positive equality we need to have skipped at least in the remaining literals
         mustPredActive = (numPosEqs >= 2);
       } else {
         mustPredActive = true;
       }
+      */
     }
     bool haveMustPred = false;
     for (unsigned ii = 0; ii < candidate->length(); ++ii) {

diff --git a/Inferences/GaussianVariableElimination.cpp b/Inferences/GaussianVariableElimination.cpp
@@ -18,7 +18,7 @@ Clause* GaussianVariableElimination::simplify(Clause* in)
 
   auto performStep = [&](Clause& cl) -> Clause& {
 
-    for(int i = 0; i < cl.size(); i++) {
+    for(unsigned i = 0; i < cl.size(); i++) {
       auto& lit = *cl[i];
       if (lit.isEquality() && lit.isNegative()) { 
         for (auto b : Balancer(lit)) {
@@ -63,11 +63,11 @@ Clause* GaussianVariableElimination::rewrite(Clause& cl, TermList find, TermList
 
   auto sz = cl.size() - 1;
   Clause& out = *new(sz) Clause(sz, inf); 
-  for (int i = 0; i < skipLiteral; i++) {
+  for (unsigned i = 0; i < skipLiteral; i++) {
     out[i] = EqHelper::replace(cl[i], find, replace);
   }
 
-  for (int i = skipLiteral; i < sz; i++)  {
+  for (unsigned i = skipLiteral; i < sz; i++)  {
     out[i] = EqHelper::replace(cl[i+1], find, replace);
   }
 

diff --git a/Kernel/InterpretedLiteralEvaluator.cpp b/Kernel/InterpretedLiteralEvaluator.cpp
@@ -106,7 +106,7 @@ void stackTraverseIf(TermList term, Predicate pred, Fn action) {
     if(t.isTerm()) {
       auto& trm = *t.term();
       if (pred(trm)) {
-        for (auto i = 0; i < trm.arity(); i++) {
+        for (unsigned i = 0; i < trm.arity(); i++) {
           todo.push(trm[i]);
         }
       } else {
@@ -120,12 +120,12 @@ void stackTraverseIf(TermList term, Predicate pred, Fn action) {
 
 
 /**
- * We want to smplify terms that are interpred by abelian groups. e.g. (1+a)+1 -> 2 + a ... 
+ * We want to simplify terms that are interpreted by abelian groups. e.g. (1+a)+1 -> 2 + a ...
  * the standard evaluation will not do this. 
  *
  * Additionally evaluator has a weekly normalizing behaviour. Namely it re-brackets sums, such that the lhs 
  * of the operation is always a non-operator term. Further all interpreted constants will be collapsed into 
- * the 'left-most' term. The left most term is ommited if it is the identity element.
+ * the 'left-most' term. The left most term is omitted if it is the identity element.
  *
  * x + ( y + ( t + 4 ) + r ) + 5  ==> ( ( (9 + x) + y ) + t ) + r
  * x + ( y + 0 )                  ==> x + y
@@ -1425,38 +1425,40 @@ bool InterpretedLiteralEvaluator::balanceDivide(Interpretation multiply,
     return false;    
 }
 
-// // TODO document me
-// Literal& balance(Literal& in)
-// {
-//   /* we only rebalance equalities */
-//   if (!in.isEquality()) {
-//     return in;
-//
-//   } else {
-//     ASS(in.arity() == 2);
-//     unsigned sort;
-//     if (!SortHelper::tryGetResultSort(in[0], sort) &&
-//         !SortHelper::tryGetResultSort(in[1], sort)) {
-//       return in;
-//     } else {
-//
-//       Literal* out;
-//       switch (sort) {
-// #define _CASE(SRT, ConstantType) \
-//         case Sorts::SRT: \
-//           if (!balance<ConstantType>(in, out)){ \
-//             return in; \
-//           } 
-//         _CASE(SRT_REAL    ,    RealConstantType)
-//         _CASE(SRT_INTEGER , IntegerConstantType)
-//         _CASE(SRT_RATIONAL,RationalConstantType)
-// #undef _CASE
-//         default: return in;
-//       }
-//       return *out;
-//     }
-//   }
-// }
+/*
+ // TODO document me
+ Literal& balance(Literal& in)
+ {
+   // we only rebalance equalities
+   if (!in.isEquality()) {
+     return in;
+
+   } else {
+     ASS(in.arity() == 2);
+     unsigned sort;
+     if (!SortHelper::tryGetResultSort(in[0], sort) &&
+         !SortHelper::tryGetResultSort(in[1], sort)) {
+       return in;
+     } else {
+
+       Literal* out;
+       switch (sort) {
+ #define _CASE(SRT, ConstantType) \
+         case Sorts::SRT: \
+           if (!balance<ConstantType>(in, out)){ \
+             return in; \
+           }
+         _CASE(SRT_REAL    ,    RealConstantType)
+         _CASE(SRT_INTEGER , IntegerConstantType)
+         _CASE(SRT_RATIONAL,RationalConstantType)
+ #undef _CASE
+         default: return in;
+       }
+       return *out;
+     }
+   }
+ }
+*/
 
 class LiteralNormalizer 
 {

diff --git a/Kernel/Rebalancing/Inverters.cpp b/Kernel/Rebalancing/Inverters.cpp
@@ -9,7 +9,7 @@ namespace Inverters {
 #define CASE_INVERT(sort, fun, expr)                                           \
   case NumTraits<sort>::fun##I: {                                             \
     _Pragma("GCC diagnostic push") \
-    _Pragma("GCC diagnostic ignored \"-Wunused-local-typedef\"") \
+    _Pragma("GCC diagnostic ignored \"-Wunused-local-typedefs\"") \
     using number = NumTraits<sort>;                                           \
     _Pragma("GCC diagnostic pop") \
     return expr;                                                               \
@@ -55,7 +55,7 @@ bool NumberTheoryInverter::canInvertTop(const InversionContext &ctxt) {
 #define CASE_DO_INVERT(sort, fun, expr)                                        \
   case NumTraits<sort>::fun##I: {                                             \
     _Pragma("GCC diagnostic push") \
-    _Pragma("GCC diagnostic ignored \"-Wunused-local-typedef\"") \
+    _Pragma("GCC diagnostic ignored \"-Wunused-local-typedefs\"") \
     using number = NumTraits<sort>;                                           \
     return expr;                                                               \
     _Pragma("GCC diagnostic pop") \

diff --git a/Lib/ScopeGuard.hpp b/Lib/ScopeGuard.hpp
@@ -122,8 +122,10 @@ ScopeGuard<Callable> make_scope_guard(Callable&& f)
   auto ON_SCOPE_EXIT_CONCAT(on_scope_exit_guard_on_line_,__LINE__) = make_scope_guard([&]() { stmt; });
 
 // We don't need make_scope_guard in C++14 or later:
-// #define ON_SCOPE_EXIT(stmt) \
-//   ScopeGuard ON_SCOPE_EXIT_CONCAT(on_scope_exit_guard_on_line_,__LINE__){[&]() { stmt; }};
+/*
+#define ON_SCOPE_EXIT(stmt) \
+  ScopeGuard ON_SCOPE_EXIT_CONCAT(on_scope_exit_guard_on_line_,__LINE__){[&]() { stmt; }};
+*/
 
 }