[CP-SAT] add more CpModel C++ methods; fix #3248; fix #3251; specify restrictions in cp_model.proto

ortools/sat/cp_model.h

@@ -19,15 +19,15 @@
  * print out the solution.
  * \code
  CpModelBuilder cp_model;
- Domain all_animals(0, 20);
- IntVar rabbits = cp_model.NewIntVar(all_animals).WithName("rabbits");
- IntVar pheasants = cp_model.NewIntVar(all_animals).WithName("pheasants");
+ const Domain all_animals(0, 20);
+ const IntVar rabbits = cp_model.NewIntVar(all_animals).WithName("rabbits");
+ const IntVar pheasants = cp_model.NewIntVar(all_animals).WithName("pheasants");
 
  cp_model.AddEquality(rabbits + pheasants, 20);
  cp_model.AddEquality(4 * rabbits + 2 * pheasants, 56);
 
  const CpSolverResponse response = Solve(cp_model.Build());
- if (response.status() == CpSolverStatus::FEASIBLE) {
+ if (response.status() == CpSolverStatus::OPTIMAL) {
    LOG(INFO) << SolutionIntegerValue(response, rabbits)
              << " rabbits, and " << SolutionIntegerValue(response, pheasants)
              << " pheasants.";
@@ -314,13 +314,7 @@ std::ostream& operator<<(std::ostream& os, const LinearExpr& e);
 
 /**
  * A dedicated container for linear expressions with double coefficients.
- *
- * This class helps building and manipulating linear expressions.
- * Note that Not(x) will be silently transformed into 1 - x when added to the
- * linear expression.
- *
- * Furthermore, static methods allows sums and scalar products, with or without
- * an additional constant.
+ * This is currently only usable to define a floating point objective.
  *
  * Usage:
  * \code
@@ -531,7 +525,7 @@ class Constraint {
    * (controlled by a literal l) and its negation (controlled by the negation of
    * l).
    *
-   * Important: as of September 2018, only a few constraint support enforcement:
+   * [Important] currently, only a few constraints support enforcement:
    * - bool_or, bool_and, linear: fully supported.
    * - interval: only support a single enforcement literal.
    * - other: no support (but can be added on a per-demand basis).
@@ -777,7 +771,7 @@ class CpModelBuilder {
   /// Adds the constraint that at least one of the literals must be true.
   Constraint AddBoolOr(absl::Span<const BoolVar> literals);
 
-  /// Same as AddBoolOr. Sum literals >= 1.
+  /// Same as AddBoolOr(). Sum literals >= 1.
   Constraint AddAtLeastOne(absl::Span<const BoolVar> literals);
 
   /// At most one literal is true. Sum literals <= 1.
@@ -797,6 +791,12 @@ class CpModelBuilder {
     return AddBoolOr({a.Not(), b});
   }
 
+  /// Adds implication: if all lhs vars are true then all rhs vars must be true.
+  Constraint AddImplication(absl::Span<const BoolVar> lhs,
+                            absl::Span<const BoolVar> rhs) {
+    return AddBoolAnd(rhs).OnlyEnforceIf(lhs);
+  }
+
   /// Adds left == right.
   Constraint AddEquality(const LinearExpr& left, const LinearExpr& right);
 
@@ -1029,15 +1029,15 @@ class CpModelBuilder {
   /// Adds a linear minimization objective.
   void Minimize(const LinearExpr& expr);
 
-  /// Adds a linear minimization objective after rescaling of the double
-  /// coefficients.
+  /// Adds a linear floating point minimization objective.
+  /// Note that the coefficients will be internally scaled to integer.
   void Minimize(const DoubleLinearExpr& expr);
 
   /// Adds a linear maximization objective.
   void Maximize(const LinearExpr& expr);
 
-  /// Adds a linear maximization objective after rescaling of the double
-  /// coefficients.
+  /// Adds a linear floating point maximization objective.
+  /// Note that the coefficients will be internally scaled to integer.
   void Maximize(const DoubleLinearExpr& expr);
 
   /// Adds a decision strategy on a list of integer variables.
@@ -1070,8 +1070,7 @@ class CpModelBuilder {
   /// Remove all assumptions from the model.
   void ClearAssumptions();
 
-  const CpModelProto& Build() const { return Proto(); }
-
+  const CpModelProto& Build() const { return cp_model_; }
   const CpModelProto& Proto() const { return cp_model_; }
   CpModelProto* MutableProto() { return &cp_model_; }
 

ortools/sat/cp_model.proto

@@ -150,6 +150,10 @@ message NoOverlap2DConstraintProto {
 // a capacity. Note that intervals are interpreted as [start, end) and as
 // such intervals like [2,3) and [3,4) do not overlap for the point of view of
 // this constraint. Moreover, intervals of size zero are ignored.
+//
+// All demands must not contain any negative value in their domains. This is
+// checked at validation. The capacity can currently contains negative values,
+// but it will be propagated to >= 0 right away.
 message CumulativeConstraintProto {
   LinearExpressionProto capacity = 1;
   repeated int32 intervals = 2;

ortools/sat/timetable.cc

@@ -366,7 +366,7 @@ bool TimeTablingPerTask::BuildProfile() {
   profile_.clear();
 
   // Start and height of the highest profile rectangle.
-  profile_max_height_ = kMinIntegerValue;
+  profile_max_height_ = 0;
   IntegerValue max_height_start = kMinIntegerValue;
 
   // Add a sentinel to simplify the algorithm.
@@ -435,8 +435,7 @@ void TimeTablingPerTask::ReverseProfile() {
 
 bool TimeTablingPerTask::SweepAllTasks() {
   // Tasks with a lower or equal demand will not be pushed.
-  const IntegerValue demand_threshold(
-      CapSub(CapacityMax().value(), profile_max_height_.value()));
+  const IntegerValue demand_threshold = CapacityMax() - profile_max_height_;
 
   // TODO(user): On some problem, a big chunk of the time is spend just checking
   // these conditions below because it requires indirect memory access to fetch
@@ -562,6 +561,10 @@ bool TimeTablingPerTask::UpdateStartingTime(int task_id, IntegerValue left,
                                             IntegerValue right) {
   helper_->ClearReason();
   AddProfileReason(task_id, left, right);
+  if (capacity_.var != kNoIntegerVariable) {
+    helper_->MutableIntegerReason()->push_back(
+        integer_trail_->UpperBoundAsLiteral(capacity_.var));
+  }
 
   // State of the task to be pushed.
   helper_->AddEndMinReason(task_id, left + 1);
@@ -655,9 +658,6 @@ bool TimeTablingPerTask::IncreaseCapacity(IntegerValue time,
   if (capacity_.var == kNoIntegerVariable) {
     return helper_->ReportConflict();
   }
-
-  helper_->MutableIntegerReason()->push_back(
-      integer_trail_->UpperBoundAsLiteral(capacity_.var));
   return helper_->PushIntegerLiteral(capacity_.GreaterOrEqual(new_min));
 }