CpModel.java

Go to the documentation of this file.

// Copyright 2010-2025 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.
 
package com.google.ortools.sat;
 
import com.google.ortools.sat.AllDifferentConstraintProto;
import com.google.ortools.sat.AutomatonConstraintProto;
import com.google.ortools.sat.BoolArgumentProto;
import com.google.ortools.sat.CpModelProto;
import com.google.ortools.sat.CpObjectiveProto;
import com.google.ortools.sat.CumulativeConstraintProto;
import com.google.ortools.sat.DecisionStrategyProto;
import com.google.ortools.sat.ElementConstraintProto;
import com.google.ortools.sat.FloatObjectiveProto;
import com.google.ortools.sat.InverseConstraintProto;
import com.google.ortools.sat.LinearArgumentProto;
import com.google.ortools.sat.LinearConstraintProto;
import com.google.ortools.sat.LinearExpressionProto;
import com.google.ortools.sat.NoOverlapConstraintProto;
import com.google.ortools.sat.ReservoirConstraintProto;
import com.google.ortools.sat.TableConstraintProto;
import com.google.ortools.util.Domain;
import java.util.Arrays;
import java.util.LinkedHashMap;
import java.util.Map;

public final class CpModel {
  static class CpModelException extends RuntimeException {
    public CpModelException(String methodName, String msg) {
      // Call constructor of parent Exception
      super(methodName + ": " + msg);
    }
  }

  public static class MismatchedArrayLengths extends CpModelException {
    public MismatchedArrayLengths(String methodName, String array1Name, String array2Name) {
      super(methodName, array1Name + " and " + array2Name + " have mismatched lengths");
    }
  }

  public static class WrongLength extends CpModelException {
    public WrongLength(String methodName, String msg) {
      super(methodName, msg);
    }
  }
 
  public CpModel() {
    modelBuilder = CpModelProto.newBuilder();
    constantMap = new LinkedHashMap<>();
  }
 
  public CpModel getClone() {
    CpModel clone = new CpModel();
    clone.modelBuilder.mergeFrom(modelBuilder.build());
    clone.constantMap.clear();
    clone.constantMap.putAll(constantMap);
    return clone;
  }
 
  // Integer variables.

  public IntVar newIntVar(long lb, long ub, String name) {
    return new IntVar(modelBuilder, new Domain(lb, ub), name);
  }

  public IntVar newIntVarFromDomain(Domain domain, String name) {
    return new IntVar(modelBuilder, domain, name);
  }

  public BoolVar newBoolVar(String name) {
    return new BoolVar(modelBuilder, new Domain(0, 1), name);
  }

  public IntVar newConstant(long value) {
    if (constantMap.containsKey(value)) {
      return new IntVar(modelBuilder, constantMap.get(value));
    }
    IntVar cste = new IntVar(modelBuilder, new Domain(value), ""); // bounds and name.
    constantMap.put(value, cste.getIndex());
    return cste;
  }

  public Literal trueLiteral() {
    if (constantMap.containsKey(1L)) {
      return new BoolVar(modelBuilder, constantMap.get(1L));
    }
    BoolVar cste = new BoolVar(modelBuilder, new Domain(1), ""); // bounds and name.
    constantMap.put(1L, cste.getIndex());
    return cste;
  }

  public Literal falseLiteral() {
    if (constantMap.containsKey(0L)) {
      return new BoolVar(modelBuilder, constantMap.get(0L));
    }
    BoolVar cste = new BoolVar(modelBuilder, new Domain(0), ""); // bounds and name.
    constantMap.put(0L, cste.getIndex());
    return cste;
  }

  public BoolVar getBoolVarFromProtoIndex(int index) {
    return new BoolVar(modelBuilder, index);
  }

  public IntVar getIntVarFromProtoIndex(int index) {
    return new IntVar(modelBuilder, index);
  }
 
  // Boolean Constraints.

  public Constraint addBoolOr(Literal[] literals) {
    return addBoolOr(Arrays.asList(literals));
  }

  public Constraint addBoolOr(Iterable<Literal> literals) {
    Constraint ct = new Constraint(modelBuilder);
    BoolArgumentProto.Builder boolOr = ct.getBuilder().getBoolOrBuilder();
    for (Literal lit : literals) {
      boolOr.addLiterals(lit.getIndex());
    }
    return ct;
  }

  public Constraint addAtLeastOne(Literal[] literals) {
    return addBoolOr(Arrays.asList(literals));
  }

  public Constraint addAtLeastOne(Iterable<Literal> literals) {
    return addBoolOr(literals);
  }

  public Constraint addAtMostOne(Literal[] literals) {
    return addAtMostOne(Arrays.asList(literals));
  }

  public Constraint addAtMostOne(Iterable<Literal> literals) {
    Constraint ct = new Constraint(modelBuilder);
    BoolArgumentProto.Builder atMostOne = ct.getBuilder().getAtMostOneBuilder();
    for (Literal lit : literals) {
      atMostOne.addLiterals(lit.getIndex());
    }
    return ct;
  }

  public Constraint addExactlyOne(Literal[] literals) {
    return addExactlyOne(Arrays.asList(literals));
  }

  public Constraint addExactlyOne(Iterable<Literal> literals) {
    Constraint ct = new Constraint(modelBuilder);
    BoolArgumentProto.Builder exactlyOne = ct.getBuilder().getExactlyOneBuilder();
    for (Literal lit : literals) {
      exactlyOne.addLiterals(lit.getIndex());
    }
    return ct;
  }

  public Constraint addBoolAnd(Literal[] literals) {
    return addBoolAnd(Arrays.asList(literals));
  }

  public Constraint addBoolAnd(Iterable<Literal> literals) {
    Constraint ct = new Constraint(modelBuilder);
    BoolArgumentProto.Builder boolAnd = ct.getBuilder().getBoolAndBuilder();
    for (Literal lit : literals) {
      boolAnd.addLiterals(lit.getIndex());
    }
    return ct;
  }

  public Constraint addBoolXor(Literal[] literals) {
    return addBoolXor(Arrays.asList(literals));
  }

  public Constraint addBoolXor(Iterable<Literal> literals) {
    Constraint ct = new Constraint(modelBuilder);
    BoolArgumentProto.Builder boolXOr = ct.getBuilder().getBoolXorBuilder();
    for (Literal lit : literals) {
      boolXOr.addLiterals(lit.getIndex());
    }
    return ct;
  }

  public Constraint addImplication(Literal a, Literal b) {
    return addBoolOr(new Literal[] {a.not(), b});
  }
 
  // Linear constraints.

  public Constraint addLinearExpressionInDomain(LinearArgument expr, Domain domain) {
    Constraint ct = new Constraint(modelBuilder);
    LinearConstraintProto.Builder lin = ct.getBuilder().getLinearBuilder();
    final LinearExpr e = expr.build();
    for (int i = 0; i < e.numElements(); ++i) {
      lin.addVars(e.getVariableIndex(i)).addCoeffs(e.getCoefficient(i));
    }
    long offset = e.getOffset();
    for (long b : domain.flattenedIntervals()) {
      if (b == Long.MIN_VALUE || b == Long.MAX_VALUE) {
        lin.addDomain(b);
      } else {
        lin.addDomain(b - offset);
      }
    }
    return ct;
  }

  public Constraint addLinearConstraint(LinearArgument expr, long lb, long ub) {
    return addLinearExpressionInDomain(expr, new Domain(lb, ub));
  }

  public Constraint addEquality(LinearArgument expr, long value) {
    return addLinearExpressionInDomain(expr, new Domain(value));
  }

  public Constraint addEquality(LinearArgument left, LinearArgument right) {
    LinearExprBuilder difference = LinearExpr.newBuilder();
    difference.addTerm(left, 1);
    difference.addTerm(right, -1);
    return addLinearExpressionInDomain(difference, new Domain(0));
  }

  public Constraint addLessOrEqual(LinearArgument expr, long value) {
    return addLinearExpressionInDomain(expr, new Domain(Long.MIN_VALUE, value));
  }

  public Constraint addLessOrEqual(LinearArgument left, LinearArgument right) {
    LinearExprBuilder difference = LinearExpr.newBuilder();
    difference.addTerm(left, 1);
    difference.addTerm(right, -1);
    return addLinearExpressionInDomain(difference, new Domain(Long.MIN_VALUE, 0));
  }

  public Constraint addLessThan(LinearArgument expr, long value) {
    return addLinearExpressionInDomain(expr, new Domain(Long.MIN_VALUE, value - 1));
  }

  public Constraint addLessThan(LinearArgument left, LinearArgument right) {
    LinearExprBuilder difference = LinearExpr.newBuilder();
    difference.addTerm(left, 1);
    difference.addTerm(right, -1);
    return addLinearExpressionInDomain(difference, new Domain(Long.MIN_VALUE, -1));
  }

  public Constraint addGreaterOrEqual(LinearArgument expr, long value) {
    return addLinearExpressionInDomain(expr, new Domain(value, Long.MAX_VALUE));
  }

  public Constraint addGreaterOrEqual(LinearArgument left, LinearArgument right) {
    LinearExprBuilder difference = LinearExpr.newBuilder();
    difference.addTerm(left, 1);
    difference.addTerm(right, -1);
    return addLinearExpressionInDomain(difference, new Domain(0, Long.MAX_VALUE));
  }

  public Constraint addGreaterThan(LinearArgument expr, long value) {
    return addLinearExpressionInDomain(expr, new Domain(value + 1, Long.MAX_VALUE));
  }

  public Constraint addGreaterThan(LinearArgument left, LinearArgument right) {
    LinearExprBuilder difference = LinearExpr.newBuilder();
    difference.addTerm(left, 1);
    difference.addTerm(right, -1);
    return addLinearExpressionInDomain(difference, new Domain(1, Long.MAX_VALUE));
  }

  public Constraint addDifferent(LinearArgument expr, long value) {
    return addLinearExpressionInDomain(expr,
        Domain.fromFlatIntervals(
            new long[] {Long.MIN_VALUE, value - 1, value + 1, Long.MAX_VALUE}));
  }

  public Constraint addDifferent(LinearArgument left, LinearArgument right) {
    LinearExprBuilder difference = LinearExpr.newBuilder();
    difference.addTerm(left, 1);
    difference.addTerm(right, -1);
    return addLinearExpressionInDomain(
        difference, Domain.fromFlatIntervals(new long[] {Long.MIN_VALUE, -1, 1, Long.MAX_VALUE}));
  }
 
  // Integer constraints.

  public Constraint addAllDifferent(LinearArgument[] expressions) {
    return addAllDifferent(Arrays.asList(expressions));
  }

  public Constraint addAllDifferent(Iterable<? extends LinearArgument> expressions) {
    Constraint ct = new Constraint(modelBuilder);
    AllDifferentConstraintProto.Builder allDiff = ct.getBuilder().getAllDiffBuilder();
    for (LinearArgument expr : expressions) {
      allDiff.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(expr, /*negate=*/false));
    }
    return ct;
  }

  public Constraint addElement(
      LinearArgument index, LinearArgument[] expressions, LinearArgument target) {
    Constraint ct = new Constraint(modelBuilder);
    ElementConstraintProto.Builder element = ct.getBuilder().getElementBuilder().setLinearIndex(
        getLinearExpressionProtoBuilderFromLinearArgument(index, /* negate= */ false));
    for (LinearArgument expr : expressions) {
      element.addExprs(
          getLinearExpressionProtoBuilderFromLinearArgument(expr, /* negate= */ false));
    }
    element.setLinearTarget(
        getLinearExpressionProtoBuilderFromLinearArgument(target, /* negate= */ false));
    return ct;
  }

  public Constraint addElement(
      LinearArgument index, Iterable<? extends LinearArgument> expressions, LinearArgument target) {
    Constraint ct = new Constraint(modelBuilder);
    ElementConstraintProto.Builder element = ct.getBuilder().getElementBuilder().setLinearIndex(
        getLinearExpressionProtoBuilderFromLinearArgument(index, /* negate= */ false));
    for (LinearArgument expr : expressions) {
      element.addExprs(
          getLinearExpressionProtoBuilderFromLinearArgument(expr, /* negate= */ false));
    }
    element.setLinearTarget(
        getLinearExpressionProtoBuilderFromLinearArgument(target, /* negate= */ false));
    return ct;
  }

  public Constraint addElement(LinearArgument index, long[] values, LinearArgument target) {
    Constraint ct = new Constraint(modelBuilder);
    ElementConstraintProto.Builder element = ct.getBuilder().getElementBuilder().setLinearIndex(
        getLinearExpressionProtoBuilderFromLinearArgument(index, /* negate= */ false));
    for (long v : values) {
      element.addExprs(LinearExpressionProto.newBuilder().setOffset(v));
    }
    element.setLinearTarget(
        getLinearExpressionProtoBuilderFromLinearArgument(target, /* negate= */ false));
    return ct;
  }

  public Constraint addElement(LinearArgument index, int[] values, LinearArgument target) {
    Constraint ct = new Constraint(modelBuilder);
    ElementConstraintProto.Builder element = ct.getBuilder().getElementBuilder().setLinearIndex(
        getLinearExpressionProtoBuilderFromLinearArgument(index, /* negate= */ false));
    for (long v : values) {
      element.addExprs(LinearExpressionProto.newBuilder().setOffset(v));
    }
    element.setLinearTarget(
        getLinearExpressionProtoBuilderFromLinearArgument(target, /* negate= */ false));
    return ct;
  }

  public CircuitConstraint addCircuit() {
    return new CircuitConstraint(modelBuilder);
  }

  public MultipleCircuitConstraint addMultipleCircuit() {
    return new MultipleCircuitConstraint(modelBuilder);
  }

  public TableConstraint addAllowedAssignments(LinearArgument[] expressions) {
    return addAllowedAssignments(Arrays.asList(expressions));
  }

  public TableConstraint addAllowedAssignments(Iterable<? extends LinearArgument> expressions) {
    TableConstraint ct = new TableConstraint(modelBuilder);
    TableConstraintProto.Builder table = ct.getBuilder().getTableBuilder();
    for (LinearArgument expr : expressions) {
      table.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(expr, /* negate= */ false));
    }
    table.setNegated(false);
    return ct;
  }

  public TableConstraint addForbiddenAssignments(LinearArgument[] expressions) {
    return addForbiddenAssignments(Arrays.asList(expressions));
  }

  public TableConstraint addForbiddenAssignments(Iterable<? extends LinearArgument> expressions) {
    TableConstraint ct = new TableConstraint(modelBuilder);
    TableConstraintProto.Builder table = ct.getBuilder().getTableBuilder();
    for (LinearArgument expr : expressions) {
      table.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(expr, /* negate= */ false));
    }
    table.setNegated(true);
    return ct;
  }

  public AutomatonConstraint addAutomaton(
      LinearArgument[] transitionExpressions, long startingState, long[] finalStates) {
    AutomatonConstraint ct = new AutomatonConstraint(modelBuilder);
    AutomatonConstraintProto.Builder automaton = ct.getBuilder().getAutomatonBuilder();
    for (LinearArgument expr : transitionExpressions) {
      automaton.addExprs(
          getLinearExpressionProtoBuilderFromLinearArgument(expr, /* negate= */ false));
    }
    automaton.setStartingState(startingState);
    for (long c : finalStates) {
      automaton.addFinalStates(c);
    }
    return ct;
  }

  public AutomatonConstraint addAutomaton(Iterable<? extends LinearArgument> transitionExpressions,
      long startingState, long[] finalStates) {
    AutomatonConstraint ct = new AutomatonConstraint(modelBuilder);
    AutomatonConstraintProto.Builder automaton = ct.getBuilder().getAutomatonBuilder();
    for (LinearArgument expr : transitionExpressions) {
      automaton.addExprs(
          getLinearExpressionProtoBuilderFromLinearArgument(expr, /* negate= */ false));
    }
    automaton.setStartingState(startingState);
    for (long c : finalStates) {
      automaton.addFinalStates(c);
    }
    return ct;
  }

  public Constraint addInverse(IntVar[] variables, IntVar[] inverseVariables) {
    if (variables.length != inverseVariables.length) {
      throw new MismatchedArrayLengths("CpModel.addInverse", "variables", "inverseVariables");
    }
    Constraint ct = new Constraint(modelBuilder);
    InverseConstraintProto.Builder inverse = ct.getBuilder().getInverseBuilder();
    for (IntVar var : variables) {
      inverse.addFDirect(var.getIndex());
    }
    for (IntVar var : inverseVariables) {
      inverse.addFInverse(var.getIndex());
    }
    return ct;
  }

  public ReservoirConstraint addReservoirConstraint(long minLevel, long maxLevel) {
    if (minLevel > 0) {
      throw new IllegalArgumentException("CpModel.addReservoirConstraint: minLevel must be <= 0");
    }
    if (maxLevel < 0) {
      throw new IllegalArgumentException("CpModel.addReservoirConstraint: maxLevel must be >= 0");
    }
    ReservoirConstraint ct = new ReservoirConstraint(this);
    ReservoirConstraintProto.Builder reservoir = ct.getBuilder().getReservoirBuilder();
    reservoir.setMinLevel(minLevel).setMaxLevel(maxLevel);
    return ct;
  }

  public void addMapDomain(IntVar var, Literal[] booleans, long offset) {
    for (int i = 0; i < booleans.length; ++i) {
      addEquality(var, offset + i).onlyEnforceIf(booleans[i]);
      addDifferent(var, offset + i).onlyEnforceIf(booleans[i].not());
    }
  }

  public Constraint addMinEquality(LinearArgument target, LinearArgument[] exprs) {
    Constraint ct = new Constraint(modelBuilder);
    LinearArgumentProto.Builder linMax = ct.getBuilder().getLinMaxBuilder();
    linMax.setTarget(getLinearExpressionProtoBuilderFromLinearArgument(target, /*negate=*/true));
    for (LinearArgument expr : exprs) {
      linMax.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(expr, /*negate=*/true));
    }
    return ct;
  }

  public Constraint addMinEquality(
      LinearArgument target, Iterable<? extends LinearArgument> exprs) {
    Constraint ct = new Constraint(modelBuilder);
    LinearArgumentProto.Builder linMax = ct.getBuilder().getLinMaxBuilder();
    linMax.setTarget(getLinearExpressionProtoBuilderFromLinearArgument(target, /*negate=*/true));
    for (LinearArgument expr : exprs) {
      linMax.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(expr, /*negate=*/true));
    }
    return ct;
  }

  public Constraint addMaxEquality(LinearArgument target, LinearArgument[] exprs) {
    Constraint ct = new Constraint(modelBuilder);
    LinearArgumentProto.Builder linMax = ct.getBuilder().getLinMaxBuilder();
    linMax.setTarget(getLinearExpressionProtoBuilderFromLinearArgument(target, /*negate=*/false));
    for (LinearArgument expr : exprs) {
      linMax.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(expr, /*negate=*/false));
    }
    return ct;
  }

  public Constraint addMaxEquality(
      LinearArgument target, Iterable<? extends LinearArgument> exprs) {
    Constraint ct = new Constraint(modelBuilder);
    LinearArgumentProto.Builder linMax = ct.getBuilder().getLinMaxBuilder();
    linMax.setTarget(getLinearExpressionProtoBuilderFromLinearArgument(target, /*negate=*/false));
    for (LinearArgument expr : exprs) {
      linMax.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(expr, /*negate=*/false));
    }
    return ct;
  }

  public Constraint addDivisionEquality(
      LinearArgument target, LinearArgument num, LinearArgument denom) {
    Constraint ct = new Constraint(modelBuilder);
    ct.getBuilder()
        .getIntDivBuilder()
        .setTarget(getLinearExpressionProtoBuilderFromLinearArgument(target, /*negate=*/false))
        .addExprs(getLinearExpressionProtoBuilderFromLinearArgument(num, /*negate=*/false))
        .addExprs(getLinearExpressionProtoBuilderFromLinearArgument(denom, /*negate=*/false));
    return ct;
  }

  public Constraint addAbsEquality(LinearArgument target, LinearArgument expr) {
    Constraint ct = new Constraint(modelBuilder);
    LinearArgumentProto.Builder linMax = ct.getBuilder().getLinMaxBuilder();
    linMax.setTarget(getLinearExpressionProtoBuilderFromLinearArgument(target, /*negate=*/false));
    linMax.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(expr, /*negate=*/false));
    linMax.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(expr, /*negate=*/true));
    return ct;
  }

  public Constraint addModuloEquality(
      LinearArgument target, LinearArgument var, LinearArgument mod) {
    Constraint ct = new Constraint(modelBuilder);
    ct.getBuilder()
        .getIntModBuilder()
        .setTarget(getLinearExpressionProtoBuilderFromLinearArgument(target, /*negate=*/false))
        .addExprs(getLinearExpressionProtoBuilderFromLinearArgument(var, /*negate=*/false))
        .addExprs(getLinearExpressionProtoBuilderFromLinearArgument(mod, /*negate=*/false));
    return ct;
  }

  public Constraint addModuloEquality(LinearArgument target, LinearArgument var, long mod) {
    Constraint ct = new Constraint(modelBuilder);
    ct.getBuilder()
        .getIntModBuilder()
        .setTarget(getLinearExpressionProtoBuilderFromLinearArgument(target, /*negate=*/false))
        .addExprs(getLinearExpressionProtoBuilderFromLinearArgument(var, /*negate=*/false))
        .addExprs(getLinearExpressionProtoBuilderFromLong(mod));
    return ct;
  }

  public Constraint addMultiplicationEquality(LinearArgument target, LinearArgument[] exprs) {
    Constraint ct = new Constraint(modelBuilder);
    LinearArgumentProto.Builder intProd = ct.getBuilder().getIntProdBuilder();
    intProd.setTarget(getLinearExpressionProtoBuilderFromLinearArgument(target, /*negate=*/false));
    for (LinearArgument expr : exprs) {
      intProd.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(expr, /*negate=*/false));
    }
    return ct;
  }

  public Constraint addMultiplicationEquality(
      LinearArgument target, LinearArgument left, LinearArgument right) {
    Constraint ct = new Constraint(modelBuilder);
    LinearArgumentProto.Builder intProd = ct.getBuilder().getIntProdBuilder();
    intProd.setTarget(getLinearExpressionProtoBuilderFromLinearArgument(target, /*negate=*/false));
    intProd.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(left, /*negate=*/false));
    intProd.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(right, /*negate=*/false));
    return ct;
  }
 
  // Scheduling support.

  public IntervalVar newIntervalVar(
      LinearArgument start, LinearArgument size, LinearArgument end, String name) {
    return new IntervalVar(modelBuilder,
        getLinearExpressionProtoBuilderFromLinearArgument(start, /*negate=*/false),
        getLinearExpressionProtoBuilderFromLinearArgument(size, /*negate=*/false),
        getLinearExpressionProtoBuilderFromLinearArgument(end, /*negate=*/false), name);
  }

  public IntervalVar newFixedSizeIntervalVar(LinearArgument start, long size, String name) {
    return new IntervalVar(modelBuilder,
        getLinearExpressionProtoBuilderFromLinearArgument(start, /*negate=*/false),
        getLinearExpressionProtoBuilderFromLong(size),
        getLinearExpressionProtoBuilderFromLinearArgument(
            LinearExpr.newBuilder().add(start).add(size), /*negate=*/false),
        name);
  }

  public IntervalVar newFixedInterval(long start, long size, String name) {
    return new IntervalVar(modelBuilder, getLinearExpressionProtoBuilderFromLong(start),
        getLinearExpressionProtoBuilderFromLong(size),
        getLinearExpressionProtoBuilderFromLong(start + size), name);
  }

  public IntervalVar newOptionalIntervalVar(LinearArgument start, LinearArgument size,
      LinearArgument end, Literal isPresent, String name) {
    return new IntervalVar(modelBuilder,
        getLinearExpressionProtoBuilderFromLinearArgument(start, /*negate=*/false),
        getLinearExpressionProtoBuilderFromLinearArgument(size, /*negate=*/false),
        getLinearExpressionProtoBuilderFromLinearArgument(end, /*negate=*/false),
        isPresent.getIndex(), name);
  }

  public IntervalVar newOptionalFixedSizeIntervalVar(
      LinearArgument start, long size, Literal isPresent, String name) {
    return new IntervalVar(modelBuilder,
        getLinearExpressionProtoBuilderFromLinearArgument(start, /*negate=*/false),
        getLinearExpressionProtoBuilderFromLong(size),
        getLinearExpressionProtoBuilderFromLinearArgument(
            LinearExpr.newBuilder().add(start).add(size), /*negate=*/false),
        isPresent.getIndex(), name);
  }

  public IntervalVar newOptionalFixedInterval(
      long start, long size, Literal isPresent, String name) {
    return new IntervalVar(modelBuilder, getLinearExpressionProtoBuilderFromLong(start),
        getLinearExpressionProtoBuilderFromLong(size),
        getLinearExpressionProtoBuilderFromLong(start + size), isPresent.getIndex(), name);
  }

  public Constraint addNoOverlap(IntervalVar[] intervalVars) {
    return addNoOverlap(Arrays.asList(intervalVars));
  }

  public Constraint addNoOverlap(Iterable<IntervalVar> intervalVars) {
    Constraint ct = new Constraint(modelBuilder);
    NoOverlapConstraintProto.Builder noOverlap = ct.getBuilder().getNoOverlapBuilder();
    for (IntervalVar var : intervalVars) {
      noOverlap.addIntervals(var.getIndex());
    }
    return ct;
  }

  public NoOverlap2dConstraint addNoOverlap2D() {
    return new NoOverlap2dConstraint(modelBuilder);
  }

  public CumulativeConstraint addCumulative(LinearArgument capacity) {
    CumulativeConstraint ct = new CumulativeConstraint(this);
    CumulativeConstraintProto.Builder cumul = ct.getBuilder().getCumulativeBuilder();
    cumul.setCapacity(getLinearExpressionProtoBuilderFromLinearArgument(capacity, false));
    return ct;
  }

  public CumulativeConstraint addCumulative(long capacity) {
    CumulativeConstraint ct = new CumulativeConstraint(this);
    CumulativeConstraintProto.Builder cumul = ct.getBuilder().getCumulativeBuilder();
    cumul.setCapacity(getLinearExpressionProtoBuilderFromLong(capacity));
    return ct;
  }

  public void addHint(IntVar var, long value) {
    modelBuilder.getSolutionHintBuilder().addVars(var.getIndex());
    modelBuilder.getSolutionHintBuilder().addValues(value);
  }

  public void addHint(Literal lit, boolean value) {
    if (isPositive(lit)) {
      modelBuilder.getSolutionHintBuilder().addVars(lit.getIndex());
      modelBuilder.getSolutionHintBuilder().addValues(value ? 1 : 0);
    } else {
      modelBuilder.getSolutionHintBuilder().addVars(negated(lit.getIndex()));
      modelBuilder.getSolutionHintBuilder().addValues(value ? 0 : 1);
    }
  }

  public void clearHints() {
    modelBuilder.clearSolutionHint();
  }

  public void addAssumption(Literal lit) {
    modelBuilder.addAssumptions(lit.getIndex());
  }

  public void addAssumptions(Literal[] literals) {
    for (Literal lit : literals) {
      addAssumption(lit);
    }
  }

  public void clearAssumptions() {
    modelBuilder.clearAssumptions();
  }
 
  // Objective.

  public void minimize(LinearArgument expr) {
    clearObjective();
    CpObjectiveProto.Builder obj = modelBuilder.getObjectiveBuilder();
    final LinearExpr e = expr.build();
    for (int i = 0; i < e.numElements(); ++i) {
      obj.addVars(e.getVariableIndex(i)).addCoeffs(e.getCoefficient(i));
    }
    obj.setOffset((double) e.getOffset());
  }

  public void minimize(DoubleLinearExpr expr) {
    clearObjective();
    FloatObjectiveProto.Builder obj = modelBuilder.getFloatingPointObjectiveBuilder();
    for (int i = 0; i < expr.numElements(); ++i) {
      obj.addVars(expr.getVariableIndex(i)).addCoeffs(expr.getCoefficient(i));
    }
    obj.setOffset(expr.getOffset()).setMaximize(false);
  }

  public void maximize(LinearArgument expr) {
    clearObjective();
    CpObjectiveProto.Builder obj = modelBuilder.getObjectiveBuilder();
    final LinearExpr e = expr.build();
    for (int i = 0; i < e.numElements(); ++i) {
      obj.addVars(e.getVariableIndex(i)).addCoeffs(-e.getCoefficient(i));
    }
    obj.setOffset((double) -e.getOffset());
    obj.setScalingFactor(-1.0);
  }

  public void maximize(DoubleLinearExpr expr) {
    clearObjective();
    FloatObjectiveProto.Builder obj = modelBuilder.getFloatingPointObjectiveBuilder();
    for (int i = 0; i < expr.numElements(); ++i) {
      obj.addVars(expr.getVariableIndex(i)).addCoeffs(expr.getCoefficient(i));
    }
    obj.setOffset(expr.getOffset()).setMaximize(true);
  }

  public void clearObjective() {
    modelBuilder.clearObjective();
    modelBuilder.clearFloatingPointObjective();
  }

  public boolean hasObjective() {
    return modelBuilder.hasObjective() || modelBuilder.hasFloatingPointObjective();
  }
 
  // DecisionStrategy

  public void addDecisionStrategy(LinearArgument[] expressions,
      DecisionStrategyProto.VariableSelectionStrategy varStr,
      DecisionStrategyProto.DomainReductionStrategy domStr) {
    DecisionStrategyProto.Builder ds = modelBuilder.addSearchStrategyBuilder();
    for (LinearArgument arg : expressions) {
      ds.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(arg, /* negate= */ false));
    }
    ds.setVariableSelectionStrategy(varStr).setDomainReductionStrategy(domStr);
  }

  public void addDecisionStrategy(Iterable<? extends LinearArgument> expressions,
      DecisionStrategyProto.VariableSelectionStrategy varStr,
      DecisionStrategyProto.DomainReductionStrategy domStr) {
    DecisionStrategyProto.Builder ds = modelBuilder.addSearchStrategyBuilder();
    for (LinearArgument arg : expressions) {
      ds.addExprs(getLinearExpressionProtoBuilderFromLinearArgument(arg, /* negate= */ false));
    }
    ds.setVariableSelectionStrategy(varStr).setDomainReductionStrategy(domStr);
  }

  public String modelStats() {
    return CpSatHelper.modelStats(model());
  }

  public String validate() {
    return CpSatHelper.validateModel(model());
  }

  public Boolean exportToFile(String file) {
    return CpSatHelper.writeModelToFile(model(), file);
  }
 
  // Helpers
  LinearExpressionProto.Builder getLinearExpressionProtoBuilderFromLinearArgument(
      LinearArgument arg, boolean negate) {
    LinearExpressionProto.Builder builder = LinearExpressionProto.newBuilder();
    final LinearExpr expr = arg.build();
    final int numVariables = expr.numElements();
    final long mult = negate ? -1 : 1;
    for (int i = 0; i < numVariables; ++i) {
      builder.addVars(expr.getVariableIndex(i));
      builder.addCoeffs(expr.getCoefficient(i) * mult);
    }
    builder.setOffset(expr.getOffset() * mult);
    return builder;
  }
 
  LinearExpressionProto.Builder getLinearExpressionProtoBuilderFromLong(long value) {
    LinearExpressionProto.Builder builder = LinearExpressionProto.newBuilder();
    builder.setOffset(value);
    return builder;
  }
 
  // Getters.
 
  public CpModelProto model() {
    return modelBuilder.build();
  }
 
  public int negated(int index) {
    return -index - 1;
  }
 
  public boolean isPositive(Literal lit) {
    return lit.getIndex() >= 0;
  }

  public CpModelProto.Builder getBuilder() {
    return modelBuilder;
  }
 
  private final CpModelProto.Builder modelBuilder;
  private final Map<Long, Integer> constantMap;
}