fix flags support for fz

This commit is contained in:
Laurent Perron
2023-10-18 15:44:19 +02:00
parent 57ec0e6561
commit 02c993cebe
3 changed files with 19 additions and 12 deletions

View File

@@ -1331,19 +1331,20 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
// Fill the search order.
m.TranslateSearchAnnotations(fz_model.search_annotations(), logger);
if (p.display_all_solutions && !m.proto.has_objective()) {
if (p.search_all_solutions && !m.proto.has_objective()) {
// Enumerate all sat solutions.
m.parameters.set_enumerate_all_solutions(true);
}
m.parameters.set_log_search_progress(p.log_search_progress);
m.parameters.set_log_to_stdout(!p.ortools_mode);
// Helps with challenge unit tests.
m.parameters.set_max_domain_size_when_encoding_eq_neq_constraints(32);
// Computes the number of workers.
int num_workers = 1;
if (p.display_all_solutions && fz_model.objective() == nullptr) {
if (p.search_all_solutions && fz_model.objective() == nullptr) {
if (p.number_of_threads > 1) {
// We don't support enumerating all solution in parallel for a SAT
// problem. But note that we do support it for an optimization problem
@@ -1371,7 +1372,7 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
m.parameters.set_keep_all_feasible_solutions_in_presolve(true);
} else if (num_workers == 1 && p.use_free_search) { // Free search.
m.parameters.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
if (!p.display_all_solutions && p.ortools_mode) {
if (!p.search_all_solutions && p.ortools_mode) {
m.parameters.set_interleave_search(true);
if (fz_model.objective() != nullptr) {
m.parameters.add_subsolvers("default_lp");
@@ -1408,9 +1409,10 @@ void SolveFzWithCpModelProto(const fz::Model& fz_model,
<< sat_params;
m.parameters.MergeFrom(flag_parameters);
// We only need an observer if 'p.all_solutions' is true.
// We only need an observer if 'p.display_all_solutions' or
// 'p.search_all_solutions' are true.
std::function<void(const CpSolverResponse&)> solution_observer = nullptr;
if (p.display_all_solutions) {
if (p.display_all_solutions || p.search_all_solutions) {
solution_observer = [&fz_model, &m, &p,
solution_logger](const CpSolverResponse& r) {
const std::string solution_string =

View File

@@ -23,6 +23,7 @@ namespace operations_research {
namespace fz {
struct FlatzincSatParameters {
bool search_all_solutions = false;
bool display_all_solutions = false;
bool use_free_search = false;
bool log_search_progress = false;

View File

@@ -21,9 +21,7 @@
#include <signal.h>
#endif // __GNUC__
#include <csignal>
#include <iostream>
#include <limits>
#include <ostream>
#include <string>
#include <vector>
@@ -38,7 +36,6 @@
#include "ortools/base/logging.h"
#include "ortools/base/path.h"
#include "ortools/base/timer.h"
#include "ortools/base/types.h"
#include "ortools/flatzinc/cp_model_fz_solver.h"
#include "ortools/flatzinc/model.h"
#include "ortools/flatzinc/parser.h"
@@ -46,7 +43,9 @@
#include "ortools/util/logging.h"
ABSL_FLAG(double, time_limit, 0, "time limit in seconds.");
ABSL_FLAG(bool, all_solutions, false, "Search for all solutions.");
ABSL_FLAG(bool, search_all_solutions, false, "Search for all solutions.");
ABSL_FLAG(bool, display_all_solutions, false,
"Display all improving solutions.");
ABSL_FLAG(bool, free_search, false,
"If false, the solver must follow the defined search."
"If true, other search are allowed.");
@@ -67,7 +66,8 @@ namespace operations_research {
namespace fz {
std::vector<char*> FixAndParseParameters(int* argc, char*** argv) {
char all_param[] = "--all_solutions";
char all_param[] = "--search_all_solutions";
char print_solutions[] = "--display_all_solutions";
char free_param[] = "--free_search";
char threads_param[] = "--threads";
char logging_param[] = "--fz_logging";
@@ -80,6 +80,9 @@ std::vector<char*> FixAndParseParameters(int* argc, char*** argv) {
if (strcmp((*argv)[i], "-a") == 0) {
(*argv)[i] = all_param;
}
if (strcmp((*argv)[i], "-i") == 0) {
(*argv)[i] = print_solutions;
}
if (strcmp((*argv)[i], "-f") == 0) {
(*argv)[i] = free_param;
set_free_search = true;
@@ -206,7 +209,7 @@ int main(int argc, char** argv) {
operations_research::SolverLogger logger;
if (absl::GetFlag(FLAGS_ortools_mode)) {
logger.EnableLogging(true);
logger.SetLogToStdOut(false);
// log_to_stdout is disabled later.
logger.AddInfoLoggingCallback(operations_research::fz::LogInFlatzincFormat);
} else {
logger.EnableLogging(true);
@@ -218,7 +221,8 @@ int main(int argc, char** argv) {
input, !absl::GetFlag(FLAGS_read_from_stdin), &logger);
operations_research::fz::FlatzincSatParameters parameters;
parameters.display_all_solutions = absl::GetFlag(FLAGS_all_solutions);
parameters.display_all_solutions = absl::GetFlag(FLAGS_display_all_solutions);
parameters.search_all_solutions = absl::GetFlag(FLAGS_search_all_solutions);
parameters.use_free_search = absl::GetFlag(FLAGS_free_search);
parameters.log_search_progress =
absl::GetFlag(FLAGS_fz_logging) || !absl::GetFlag(FLAGS_ortools_mode);