[CP-SAT] more spans; more fuzztest seeds; generate doc for the pybind…

…11 wrapped C++ classes; rename cp_model.py helper modules

ortools/sat/BUILD.bazel

@@ -3818,9 +3818,11 @@ cc_test(
     data = glob(["fuzz_testdata/*"]),
     deps = [
         ":cp_model_cc_proto",
+        ":cp_model_checker",
         ":cp_model_solver",
         "//ortools/base:fuzztest",
         "//ortools/base:path",
+        "//ortools/util:saturated_arithmetic",
         "@bazel_tools//tools/cpp/runfiles",
         "@com_google_absl//absl/log:check",
         "@com_google_fuzztest//fuzztest:fuzztest_gtest_main",

ortools/sat/circuit.cc

@@ -646,10 +646,9 @@ std::function<void(Model*)> ExactlyOnePerRowAndPerColumn(
   };
 }
 
-void LoadSubcircuitConstraint(int num_nodes, const std::vector<int>& tails,
-                              const std::vector<int>& heads,
-                              const std::vector<Literal>& literals,
-                              Model* model,
+void LoadSubcircuitConstraint(int num_nodes, absl::Span<const int> tails,
+                              absl::Span<const int> heads,
+                              absl::Span<const Literal> literals, Model* model,
                               bool multiple_subcircuit_through_zero) {
   const int num_arcs = tails.size();
   CHECK_GT(num_arcs, 0);

ortools/sat/circuit.h

@@ -244,10 +244,9 @@ int ReindexArcs(IntContainer* tails, IntContainer* heads,
 // This just wraps CircuitPropagator. See the comment there to see what this
 // does. Note that any nodes with no outgoing or no incoming arc will cause the
 // problem to be UNSAT. One can call ReindexArcs() first to ignore such nodes.
-void LoadSubcircuitConstraint(int num_nodes, const std::vector<int>& tails,
-                              const std::vector<int>& heads,
-                              const std::vector<Literal>& literals,
-                              Model* model,
+void LoadSubcircuitConstraint(int num_nodes, absl::Span<const int> tails,
+                              absl::Span<const int> heads,
+                              absl::Span<const Literal> literals, Model* model,
                               bool multiple_subcircuit_through_zero = false);
 
 // TODO(user): Change to a sparse API like for the function above.

ortools/sat/cp_model_solver_fuzz.cc

@@ -11,14 +11,21 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
+#include <algorithm>
+#include <cstdint>
+#include <limits>
+#include <optional>
 #include <string>
+#include <utility>
 
 #include "absl/log/check.h"
 #include "gtest/gtest.h"  // IWYU pragma: keep
 #include "ortools/base/fuzztest.h"
 #include "ortools/base/path.h"  // IWYU pragma: keep
 #include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_checker.h"
 #include "ortools/sat/cp_model_solver.h"
+#include "ortools/util/saturated_arithmetic.h"
 #include "tools/cpp/runfiles/runfiles.h"
 
 namespace operations_research::sat {
@@ -76,10 +83,93 @@ void Solve(const CpModelProto& proto) {
       << "Presolve should not change feasibility";
 }
 
+fuzztest::Domain<IntegerVariableProto> CpVariableDomain() {
+  fuzztest::Domain<int64_t> bound_domain =
+      fuzztest::InRange<int64_t>(-std::numeric_limits<int64_t>::max() / 2,
+                                 std::numeric_limits<int64_t>::max() / 2);
+  fuzztest::Domain<std::pair<int64_t, int64_t>> complex_domain_gap_and_size =
+      fuzztest::PairOf(fuzztest::InRange<int64_t>(
+                           1, std::numeric_limits<int64_t>::max() / 2),
+                       fuzztest::InRange<int64_t>(
+                           0, std::numeric_limits<int64_t>::max() / 2));
+  fuzztest::Domain<IntegerVariableProto> var_domain = fuzztest::ReversibleMap(
+      [](int64_t bound1, int64_t bound2,
+         std::vector<std::pair<int64_t, int64_t>> complex_domain_segments) {
+        IntegerVariableProto var;
+        var.add_domain(std::min(bound1, bound2));
+        var.add_domain(std::max(bound1, bound2));
+
+        for (const auto& [gap, size] : complex_domain_segments) {
+          var.add_domain(CapAdd(var.domain(var.domain().size() - 1), gap));
+          var.add_domain(CapAdd(var.domain(var.domain().size() - 1), size));
+        }
+        return var;
+      },
+      [](IntegerVariableProto var) {
+        using Type = std::tuple<int64_t, int64_t,
+                                std::vector<std::pair<int64_t, int64_t>>>;
+        Type domain_inputs;
+        if (var.domain().size() < 2 || var.domain().size() % 2 != 0) {
+          return std::optional<Type>();
+        }
+        domain_inputs = {var.domain(0), var.domain(1), {}};
+        std::vector<std::pair<int64_t, int64_t>>& complex_domain_segments =
+            std::get<2>(domain_inputs);
+        for (int i = 2; i + 1 < var.domain().size(); i += 2) {
+          const int64_t gap = CapSub(var.domain(i), var.domain(i - 1));
+          const int64_t size = CapSub(var.domain(i + 1), var.domain(i));
+          if (gap <= 0 || size < 0) {
+            return std::optional<Type>();
+          }
+          complex_domain_segments.push_back({gap, size});
+        }
+        return std::optional<Type>(domain_inputs);
+      },
+      bound_domain, bound_domain,
+      fuzztest::VectorOf(complex_domain_gap_and_size));
+
+  return fuzztest::Filter(
+      [](IntegerVariableProto var) {
+        return var.domain(var.domain().size() - 1) <=
+               std::numeric_limits<int64_t>::max() / 2;
+      },
+      var_domain);
+}
+
+fuzztest::Domain<std::vector<IntegerVariableProto>>
+ModelProtoVariablesDomain() {
+  return fuzztest::Filter(
+      [](const std::vector<IntegerVariableProto>& vars) {
+        // Check if the variables in isolation doesn't make for a invalid model.
+        CpModelProto model;
+        for (const IntegerVariableProto& var : vars) {
+          *model.add_variables() = var;
+        }
+        return ValidateCpModel(model).empty();
+      },
+      fuzztest::VectorOf(CpVariableDomain()));
+}
+
 // Fuzzing repeats solve() 100 times, and timeout after 600s.
 // With a time limit of 4s, we should be fine.
 FUZZ_TEST(CpModelProtoFuzzer, Solve)
-    .WithDomains(/*proto:*/ fuzztest::Arbitrary<CpModelProto>())
+    .WithDomains(
+        fuzztest::Arbitrary<CpModelProto>()
+            .WithRepeatedProtobufField("variables", ModelProtoVariablesDomain())
+            .WithRepeatedProtobufField(
+                "constraints",
+                fuzztest::VectorOf(fuzztest::Arbitrary<ConstraintProto>()
+                                       .WithOneofAlwaysSet("constraint")
+                                       .WithFieldUnset("name")
+                                       .WithFieldUnset("dummy_constraint")))
+            .WithFieldUnset("name")
+            .WithFieldUnset("symmetry")
+            .WithProtobufField("objective",
+                               fuzztest::Arbitrary<CpObjectiveProto>()
+                                   .WithFieldUnset("scaling_was_exact")
+                                   .WithFieldUnset("integer_scaling_factor")
+                                   .WithFieldUnset("integer_before_offset")
+                                   .WithFieldUnset("integer_after_offset")))
     .WithSeeds([]() {
       return fuzztest::ReadFilesFromDirectory<CpModelProto>(GetTestDataDir());
     });

ortools/sat/fuzz_testdata/AtMostOneModel

@@ -0,0 +1,15 @@
+# proto-file: ortools/sat/cp_model.proto
+# proto-message: operations_research.sat.CpModelProto
+
+variables { domain: [ 0, 1 ] }
+variables { domain: [ 0, 1 ] }
+variables { domain: [ 0, 1 ] }
+variables { domain: [ 0, 50 ] }
+constraints { at_most_one { literals: [ 0, 1, 2 ] } }
+constraints {
+  linear {
+    vars: [ 0, 1, 2, 3 ]
+    coeffs: [ 2, 3, 4, -1 ]
+    domain: [ 0, 10 ]
+  }
+}

ortools/sat/fuzz_testdata/AutomatonModel

@@ -0,0 +1,34 @@
+# proto-file: ortools/sat/cp_model.proto
+# proto-message: operations_research.sat.CpModelProto
+
+variables { domain: 0 domain: 1 }
+variables { domain: 0 domain: 1 }
+variables { domain: 0 domain: 1 }
+variables { domain: 0 domain: 1 }
+constraints {
+  automaton {
+    final_states: 3
+    transition_tail: 0
+    transition_tail: 0
+    transition_tail: 1
+    transition_tail: 2
+    transition_tail: 1
+    transition_tail: 2
+    transition_head: 1
+    transition_head: 2
+    transition_head: 1
+    transition_head: 2
+    transition_head: 3
+    transition_head: 3
+    transition_label: 0
+    transition_label: 1
+    transition_label: 0
+    transition_label: 1
+    transition_label: 1
+    transition_label: 0
+    exprs { vars: 0 coeffs: 1 }
+    exprs { vars: 1 coeffs: 1 }
+    exprs { vars: 2 coeffs: 1 }
+    exprs { vars: 3 coeffs: 1 }
+  }
+}

ortools/sat/fuzz_testdata/CircuitModel

@@ -0,0 +1,17 @@
+# proto-file: ortools/sat/cp_model.proto
+# proto-message: operations_research.sat.CpModelProto
+
+variables { domain: [ 0, 1 ] }  # 0->1
+variables { domain: [ 0, 1 ] }  # 1->2
+variables { domain: [ 0, 1 ] }  # 1->0
+variables { domain: [ 0, 1 ] }  # 2->0
+variables { domain: [ 0, 1 ] }  # 2->2
+variables { domain: [ 0, 1 ] }  # 0->2
+variables { domain: [ 0, 1 ] }  # 2->1
+constraints {
+  routes {
+    tails: [ 0, 1, 1, 2, 2, 0, 2 ]
+    heads: [ 1, 2, 0, 0, 2, 2, 1 ]
+    literals: [ 0, 1, 2, 3, 4, 5, 6 ]
+  }
+}

ortools/sat/fuzz_testdata/ElementModel

@@ -0,0 +1,17 @@
+# proto-file: ortools/sat/cp_model.proto
+# proto-message: operations_research.sat.CpModelProto
+
+variables { domain: [ 0, 5 ] }
+variables { domain: [ 0, 7 ] }
+constraints {
+  element {
+    linear_index { vars: 0 coeffs: 1 }
+    linear_target { vars: 1 coeffs: 1 }
+    exprs { offset: 1 }
+    exprs { offset: 2 }
+    exprs { offset: 3 }
+    exprs { offset: 4 }
+    exprs { offset: 5 }
+    exprs { offset: 6 }
+  }
+}

ortools/sat/fuzz_testdata/ExactlyOneModel

@@ -0,0 +1,17 @@
+# proto-file: ortools/sat/cp_model.proto
+# proto-message: operations_research.sat.CpModelProto
+
+variables { domain: [ 0, 1 ] }
+variables { domain: [ 0, 1 ] }
+variables { domain: [ 0, 1 ] }
+variables { domain: [ 0, 1 ] }
+variables { domain: [ 0, 1 ] }
+variables { domain: [ -100, 100 ] }
+constraints { exactly_one { literals: [ 0, 1, 2, 3, 4 ] } }
+constraints {
+  linear {
+    vars: [ 0, 1, 3, 4, 5 ]
+    coeffs: [ 1, 7, -2, 4, 1 ]
+    domain: [ 10, 10 ]
+  }
+}

ortools/sat/fuzz_testdata/IntProdModel

@@ -0,0 +1,19 @@
+# proto-file: ortools/sat/cp_model.proto
+# proto-message: operations_research.sat.CpModelProto
+
+variables {
+  domain: [ 10, 12 ]
+}
+variables {
+  domain: [ 2, 2 ]
+}
+variables {
+  domain: [ 0, 100 ]
+}
+constraints {
+  int_prod {
+    target { vars: 2 coeffs: 1 }
+    exprs { vars: 1 coeffs: 1 }
+    exprs { vars: 0 coeffs: 1 }
+  }
+}

ortools/sat/fuzz_testdata/InverseModel

@@ -0,0 +1,17 @@
+# proto-file: ortools/sat/cp_model.proto
+# proto-message: operations_research.sat.CpModelProto
+
+variables { domain: [ 0, 3 ] }
+variables { domain: [ 0, 3 ] }
+variables { domain: [ 0, 3 ] }
+variables { domain: [ 0, 3 ] }
+variables { domain: [ 0, 3 ] }
+variables { domain: [ 0, 3 ] }
+variables { domain: [ 0, 3 ] }
+variables { domain: [ 0, 3 ] }
+constraints {
+  inverse {
+    f_direct: [ 0, 2, 4, 6 ],
+    f_inverse: [ 1, 3, 5, 7 ]
+  }
+}

ortools/sat/fuzz_testdata/LinMaxModel

@@ -0,0 +1,14 @@
+# proto-file: ortools/sat/cp_model.proto
+# proto-message: operations_research.sat.CpModelProto
+
+variables { domain: [ 0, 1 ] }
+variables { domain: [ 0, 1 ] }
+variables { domain: [ 0, 1 ] }
+constraints {
+  lin_max {
+    target { vars: 0 coeffs: 2 }
+    exprs { vars: 1 coeffs: 1 offset: 1 }
+    exprs { vars: 2 coeffs: 4 offset: 1 }
+    exprs { offset: 1 }
+  }
+}

ortools/sat/fuzz_testdata/NoOverlap2DOptimization

@@ -2,27 +2,21 @@
 # proto-message: operations_research.sat.CpModelProto
 
 variables: {
-  name: "x_0"
   domain: [ 0, 80 ]
 }
 variables: {
-  name: "y_0"
   domain: [ 0, 40 ]
 }
 variables: {
-  name: "x_1"
   domain: [ 0, 80 ]
 }
 variables: {
-  name: "y_1"
   domain: [ 0, 60 ]
 }
 variables: {
-  name: "x_2"
   domain: [ 0, 90 ]
 }
 variables: {
-  name: "y_2"
   domain: [ 0, 50 ]
 }
 variables: { domain: [ 1, 1 ] }
@@ -39,7 +33,6 @@ constraints: {
   }
 }
 constraints: {
-  name: "x_interval_0"
   enforcement_literal: 6
   interval: {
     start: { vars: 0 coeffs: 1 }
@@ -48,7 +41,6 @@ constraints: {
   }
 }
 constraints: {
-  name: "y_interval_0"
   enforcement_literal: 6
   interval: {
     start: { vars: 1 coeffs: 1 }
@@ -57,7 +49,6 @@ constraints: {
   }
 }
 constraints: {
-  name: "x_interval_1"
   enforcement_literal: 6
   interval: {
     start: { vars: 2 coeffs: 1 }
@@ -66,7 +57,6 @@ constraints: {
   }
 }
 constraints: {
-  name: "y_interval_1"
   enforcement_literal: 6
   interval: {
     start: { vars: 3 coeffs: 1 }
@@ -75,7 +65,6 @@ constraints: {
   }
 }
 constraints: {
-  name: "x_interval_2"
   enforcement_literal: 6
   interval: {
     start: { vars: 4 coeffs: 1 }
@@ -84,7 +73,6 @@ constraints: {
   }
 }
 constraints: {
-  name: "y_interval_2"
   enforcement_literal: 6
   interval: {
     start: { vars: 5 coeffs: 1 }