diff --git a/Debug/Tracer.hpp b/Debug/Tracer.hpp index 388e873f78..2a1dc9a77e 100644 --- a/Debug/Tracer.hpp +++ b/Debug/Tracer.hpp @@ -108,7 +108,7 @@ template struct _printDbg{ template 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 index b2d3d2e49d..b978bbad47 100644 --- 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 index 6ec381517b..7a24148959 100644 --- 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 index b49c72c31c..35902f63cf 100644 --- 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(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(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 index 87fae803cc..b491717e5a 100644 --- a/Kernel/Rebalancing/Inverters.cpp +++ b/Kernel/Rebalancing/Inverters.cpp @@ -9,7 +9,7 @@ namespace Inverters { #define CASE_INVERT(sort, fun, expr) \ case NumTraits::fun##I: { \ _Pragma("GCC diagnostic push") \ - _Pragma("GCC diagnostic ignored \"-Wunused-local-typedef\"") \ + _Pragma("GCC diagnostic ignored \"-Wunused-local-typedefs\"") \ using number = NumTraits; \ _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::fun##I: { \ _Pragma("GCC diagnostic push") \ - _Pragma("GCC diagnostic ignored \"-Wunused-local-typedef\"") \ + _Pragma("GCC diagnostic ignored \"-Wunused-local-typedefs\"") \ using number = NumTraits; \ return expr; \ _Pragma("GCC diagnostic pop") \ diff --git a/Lib/ScopeGuard.hpp b/Lib/ScopeGuard.hpp index e63d7fade5..d15cf18723 100644 --- a/Lib/ScopeGuard.hpp +++ b/Lib/ScopeGuard.hpp @@ -122,8 +122,10 @@ ScopeGuard 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; }}; +*/ }