From aa4821cdc8639a939a963c9db9e7fb45a8f8f787 Mon Sep 17 00:00:00 2001 From: Corentin Le Molgat Date: Wed, 12 Nov 2025 17:05:19 +0100 Subject: [PATCH] flatzinc: export from google3 --- ortools/flatzinc/BUILD.bazel | 2 ++ ortools/flatzinc/cp_model_fz_solver.cc | 32 +++++++++----------------- ortools/flatzinc/cp_model_fz_solver.h | 13 +++++++---- ortools/flatzinc/fz.cc | 30 +++++++++++++++--------- 4 files changed, 40 insertions(+), 37 deletions(-) diff --git a/ortools/flatzinc/BUILD.bazel b/ortools/flatzinc/BUILD.bazel index a07dd0f7c9..77ea81e445 100644 --- a/ortools/flatzinc/BUILD.bazel +++ b/ortools/flatzinc/BUILD.bazel @@ -183,6 +183,7 @@ 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", @@ -190,5 +191,6 @@ cc_binary( "@abseil-cpp//absl/log:flags", "@abseil-cpp//absl/strings", "@abseil-cpp//absl/time", + "@protobuf", ], ) diff --git a/ortools/flatzinc/cp_model_fz_solver.cc b/ortools/flatzinc/cp_model_fz_solver.cc index b05b82113e..883e6cc859 100644 --- a/ortools/flatzinc/cp_model_fz_solver.cc +++ b/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(); 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(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 diff --git a/ortools/flatzinc/cp_model_fz_solver.h b/ortools/flatzinc/cp_model_fz_solver.h index b155ef2e16..3da040b864 100644 --- a/ortools/flatzinc/cp_model_fz_solver.h +++ b/ortools/flatzinc/cp_model_fz_solver.h @@ -17,6 +17,9 @@ #include #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 diff --git a/ortools/flatzinc/fz.cc b/ortools/flatzinc/fz.cc index 85afa11865..e9366d2da5 100644 --- a/ortools/flatzinc/fz.cc +++ b/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(); 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; }