more CP-SAT fuzzer fixes

ortools/sat/README.md

@@ -126,8 +126,6 @@ CP solver built on top of the SAT solver:
     Propagation algorithms for the cumulative scheduling constraint.
 *   [cumulative_energy.h](../sat/cumulative_energy.h):
     Propagation algorithms for a more general cumulative constraint.
-*   [theta_tree.h](../sat/theta_tree.h):
-    Data structure used in the cumulative/disjunctive propagation algorithm.
 
 ### Packing constraints
 

ortools/sat/cp_model_expand_test.cc

@@ -1876,46 +1876,18 @@ TEST(LinMaxExpansionTest, GoldenTest) {
     variables { domain: 0 domain: 1 }
     constraints {}
     constraints {
-      linear {
-        vars: 0
-        vars: 1
-        coeffs: 1
-        coeffs: -2
-        domain: -1
-        domain: 9223372036854775806
-      }
+      linear { vars: 0 vars: 1 coeffs: 1 coeffs: -2 domain: -1 domain: 5 }
     }
     constraints {
-      linear {
-        vars: 0
-        vars: 2
-        coeffs: 1
-        coeffs: -1
-        domain: -4
-        domain: 9223372036854775803
-      }
+      linear { vars: 0 vars: 2 coeffs: 1 coeffs: -1 domain: -4 domain: 5 }
     }
     constraints {
       enforcement_literal: 3
-      linear {
-        vars: 0
-        vars: 1
-        coeffs: 1
-        coeffs: -2
-        domain: -9223372036854775808
-        domain: -1
-      }
+      linear { vars: 0 vars: 1 coeffs: 1 coeffs: -2 domain: -10 domain: -1 }
     }
     constraints {
       enforcement_literal: -4
-      linear {
-        vars: 0
-        vars: 2
-        coeffs: 1
-        coeffs: -1
-        domain: -9223372036854775808
-        domain: -4
-      }
+      linear { vars: 0 vars: 2 coeffs: 1 coeffs: -1 domain: -6 domain: -4 }
     }
   )pb");
   EXPECT_THAT(initial_model, testing::EqualsProto(expected_model));

ortools/sat/presolve_context.cc

@@ -2657,10 +2657,18 @@ bool PresolveContext::CanonicalizeLinearConstraint(ConstraintProto* ct) {
   const bool result = CanonicalizeLinearExpressionInternal(
       ct->enforcement_literal(), ct->mutable_linear(), &offset, &tmp_terms_,
       this);
-  if (offset != 0) {
-    FillDomainInProto(
-        ReadDomainFromProto(ct->linear()).AdditionWith(Domain(-offset)),
-        ct->mutable_linear());
+  const auto [min_activity, max_activity] = ComputeMinMaxActivity(ct->linear());
+  const Domain implied = Domain(min_activity, max_activity);
+  const Domain original_domain =
+      ReadDomainFromProto(ct->linear()).AdditionWith(Domain(-offset));
+  const Domain tight_domain = implied.IntersectionWith(original_domain);
+  if (tight_domain.IsEmpty()) {
+    // Canonicalization is not the right place to handle unsat constraints.
+    // Let's just replace the domain by one that is overflow-safe.
+    const Domain bad_domain = Domain(implied.Max() + 1, implied.Max() + 2);
+    FillDomainInProto(bad_domain, ct->mutable_linear());
+  } else {
+    FillDomainInProto(tight_domain, ct->mutable_linear());
   }
   return result;
 }

ortools/sat/presolve_context_test.cc

@@ -1053,7 +1053,7 @@ TEST(PresolveContextTest, CanonicalizeLinearConstraint) {
     linear {
       vars: [ 0, 1, 2 ]
       coeffs: [ -2, 2, -2 ]
-      domain: [ 0, 1000 ]
+      domain: [ 0, 16 ]
     }
   )pb");
   EXPECT_THAT(working_model.constraints(0), testing::EqualsProto(expected));