[CP-SAT] Work on linear1 encodings; more work on lrat; cleanup linear2 code; work on probing

ortools/linear_solver/proto_solver/sat_proto_solver.cc

@@ -160,7 +160,8 @@ MPSolutionResponse TimeLimitResponse(SolverLogger& logger) {
 MPSolutionResponse SatSolveProto(
     LazyMutableCopy<MPModelRequest> request, std::atomic<bool>* interrupt_solve,
     std::function<void(const std::string&)> logging_callback,
-    std::function<void(const MPSolution&)> solution_callback) {
+    std::function<void(const MPSolution&)> solution_callback,
+    std::function<void(const double)> best_bound_callback) {
   sat::SatParameters params;
   params.set_log_search_progress(request->enable_internal_solver_output());
 
@@ -431,6 +432,9 @@ MPSolutionResponse SatSolveProto(
           solution_callback(post_solve(cp_response));
         }));
   }
+  if (best_bound_callback != nullptr) {
+    sat_model.Add(sat::NewBestBoundCallback(best_bound_callback));
+  }
 
   // Solve.
   const sat::CpSolverResponse cp_response =

ortools/linear_solver/proto_solver/sat_proto_solver.h

@@ -49,11 +49,18 @@ namespace operations_research {
 // found by the solver. The solver may call solution_callback from multiple
 // threads, but it will ensure that at most one thread executes
 // solution_callback at a time.
+//
+// The optional best_bound_callback will be called each time the best bound is
+// improved. The solver may call solution_callback from multiple
+// threads, but it will ensure that at most one thread executes
+// solution_callback at a time. It is guaranteed that the best bound is strictly
+// improving.
 MPSolutionResponse SatSolveProto(
     LazyMutableCopy<MPModelRequest> request,
     std::atomic<bool>* interrupt_solve = nullptr,
     std::function<void(const std::string&)> logging_callback = nullptr,
-    std::function<void(const MPSolution&)> solution_callback = nullptr);
+    std::function<void(const MPSolution&)> solution_callback = nullptr,
+    std::function<void(const double)> best_bound_callback = nullptr);
 
 // Returns a string that describes the version of the CP-SAT solver.
 std::string SatSolverVersion();