From 0d67f77de700238c33e378b5a9197a581aa01556 Mon Sep 17 00:00:00 2001
From: Laurent Perron <lperron@google.com>
Date: Wed, 13 Oct 2021 17:12:10 +0200
Subject: [PATCH] [CP-SAT] reorder struct; fix presolve bug in cumulative

---
 ortools/sat/cp_model_checker.cc  |  7 ++++++-
 ortools/sat/cp_model_loader.cc   |  4 ++--
 ortools/sat/cp_model_presolve.cc | 18 ++++++++----------
 ortools/sat/integer.h            | 14 ++++++++------
 4 files changed, 24 insertions(+), 19 deletions(-)

diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc
index b1ceba21ff..3369edf642 100644
--- a/ortools/sat/cp_model_checker.cc
+++ b/ortools/sat/cp_model_checker.cc
@@ -1226,7 +1226,11 @@ class ConstraintChecker {
         const int64_t demand = Value(ct.cumulative().demands(i));
         for (int64_t t = start; t < start + duration; ++t) {
           usage[t] += demand;
-          if (usage[t] > capacity) return false;
+          if (usage[t] > capacity) {
+            VLOG(1) << "time: " << t << " usage: " << usage[t]
+                    << " capa: " << capacity;
+            return false;
+          }
         }
         if (!ct.cumulative().energies().empty()) {
           const LinearExpressionProto& energy_expr =
@@ -1236,6 +1240,7 @@ class ConstraintChecker {
             energy += Value(energy_expr.vars(j)) * energy_expr.coeffs(j);
           }
           if (duration * demand != energy) {
+            VLOG(1) << "duration * demand is not equal to energy";
             return false;
           }
         }
diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc
index 1789d69175..def86c6f6a 100644
--- a/ortools/sat/cp_model_loader.cc
+++ b/ortools/sat/cp_model_loader.cc
@@ -1124,8 +1124,8 @@ void LoadIntProdConstraint(const ConstraintProto& ct, Model* m) {
       mapping->Integers(ct.int_prod().vars());
   CHECK_EQ(vars.size(), 2) << "General int_prod not supported yet.";
   if (VLOG_IS_ON(1)) {
-    if (DetectLinearEncodingOfProducts(vars[0], vars[1], m,
-                                       /*product_encoding=*/nullptr)) {
+    std::vector<ValueLiteralPair> encoding;
+    if (DetectLinearEncodingOfProducts(vars[0], vars[1], m, &encoding)) {
       VLOG(1) << "Product " << ct.DebugString() << " can be linearized";
     }
   }
diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc
index 39f26a0eaa..0304d638b8 100644
--- a/ortools/sat/cp_model_presolve.cc
+++ b/ortools/sat/cp_model_presolve.cc
@@ -4095,7 +4095,6 @@ bool CpModelPresolver::PresolveCumulative(ConstraintProto* ct) {
 
   CumulativeConstraintProto* proto = ct->mutable_cumulative();
   bool changed = false;
-  int num_fixed_demands = 0;
   const int64_t capacity_max = context_->MaxOf(proto->capacity());
 
   // Checks the capacity of the constraint.
@@ -4126,9 +4125,6 @@ bool CpModelPresolver::PresolveCumulative(ConstraintProto* ct) {
         num_zero_demand_removed++;
         continue;
       }
-      if (context_->IsFixed(demand_ref)) {
-        num_fixed_demands++;
-      }
 
       if (context_->SizeMax(proto->intervals(i)) == 0) {
         // Size 0 intervals cannot contribute to a cumulative.
@@ -4360,12 +4356,16 @@ bool CpModelPresolver::PresolveCumulative(ConstraintProto* ct) {
     }
   }
 
-  if (num_fixed_demands == proto->intervals_size() &&
-      context_->IsFixed(proto->capacity())) {
+  if (context_->IsFixed(proto->capacity())) {
     int64_t gcd = 0;
     for (int i = 0; i < ct->cumulative().demands_size(); ++i) {
-      const int64_t demand = context_->MinOf(ct->cumulative().demands(i));
-      gcd = MathUtil::GCD64(gcd, demand);
+      const int demand_ref = ct->cumulative().demands(i);
+      if (!context_->IsFixed(demand_ref)) {
+        // Abort if the demand is not fixed.
+        gcd = 1;
+        break;
+      }
+      gcd = MathUtil::GCD64(gcd, context_->MinOf(demand_ref));
       if (gcd == 1) break;
     }
     if (gcd > 1) {
@@ -4392,8 +4392,6 @@ bool CpModelPresolver::PresolveCumulative(ConstraintProto* ct) {
     changed |= CanonicalizeLinearExpression(*ct, &exp);
   }
 
-  if (HasEnforcementLiteral(*ct)) return changed;
-
   const int num_intervals = proto->intervals_size();
   const int capacity_ref = proto->capacity();
 
diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h
index 56cd4c1641..0e834ab022 100644
--- a/ortools/sat/integer.h
+++ b/ortools/sat/integer.h
@@ -287,12 +287,6 @@ struct DebugSolution
 
 // A value and a literal.
 struct ValueLiteralPair {
-  bool operator==(const ValueLiteralPair& o) const {
-    return value == o.value && literal == o.literal;
-  }
-
-  IntegerValue value = IntegerValue(0);
-  Literal literal = Literal(kNoLiteralIndex);
   struct CompareByLiteral {
     bool operator()(const ValueLiteralPair& a,
                     const ValueLiteralPair& b) const {
@@ -306,7 +300,15 @@ struct ValueLiteralPair {
              (a.value == b.value && a.literal < b.literal);
     }
   };
+
+  bool operator==(const ValueLiteralPair& o) const {
+    return value == o.value && literal == o.literal;
+  }
+
   std::string DebugString() const;
+
+  IntegerValue value = IntegerValue(0);
+  Literal literal = Literal(kNoLiteralIndex);
 };
 
 std::ostream& operator<<(std::ostream& os, const ValueLiteralPair& p);