From 49b1bd617c5952993484ef28889b2e861de52fd4 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Fri, 27 Jul 2018 14:03:55 -0700 Subject: [PATCH] fix crash in presolve; minor reorg of the code --- ortools/base/hash.h | 6 +++--- ortools/flatzinc/cp_model_fz_solver.cc | 10 +++++----- ortools/linear_solver/linear_solver.h | 2 +- ortools/linear_solver/linear_solver.proto | 2 +- ortools/sat/cp_model_checker.cc | 1 - ortools/sat/cp_model_expand.cc | 9 ++------- ortools/sat/cp_model_presolve.cc | 9 ++++++++- 7 files changed, 20 insertions(+), 19 deletions(-) diff --git a/ortools/base/hash.h b/ortools/base/hash.h index c2ab2e444c..75e455505f 100644 --- a/ortools/base/hash.h +++ b/ortools/base/hash.h @@ -143,6 +143,8 @@ struct hash> { }; } // 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_ diff --git a/ortools/flatzinc/cp_model_fz_solver.cc b/ortools/flatzinc/cp_model_fz_solver.cc index 5edeb313b1..94e16fb6b8 100644 --- a/ortools/flatzinc/cp_model_fz_solver.cc +++ b/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" || diff --git a/ortools/linear_solver/linear_solver.h b/ortools/linear_solver/linear_solver.h index bfc7cfdcb5..425147c295 100644 --- a/ortools/linear_solver/linear_solver.h +++ b/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 { diff --git a/ortools/linear_solver/linear_solver.proto b/ortools/linear_solver/linear_solver.proto index a566962064..08c5119892 100644 --- a/ortools/linear_solver/linear_solver.proto +++ b/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 { diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index afd0d647cd..0918bf7213 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/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)); diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index a9b4a110ad..5d47cd3d10 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/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; } diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 36a8b2ffc7..663fab6e32 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/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)); }