diff --git a/ortools/bop/bop_fs.cc b/ortools/bop/bop_fs.cc index ae67e79c60..8e7f2f316a 100644 --- a/ortools/bop/bop_fs.cc +++ b/ortools/bop/bop_fs.cc @@ -337,14 +337,14 @@ BopOptimizerBase::Status BopRandomFirstSolutionGenerator::Optimize( // to do any extra work in these cases since the sat_propagator_ will not be // used anymore. CHECK_EQ(0, sat_propagator_->AssumptionLevel()); - sat_propagator_->RestoreSolverToAssumptionLevel(); + (void)sat_propagator_->ResetToLevelZero(); sat_propagator_->SetParameters(saved_params); sat_propagator_->ResetDecisionHeuristic(); for (const auto [literal, weight] : saved_prefs) { sat_propagator_->SetAssignmentPreference(literal, weight); } - // This can be proved during the call to RestoreSolverToAssumptionLevel(). + // This can be proved during the call to ResetToLevelZero(). if (sat_propagator_->ModelIsUnsat()) { // The solution is proved optimal (if any). learned_info->lower_bound = best_cost; diff --git a/ortools/bop/bop_lns.cc b/ortools/bop/bop_lns.cc index 32460a3c73..58a5d1193a 100644 --- a/ortools/bop/bop_lns.cc +++ b/ortools/bop/bop_lns.cc @@ -256,8 +256,7 @@ BopOptimizerBase::Status BopAdaptiveLNSOptimizer::Optimize( auto sat_propagator_cleanup = ::absl::MakeCleanup([initial_dt, this, &learned_info, &time_limit]() { if (!sat_propagator_->ModelIsUnsat()) { - sat_propagator_->SetAssumptionLevel(0); - sat_propagator_->RestoreSolverToAssumptionLevel(); + (void)sat_propagator_->ResetToLevelZero(); ExtractLearnedInfoFromSatSolver(sat_propagator_, learned_info); } time_limit->AdvanceDeterministicTime( @@ -327,14 +326,14 @@ BopOptimizerBase::Status BopAdaptiveLNSOptimizer::Optimize( // Restore to the assumption level. // This is call is important since all the fixed variable in the // propagator_ will be used to construct the local problem below. - // Note that calling RestoreSolverToAssumptionLevel() might actually prove + // Note that calling ResetToLevelZero() might actually prove // the infeasibility. It is important to check the UNSAT status afterward. if (!sat_propagator_->ModelIsUnsat()) { - sat_propagator_->RestoreSolverToAssumptionLevel(); + (void)sat_propagator_->ResetToLevelZero(); } // Check if the problem is proved UNSAT, by previous the search or the - // RestoreSolverToAssumptionLevel() call above. + // ResetToLevelZero() call above. if (sat_propagator_->ModelIsUnsat()) { return problem_state.solution().IsFeasible() ? BopOptimizerBase::OPTIMAL_SOLUTION_FOUND diff --git a/ortools/bop/bop_ls.cc b/ortools/bop/bop_ls.cc index b2d5e7620c..76e8fe83eb 100644 --- a/ortools/bop/bop_ls.cc +++ b/ortools/bop/bop_ls.cc @@ -649,6 +649,7 @@ void SatWrapper::BacktrackAll() { sat_solver_->Backtrack(0); } std::vector SatWrapper::FullSatTrail() const { std::vector propagated_literals; const sat::Trail& trail = sat_solver_->LiteralTrail(); + propagated_literals.reserve(trail.Index()); for (int trail_index = 0; trail_index < trail.Index(); ++trail_index) { propagated_literals.push_back(trail[trail_index]); } diff --git a/ortools/bop/bop_solver.cc b/ortools/bop/bop_solver.cc index 71bc5be1bc..973bfa8c8c 100644 --- a/ortools/bop/bop_solver.cc +++ b/ortools/bop/bop_solver.cc @@ -45,26 +45,6 @@ namespace { using ::operations_research::glop::ColIndex; using ::operations_research::glop::DenseRow; - -// Updates the problem_state when the solution is proved optimal or the problem -// is proved infeasible. -// Returns true when the problem_state has been changed. -bool UpdateProblemStateBasedOnStatus(BopOptimizerBase::Status status, - ProblemState* problem_state) { - CHECK(nullptr != problem_state); - - if (BopOptimizerBase::OPTIMAL_SOLUTION_FOUND == status) { - problem_state->MarkAsOptimal(); - return true; - } - - if (BopOptimizerBase::INFEASIBLE == status) { - problem_state->MarkAsInfeasible(); - return true; - } - - return false; -} } // anonymous namespace //------------------------------------------------------------------------------