[CP-SAT] fix more fuzzer bugs; polish python code

ortools/sat/cp_model_presolve.cc

@@ -608,7 +608,7 @@ bool CpModelPresolver::PresolveAtMostOrExactlyOne(ConstraintProto* ct) {
 
     // By domination argument, we can fix to false everything but the minimum.
     if (singleton_literal_with_cost.size() > 1) {
-      std::sort(
+      std::stable_sort(
           singleton_literal_with_cost.begin(),
           singleton_literal_with_cost.end(),
           [](const std::pair<int, int64_t>& a,
@@ -1629,8 +1629,8 @@ bool CpModelPresolver::PresolveIntProd(ConstraintProto* ct) {
         PossibleIntegerOverflow(*context_->working_model, lin->vars(),
                                 lin->coeffs(), lin->domain(0))) {
       context_->working_model->mutable_constraints()->RemoveLast();
-      // Re-add a new term with the constant factor.
-      ct->mutable_int_prod()->add_exprs()->set_offset(constant_factor);
+      // The constant factor will be handled by the creation of an affine
+      // relation below.
     } else {  // Replace with a linear equation.
       context_->UpdateNewConstraintsVariableUsage();
       context_->UpdateRuleStats("int_prod: linearize product by constant.");

ortools/sat/cp_model_table.cc

@@ -191,7 +191,7 @@ void CompressTuples(absl::Span<const int64_t> domain_sizes,
   std::vector<int> to_remove;
   std::vector<int64_t> tuple_minus_var_i(num_vars - 1);
   for (int i = 0; i < num_vars; ++i) {
-    const int domain_size = domain_sizes[i];
+    const int64_t domain_size = domain_sizes[i];
     if (domain_size == 1) continue;
     absl::flat_hash_map<std::vector<int64_t>, std::vector<int>>
         masked_tuples_to_indices;

ortools/sat/cp_model_table_test.cc

@@ -196,6 +196,18 @@ TEST(CompressTuplesTest, NotPerfect) {
   EXPECT_EQ(tuples, expected_tuples);
 }
 
+TEST(CompressTuplesTest, BigInteger) {
+  const std::vector<int64_t> domain_sizes = {576460752303423490};
+  const std::vector<std::vector<int64_t>> original_tuples = {
+      {1},
+      {2},
+  };
+  std::vector<std::vector<int64_t>> tuples = original_tuples;
+  CompressTuples(domain_sizes, &tuples);
+
+  EXPECT_EQ(tuples, original_tuples);
+}
+
 TEST(FullyCompressTuplesTest, BasicTest) {
   const std::vector<int64_t> domain_sizes = {4, 4};
   std::vector<std::vector<int64_t>> tuples = {

ortools/sat/diffn.cc

@@ -106,8 +106,14 @@ void AddDiffnCumulativeRelationOnX(SchedulingConstraintHelper* x,
   const IntegerVariable max_end_var =
       CreateVariableAtOrBelowMaxOf(y->Ends(), model);
 
-  // (max_end - min_start) >= capacity.
   auto* integer_trail = model->GetOrCreate<IntegerTrail>();
+  if (integer_trail->UpperBound(max_end_var) <
+      integer_trail->LowerBound(min_start_var)) {
+    // Trivial infeasible case, will be handled by the linear constraint
+    // from the interval.
+    return;
+  }
+  // (max_end - min_start) >= capacity.
   const AffineExpression capacity(model->Add(NewIntegerVariable(
       0, CapSub(integer_trail->UpperBound(max_end_var).value(),
                 integer_trail->LowerBound(min_start_var).value()))));

ortools/sat/linear_constraint.cc

@@ -61,6 +61,7 @@ void LinearConstraintBuilder::AddTerm(AffineExpression expr,
       terms_.push_back({NegationOf(expr.var), -coeff * expr.coeff});
     }
   }
+  DCHECK(!ProdOverflow(coeff, expr.constant));
   offset_ += coeff * expr.constant;
 }
 

ortools/sat/linear_programming_constraint.cc

@@ -359,12 +359,13 @@ LinearProgrammingConstraint::LinearProgrammingConstraint(
   lp_reduced_cost_.assign(vars.size(), 0.0);
 
   if (!vars.empty()) {
-    const int max_index = NegationOf(vars.back()).value();
+    const IntegerVariable max_index = std::max(
+        NegationOf(vars.back()), integer_trail_->NumIntegerVariables() - 1);
     if (max_index >= expanded_lp_solution_.size()) {
-      expanded_lp_solution_.assign(max_index + 1, 0.0);
+      expanded_lp_solution_.assign(max_index.value() + 1, 0.0);
     }
     if (max_index >= expanded_reduced_costs_.size()) {
-      expanded_reduced_costs_.assign(max_index + 1, 0.0);
+      expanded_reduced_costs_.assign(max_index.value() + 1, 0.0);
     }
   }
 }
@@ -805,6 +806,17 @@ void LinearProgrammingConstraint::SetLevel(int level) {
     lp_solution_is_set_ = true;
     lp_solution_ = level_zero_lp_solution_;
     lp_solution_level_ = 0;
+    // Add the fixed variables. They might have been skipped when we did the
+    // linear relaxation of the model, but cut generators expect all variables
+    // to have an LP value.
+    if (expanded_lp_solution_.size() < integer_trail_->NumIntegerVariables()) {
+      expanded_lp_solution_.resize(integer_trail_->NumIntegerVariables());
+    }
+    for (IntegerVariable i(0); i < integer_trail_->NumIntegerVariables(); ++i) {
+      if (integer_trail_->IsFixed(i)) {
+        expanded_lp_solution_[i] = ToDouble(integer_trail_->LowerBound(i));
+      }
+    }
     for (int i = 0; i < lp_solution_.size(); i++) {
       const IntegerVariable var = extended_integer_variables_[i];
       expanded_lp_solution_[var] = lp_solution_[i];
@@ -1175,7 +1187,7 @@ bool LinearProgrammingConstraint::AnalyzeLp() {
 // linear expression == rhs, we can use this to propagate more!
 //
 // TODO(user): Also propagate on -cut ? in practice we already do that in many
-// places were we try to generate the cut on -cut... But we coould do it sooner
+// places were we try to generate the cut on -cut... But we could do it sooner
 // and more cleanly here.
 bool LinearProgrammingConstraint::PreprocessCut(IntegerVariable first_slack,
                                                 CutData* cut) {

ortools/sat/linear_relaxation.cc

@@ -1302,7 +1302,10 @@ void AppendLinearConstraintRelaxation(const ConstraintProto& ct,
       const IntegerVariable int_var = mapping->Integer(ref);
       lc.AddTerm(int_var, coeff);
     }
-    relaxation->linear_constraints.push_back(lc.Build());
+    LinearConstraint built_ct = lc.Build();
+    if (!PossibleOverflow(*integer_trail, built_ct)) {
+      relaxation->linear_constraints.push_back(std::move(built_ct));
+    }
   }
   if (rhs_domain_max < max_activity) {
     // And(ei) => terms <= rhs_domain_max
@@ -1319,7 +1322,10 @@ void AppendLinearConstraintRelaxation(const ConstraintProto& ct,
       const IntegerVariable int_var = mapping->Integer(ref);
       lc.AddTerm(int_var, coeff);
     }
-    relaxation->linear_constraints.push_back(lc.Build());
+    LinearConstraint built_ct = lc.Build();
+    if (!PossibleOverflow(*integer_trail, built_ct)) {
+      relaxation->linear_constraints.push_back(std::move(built_ct));
+    }
   }
 }
 

ortools/sat/python/BUILD.bazel

@@ -23,6 +23,7 @@ cc_library(
     hdrs = ["linear_expr.h"],
     deps = [
         "//ortools/sat:cp_model_cc_proto",
+        "//ortools/util:fp_roundtrip_conv",
         "//ortools/util:sorted_interval_list",
         "@com_google_absl//absl/container:btree",
         "@com_google_absl//absl/container:fixed_array",

ortools/sat/python/cp_model.py

@@ -721,7 +721,7 @@ def new_int_var_series(
         if not isinstance(index, pd.Index):
             raise TypeError("Non-index object is used as index")
         if not name.isidentifier():
-            raise ValueError(f"name={name} is not a valid identifier")
+            raise ValueError(f"name={name!r} is not a valid identifier")
         if (
             isinstance(lower_bounds, IntegralTypes)
             and isinstance(upper_bounds, IntegralTypes)
@@ -775,7 +775,7 @@ def new_bool_var_series(
         if not isinstance(index, pd.Index):
             raise TypeError("Non-index object is used as index")
         if not name.isidentifier():
-            raise ValueError(f"name={name} is not a valid identifier")
+            raise ValueError(f"name={name!r} is not a valid identifier")
         return pd.Series(
             index=index,
             data=[
@@ -824,17 +824,9 @@ def add_linear_expression_in_domain(
             else:
                 return self.add_bool_and([])  # Evaluate to true.
         raise TypeError(
-            "not supported: CpModel.add_linear_expression_in_domain("
-            + str(linear_expr)
-            + " "
-            + str(type(linear_expr))
-            + " "
-            + str(linear_expr.is_integer())
-            + " "
-            + str(domain)
-            + " "
-            + str(type(domain))
-            + ")"
+            f"not supported: CpModel.add_linear_expression_in_domain({linear_expr} "
+            f" {type(linear_expr)} {linear_expr.is_integer()} {domain} "
+            f"{type(domain)}"
         )
 
     def add(self, ct: Union[BoundedLinearExpression, bool, np.bool_]) -> Constraint:
@@ -1642,7 +1634,7 @@ def new_interval_var_series(
         if not isinstance(index, pd.Index):
             raise TypeError("Non-index object is used as index")
         if not name.isidentifier():
-            raise ValueError(f"name={name} is not a valid identifier")
+            raise ValueError(f"name={name!r} is not a valid identifier")
 
         starts = _convert_to_linear_expr_series_and_validate_index(starts, index)
         sizes = _convert_to_linear_expr_series_and_validate_index(sizes, index)
@@ -1715,7 +1707,7 @@ def new_fixed_size_interval_var_series(
         if not isinstance(index, pd.Index):
             raise TypeError("Non-index object is used as index")
         if not name.isidentifier():
-            raise ValueError(f"name={name} is not a valid identifier")
+            raise ValueError(f"name={name!r} is not a valid identifier")
 
         starts = _convert_to_linear_expr_series_and_validate_index(starts, index)
         sizes = _convert_to_integral_series_and_validate_index(sizes, index)
@@ -1819,7 +1811,7 @@ def new_optional_interval_var_series(
         if not isinstance(index, pd.Index):
             raise TypeError("Non-index object is used as index")
         if not name.isidentifier():
-            raise ValueError(f"name={name} is not a valid identifier")
+            raise ValueError(f"name={name!r} is not a valid identifier")
 
         starts = _convert_to_linear_expr_series_and_validate_index(starts, index)
         sizes = _convert_to_linear_expr_series_and_validate_index(sizes, index)
@@ -1913,7 +1905,7 @@ def new_optional_fixed_size_interval_var_series(
         if not isinstance(index, pd.Index):
             raise TypeError("Non-index object is used as index")
         if not name.isidentifier():
-            raise ValueError(f"name={name} is not a valid identifier")
+            raise ValueError(f"name={name!r} is not a valid identifier")
 
         starts = _convert_to_linear_expr_series_and_validate_index(starts, index)
         sizes = _convert_to_integral_series_and_validate_index(sizes, index)
@@ -2857,7 +2849,8 @@ def on_solution_callback(self) -> None:
         obj = self.objective_value
         print(
             f"Solution {self.__solution_count}, time ="
-            f" {current_time - self.__start_time:0.2f} s, objective = {obj}"
+            f" {current_time - self.__start_time:0.2f} s, objective = {obj}",
+            flush=True,
         )
         self.__solution_count += 1
 
@@ -2885,7 +2878,7 @@ def on_solution_callback(self) -> None:
         )
         for v in self.__variables:
             print(f"  {v} = {self.value(v)}", end=" ")
-        print()
+        print(flush=True)
         self.__solution_count += 1
 
     @property
@@ -2912,7 +2905,7 @@ def on_solution_callback(self) -> None:
         )
         for v in self.__variables:
             print(f"  {v} = {self.value(v)}", end=" ")
-        print()
+        print(flush=True)
         self.__solution_count += 1
 
     @property