From: Gereon Kremer Date: Fri, 5 Nov 2021 00:42:06 +0000 (-0700) Subject: Remove a bunch of debugging/logging code from the linear solver (#7576) X-Git-Tag: cvc5-1.0.0~886 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6d947b4f85d005681ff438c6bd8ef7bba557be10;p=cvc5.git Remove a bunch of debugging/logging code from the linear solver (#7576) This PR removes old debugging code from the linear solver. The removed code was either redundant, already in comments, or manually disabled by a constant false. --- diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 89d7619cf..fdcfb063b 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -405,8 +405,6 @@ private: bool d_solvedRelaxation; bool d_solvedMIP; - static int s_verbosity; - CutScratchPad d_pad; std::vector d_denomGuesses; @@ -524,8 +522,6 @@ private: double sumInfeasibilities(glp_prob* prob, bool mip) const; }; -int ApproxGLPK::s_verbosity = 0; - } // namespace arith } // namespace theory } // namespace cvc5 @@ -629,12 +625,6 @@ ApproxGLPK::ApproxGLPK(const ArithVariables& var, for(ArithVariables::var_iterator vi = d_vars.var_begin(), vi_end = d_vars.var_end(); vi != vi_end; ++vi){ ArithVar v = *vi; - if (s_verbosity >= 2) - { - // CVC5Message() << v << " "; - // d_vars.printModel(v, CVC5Message()); - } - int type; double lb = 0.0; double ub = 0.0; @@ -764,12 +754,6 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{ for(ArithVariables::var_iterator vi = d_vars.var_begin(), vi_end = d_vars.var_end(); vi != vi_end; ++vi){ ArithVar v = *vi; - if (s_verbosity >= 2) - { - CVC5Message() << v << " "; - d_vars.printModel(v, CVC5Message()); - } - int type; if(d_vars.hasUpperBound(v) && d_vars.hasLowerBound(v)){ if(d_vars.boundsAreEqual(v)){ @@ -868,12 +852,6 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{ int dir = guessDir(r); if(len >= rowLengthReq){ - if (s_verbosity >= 1) - { - CVC5Message() << "high row " << r << " " << len << " " << avgRowLength - << " " << dir << endl; - d_vars.printModel(r, CVC5Message()); - } ret.push_back(ArithRatPair(r, Rational(dir))); } } @@ -891,12 +869,6 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{ double ubScore = double(bc.upperBoundCount()) / maxCount; double lbScore = double(bc.lowerBoundCount()) / maxCount; if(ubScore >= .9 || lbScore >= .9){ - if (s_verbosity >= 1) - { - CVC5Message() << "high col " << c << " " << bc << " " << ubScore - << " " << lbScore << " " << dir << endl; - d_vars.printModel(c, CVC5Message()); - } ret.push_back(ArithRatPair(c, Rational(c))); } } @@ -1016,26 +988,17 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const int status = isAux ? glp_get_row_stat(prob, glpk_index) : glp_get_col_stat(prob, glpk_index); - if (s_verbosity >= 2) - { - CVC5Message() << "assignment " << vi << endl; - } bool useDefaultAssignment = false; switch(status){ case GLP_BS: - // CVC5Message() << "basic" << endl; newBasis.add(vi); useDefaultAssignment = true; break; case GLP_NL: case GLP_NS: if(!mip){ - if (s_verbosity >= 2) - { - CVC5Message() << "non-basic lb" << endl; - } newValues.set(vi, d_vars.getLowerBound(vi)); }else{// intentionally fall through otherwise useDefaultAssignment = true; @@ -1043,10 +1006,6 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const break; case GLP_NU: if(!mip){ - if (s_verbosity >= 2) - { - CVC5Message() << "non-basic ub" << endl; - } newValues.set(vi, d_vars.getUpperBound(vi)); }else {// intentionally fall through otherwise useDefaultAssignment = true; @@ -1060,10 +1019,6 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const } if(useDefaultAssignment){ - if (s_verbosity >= 2) - { - CVC5Message() << "non-basic other" << endl; - } double newAssign; if(mip){ @@ -1079,7 +1034,6 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const && roughlyEqual(newAssign, d_vars.getLowerBound(vi).approx(SMALL_FIXED_DELTA))) { - // CVC5Message() << " to lb" << endl; newValues.set(vi, d_vars.getLowerBound(vi)); } @@ -1089,22 +1043,14 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const d_vars.getUpperBound(vi).approx(SMALL_FIXED_DELTA))) { newValues.set(vi, d_vars.getUpperBound(vi)); - // CVC5Message() << " to ub" << endl; } else { double rounded = round(newAssign); if (roughlyEqual(newAssign, rounded)) { - // CVC5Message() << "roughly equal " << rounded << " " << newAssign << - // " " << oldAssign << endl; newAssign = rounded; } - else - { - // CVC5Message() << "not roughly equal " << rounded << " " << - // newAssign << " " << oldAssign << endl; - } DeltaRational proposal; if (std::optional maybe_new = estimateWithCFE(newAssign)) @@ -1119,28 +1065,17 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const if (roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA))) { - // CVC5Message() << " to prev value" << newAssign << " " << oldAssign - // << endl; proposal = d_vars.getAssignment(vi); } if (d_vars.strictlyLessThanLowerBound(vi, proposal)) { - // CVC5Message() << " round to lb " << d_vars.getLowerBound(vi) << - // endl; proposal = d_vars.getLowerBound(vi); } else if (d_vars.strictlyGreaterThanUpperBound(vi, proposal)) { - // CVC5Message() << " round to ub " << d_vars.getUpperBound(vi) << - // endl; proposal = d_vars.getUpperBound(vi); } - else - { - // CVC5Message() << " use proposal" << proposal << " " << oldAssign - // << endl; - } newValues.set(vi, proposal); } } @@ -1202,9 +1137,6 @@ LinResult ApproxGLPK::solveRelaxation(){ parm.pricing = GLP_PT_PSE; parm.it_lim = d_pivotLimit; parm.msg_lev = GLP_MSG_OFF; - if(s_verbosity >= 1){ - parm.msg_lev = GLP_MSG_ALL; - } glp_erase_prob(d_realProb); glp_copy_prob(d_realProb, d_inputProb, GLP_OFF); @@ -1735,9 +1667,6 @@ MipResult ApproxGLPK::solveMIP(bool activelyLog){ parm.cb_func = glpkCallback; parm.cb_info = &aux; parm.msg_lev = GLP_MSG_OFF; - if(s_verbosity >= 1){ - parm.msg_lev = GLP_MSG_ALL; - } glp_erase_prob(d_mipProb); glp_copy_prob(d_mipProb, d_realProb, GLP_OFF); diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index 11a9cc6f2..fbd6b33f6 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -124,12 +124,10 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol) Assert(toAdd != ARITHVAR_SENTINEL); Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl; - // CVC5Message() << toRemove << " " << toAdd << endl; d_linEq.pivotAndUpdate(toRemove, toAdd, newValues[toRemove]); Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl; - // CVC5Message() << needsToBeAdded.size() << "to go" << endl; needsToBeAdded.remove(toAdd); bool conflict = processSignals(); diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index defcc8aff..2958b5f48 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -222,8 +222,6 @@ std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v){ return o; } -void Constraint::debugPrint() const { CVC5Message() << *this << endl; } - ValueCollection::ValueCollection() : d_lowerBound(NullConstraint), d_upperBound(NullConstraint), @@ -699,8 +697,6 @@ bool Constraint::sanityChecking(Node n) const { } } -void ConstraintRule::debugPrint() const { print(std::cerr, false); } - ConstraintCP ConstraintDatabase::getAntecedent (AntecedentId p) const { Assert(p < d_antecedents.size()); return d_antecedents[p]; diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 1262181db..e335b2e55 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -322,7 +322,6 @@ struct ConstraintRule { RationalVectorCP coeffs); void print(std::ostream& out, bool produceProofs) const; - void debugPrint() const; }; /* class ConstraintRule */ class Constraint { @@ -882,8 +881,6 @@ class Constraint { return d_produceProofs ? getConstraintRule().d_farkasCoefficients : nullptr; } - void debugPrint() const; - /** * The proof of the node is empty. * The proof must be a special proof. Either diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 08e9edc79..99dcc93ca 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -74,7 +74,6 @@ DioSolver::Statistics::Statistics() } bool DioSolver::queueConditions(TrailIndex t){ - /* debugPrintTrail(t); */ Debug("queueConditions") << !inConflict() << std::endl; Debug("queueConditions") << gcdIsOne(t) << std::endl; Debug("queueConditions") << !debugAnySubstitionApplies(t) << std::endl; @@ -228,8 +227,13 @@ bool DioSolver::anyCoefficientExceedsMaximum(TrailIndex j) const{ nmonos >= 2 && length > d_maxInputCoefficientLength + MAX_GROWTH_RATE; if(Debug.isOn("arith::dio::max") && result){ - Debug("arith::dio::max") << "about to drop:"; - debugPrintTrail(j); + + const SumPair& eq = d_trail[j].d_eq; + const Polynomial& proof = d_trail[j].d_proof; + + Debug("arith::dio::max") << "about to drop:" << std::endl; + Debug("arith::dio::max") << "d_trail[" << j << "].d_eq = " << eq.getNode() << std::endl; + Debug("arith::dio::max") << "d_trail[" << j << "].d_proof = " << proof.getNode() << std::endl; } return result; } @@ -776,14 +780,6 @@ bool DioSolver::gcdIsOne(DioSolver::TrailIndex i){ return eq.gcd() == Integer(1); } -void DioSolver::debugPrintTrail(DioSolver::TrailIndex i) const{ - const SumPair& eq = d_trail[i].d_eq; - const Polynomial& proof = d_trail[i].d_proof; - - CVC5Message() << "d_trail[" << i << "].d_eq = " << eq.getNode() << endl; - CVC5Message() << "d_trail[" << i << "].d_proof = " << proof.getNode() << endl; -} - void DioSolver::subAndReduceCurrentFByIndex(DioSolver::SubIndex subIndex){ size_t N = d_currentF.size(); diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 6be26e854..054fceb46 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -383,9 +383,6 @@ private: */ SumPair purifyIndex(TrailIndex i); - - void debugPrintTrail(TrailIndex i) const; - public: bool hasMoreDecompositionLemmas() const{ return !d_decompositionLemmaQueue.empty(); diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index ea7773f76..147d0a1ff 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -89,7 +89,6 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ Result::Sat result = Result::SAT_UNKNOWN; - static const bool verbose = false; exactResult |= d_varOrderPivotLimit < 0; uint32_t checkPeriod = options().arith.arithSimplexCheckPeriod; @@ -105,22 +104,6 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ result = Result::UNSAT; } } - - if (verbose && numDifferencePivots > 0) - { - if (result == Result::UNSAT) - { - CVC5Message() << "diff order found unsat" << endl; - } - else if (d_errorSet.errorEmpty()) - { - CVC5Message() << "diff order found model" << endl; - } - else - { - CVC5Message() << "diff order missed" << endl; - } - } } Assert(!d_errorSet.moreSignals()); @@ -141,21 +124,6 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ { result = Result::UNSAT; } - if (verbose) - { - if (result == Result::UNSAT) - { - CVC5Message() << "restricted var order found unsat" << endl; - } - else if (d_errorSet.errorEmpty()) - { - CVC5Message() << "restricted var order found model" << endl; - } - else - { - CVC5Message() << "restricted var order missed" << endl; - } - } } } diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 54d19000b..5b9f37f93 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -74,15 +74,10 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ d_pivots = 0; static thread_local unsigned int instance = 0; instance = instance + 1; - static const bool verbose = false; if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){ Debug("arith::findModel") << "fcFindModel("<< instance <<") trivial" << endl; Assert(d_conflictVariables.empty()); - // if (verbose) - //{ - // CVC5Message() << "fcFindModel(" << instance << ") trivial" << endl; - //} return Result::SAT; } @@ -94,20 +89,11 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ if(initialProcessSignals()){ d_conflictVariables.purge(); - if (verbose) - { - CVC5Message() << "fcFindModel(" << instance << ") early conflict" << endl; - } Debug("arith::findModel") << "fcFindModel("<< instance <<") early conflict" << endl; Assert(d_conflictVariables.empty()); return Result::UNSAT; }else if(d_errorSet.errorEmpty()){ - // if (verbose) - //{ - // CVC5Message() << "fcFindModel(" << instance << ") fixed itself" << endl; - //} Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl; - if (verbose) Assert(!d_errorSet.moreSignals()); Assert(d_conflictVariables.empty()); return Result::SAT; } @@ -132,28 +118,12 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ if(result == Result::UNSAT){ ++(d_statistics.d_fcFoundUnsat); - if (verbose) - { - CVC5Message() << "fc found unsat"; - } }else if(d_errorSet.errorEmpty()){ ++(d_statistics.d_fcFoundSat); - if (verbose) - { - CVC5Message() << "fc found model"; - } }else{ ++(d_statistics.d_fcMissed); - if (verbose) - { - CVC5Message() << "fc missed"; - } } } - if (verbose) - { - CVC5Message() << "(" << instance << ") pivots " << d_pivots << endl; - } Assert(!d_errorSet.moreSignals()); if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){ @@ -508,28 +478,9 @@ bool debugUpdatedBasic(const UpdateInfo& selected, ArithVar updated){ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, WitnessImprovement w){ ArithVar nonbasic = selected.nonbasic(); - static bool verbose = false; - Debug("updateAndSignal") << "updateAndSignal " << selected << endl; stringstream ss; - if(verbose){ - d_errorSet.debugPrint(ss); - if(selected.describesPivot()){ - ArithVar leaving = selected.leaving(); - ss << "leaving " << leaving - << " " << d_tableau.basicRowLength(leaving) - << " " << d_linEq.debugBasicAtBoundCount(leaving) - << endl; - } - if(degenerate(w) && selected.describesPivot()){ - ArithVar leaving = selected.leaving(); - CVC5Message() << "degenerate " << leaving << ", atBounds " - << d_linEq.basicsAtBounds(selected) << ", len " - << d_tableau.basicRowLength(leaving) << ", bc " - << d_linEq.debugBasicAtBoundCount(leaving) << endl; - } - } if(selected.describesPivot()){ ConstraintP limiting = selected.limiting(); @@ -573,11 +524,6 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit } } - if (verbose) - { - CVC5Message() << "conflict variable " << selected << endl; - CVC5Message() << ss.str(); - } if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); } Assert( @@ -715,7 +661,6 @@ bool FCSimplexDecisionProcedure::debugDualLike(WitnessImprovement w, ostream& ou Result::Sat FCSimplexDecisionProcedure::dualLike(){ static int instance = 0; - static bool verbose = false; TimerStat::CodeTimer codeTimer(d_statistics.d_fcTimer); @@ -787,15 +732,14 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){ w = selectFocusImproving(); } } + Debug("dualLike") << "witnessImprovement: " << w << endl; Assert(d_focusSize == d_errorSet.focusSize()); Assert(d_errorSize == d_errorSet.errorSize()); - if (verbose) - { - debugDualLike(w, CVC5Message(), instance, prevFocusSize, prevErrorSize); - } Assert(debugDualLike( w, Debug("dualLike"), instance, 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/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 8e7588847..ab6339fd5 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -167,12 +167,10 @@ void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis){ Assert(toAdd != ARITHVAR_SENTINEL); Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl; - CVC5Message() << toRemove << " " << toAdd << endl; d_tableau.pivot(toRemove, toAdd, d_trackCallback); d_basicVariableUpdates(toAdd); Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl; - CVC5Message() << needsToBeAdded.size() << "to go" << endl; needsToBeAdded.remove(toAdd); } } diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index d6cdb3a13..5a834ad42 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -80,7 +80,6 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ d_pivots = 0; static thread_local unsigned int instance = 0; instance = instance + 1; - static const bool verbose = false; if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){ Debug("soi::findModel") << "soiFindModel("<< instance <<") trivial" << endl; @@ -96,10 +95,6 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ if(initialProcessSignals()){ d_conflictVariables.purge(); - if (verbose) - { - CVC5Message() << "fcFindModel(" << instance << ") early conflict" << endl; - } Debug("soi::findModel") << "fcFindModel("<< instance <<") early conflict" << endl; Assert(d_conflictVariables.empty()); return Result::UNSAT; @@ -130,28 +125,12 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ if(result == Result::UNSAT){ ++(d_statistics.d_soiFoundUnsat); - if (verbose) - { - CVC5Message() << "fc found unsat"; - } }else if(d_errorSet.errorEmpty()){ ++(d_statistics.d_soiFoundSat); - if (verbose) - { - CVC5Message() << "fc found model"; - } }else{ ++(d_statistics.d_soiMissed); - if (verbose) - { - CVC5Message() << "fc missed"; - } } } - if (verbose) - { - CVC5Message() << "(" << instance << ") pivots " << d_pivots << endl; - } Assert(!d_errorSet.moreSignals()); if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){ @@ -345,29 +324,8 @@ void SumOfInfeasibilitiesSPD::debugPrintSignal(ArithVar updated) const{ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, WitnessImprovement w){ ArithVar nonbasic = selected.nonbasic(); - static bool verbose = false; - Debug("updateAndSignal") << "updateAndSignal " << selected << endl; - stringstream ss; - if(verbose){ - d_errorSet.debugPrint(ss); - if(selected.describesPivot()){ - ArithVar leaving = selected.leaving(); - ss << "leaving " << leaving - << " " << d_tableau.basicRowLength(leaving) - << " " << d_linEq.debugBasicAtBoundCount(leaving) - << endl; - } - if(degenerate(w) && selected.describesPivot()){ - ArithVar leaving = selected.leaving(); - CVC5Message() << "degenerate " << leaving << ", atBounds " - << d_linEq.basicsAtBounds(selected) << ", len " - << d_tableau.basicRowLength(leaving) << ", bc " - << d_linEq.debugBasicAtBoundCount(leaving) << endl; - } - } - if(selected.describesPivot()){ ConstraintP limiting = selected.limiting(); ArithVar basic = limiting->getVariable(); @@ -410,11 +368,6 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes } } - if (verbose) - { - CVC5Message() << "conflict variable " << selected << endl; - CVC5Message() << ss.str(); - } if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); } //Assert(debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize())); @@ -944,8 +897,7 @@ bool SumOfInfeasibilitiesSPD::debugSOI(WitnessImprovement w, ostream& out, int i Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){ static int instance = 0; - static bool verbose = false; - + TimerStat::CodeTimer codeTimer(d_statistics.d_soiTimer); Assert(d_sgnDisagreements.empty()); @@ -968,15 +920,11 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){ // - conflict // - budget was exhausted // - focus went down - Debug("dualLike") << "selectFocusImproving " << endl; WitnessImprovement w = soiRound(); + Debug("dualLike") << "selectFocusImproving -> " << w << endl; Assert(d_errorSize == d_errorSet.errorSize()); - if (verbose) - { - debugSOI(w, CVC5Message(), instance); - } Assert(debugSOI(w, Debug("dualLike"), instance)); }