From: Gereon Kremer Date: Thu, 24 Feb 2022 17:44:40 +0000 (+0100) Subject: Get rid of some static objects in arithmetic theory (#8146) X-Git-Tag: cvc5-1.0.0~388 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1f06dc65f3e12a463a9f97f22d0a7097f4b9b3a8;p=cvc5.git Get rid of some static objects in arithmetic theory (#8146) This PR tackles cvc5/cvc5-projects#17 by removing static variables or making them constexpr. Most static variables are either compile-time constants (we make them static constexpr) or used to count how often a function is called for debug output (we remove these). --- diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 5ec46b00c..26f5ed1b4 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -168,8 +168,6 @@ ApproximateStatistics::ApproximateStatistics() { } -Integer ApproximateSimplex::s_defaultMaxDenom(1<<26); - ApproximateSimplex::ApproximateSimplex(const ArithVariables& v, TreeLog& l, ApproximateStatistics& s) : d_vars(v) @@ -195,9 +193,6 @@ void ApproximateSimplex::setBranchOnVariableLimit(int bl){ d_branchLimit = bl; } -const double ApproximateSimplex::SMALL_FIXED_DELTA = .000000001; -const double ApproximateSimplex::TOLERENCE = 1 + .000000001; - bool ApproximateSimplex::roughlyEqual(double a, double b){ if (a == 0){ return -SMALL_FIXED_DELTA <= b && b <= SMALL_FIXED_DELTA; @@ -320,7 +315,7 @@ std::optional ApproximateSimplex::estimateWithCFE(double d, std::optional ApproximateSimplex::estimateWithCFE(double d) { - return estimateWithCFE(d, s_defaultMaxDenom); + return estimateWithCFE(d, Integer(s_defaultMaxDenom)); } class ApproxNoOp : public ApproximateSimplex { @@ -400,8 +395,6 @@ private: //DenseMap d_rowToArithVar; DenseMap d_colToArithVar; - int d_instanceID; - bool d_solvedRelaxation; bool d_solvedMIP; @@ -579,12 +572,9 @@ ApproxGLPK::ApproxGLPK(const ArithVariables& var, d_solvedRelaxation(false), d_solvedMIP(false) { - static int instance = 0; - ++instance; - d_instanceID = instance; d_denomGuesses.push_back(Integer(1<<22)); - d_denomGuesses.push_back(ApproximateSimplex::s_defaultMaxDenom); + d_denomGuesses.push_back(Integer(ApproximateSimplex::s_defaultMaxDenom)); d_denomGuesses.push_back(Integer(1ul<<29)); d_denomGuesses.push_back(Integer(1ul<<31)); @@ -2142,31 +2132,30 @@ bool ApproxGLPK::attemptMir(int nid, const MirInfo& mir){ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound& tmp){ if(ri <= 0) { return true; } - static int instance = 0; - ++instance; - Debug("glpk::loadVB") << "loadVB() " << instance << endl; + Debug("glpk::loadVB") << "loadVB()" << endl; ArithVar rowVar = _getArithVar(nid, M, ri); ArithVar contVar = _getArithVar(nid, M, j); if(rowVar == ARITHVAR_SENTINEL){ - Debug("glpk::loadVB") << "loadVB() " << instance + Debug("glpk::loadVB") << "loadVB()" << " rowVar is ARITHVAR_SENTINEL " << rowVar << endl; return true; } if(contVar == ARITHVAR_SENTINEL){ - Debug("glpk::loadVB") << "loadVB() " << instance - << " contVar is ARITHVAR_SENTINEL " << contVar << endl; + Debug("glpk::loadVB") << "loadVB()" + << " contVar is ARITHVAR_SENTINEL " << contVar + << endl; return true; } if(!d_vars.isAuxiliary(rowVar)){ - Debug("glpk::loadVB") << "loadVB() " << instance - << " rowVar is not auxilliary " << rowVar << endl; + Debug("glpk::loadVB") << "loadVB()" + << " rowVar is not auxilliary " << rowVar << endl; return true; } // is integer is correct here if(d_vars.isInteger(contVar)){ - Debug("glpk::loadVB") << "loadVB() " << instance - << " contVar is integer " << contVar << endl; + Debug("glpk::loadVB") << "loadVB()" + << " contVar is integer " << contVar << endl; return true; } @@ -2174,33 +2163,38 @@ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound ConstraintP ub = d_vars.getUpperBoundConstraint(rowVar); if(lb != NullConstraint && ub != NullConstraint){ - Debug("glpk::loadVB") << "loadVB() " << instance - << " lb and ub are both NULL " << lb << " " << ub << endl; + Debug("glpk::loadVB") << "loadVB()" + << " lb and ub are both NULL " << lb << " " << ub + << endl; return true; } ConstraintP rcon = lb == NullConstraint ? ub : lb; if(rcon == NullConstraint) { - Debug("glpk::loadVB") << "loadVB() " << instance - << " rcon is NULL " << rcon << endl; + Debug("glpk::loadVB") << "loadVB()" + << " rcon is NULL " << rcon << endl; return true; } if(!rcon->getValue().isZero()){ - Debug("glpk::loadVB") << "loadVB() " << instance - << " rcon value is not 0 " << rcon->getValue() << endl; + Debug("glpk::loadVB") << "loadVB()" + << " rcon value is not 0 " << rcon->getValue() + << endl; return true; } if(!d_vars.hasNode(rowVar)){ - Debug("glpk::loadVB") << "loadVB() " << instance + Debug("glpk::loadVB") << "loadVB()" << " does not have node " << rowVar << endl; return true; } Polynomial p = Polynomial::parsePolynomial(d_vars.asNode(rowVar)); - if(p.size() != 2) { - Debug("glpk::loadVB") << "loadVB() " << instance << " polynomial is not binary: " << p.getNode() << endl; + if (p.size() != 2) + { + Debug("glpk::loadVB") << "loadVB()" + << " polynomial is not binary: " << p.getNode() + << endl; return true; } @@ -2211,13 +2205,15 @@ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound Node nx2 = second.getVarList().getNode(); if(!d_vars.hasArithVar(nx1)) { - Debug("glpk::loadVB") << "loadVB() " << instance - << " does not have a variable for nx1: " << nx1 << endl; + Debug("glpk::loadVB") << "loadVB()" + << " does not have a variable for nx1: " << nx1 + << endl; return true; } if(!d_vars.hasArithVar(nx2)) { - Debug("glpk::loadVB") << "loadVB() " << instance - << " does not have a variable for nx2 " << nx2 << endl; + Debug("glpk::loadVB") << "loadVB()" + << " does not have a variable for nx2 " << nx2 + << endl; return true; } ArithVar x1 = d_vars.asArithVar(nx1), x2 = d_vars.asArithVar(nx2); @@ -2246,8 +2242,9 @@ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound << " c2 " << ic << endl; if(!d_vars.isIntegerInput(iv)){ - Debug("glpk::loadVB") << "loadVB() " << instance - << " iv is not an integer input variable " << iv << endl; + Debug("glpk::loadVB") << "loadVB()" + << " iv is not an integer input variable " << iv + << endl; return true; } // cc * cv + ic * iv <= 0 or @@ -2272,16 +2269,18 @@ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound Debug("glpk::loadVB") << d << " " << cc.sgn() << endl; bool nowUb = cc.sgn() < 0; if(wantUb != nowUb) { - Debug("glpk::loadVB") << "loadVB() " << instance - << " wantUb is not nowUb " << wantUb << " " << nowUb << endl; - + Debug("glpk::loadVB") << "loadVB()" + << " wantUb is not nowUb " << wantUb << " " << nowUb + << endl; + return true; } Kind rel = wantUb ? kind::LEQ : kind::GEQ; tmp = VirtualBound(contVar, rel, d, iv, rcon); - Debug("glpk::loadVB") << "loadVB() " << instance << " was successful" << endl; + Debug("glpk::loadVB") << "loadVB()" + << " was successful" << endl; return false; } diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index c0d6990a4..f2a35f823 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -116,8 +116,8 @@ class ApproximateSimplex{ /** UTILITIES FOR DEALING WITH ESTIMATES */ - static const double SMALL_FIXED_DELTA; - static const double TOLERENCE; + static constexpr double SMALL_FIXED_DELTA = .000000001; + static constexpr double TOLERENCE = 1 + .000000001; /** Returns true if two doubles are roughly equal based on TOLERENCE and SMALL_FIXED_DELTA.*/ static bool roughlyEqual(double a, double b); @@ -160,7 +160,7 @@ class ApproximateSimplex{ int d_maxDepth; /* Default denominator for diophatine approximation, 2^{26} .*/ - static Integer s_defaultMaxDenom; + static constexpr uint64_t s_defaultMaxDenom = (1 << 26); };/* class ApproximateSimplex */ } // namespace arith diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index fbd6b33f6..be1c103fa 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -82,15 +82,12 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol) d_errorSet.reduceToSignals(); d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER); - static int instance = 0; - ++instance; - if(processSignals()){ - Debug("arith::findModel") << "attemptSolution("<< instance <<") early conflict" << endl; + Debug("arith::findModel") << "attemptSolution() early conflict" << endl; d_conflictVariables.purge(); return Result::UNSAT; }else if(d_errorSet.errorEmpty()){ - Debug("arith::findModel") << "attemptSolution("<< instance <<") fixed itself" << endl; + Debug("arith::findModel") << "attemptSolution() fixed itself" << endl; return Result::SAT; } diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index e335b2e55..82ee832b7 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -158,15 +158,16 @@ typedef context::CDList CDConstraintList; typedef std::unordered_map NodetoConstraintMap; typedef size_t ConstraintRuleID; -static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits::max(); +static constexpr ConstraintRuleID ConstraintRuleIdSentinel = + std::numeric_limits::max(); typedef size_t AntecedentId; -static const AntecedentId AntecedentIdSentinel = std::numeric_limits::max(); - +static constexpr AntecedentId AntecedentIdSentinel = + std::numeric_limits::max(); typedef size_t AssertionOrder; -static const AssertionOrder AssertionOrderSentinel = std::numeric_limits::max(); - +static constexpr AssertionOrder AssertionOrderSentinel = + std::numeric_limits::max(); /** * A ValueCollection binds together convex constraints that have the same diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h index 5f0e124fb..e9a64ce19 100644 --- a/src/theory/arith/constraint_forward.h +++ b/src/theory/arith/constraint_forward.h @@ -34,7 +34,7 @@ class Constraint; typedef Constraint* ConstraintP; typedef const Constraint* ConstraintCP; -static const ConstraintP NullConstraint = NULL; +static constexpr ConstraintP NullConstraint = nullptr; class ConstraintDatabase; @@ -43,8 +43,8 @@ typedef std::vector ConstraintCPVec; typedef std::vector RationalVector; typedef RationalVector* RationalVectorP; typedef const RationalVector* RationalVectorCP; -static const RationalVectorCP RationalVectorCPSentinel = NULL; -static const RationalVectorP RationalVectorPSentinel = NULL; +static constexpr RationalVectorCP RationalVectorCPSentinel = nullptr; +static constexpr RationalVectorP RationalVectorPSentinel = nullptr; } // namespace arith } // namespace theory diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 054fceb46..2e99f04e4 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -157,7 +157,7 @@ class DioSolver : protected EnvObj * the maximum input constraints length than 2**MAX_GROWTH_RATE. */ context::CDO d_maxInputCoefficientLength; - static const uint32_t MAX_GROWTH_RATE = 3; + static constexpr uint32_t MAX_GROWTH_RATE = 3; /** Returns true if the element on the trail should be dropped.*/ bool anyCoefficientExceedsMaximum(TrailIndex j) const; diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 147d0a1ff..84cd0fe5a 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -61,12 +61,10 @@ DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots) Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ Assert(d_conflictVariables.empty()); - static thread_local unsigned int instance = 0; - instance = instance + 1; d_pivots = 0; if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){ - Debug("arith::findModel") << "dualFindModel("<< instance <<") trivial" << endl; + Debug("arith::findModel") << "dualFindModel() trivial" << endl; return Result::SAT; } @@ -77,15 +75,15 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ if(processSignals()){ d_conflictVariables.purge(); - Debug("arith::findModel") << "dualFindModel("<< instance <<") early conflict" << endl; + Debug("arith::findModel") << "dualFindModel() early conflict" << endl; return Result::UNSAT; }else if(d_errorSet.errorEmpty()){ - Debug("arith::findModel") << "dualFindModel("<< instance <<") fixed itself" << endl; + Debug("arith::findModel") << "dualFindModel() fixed itself" << endl; Assert(!d_errorSet.moreSignals()); return Result::SAT; } - Debug("arith::findModel") << "dualFindModel(" << instance <<") start non-trivial" << endl; + Debug("arith::findModel") << "dualFindModel() start non-trivial" << endl; Result::Sat result = Result::SAT_UNKNOWN; @@ -136,7 +134,7 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ // ensure that the conflict variable is still in the queue. d_conflictVariables.purge(); - Debug("arith::findModel") << "end findModel() " << instance << " " << result << endl; + Debug("arith::findModel") << "end findModel() " << result << endl; return result; } diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp index 19d6149f5..c7666fff3 100644 --- a/src/theory/arith/error_set.cpp +++ b/src/theory/arith/error_set.cpp @@ -446,9 +446,7 @@ DeltaRational ErrorSet::computeDiff(ArithVar v) const{ } void ErrorSet::debugPrint(std::ostream& out) const { - static int instance = 0; - ++instance; - out << "error set debugprint " << instance << endl; + out << "error set debugprint" << endl; for(error_iterator i = errorBegin(), i_end = errorEnd(); i != i_end; ++i){ ArithVar e = *i; diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 5b9f37f93..d3f7e071f 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -72,11 +72,9 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ Assert(d_sgnDisagreements.empty()); d_pivots = 0; - static thread_local unsigned int instance = 0; - instance = instance + 1; if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){ - Debug("arith::findModel") << "fcFindModel("<< instance <<") trivial" << endl; + Debug("arith::findModel") << "fcFindModel() trivial" << endl; Assert(d_conflictVariables.empty()); return Result::SAT; } @@ -89,16 +87,16 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ if(initialProcessSignals()){ d_conflictVariables.purge(); - Debug("arith::findModel") << "fcFindModel("<< instance <<") early conflict" << endl; + Debug("arith::findModel") << "fcFindModel() early conflict" << endl; Assert(d_conflictVariables.empty()); return Result::UNSAT; }else if(d_errorSet.errorEmpty()){ - Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl; + Debug("arith::findModel") << "fcFindModel() fixed itself" << endl; Assert(d_conflictVariables.empty()); return Result::SAT; } - Debug("arith::findModel") << "fcFindModel(" << instance <<") start non-trivial" << endl; + Debug("arith::findModel") << "fcFindModel() start non-trivial" << endl; exactResult |= d_varOrderPivotLimit < 0; @@ -133,7 +131,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ // ensure that the conflict variable is still in the queue. d_conflictVariables.purge(); - Debug("arith::findModel") << "end findModel() " << instance << " " << result << endl; + Debug("arith::findModel") << "end findModel() " << result << endl; Assert(d_conflictVariables.empty()); return result; @@ -251,15 +249,12 @@ WitnessImprovement FCSimplexDecisionProcedure::focusDownToJust(ArithVar v){ UpdateInfo FCSimplexDecisionProcedure::selectPrimalUpdate(ArithVar basic, LinearEqualityModule::UpdatePreferenceFunction upf, LinearEqualityModule::VarPreferenceFunction bpf) { UpdateInfo selected; - static int instance = 0 ; - ++instance; - Debug("arith::selectPrimalUpdate") - << "selectPrimalUpdate " << instance << endl - << basic << " " << d_tableau.basicRowLength(basic) - << " " << d_linEq.debugBasicAtBoundCount(basic) << endl; + << "selectPrimalUpdate" << endl + << basic << " " << d_tableau.basicRowLength(basic) << " " + << d_linEq.debugBasicAtBoundCount(basic) << endl; - static const int s_maxCandidatesAfterImprove = 3; + static constexpr int s_maxCandidatesAfterImprove = 3; bool isFocus = basic == d_focusErrorVar; Assert(isFocus || d_errorSet.inError(basic)); int basicDir = isFocus? 1 : d_errorSet.getSgn(basic); @@ -629,8 +624,12 @@ WitnessImprovement FCSimplexDecisionProcedure::selectFocusImproving() { return w; } -bool FCSimplexDecisionProcedure::debugDualLike(WitnessImprovement w, ostream& out, int instance, uint32_t prevFocusSize, uint32_t prevErrorSize ) const{ - out << "DLV("< 0 && d_conflictVariables.empty()){ - ++instance; - Debug("dualLike") << "dualLike " << instance << endl; + Debug("dualLike") << "dualLike " << endl; Assert(d_errorSet.noSignals()); @@ -723,7 +720,7 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){ // - focus went down Assert(d_focusSize > 1); ArithVar e = d_errorSet.topFocusVariable(); - static const unsigned s_sumMetricThreshold = 1; + static constexpr unsigned s_sumMetricThreshold = 1; if(d_errorSet.sumMetric(e) <= s_sumMetricThreshold){ Debug("dualLike") << "dualLikeImproveError " << e << endl; w = dualLikeImproveError(e); @@ -736,8 +733,7 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){ Assert(d_focusSize == d_errorSet.focusSize()); Assert(d_errorSize == d_errorSet.errorSize()); - Assert(debugDualLike( - w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize)); + Assert(debugDualLike(w, Debug("dualLike"), prevFocusSize, prevErrorSize)); Debug("dualLike") << "Focus size " << d_focusSize << " (was " << prevFocusSize << ")" << endl; Debug("dualLike") << "Error size " << d_errorSize << " (was " << prevErrorSize << ")" << endl; } diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index ddd868aca..f3dbccc6e 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -86,19 +86,24 @@ public: Result::Sat dualLike(); private: - static const uint32_t PENALTY = 4; - DenseMultiset d_scores; - void decreasePenalties(){ d_scores.removeOneOfEverything(); } - uint32_t penalty(ArithVar x) const { return d_scores.count(x); } - void setPenalty(ArithVar x, WitnessImprovement w){ - if(improvement(w)){ - if(d_scores.count(x) > 0){ - d_scores.removeAll(x); - } - }else{ - d_scores.setCount(x, PENALTY); - } - } + static constexpr uint32_t PENALTY = 4; + DenseMultiset d_scores; + void decreasePenalties() { d_scores.removeOneOfEverything(); } + uint32_t penalty(ArithVar x) const { return d_scores.count(x); } + void setPenalty(ArithVar x, WitnessImprovement w) + { + if (improvement(w)) + { + if (d_scores.count(x) > 0) + { + d_scores.removeAll(x); + } + } + else + { + d_scores.setCount(x, PENALTY); + } + } /** The size of the focus set. */ uint32_t d_focusSize; @@ -128,21 +133,15 @@ private: const Rational& focusCoefficient(ArithVar nb) const; int32_t d_pivotBudget; - // enum PivotImprovement { - // ErrorDropped, - // NonDegenerate, - // HeuristicDegenerate, - // BlandsDegenerate - // }; WitnessImprovement d_prevWitnessImprovement; uint32_t d_witnessImprovementInARow; uint32_t degeneratePivotsInARow() const; - static const uint32_t s_focusThreshold = 6; - static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100; - static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10; + static constexpr uint32_t s_focusThreshold = 6; + static constexpr uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100; + static constexpr uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10; DenseMap d_leavingCountSinceImprovement; void increaseLeavingCount(ArithVar x){ @@ -163,15 +162,12 @@ private: } bool debugDualLike(WitnessImprovement w, std::ostream& out, - int instance, uint32_t prevFocusSize, uint32_t prevErrorSize) const; void debugPrintSignal(ArithVar updated) const; ArithVarVec d_sgnDisagreements; - //static PivotImprovement pivotImprovement(const UpdateInfo& selected, bool useBlands = false); - void logPivot(WitnessImprovement w); void updateAndSignal(const UpdateInfo& selected, WitnessImprovement w); diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index a0cc5499d..bc4f11e9d 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -261,11 +261,8 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const Delt TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime); - static int instance = 0; - if(Debug.isOn("arith::tracking::pre")){ - ++instance; - Debug("arith::tracking") << "pre update #" << instance << endl; + Debug("arith::tracking") << "pre update" << endl; debugCheckTracking(); } @@ -283,7 +280,7 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const Delt updateTracked(x_j, x_j_value); if(Debug.isOn("arith::tracking::mid")){ - Debug("arith::tracking") << "postupdate prepivot #" << instance << endl; + Debug("arith::tracking") << "postupdate prepivot" << endl; debugCheckTracking(); } @@ -293,7 +290,7 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const Delt d_tableau.pivot(x_i, x_j, d_trackCallback); if(Debug.isOn("arith::tracking::post")){ - Debug("arith::tracking") << "postpivot #" << instance << endl; + Debug("arith::tracking") << "postpivot" << endl; debugCheckTracking(); } @@ -1118,9 +1115,7 @@ UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational& int focusCoeffSgn = focusCoeff.sgn(); - static int instance = 0; - ++instance; - Debug("speculativeUpdate") << "speculativeUpdate " << instance << endl; + Debug("speculativeUpdate") << "speculativeUpdate" << endl; Debug("speculativeUpdate") << "nb " << nb << endl; Debug("speculativeUpdate") << "focusCoeff " << focusCoeff << endl; diff --git a/src/theory/arith/nl/cad/lazard_evaluation.cpp b/src/theory/arith/nl/cad/lazard_evaluation.cpp index 032565d3d..91d775d16 100644 --- a/src/theory/arith/nl/cad/lazard_evaluation.cpp +++ b/src/theory/arith/nl/cad/lazard_evaluation.cpp @@ -106,7 +106,15 @@ std::ostream& operator<<(std::ostream& os, const LazardEvaluationState& state); struct LazardEvaluationState { CoCoA::GlobalManager d_gm; - static std::unique_ptr d_stats; + + /** + * Statistics about the lazard evaluation. + * Although this class is short-lived, there is no need to make the statistics + * static or store them persistently: this is handled by the statistics + * registry, which recovers statistics from their name. + * This member is mutable to allow collecting statistics from const methods. + */ + mutable LazardEvaluationStats d_stats; /** * Maps libpoly variables to indets in J0. Used when constructing the input @@ -185,14 +193,6 @@ struct LazardEvaluationState */ std::vector> d_direct; - LazardEvaluationState() - { - if (!d_stats) - { - d_stats = std::make_unique(); - } - } - /** * Converts a libpoly integer to a CoCoA::BigInt. */ @@ -595,7 +595,7 @@ struct LazardEvaluationState */ std::vector reduce(const poly::Polynomial& qpoly) const { - d_stats->d_evaluations++; + d_stats.d_evaluations++; std::vector res; Trace("cad::lazard") << "Reducing " << qpoly << std::endl; auto input = convertQ(qpoly); @@ -621,7 +621,7 @@ struct LazardEvaluationState while (CoCoA::IsZero(hom(q))) { q = q / (var - indets[0]); - d_stats->d_reductions++; + d_stats.d_reductions++; } // substitute x_i -> a_i q = hom(q); @@ -634,7 +634,7 @@ struct LazardEvaluationState while (CoCoA::IsDivisible(q, tmp)) { q /= tmp; - d_stats->d_reductions++; + d_stats.d_reductions++; } } q = d_qhom[i](q); @@ -682,7 +682,6 @@ std::ostream& operator<<(std::ostream& os, const LazardEvaluationState& state) os << "Done" << std::endl; return os; } -std::unique_ptr LazardEvaluationState::d_stats; LazardEvaluation::LazardEvaluation() : d_state(std::make_unique()) @@ -747,7 +746,7 @@ void LazardEvaluation::add(const poly::Variable& var, const poly::Value& val) { d_state->addKRational(var, CoCoA::RingElem(d_state->d_K.back(), *rational)); - d_state->d_stats->d_directAssignments++; + d_state->d_stats.d_directAssignments++; return; } Trace("cad::lazard") << "Got mipo " << polymipo << std::endl; @@ -768,13 +767,13 @@ void LazardEvaluation::add(const poly::Variable& var, const poly::Value& val) Trace("cad::lazard") << "Using linear factor " << f << " -> " << var << " = " << rat << std::endl; d_state->addKRational(var, rat); - d_state->d_stats->d_directAssignments++; + d_state->d_stats.d_directAssignments++; } else { Trace("cad::lazard") << "Using nonlinear factor " << f << std::endl; d_state->addK(var, f); - d_state->d_stats->d_ranAssignments++; + d_state->d_stats.d_ranAssignments++; } used_factor = true; break; diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 5a834ad42..e8afb6413 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -78,11 +78,9 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ Assert(d_sgnDisagreements.empty()); d_pivots = 0; - static thread_local unsigned int instance = 0; - instance = instance + 1; if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){ - Debug("soi::findModel") << "soiFindModel("<< instance <<") trivial" << endl; + Debug("soi::findModel") << "soiFindModel() trivial" << endl; Assert(d_conflictVariables.empty()); return Result::SAT; } @@ -95,17 +93,17 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ if(initialProcessSignals()){ d_conflictVariables.purge(); - Debug("soi::findModel") << "fcFindModel("<< instance <<") early conflict" << endl; + Debug("soi::findModel") << "fcFindModel() early conflict" << endl; Assert(d_conflictVariables.empty()); return Result::UNSAT; }else if(d_errorSet.errorEmpty()){ - Debug("soi::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl; + Debug("soi::findModel") << "fcFindModel() fixed itself" << endl; Assert(!d_errorSet.moreSignals()); Assert(d_conflictVariables.empty()); return Result::SAT; } - Debug("soi::findModel") << "fcFindModel(" << instance <<") start non-trivial" << endl; + Debug("soi::findModel") << "fcFindModel() start non-trivial" << endl; exactResult |= d_varOrderPivotLimit < 0; @@ -140,7 +138,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ // ensure that the conflict variable is still in the queue. d_conflictVariables.purge(); - Debug("soi::findModel") << "end findModel() " << instance << " " << result << endl; + Debug("soi::findModel") << "end findModel() " << result << endl; Assert(d_conflictVariables.empty()); return result; @@ -200,13 +198,10 @@ void SumOfInfeasibilitiesSPD::adjustFocusAndError(const UpdateInfo& up, const AV UpdateInfo SumOfInfeasibilitiesSPD::selectUpdate(LinearEqualityModule::UpdatePreferenceFunction upf, LinearEqualityModule::VarPreferenceFunction bpf) { UpdateInfo selected; - static int instance = 0 ; - ++instance; - Debug("soi::selectPrimalUpdate") - << "selectPrimalUpdate " << instance << endl - << d_soiVar << " " << d_tableau.basicRowLength(d_soiVar) - << " " << d_linEq.debugBasicAtBoundCount(d_soiVar) << endl; + << "selectPrimalUpdate " << endl + << d_soiVar << " " << d_tableau.basicRowLength(d_soiVar) << " " + << d_linEq.debugBasicAtBoundCount(d_soiVar) << endl; typedef std::vector CandVector; CandVector candidates; @@ -786,11 +781,8 @@ bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){ - static int instance = 0; - instance++; - Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() start " - << instance << ": |E| = " << d_errorSize << endl; + << ": |E| = " << d_errorSize << endl; if(Debug.isOn("arith::SOIConflict")){ d_errorSet.debugPrint(cout); } @@ -828,8 +820,8 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){ //reportConflict(conf); do not do this. We need a custom explanations! d_conflictVariables.add(d_soiVar); - Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() done " - << instance << "end" << endl; + Debug("arith::SOIConflict") + << "SumOfInfeasibilitiesSPD::SOIConflict() end" << endl; return ConflictFound; } @@ -865,39 +857,7 @@ WitnessImprovement SumOfInfeasibilitiesSPD::soiRound() { } } -bool SumOfInfeasibilitiesSPD::debugSOI(WitnessImprovement w, ostream& out, int instance) const{ - return true; - // out << "DLV("< 0 && d_conflictVariables.empty()){ - ++instance; - Debug("dualLike") << "dualLike " << instance << endl; + Debug("dualLike") << "dualLike" << endl; Assert(d_errorSet.noSignals()); // Possible outcomes: @@ -924,8 +883,6 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){ Debug("dualLike") << "selectFocusImproving -> " << w << endl; Assert(d_errorSize == d_errorSet.errorSize()); - - Assert(debugSOI(w, Debug("dualLike"), instance)); } diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index 71b0b36d8..96e1de531 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -88,36 +88,16 @@ private: // - satisfied error set Result::Sat sumOfInfeasibilities(); - // static const uint32_t PENALTY = 4; - // DenseMultiset d_scores; - // void decreasePenalties(){ d_scores.removeOneOfEverything(); } - // uint32_t penalty(ArithVar x) const { return d_scores.count(x); } - // void setPenalty(ArithVar x, WitnessImprovement w){ - // if(improvement(w)){ - // if(d_scores.count(x) > 0){ - // d_scores.removeAll(x); - // } - // }else{ - // d_scores.setCount(x, PENALTY); - // } - // } - int32_t d_pivotBudget; - // enum PivotImprovement { - // ErrorDropped, - // NonDegenerate, - // HeuristicDegenerate, - // BlandsDegenerate - // }; WitnessImprovement d_prevWitnessImprovement; uint32_t d_witnessImprovementInARow; uint32_t degeneratePivotsInARow() const; - static const uint32_t s_focusThreshold = 6; - static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100; - static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10; + static constexpr uint32_t s_focusThreshold = 6; + static constexpr uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100; + static constexpr uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10; DenseMap d_leavingCountSinceImprovement; void increaseLeavingCount(ArithVar x){ @@ -137,8 +117,6 @@ private: } } - bool debugSOI(WitnessImprovement w, std::ostream& out, int instance) const; - void debugPrintSignal(ArithVar updated) const; ArithVarVec d_sgnDisagreements; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index c540aa384..ac7acb4be 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1712,7 +1712,6 @@ Node flattenAndSort(Node n){ void TheoryArithPrivate::outputConflicts(){ Debug("arith::conflict") << "outputting conflicts" << std::endl; Assert(anyConflict()); - static unsigned int conflicts = 0; if(!conflictQueueEmpty()){ Assert(!d_conflicts.empty()); @@ -1737,7 +1736,6 @@ void TheoryArithPrivate::outputConflicts(){ TrustNode trustedConflict = confConstraint->externalExplainConflict(); Node conflict = trustedConflict.getNode(); - ++conflicts; Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict << " has proof: " << hasProof << ", id = " << conf.second << endl; @@ -1758,9 +1756,7 @@ void TheoryArithPrivate::outputConflicts(){ } if(!d_blackBoxConflict.get().isNull()){ Node bb = d_blackBoxConflict.get(); - ++conflicts; Debug("arith::conflict") << "black box conflict" << bb - //<< "("<getLevel(); d_lastContextIntegerAttempted = level; - - static const int32_t mipLimit = 200000; + static constexpr int32_t mipLimit = 200000; TreeLog& tl = getTreeLog(); ApproximateStatistics& stats = getApproxStats(); @@ -2718,7 +2713,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ if(!d_guessedCoeffs.empty()){ approx->setOptCoeffs(d_guessedCoeffs); } - static const int32_t depthForLikelyInfeasible = 10; + static constexpr int32_t depthForLikelyInfeasible = 10; int maxDepthPass1 = d_likelyIntegerInfeasible ? depthForLikelyInfeasible : options().arith.maxApproxDepth; @@ -2873,7 +2868,7 @@ void TheoryArithPrivate::importSolution(const ApproximateSimplex::Solution& solu } if(d_qflraStatus != Result::UNSAT){ - static const int64_t pass2Limit = 20; + static constexpr int64_t pass2Limit = 20; SimplexDecisionProcedure& simplex = selectSimplex(false); simplex.setVarOrderPivotLimit(pass2Limit); d_qflraStatus = simplex.findModel(false); @@ -2945,7 +2940,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ if(d_qflraStatus == Result::SAT_UNKNOWN && useApprox && safeToCallApprox()){ // pass2: fancy-final - static const int32_t relaxationLimit = 10000; + static constexpr int32_t relaxationLimit = 10000; Assert(ApproximateSimplex::enabled()); TreeLog& tl = getTreeLog(); @@ -4004,10 +3999,8 @@ void TheoryArithPrivate::presolve(){ if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } - static thread_local unsigned callCount = 0; if(Debug.isOn("arith::presolve")) { - Debug("arith::presolve") << "TheoryArithPrivate::presolve #" << callCount << endl; - callCount = callCount + 1; + Debug("arith::presolve") << "TheoryArithPrivate::presolve" << endl; } vector lemmas; @@ -4520,11 +4513,9 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){ uint32_t rowLength = d_tableau.getRowLength(ridx); bool success = false; - static int instance = 0; - ++instance; - Debug("arith::prop") - << "propagateCandidateRow " << instance << " attempt " << rowLength << " " << hasCount << endl; + Debug("arith::prop") << "propagateCandidateRow attempt " << rowLength << " " + << hasCount << endl; if (rowLength >= options().arith.arithPropagateMaxLength && Random::getRandom().pickWithProb( diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 7c90352d2..c10a4ad84 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -85,7 +85,7 @@ class InferBoundsResult; class TheoryArithPrivate : protected EnvObj { private: - static const uint32_t RESET_START = 2; + static constexpr uint32_t RESET_START = 2; TheoryArith& d_containing; @@ -316,8 +316,7 @@ private: bool d_tableauSizeHasBeenModified; double d_tableauResetDensity; uint32_t d_tableauResetPeriod; - static const uint32_t s_TABLEAU_RESET_INCREMENT = 5; - + static constexpr uint32_t s_TABLEAU_RESET_INCREMENT = 5; /** This is only used by simplex at the moment. */ context::CDList> d_conflicts;