flatzinc: export from google3

Author: Mizux

ortools/flatzinc/BUILD.bazel

@@ -183,12 +183,14 @@ cc_binary(
         "//ortools/base",
         "//ortools/base:path",
         "//ortools/base:timer",
+        "//ortools/sat:model",
         "//ortools/util:logging",
         "@abseil-cpp//absl/flags:flag",
         "@abseil-cpp//absl/log",
         "@abseil-cpp//absl/log:check",
         "@abseil-cpp//absl/log:flags",
         "@abseil-cpp//absl/strings",
         "@abseil-cpp//absl/time",
+        "@protobuf",
     ],
 )

ortools/flatzinc/cp_model_fz_solver.cc

@@ -40,7 +40,6 @@
 #include "absl/strings/str_join.h"
 #include "absl/types/span.h"
 #include "google/protobuf/arena.h"
-#include "google/protobuf/text_format.h"
 #include "ortools/base/iterator_adaptors.h"
 #include "ortools/base/stl_util.h"
 #include "ortools/flatzinc/checker.h"
@@ -3714,11 +3713,12 @@ void ProcessFloatingPointOVariablesAndObjective(fz::Model* fz_model) {
   }
 }
 
-void SolveFzWithCpModelProto(const fz::Model& fz_model,
-                             const fz::FlatzincSatParameters& p,
-                             const std::string& sat_params,
-                             SolverLogger* logger,
-                             SolverLogger* solution_logger) {
+CpSolverResponse SolveFzWithCpModelProto(const fz::Model& fz_model,
+                                         const fz::FlatzincSatParameters& p,
+                                         const SatParameters& sat_params,
+                                         Model* sat_model,
+                                         SolverLogger* solution_logger) {
+  SolverLogger* logger = sat_model->GetOrCreate<SolverLogger>();
   const bool enumerate_all_solutions_of_a_sat_problem =
       p.search_all_solutions && fz_model.objective() == nullptr;
   CpModelProtoWithMapping m(enumerate_all_solutions_of_a_sat_problem);
@@ -3924,11 +3924,7 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
 
   // The order is important, we want the flag parameters to overwrite anything
   // set in m.parameters.
-  sat::SatParameters flag_parameters;
-  CHECK(google::protobuf::TextFormat::ParseFromString(sat_params,
-                                                      &flag_parameters))
-      << sat_params;
-  m.parameters.MergeFrom(flag_parameters);
+  m.parameters.MergeFrom(sat_params);
 
   // We only need an observer if 'p.display_all_solutions' or
   // 'p.search_all_solutions' are true.
@@ -3979,19 +3975,12 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
     };
   }
 
-  Model sat_model;
-
-  // Setup logging.
-  // Note that we need to do that before we start calling the sat functions
-  // below that might create a SolverLogger() themselves.
-  sat_model.Register<SolverLogger>(logger);
-
-  sat_model.Add(NewSatParameters(m.parameters));
+  sat_model->Add(NewSatParameters(m.parameters));
   if (solution_observer != nullptr) {
-    sat_model.Add(NewFeasibleSolutionObserver(solution_observer));
+    sat_model->Add(NewFeasibleSolutionObserver(solution_observer));
   }
 
-  const CpSolverResponse response = SolveCpModel(m.proto, &sat_model);
+  const CpSolverResponse response = SolveCpModel(m.proto, sat_model);
 
   // Check the returned solution with the fz model checker.
   if (response.status() == CpSolverStatus::FEASIBLE ||
@@ -4065,6 +4054,7 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
       OutputFlatzincStats(response, solution_logger);
     }
   }
+  return response;
 }
 
 }  // namespace sat

ortools/flatzinc/cp_model_fz_solver.h

@@ -17,6 +17,9 @@
 #include <string>
 
 #include "ortools/flatzinc/model.h"
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
 #include "ortools/util/logging.h"
 
 namespace operations_research {
@@ -49,11 +52,11 @@ namespace sat {
 void ProcessFloatingPointOVariablesAndObjective(fz::Model* fz_model);
 
 // Solves the given flatzinc model using the CP-SAT solver.
-void SolveFzWithCpModelProto(const fz::Model& model,
-                             const fz::FlatzincSatParameters& p,
-                             const std::string& sat_params,
-                             SolverLogger* logger,
-                             SolverLogger* solution_logger);
+CpSolverResponse SolveFzWithCpModelProto(const fz::Model& model,
+                                         const fz::FlatzincSatParameters& p,
+                                         const SatParameters& sat_params,
+                                         Model* sat_model,
+                                         SolverLogger* solution_logger);
 
 }  // namespace sat
 }  // namespace operations_research

ortools/flatzinc/fz.cc

@@ -37,12 +37,14 @@
 #include "absl/strings/str_split.h"
 #include "absl/strings/string_view.h"
 #include "absl/time/time.h"
+#include "google/protobuf/text_format.h"
 #include "ortools/base/logging.h"
 #include "ortools/base/path.h"
 #include "ortools/base/timer.h"
 #include "ortools/flatzinc/cp_model_fz_solver.h"
 #include "ortools/flatzinc/model.h"
 #include "ortools/flatzinc/parser.h"
+#include "ortools/sat/model.h"
 #include "ortools/util/logging.h"
 
 constexpr bool kOrToolsMode = true;
@@ -234,20 +236,23 @@ int main(int argc, char** argv) {
     input = residual_flags.back();
   }
 
-  operations_research::SolverLogger logger;
+  operations_research::sat::Model sat_model;
+  operations_research::SolverLogger* logger =
+      sat_model.GetOrCreate<operations_research::SolverLogger>();
   if (absl::GetFlag(FLAGS_ortools_mode)) {
-    logger.EnableLogging(absl::GetFlag(FLAGS_fz_logging));
+    logger->EnableLogging(absl::GetFlag(FLAGS_fz_logging));
     // log_to_stdout is disabled later.
-    logger.AddInfoLoggingCallback(operations_research::fz::LogInFlatzincFormat);
+    logger->AddInfoLoggingCallback(
+        operations_research::fz::LogInFlatzincFormat);
   } else {
-    logger.EnableLogging(true);
-    logger.SetLogToStdOut(true);
+    logger->EnableLogging(true);
+    logger->SetLogToStdOut(true);
   }
 
   absl::Duration parse_duration;
   operations_research::fz::Model model =
       operations_research::fz::ParseFlatzincModel(
-          input, !absl::GetFlag(FLAGS_read_from_stdin), &logger,
+          input, !absl::GetFlag(FLAGS_read_from_stdin), logger,
           &parse_duration);
   operations_research::sat::ProcessFloatingPointOVariablesAndObjective(&model);
 
@@ -275,14 +280,17 @@ int main(int argc, char** argv) {
       SOLVER_LOG(&solution_logger, "%% TIMEOUT");
     }
     if (parameters.log_search_progress) {
-      SOLVER_LOG(&logger, "CpSolverResponse summary:");
-      SOLVER_LOG(&logger, "status: UNKNOWN");
+      SOLVER_LOG(logger, "CpSolverResponse summary:");
+      SOLVER_LOG(logger, "status: UNKNOWN");
     }
     return EXIT_SUCCESS;
   }
 
-  operations_research::sat::SolveFzWithCpModelProto(model, parameters,
-                                                    absl::GetFlag(FLAGS_params),
-                                                    &logger, &solution_logger);
+  operations_research::sat::SatParameters flag_parameters;
+  CHECK(google::protobuf::TextFormat::ParseFromString(
+      absl::GetFlag(FLAGS_params), &flag_parameters))
+      << absl::GetFlag(FLAGS_params);
+  operations_research::sat::SolveFzWithCpModelProto(
+      model, parameters, flag_parameters, &sat_model, &solution_logger);
   return EXIT_SUCCESS;
 }