fix examples

examples/cpp/BUILD

@@ -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",
     ],
 )
 
@@ -230,7 +230,7 @@ cc_binary(
     srcs = ["integer_programming.cc"],
     deps = [
         "//ortools/base",
-        "//ortools/linear_solver:linear_solver",
+        "//ortools/linear_solver",
     ],
 )
 
@@ -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",
     ],
 )
@@ -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",
     ],
 )
@@ -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",
     ],
 )
 
@@ -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",
     ],
@@ -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",
     ],
 )
 
@@ -513,7 +513,6 @@ cc_binary(
         "weighted_tardiness_sat.cc",
     ],
     deps = [
-        "@com_google_protobuf_cc//:protobuf",
         "//ortools/base",
         "//ortools/base:file",
         "//ortools/base:strings",
@@ -526,5 +525,6 @@ cc_binary(
         "//ortools/sat:precedences",
         "//ortools/sat:sat_solver",
         "//ortools/util:filelineiter",
+        "@com_google_protobuf_cc//:protobuf",
     ],
 )

examples/cpp/sat_cnf_reader.h

@@ -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) {
@@ -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.
@@ -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) {

examples/cpp/sat_runner.cc

@@ -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"
@@ -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"
@@ -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 {
@@ -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;
@@ -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);
   }
 }
 
@@ -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));
 
@@ -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()) {
@@ -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?
@@ -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));
       }

examples/cpp/solve.cc

@@ -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");