Skip to content

Commit

Permalink
fix examples
Browse files Browse the repository at this point in the history
  • Loading branch information
@lperron
lperron committed Jun 29, 2017
1 parent 94b3832 commit 8ecbea3
Show file tree
Hide file tree
Showing 4 changed files with 73 additions and 36 deletions.
40 changes: 20 additions & 20 deletions examples/cpp/BUILD
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,9 @@ cc_binary(
name = "cryptarithm",
srcs = ["cryptarithm.cc"],
deps = [
"@com_google_protobuf_cc//:protobuf",
"//ortools/base",
"//ortools/constraint_solver:cp",
"@com_google_protobuf_cc//:protobuf",
],
)

Expand Down Expand Up @@ -230,7 +230,7 @@ cc_binary(
srcs = ["integer_programming.cc"],
deps = [
"//ortools/base",
"//ortools/linear_solver:linear_solver",
"//ortools/linear_solver",
],
)

Expand Down Expand Up @@ -309,7 +309,7 @@ cc_binary(
copts = ["-DUSE_GLOP"],
deps = [
"//ortools/base",
"//ortools/linear_solver:linear_solver",
"//ortools/linear_solver",
"//ortools/linear_solver:linear_solver_cc_proto",
],
)
Expand All @@ -319,7 +319,7 @@ cc_binary(
srcs = ["linear_solver_protocol_buffers.cc"],
deps = [
"//ortools/base",
"//ortools/linear_solver:linear_solver",
"//ortools/linear_solver",
"//ortools/linear_solver:linear_solver_cc_proto",
],
)
Expand Down Expand Up @@ -415,28 +415,28 @@ cc_binary(
"sat_runner.cc",
],
deps = [
"@com_google_protobuf_cc//:protobuf",
"//ortools/algorithms:sparse_permutation",
"//ortools/base",
"//ortools/base:file",
"//ortools/base:random",
"//ortools/base:status",
"//ortools/base:strings",
"//ortools/base:threadpool",
"//ortools/lp_data:mps_reader",
"//ortools/lp_data:proto_utils",
"//ortools/sat:boolean_problem",
"//ortools/sat:boolean_problem_cc_proto",
# "//ortools/sat:cp_model_proto",
# "//ortools/sat:cp_model_solver",
"//ortools/sat:cp_model_cc_proto",
"//ortools/sat:cp_model_solver",
"//ortools/sat:drat",
"//ortools/sat:lp_utils",
"//ortools/sat:optimization",
"//ortools/sat:sat_solver",
"//ortools/sat:simplification",
"//ortools/sat:symmetry",
"//ortools/base",
"//ortools/base:file",
"//ortools/base:strings",
"//ortools/base:status",
"//ortools/base:random",
"//ortools/base:threadpool",
"//ortools/algorithms:sparse_permutation",
"//ortools/lp_data:mps_reader",
"//ortools/lp_data:proto_utils",
"//ortools/util:filelineiter",
"//ortools/util:time_limit",
"@com_google_protobuf_cc//:protobuf",
],
)

Expand Down Expand Up @@ -470,7 +470,7 @@ cc_binary(
],
deps = [
"//ortools/base",
"//ortools/linear_solver:linear_solver",
"//ortools/linear_solver",
"//ortools/linear_solver:linear_solver_cc_proto",
"//ortools/lp_data:mps_reader",
],
Expand All @@ -491,19 +491,19 @@ cc_binary(
copts = ["-DUSE_GLOP"],
deps = [
"//ortools/base",
"//ortools/linear_solver:linear_solver",
"//ortools/linear_solver",
],
)

cc_binary(
name = "tsp",
srcs = ["tsp.cc"],
deps = [
"@com_google_protobuf_cc//:protobuf",
"//ortools/base",
"//ortools/constraint_solver:cp",
"//ortools/constraint_solver:routing",
"//ortools/constraint_solver:routing_flags",
"@com_google_protobuf_cc//:protobuf",
],
)

Expand All @@ -513,7 +513,6 @@ cc_binary(
"weighted_tardiness_sat.cc",
],
deps = [
"@com_google_protobuf_cc//:protobuf",
"//ortools/base",
"//ortools/base:file",
"//ortools/base:strings",
Expand All @@ -526,5 +525,6 @@ cc_binary(
"//ortools/sat:precedences",
"//ortools/sat:sat_solver",
"//ortools/util:filelineiter",
"@com_google_protobuf_cc//:protobuf",
],
)
12 changes: 6 additions & 6 deletions examples/cpp/sat_cnf_reader.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,11 +103,11 @@ class SatCnfReader {
return problem_name;
}

int64 StringViewAtoi(const string_view& input) {
int64 StringPieceAtoi(string_view input) {
// Hack: data() is not null terminated, but we do know that it points
// inside a std::string where numbers are separated by " " and since atoi64 will
// stop at the first invalid char, this works.
return atoi64(input.data());
return atoi64(input.data()); // NOLINT
}

void ProcessNewLine(const std::string& line, LinearBooleanProblem* problem) {
Expand All @@ -123,11 +123,11 @@ class SatCnfReader {

if (words_[0] == "p") {
if (words_[1] == "cnf" || words_[1] == "wcnf") {
num_variables_ = StringViewAtoi(words_[2]);
num_clauses_ = StringViewAtoi(words_[3]);
num_variables_ = StringPieceAtoi(words_[2]);
num_clauses_ = StringPieceAtoi(words_[3]);
if (words_[1] == "wcnf") {
is_wcnf_ = true;
hard_weight_ = (words_.size() > 4) ? StringViewAtoi(words_[4]) : 0;
hard_weight_ = (words_.size() > 4) ? StringPieceAtoi(words_[4]) : 0;
}
} else {
// TODO(user): The ToString() is only required for the open source. Fix.
Expand All @@ -148,7 +148,7 @@ class SatCnfReader {
int64 weight =
(!is_wcnf_ && interpret_cnf_as_max_sat_) ? 1 : hard_weight_;
for (int i = 0; i < size; ++i) {
const int64 signed_value = StringViewAtoi(words_[i]);
const int64 signed_value = StringPieceAtoi(words_[i]);
if (i == 0 && is_wcnf_) {
// Mathematically, a soft clause of weight 0 can be removed.
if (signed_value == 0) {
Expand Down
53 changes: 45 additions & 8 deletions examples/cpp/sat_runner.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@
#include "ortools/base/threadpool.h"
#include "ortools/algorithms/sparse_permutation.h"
#include "ortools/sat/boolean_problem.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/sat/drat.h"
#include "examples/cpp/opb_reader.h"
#include "ortools/sat/optimization.h"
Expand All @@ -38,6 +40,7 @@
#include "ortools/sat/sat_solver.h"
#include "ortools/sat/simplification.h"
#include "ortools/sat/symmetry.h"
#include "ortools/util/file_util.h"
#include "ortools/util/time_limit.h"
#include "ortools/base/random.h"
#include "ortools/base/status.h"
Expand Down Expand Up @@ -106,11 +109,19 @@ DEFINE_bool(presolve, true,
DEFINE_bool(probing, false, "If true, presolve the problem using probing.");


DEFINE_bool(use_cp_model, true,
"Whether to interpret a linear program input as a CpModelProto or "
"to read by default a CpModelProto.");

DEFINE_bool(reduce_memory_usage, false,
"If true, do not keep a copy of the original problem in memory."
"This reduce the memory usage, but disable the solution cheking at "
"the end.");

DEFINE_string(
drat_output, "",
"If non-empty, a proof in DRAT format will be written to this file.");

namespace operations_research {
namespace sat {
namespace {
Expand All @@ -126,7 +137,8 @@ double GetScaledTrivialBestBound(const LinearBooleanProblem& problem) {
return AddOffsetAndScaleObjectiveValue(problem, best_bound);
}

void LoadBooleanProblem(std::string filename, LinearBooleanProblem* problem) {
void LoadBooleanProblem(const std::string& filename, LinearBooleanProblem* problem,
CpModelProto* cp_model) {
if (strings::EndsWith(filename, ".opb") ||
strings::EndsWith(filename, ".opb.bz2")) {
OpbReader reader;
Expand All @@ -145,8 +157,12 @@ void LoadBooleanProblem(std::string filename, LinearBooleanProblem* problem) {
if (!reader.Load(filename, problem)) {
LOG(FATAL) << "Cannot load file '" << filename << "'.";
}
} else if (FLAGS_use_cp_model) {
LOG(INFO) << "Reading a CpModelProto.";
*cp_model = ReadFileToProtoOrDie<CpModelProto>(filename);
} else {
file::ReadFileToProtoOrDie(filename, problem);
LOG(INFO) << "Reading a LinearBooleanProblem.";
*problem = ReadFileToProtoOrDie<LinearBooleanProblem>(filename);
}
}

Expand Down Expand Up @@ -178,14 +194,20 @@ int Run() {
<< FLAGS_params;
}

Model model;
DratWriter* drat_writer = model.GetOrCreate<DratWriter>();

// Initialize the solver.
std::unique_ptr<SatSolver> solver(new SatSolver());
solver->SetDratWriter(drat_writer);
solver->SetParameters(parameters);

// Create a DratWriter?
std::unique_ptr<DratWriter> drat_writer;
if (!FLAGS_drat_output.empty()) {
File* output;
CHECK_OK(file::Open(FLAGS_drat_output, "w", &output, file::Defaults()));
drat_writer.reset(new DratWriter(/*in_binary_format=*/false, output));
solver->SetDratWriter(drat_writer.get());
}

// The global time limit.
std::unique_ptr<TimeLimit> time_limit(TimeLimit::FromParameters(parameters));

Expand All @@ -195,7 +217,21 @@ int Run() {

// Read the problem.
LinearBooleanProblem problem;
LoadBooleanProblem(FLAGS_input, &problem);
CpModelProto cp_model;
LoadBooleanProblem(FLAGS_input, &problem, &cp_model);

// TODO(user): clean this hack. Ideally LinearBooleanProblem should be
// completely replaced by the more general CpModelProto.
if (cp_model.variables_size() != 0) {
Model model;
model.GetOrCreate<SatSolver>()->SetParameters(parameters);
model.SetSingleton(std::move(time_limit));
LOG(INFO) << CpModelStats(cp_model);
const CpSolverResponse response = SolveCpModel(cp_model, &model);
LOG(INFO) << CpSolverResponseStats(response);
exit(EXIT_SUCCESS);
}

if (FLAGS_strict_validity) {
const util::Status status = ValidateBooleanProblem(problem);
if (!status.ok()) {
Expand Down Expand Up @@ -255,7 +291,8 @@ int Run() {
for (int i = 0; i < generators.size(); ++i) {
propagator->AddSymmetry(std::move(generators[i]));
}
solver->AddPropagator(std::move(propagator));
solver->AddPropagator(propagator.get());
solver->TakePropagatorOwnership(std::move(propagator));
}

// Optimize?
Expand Down Expand Up @@ -292,7 +329,7 @@ int Run() {
parameters.set_log_search_progress(true);
solver->SetParameters(parameters);
if (FLAGS_presolve) {
result = SolveWithPresolve(&solver, &solution, drat_writer);
result = SolveWithPresolve(&solver, &solution, drat_writer.get());
if (result == SatSolver::MODEL_SAT) {
CHECK(IsAssignmentValid(problem, solution));
}
Expand Down
4 changes: 2 additions & 2 deletions examples/cpp/solve.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,8 +45,8 @@ DEFINE_string(params_file, "",
"If this flag is set, the --params flag is ignored.");
DEFINE_string(params, "", "Solver specific parameters");
DEFINE_int64(time_limit_ms, 0,
"If stricitly positive, specifies a limit in ms on the solving"
" time.");
"If strictly positive, specifies a limit in ms on the solving "
"time. Otherwise, no time limit will be imposed.");
DEFINE_string(forced_mps_format, "",
"Set to force the mps format to use: free, fixed");

Expand Down

0 comments on commit 8ecbea3

Please sign in to comment.