fix crash in presolve; minor reorg of the code

ortools/base/hash.h

@@ -143,6 +143,8 @@ struct hash<std::array<T, N>> {
 };
 }  // namespace std
 
+#endif  // SWIG
+
 namespace util_hash {
 
 inline uint64 Hash(uint64 num, uint64 c) {
@@ -151,8 +153,6 @@ inline uint64 Hash(uint64 num, uint64 c) {
   return c;
 }
 
-}  // namespace hash
-
-#endif  // SWIG
+}  // namespace util_hash
 
 #endif  // OR_TOOLS_BASE_HASH_H_

ortools/flatzinc/cp_model_fz_solver.cc

@@ -304,11 +304,6 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
     arg->set_target(LookupVar(fz_ct.arguments[2]));
     arg->add_vars(LookupVar(fz_ct.arguments[0]));
     arg->add_vars(LookupVar(fz_ct.arguments[1]));
-  } else if (fz_ct.type == "int_mod") {
-    auto* arg = ct->mutable_int_mod();
-    arg->set_target(LookupVar(fz_ct.arguments[2]));
-    arg->add_vars(LookupVar(fz_ct.arguments[0]));
-    arg->add_vars(LookupVar(fz_ct.arguments[1]));
   } else if (fz_ct.type == "int_abs") {
     auto* arg = ct->mutable_int_max();
     arg->set_target(LookupVar(fz_ct.arguments[1]));
@@ -328,6 +323,11 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
     arg->add_vars(LookupVar(fz_ct.arguments[0]));
     arg->add_vars(LookupVar(fz_ct.arguments[1]));
     arg->set_target(LookupVar(fz_ct.arguments[2]));
+  } else if (fz_ct.type == "int_mod") {
+    auto* arg = ct->mutable_int_mod();
+    arg->set_target(LookupVar(fz_ct.arguments[2]));
+    arg->add_vars(LookupVar(fz_ct.arguments[0]));
+    arg->add_vars(LookupVar(fz_ct.arguments[1]));
   } else if (fz_ct.type == "array_int_element" ||
              fz_ct.type == "array_bool_element" ||
              fz_ct.type == "array_var_int_element" ||

ortools/linear_solver/linear_solver.h

@@ -330,7 +330,7 @@ class MPSolver {
   // ----- Solve -----
 
   // The status of solving the problem. The straightforward translation to
-  // homonymous enum values of MPSolutionResponse::Status
+  // homonymous enum values of MPSolverResponseStatus
   // (see ./linear_solver.proto) is guaranteed by ./enum_consistency_test.cc,
   // you may rely on it.
   enum ResultStatus {

ortools/linear_solver/linear_solver.proto

@@ -276,7 +276,7 @@ message MPModelRequest {
 //
 // bool InCategory(MPSolverResponseStatus status, MPSolverResponseStatus cat) {
 //   if (cat == MPSOLVER_OPTIMAL) return status == MPSOLVER_OPTIMAL;
-//   while (status > cat) status <<= 4;
+//   while (status > cat) status >>= 4;
 //   return status == cat;
 // }
 enum MPSolverResponseStatus {

ortools/sat/cp_model_checker.cc

@@ -373,7 +373,6 @@ class ConstraintChecker {
            Value(ct.int_div().vars(0)) / Value(ct.int_div().vars(1));
   }
 
-
   bool IntModConstraintIsFeasible(const ConstraintProto& ct) {
     return Value(ct.int_mod().target()) ==
            Value(ct.int_mod().vars(0)) % Value(ct.int_mod().vars(1));

ortools/sat/cp_model_expand.cc

@@ -48,13 +48,6 @@ struct ExpansionHelper {
     imply->mutable_linear()->add_domain(ub);
   }
 
-  int AddBoolVar() {
-    IntegerVariableProto* const var = expanded_proto.add_variables();
-    var->add_domain(0);
-    var->add_domain(1);
-    return expanded_proto.variables_size() - 1;
-  }
-
   int AddIntVar(int64 lb, int64 ub) {
     IntegerVariableProto* const var = expanded_proto.add_variables();
     var->add_domain(lb);
@@ -62,6 +55,8 @@ struct ExpansionHelper {
     return expanded_proto.variables_size() - 1;
   }
 
+  int AddBoolVar() { return AddIntVar(0, 1); }
+
   int VariableIsOptional(int index) const {
     return expanded_proto.variables(index).enforcement_literal_size() > 0;
   }

ortools/sat/cp_model_presolve.cc

@@ -122,7 +122,14 @@ struct PresolveContext {
   void SetLiteralToFalse(int lit) {
     const int var = PositiveRef(lit);
     const int64 value = RefIsPositive(lit) ? 0ll : 1ll;
-    IntersectDomainWith(var, {{value, value}});
+    if (IsFixed(var)) {
+      const int64 fixed_value = MinOf(var);
+      if (value != fixed_value) {
+        is_unsat = true;
+      }
+    } else {
+      IntersectDomainWith(var, {{value, value}});
+    }
   }
 
   void SetLiteralToTrue(int lit) { return SetLiteralToFalse(NegatedRef(lit)); }