flatzinc: export from google3

This commit is contained in:
Corentin Le Molgat
2025-11-12 17:05:19 +01:00
parent e7e9e0c166
commit aa4821cdc8
4 changed files with 40 additions and 37 deletions

View File

@@ -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",
],
)

View File

@@ -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

View File

@@ -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

View File

@@ -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;
}