cp_model.h

Go to the documentation of this file.

// Copyright 2010-2018 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
 
#ifndef OR_TOOLS_SAT_CP_MODEL_H_
#define OR_TOOLS_SAT_CP_MODEL_H_
 
#include <string>
 
#include "absl/container/flat_hash_map.h"
#include "absl/types/span.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/sat/cp_model_utils.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/util/sorted_interval_list.h"
 
namespace operations_research {
namespace sat {
 
class CpModelBuilder;
class LinearExpr;
class IntVar;
 
class BoolVar {
 public:
  BoolVar();
 
  BoolVar WithName(const std::string& name);
 
  const std::string& Name() const { return Proto().name(); }
 
  BoolVar Not() const { return BoolVar(NegatedRef(index_), cp_model_); }
 
  bool operator==(const BoolVar& other) const {
    return other.cp_model_ == cp_model_ && other.index_ == index_;
  }
 
  bool operator!=(const BoolVar& other) const {
    return other.cp_model_ != cp_model_ || other.index_ != index_;
  }
 
  std::string DebugString() const;
 
  const IntegerVariableProto& Proto() const {
    return cp_model_->variables(index_);
  }
 
  IntegerVariableProto* MutableProto() const {
    return cp_model_->mutable_variables(index_);
  }
 
  int index() const { return index_; }
 
 private:
  friend class CircuitConstraint;
  friend class Constraint;
  friend class CpModelBuilder;
  friend class IntVar;
  friend class IntervalVar;
  friend class MultipleCircuitConstraint;
  friend class LinearExpr;
  friend class ReservoirConstraint;
  friend bool SolutionBooleanValue(const CpSolverResponse& r, BoolVar x);
 
  BoolVar(int index, CpModelProto* cp_model);
 
  CpModelProto* cp_model_ = nullptr;
  int index_ = kint32min;
};
 
std::ostream& operator<<(std::ostream& os, const BoolVar& var);
 
BoolVar Not(BoolVar x);
 
class IntVar {
 public:
  IntVar();
 
  IntVar(const BoolVar& var);  // NOLINT(runtime/explicit)
 
  BoolVar ToBoolVar() const;
 
  IntVar WithName(const std::string& name);
 
  const std::string& Name() const { return Proto().name(); }
 
  LinearExpr AddConstant(int64 value) const;
 
  bool operator==(const IntVar& other) const {
    return other.cp_model_ == cp_model_ && other.index_ == index_;
  }
 
  bool operator!=(const IntVar& other) const {
    return other.cp_model_ != cp_model_ || other.index_ != index_;
  }
 
  std::string DebugString() const;
 
  const IntegerVariableProto& Proto() const {
    return cp_model_->variables(index_);
  }
 
  IntegerVariableProto* MutableProto() const {
    return cp_model_->mutable_variables(index_);
  }
 
  int index() const { return index_; }
 
 private:
  friend class BoolVar;
  friend class CpModelBuilder;
  friend class CumulativeConstraint;
  friend class LinearExpr;
  friend class IntervalVar;
  friend class ReservoirConstraint;
  friend int64 SolutionIntegerValue(const CpSolverResponse& r,
                                    const LinearExpr& expr);
  friend int64 SolutionIntegerMin(const CpSolverResponse& r, IntVar x);
  friend int64 SolutionIntegerMax(const CpSolverResponse& r, IntVar x);
 
  IntVar(int index, CpModelProto* cp_model);
 
  CpModelProto* cp_model_ = nullptr;
  int index_ = kint32min;
};
 
std::ostream& operator<<(std::ostream& os, const IntVar& var);
 
class LinearExpr {
 public:
  LinearExpr();
 
  LinearExpr(BoolVar var);  // NOLINT(runtime/explicit)
 
  LinearExpr(IntVar var);  // NOLINT(runtime/explicit)
 
  LinearExpr(int64 constant);  // NOLINT(runtime/explicit)
 
  LinearExpr& AddConstant(int64 value);
 
  void AddVar(IntVar var);
 
  void AddTerm(IntVar var, int64 coeff);
 
  static LinearExpr Sum(absl::Span<const IntVar> vars);
 
  static LinearExpr ScalProd(absl::Span<const IntVar> vars,
                             absl::Span<const int64> coeffs);
 
  static LinearExpr BooleanSum(absl::Span<const BoolVar> vars);
 
  static LinearExpr BooleanScalProd(absl::Span<const BoolVar> vars,
                                    absl::Span<const int64> coeffs);
  static LinearExpr Term(IntVar var, int64 coefficient);
 
  const std::vector<IntVar>& variables() const { return variables_; }
 
  const std::vector<int64>& coefficients() const { return coefficients_; }
 
  int64 constant() const { return constant_; }
 
  // TODO(user): LinearExpr.DebugString() and operator<<.
 
 private:
  std::vector<IntVar> variables_;
  std::vector<int64> coefficients_;
  int64 constant_ = 0;
};
 
class IntervalVar {
 public:
  IntervalVar();
 
  IntervalVar WithName(const std::string& name);
 
  std::string Name() const;
 
  IntVar StartVar() const;
 
  IntVar SizeVar() const;
 
  IntVar EndVar() const;
 
  BoolVar PresenceBoolVar() const;
 
  bool operator==(const IntervalVar& other) const {
    return other.cp_model_ == cp_model_ && other.index_ == index_;
  }
 
  bool operator!=(const IntervalVar& other) const {
    return other.cp_model_ != cp_model_ || other.index_ != index_;
  }
 
  std::string DebugString() const;
 
  const IntervalConstraintProto& Proto() const {
    return cp_model_->constraints(index_).interval();
  }
 
  IntervalConstraintProto* MutableProto() const {
    return cp_model_->mutable_constraints(index_)->mutable_interval();
  }
 
  int index() const { return index_; }
 
 private:
  friend class CpModelBuilder;
  friend class CumulativeConstraint;
  friend class NoOverlap2DConstraint;
  friend std::ostream& operator<<(std::ostream& os, const IntervalVar& var);
 
  IntervalVar(int index, CpModelProto* cp_model);
 
  CpModelProto* cp_model_ = nullptr;
  int index_ = kint32min;
};
 
std::ostream& operator<<(std::ostream& os, const IntervalVar& var);
 
class Constraint {
 public:
  Constraint OnlyEnforceIf(absl::Span<const BoolVar> literals);
 
  Constraint OnlyEnforceIf(BoolVar literal);
 
  Constraint WithName(const std::string& name);
 
  const std::string& Name() const;
 
  const ConstraintProto& Proto() const { return *proto_; }
 
  ConstraintProto* MutableProto() const { return proto_; }
 
 protected:
  friend class CpModelBuilder;
 
  explicit Constraint(ConstraintProto* proto);
 
  ConstraintProto* proto_ = nullptr;
};
 
class CircuitConstraint : public Constraint {
 public:
  void AddArc(int tail, int head, BoolVar literal);
 
 private:
  friend class CpModelBuilder;
 
  using Constraint::Constraint;
};
 
class MultipleCircuitConstraint : public Constraint {
 public:
  void AddArc(int tail, int head, BoolVar literal);
 
 private:
  friend class CpModelBuilder;
 
  using Constraint::Constraint;
};
 
class TableConstraint : public Constraint {
 public:
  void AddTuple(absl::Span<const int64> tuple);
 
 private:
  friend class CpModelBuilder;
 
  using Constraint::Constraint;
};
 
class ReservoirConstraint : public Constraint {
 public:
  void AddEvent(IntVar time, int64 demand);
 
  void AddOptionalEvent(IntVar time, int64 demand, BoolVar is_active);
 
 private:
  friend class CpModelBuilder;
 
  ReservoirConstraint(ConstraintProto* proto, CpModelBuilder* builder);
 
  CpModelBuilder* builder_;
};
 
class AutomatonConstraint : public Constraint {
 public:
  void AddTransition(int tail, int head, int64 transition_label);
 
 private:
  friend class CpModelBuilder;
 
  using Constraint::Constraint;
};
 
class NoOverlap2DConstraint : public Constraint {
 public:
  void AddRectangle(IntervalVar x_coordinate, IntervalVar y_coordinate);
 
 private:
  friend class CpModelBuilder;
 
  using Constraint::Constraint;
};
 
class CumulativeConstraint : public Constraint {
 public:
  void AddDemand(IntervalVar interval, IntVar demand);
 
 private:
  friend class CpModelBuilder;
 
  CumulativeConstraint(ConstraintProto* proto, CpModelBuilder* builder);
 
  CpModelBuilder* builder_;
};
 
class CpModelBuilder {
 public:
  IntVar NewIntVar(const Domain& domain);
 
  BoolVar NewBoolVar();
 
  IntVar NewConstant(int64 value);
 
  BoolVar TrueVar();
 
  BoolVar FalseVar();
 
  IntervalVar NewIntervalVar(IntVar start, IntVar size, IntVar end);
 
  IntervalVar NewOptionalIntervalVar(IntVar start, IntVar size, IntVar end,
                                     BoolVar presence);
 
  Constraint AddBoolOr(absl::Span<const BoolVar> literals);
 
  Constraint AddBoolAnd(absl::Span<const BoolVar> literals);
 
  Constraint AddBoolXor(absl::Span<const BoolVar> literals);
 
  Constraint AddImplication(BoolVar a, BoolVar b) {
    return AddBoolOr({a.Not(), b});
  }
 
  Constraint AddEquality(const LinearExpr& left, const LinearExpr& right);
 
  Constraint AddGreaterOrEqual(const LinearExpr& left, const LinearExpr& right);
 
  Constraint AddGreaterThan(const LinearExpr& left, const LinearExpr& right);
 
  Constraint AddLessOrEqual(const LinearExpr& left, const LinearExpr& right);
 
  Constraint AddLessThan(const LinearExpr& left, const LinearExpr& right);
 
  Constraint AddLinearConstraint(const LinearExpr& expr, const Domain& domain);
 
  Constraint AddNotEqual(const LinearExpr& left, const LinearExpr& right);
 
  Constraint AddAllDifferent(absl::Span<const IntVar> vars);
 
  Constraint AddVariableElement(IntVar index,
                                absl::Span<const IntVar> variables,
                                IntVar target);
 
  Constraint AddElement(IntVar index, absl::Span<const int64> values,
                        IntVar target);
 
  CircuitConstraint AddCircuitConstraint();
 
  MultipleCircuitConstraint AddMultipleCircuitConstraint();
 
  TableConstraint AddAllowedAssignments(absl::Span<const IntVar> vars);
 
  TableConstraint AddForbiddenAssignments(absl::Span<const IntVar> vars);
 
  Constraint AddInverseConstraint(absl::Span<const IntVar> variables,
                                  absl::Span<const IntVar> inverse_variables);
 
  ReservoirConstraint AddReservoirConstraint(int64 min_level, int64 max_level);
 
  AutomatonConstraint AddAutomaton(
      absl::Span<const IntVar> transition_variables, int starting_state,
      absl::Span<const int> final_states);
 
  Constraint AddMinEquality(IntVar target, absl::Span<const IntVar> vars);
 
  Constraint AddLinMinEquality(const LinearExpr& target,
                               absl::Span<const LinearExpr> exprs);
 
  Constraint AddMaxEquality(IntVar target, absl::Span<const IntVar> vars);
 
  Constraint AddLinMaxEquality(const LinearExpr& target,
                               absl::Span<const LinearExpr> exprs);
 
  Constraint AddDivisionEquality(IntVar target, IntVar numerator,
                                 IntVar denominator);
 
  Constraint AddAbsEquality(IntVar target, IntVar var);
 
  Constraint AddModuloEquality(IntVar target, IntVar var, IntVar mod);
 
  Constraint AddProductEquality(IntVar target, absl::Span<const IntVar> vars);
 
  Constraint AddNoOverlap(absl::Span<const IntervalVar> vars);
 
  NoOverlap2DConstraint AddNoOverlap2D();
 
  CumulativeConstraint AddCumulative(IntVar capacity);
 
  void Minimize(const LinearExpr& expr);
 
  void Maximize(const LinearExpr& expr);
 
  void ScaleObjectiveBy(double scaling);
 
  void AddDecisionStrategy(
      absl::Span<const IntVar> variables,
      DecisionStrategyProto::VariableSelectionStrategy var_strategy,
      DecisionStrategyProto::DomainReductionStrategy domain_strategy);
 
  void AddDecisionStrategy(
      absl::Span<const BoolVar> variables,
      DecisionStrategyProto::VariableSelectionStrategy var_strategy,
      DecisionStrategyProto::DomainReductionStrategy domain_strategy);
 
  void AddHint(IntVar var, int64 value);
 
  // TODO(user) : add MapDomain?
 
  const CpModelProto& Build() const { return Proto(); }
 
  const CpModelProto& Proto() const { return cp_model_; }
  CpModelProto* MutableProto() { return &cp_model_; }
 
 private:
  friend class CumulativeConstraint;
  friend class ReservoirConstraint;
 
  // Fills the 'expr_proto' with the linear expression represented by 'expr'.
  void LinearExprToProto(const LinearExpr& expr,
                         LinearExpressionProto* expr_proto);
 
  // Returns a (cached) integer variable index with a constant value.
  int IndexFromConstant(int64 value);
 
  // Returns a valid integer index from a BoolVar index.
  // If the input index is a positive, it returns this index.
  // If the input index is negative, it creates a cached IntVar equal to
  // 1 - BoolVar(PositiveRef(index)), and returns the index of this new
  // variable.
  int GetOrCreateIntegerIndex(int index);
 
  void FillLinearTerms(const LinearExpr& left, const LinearExpr& right,
                       LinearConstraintProto* proto);
 
  CpModelProto cp_model_;
  absl::flat_hash_map<int64, int> constant_to_index_map_;
  absl::flat_hash_map<int, int> bool_to_integer_index_map_;
};
 
int64 SolutionIntegerValue(const CpSolverResponse& r, const LinearExpr& expr);
 
int64 SolutionIntegerMin(const CpSolverResponse& r, IntVar x);
 
int64 SolutionIntegerMax(const CpSolverResponse& r, IntVar x);
 
bool SolutionBooleanValue(const CpSolverResponse& r, BoolVar x);
 
}  // namespace sat
}  // namespace operations_research
 
#endif  // OR_TOOLS_SAT_CP_MODEL_H_