CpModel.java

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.

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.CircuitConstraintProto;
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.IntegerArgumentProto;
import com.google.ortools.sat.IntegerVariableProto;
import com.google.ortools.sat.InverseConstraintProto;
import com.google.ortools.sat.LinearConstraintProto;
import com.google.ortools.sat.NoOverlap2DConstraintProto;
import com.google.ortools.sat.NoOverlapConstraintProto;
import com.google.ortools.sat.ReservoirConstraintProto;
import com.google.ortools.sat.TableConstraintProto;
import com.google.ortools.util.Domain;

public final class CpModel {
  static class CpModelException extends Exception {
    public CpModelException(String methodName, String msg) {
      // Call constructor of parent Exception
      super("CpModel." + 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();
  }

  // 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 IntVar newBoolVar(String name) {
    return new IntVar(modelBuilder, new Domain(0, 1), name);
  }

  public IntVar newConstant(long value) {
    return new IntVar(modelBuilder, new Domain(value), ""); // bounds and name.
  }

  // Boolean Constraints.

  public Constraint addBoolOr(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 addBoolAnd(Literal[] literals) {
    Constraint ct = new Constraint(modelBuilder);
    BoolArgumentProto.Builder boolOr = ct.getBuilder().getBoolAndBuilder();
    for (Literal lit : literals) {
      boolOr.addLiterals(lit.getIndex());
    }
    return ct;
  }

  public Constraint addBoolXor(Literal[] literals) {
    Constraint ct = new Constraint(modelBuilder);
    BoolArgumentProto.Builder boolOr = ct.getBuilder().getBoolXorBuilder();
    for (Literal lit : literals) {
      boolOr.addLiterals(lit.getIndex());
    }
    return ct;
  }

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

  // Linear constraints.

  public Constraint addLinearExpressionInDomain(LinearExpr expr, Domain domain) {
    Constraint ct = new Constraint(modelBuilder);
    LinearConstraintProto.Builder lin = ct.getBuilder().getLinearBuilder();
    for (int i = 0; i < expr.numElements(); ++i) {
      lin.addVars(expr.getVariable(i).getIndex());
      lin.addCoeffs(expr.getCoefficient(i));
    }
    for (long b : domain.flattenedIntervals()) {
      lin.addDomain(b);
    }
    return ct;
  }

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

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

  public Constraint addEquality(LinearExpr left, LinearExpr right) {
    return addLinearExpressionInDomain(new Difference(left, right), new Domain(0));
  }

  public Constraint addEqualityWithOffset(LinearExpr left, LinearExpr right, long offset) {
    return addLinearExpressionInDomain(new Difference(left, right), new Domain(-offset));
  }

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

  public Constraint addLessOrEqual(LinearExpr left, LinearExpr right) {
    return addLinearExpressionInDomain(new Difference(left, right), new Domain(Long.MIN_VALUE, 0));
  }

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

  public Constraint addLessThan(LinearExpr left, LinearExpr right) {
    return addLinearExpressionInDomain(new Difference(left, right), new Domain(Long.MIN_VALUE, -1));
  }

  public Constraint addLessOrEqualWithOffset(LinearExpr left, LinearExpr right, long offset) {
    return addLinearExpressionInDomain(
        new Difference(left, right), new Domain(Long.MIN_VALUE, -offset));
  }

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

  public Constraint addGreaterOrEqual(LinearExpr left, LinearExpr right) {
    return addLinearExpressionInDomain(new Difference(left, right), new Domain(0, Long.MAX_VALUE));
  }

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

  public Constraint addGreaterThan(LinearExpr left, LinearExpr right) {
    return addLinearExpressionInDomain(new Difference(left, right), new Domain(1, Long.MAX_VALUE));
  }

  public Constraint addGreaterOrEqualWithOffset(LinearExpr left, LinearExpr right, long offset) {
    return addLinearExpressionInDomain(
        new Difference(left, right), new Domain(-offset, Long.MAX_VALUE));
  }

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

  public Constraint addDifferent(IntVar left, IntVar right) {
    return addLinearExpressionInDomain(new Difference(left, right),
        Domain.fromFlatIntervals(new long[] {Long.MIN_VALUE, -1, 1, Long.MAX_VALUE}));
  }

  public Constraint addDifferentWithOffset(IntVar left, IntVar right, long offset) {
    return addLinearExpressionInDomain(new Difference(left, right),
        Domain.fromFlatIntervals(
            new long[] {Long.MIN_VALUE, -offset - 1, -offset + 1, Long.MAX_VALUE}));
  }

  // Integer constraints.

  public Constraint addAllDifferent(IntVar[] variables) {
    Constraint ct = new Constraint(modelBuilder);
    AllDifferentConstraintProto.Builder allDiff = ct.getBuilder().getAllDiffBuilder();
    for (IntVar var : variables) {
      allDiff.addVars(var.getIndex());
    }
    return ct;
  }

  public Constraint addElement(IntVar index, IntVar[] variables, IntVar target) {
    Constraint ct = new Constraint(modelBuilder);
    ElementConstraintProto.Builder element = ct.getBuilder().getElementBuilder();
    element.setIndex(index.getIndex());
    for (IntVar var : variables) {
      element.addVars(var.getIndex());
    }
    element.setTarget(target.getIndex());
    return ct;
  }

  public Constraint addElement(IntVar index, long[] values, IntVar target) {
    Constraint ct = new Constraint(modelBuilder);
    ElementConstraintProto.Builder element = ct.getBuilder().getElementBuilder();
    element.setIndex(index.getIndex());
    for (long v : values) {
      element.addVars(indexFromConstant(v));
    }
    element.setTarget(target.getIndex());
    return ct;
  }

  public Constraint addElement(IntVar index, int[] values, IntVar target) {
    Constraint ct = new Constraint(modelBuilder);
    ElementConstraintProto.Builder element = ct.getBuilder().getElementBuilder();
    element.setIndex(index.getIndex());
    for (long v : values) {
      element.addVars(indexFromConstant(v));
    }
    element.setTarget(target.getIndex());
    return ct;
  }

  public Constraint addCircuit(int[] tails, int[] heads, Literal[] literals)
      throws MismatchedArrayLengths {
    if (tails.length != heads.length) {
      throw new MismatchedArrayLengths("addCircuit", "tails", "heads");
    }
    if (tails.length != literals.length) {
      throw new MismatchedArrayLengths("addCircuit", "tails", "literals");
    }

    Constraint ct = new Constraint(modelBuilder);
    CircuitConstraintProto.Builder circuit = ct.getBuilder().getCircuitBuilder();
    for (int t : tails) {
      circuit.addTails(t);
    }
    for (int h : heads) {
      circuit.addHeads(h);
    }
    for (Literal lit : literals) {
      circuit.addLiterals(lit.getIndex());
    }
    return ct;
  }

  public Constraint addAllowedAssignments(IntVar[] variables, long[][] tuplesList)
      throws WrongLength {
    Constraint ct = new Constraint(modelBuilder);
    TableConstraintProto.Builder table = ct.getBuilder().getTableBuilder();
    for (IntVar var : variables) {
      table.addVars(var.getIndex());
    }
    int numVars = variables.length;
    for (int t = 0; t < tuplesList.length; ++t) {
      if (tuplesList[t].length != numVars) {
        throw new WrongLength("addAllowedAssignments",
            "tuple " + t + " does not have the same length as the variables");
      }
      for (int i = 0; i < tuplesList[t].length; ++i) {
        table.addValues(tuplesList[t][i]);
      }
    }
    return ct;
  }

  public Constraint addAllowedAssignments(IntVar[] variables, int[][] tuplesList)
      throws WrongLength {
    Constraint ct = new Constraint(modelBuilder);
    TableConstraintProto.Builder table = ct.getBuilder().getTableBuilder();
    for (IntVar var : variables) {
      table.addVars(var.getIndex());
    }
    int numVars = variables.length;
    for (int t = 0; t < tuplesList.length; ++t) {
      if (tuplesList[t].length != numVars) {
        throw new WrongLength("addAllowedAssignments",
            "tuple " + t + " does not have the same length as the variables");
      }
      for (int i = 0; i < tuplesList[t].length; ++i) {
        table.addValues(tuplesList[t][i]);
      }
    }
    return ct;
  }

  public Constraint addForbiddenAssignments(IntVar[] variables, long[][] tuplesList)
      throws WrongLength {
    Constraint ct = addAllowedAssignments(variables, tuplesList);
    // Reverse the flag.
    ct.getBuilder().getTableBuilder().setNegated(true);
    return ct;
  }

  public Constraint addForbiddenAssignments(IntVar[] variables, int[][] tuplesList)
      throws WrongLength {
    Constraint ct = addAllowedAssignments(variables, tuplesList);
    // Reverse the flag.
    ct.getBuilder().getTableBuilder().setNegated(true);
    return ct;
  }

  public Constraint addAutomaton(IntVar[] transitionVariables, long startingState,
      long[] finalStates, long[][] transitions) throws WrongLength {
    Constraint ct = new Constraint(modelBuilder);
    AutomatonConstraintProto.Builder automaton = ct.getBuilder().getAutomatonBuilder();
    for (IntVar var : transitionVariables) {
      automaton.addVars(var.getIndex());
    }
    automaton.setStartingState(startingState);
    for (long c : finalStates) {
      automaton.addFinalStates(c);
    }
    for (long[] t : transitions) {
      if (t.length != 3) {
        throw new WrongLength("addAutomaton", "transition does not have length 3");
      }
      automaton.addTransitionTail(t[0]);
      automaton.addTransitionLabel(t[1]);
      automaton.addTransitionHead(t[2]);
    }
    return ct;
  }

  public Constraint addInverse(IntVar[] variables, IntVar[] inverseVariables)
      throws MismatchedArrayLengths {
    if (variables.length != inverseVariables.length) {
      throw new MismatchedArrayLengths("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 Constraint addReservoirConstraint(
      IntVar[] times, long[] demands, long minLevel, long maxLevel) throws MismatchedArrayLengths {
    if (times.length != demands.length) {
      throw new MismatchedArrayLengths("addReservoirConstraint", "times", "demands");
    }
    Constraint ct = new Constraint(modelBuilder);
    ReservoirConstraintProto.Builder reservoir = ct.getBuilder().getReservoirBuilder();
    for (IntVar var : times) {
      reservoir.addTimes(var.getIndex());
    }
    for (long d : demands) {
      reservoir.addDemands(d);
    }
    reservoir.setMinLevel(minLevel);
    reservoir.setMaxLevel(maxLevel);
    return ct;
  }

  public Constraint addReservoirConstraint(
      IntVar[] times, int[] demands, long minLevel, long maxLevel) throws MismatchedArrayLengths {
    return addReservoirConstraint(times, toLongArray(demands), minLevel, maxLevel);
  }

  public Constraint addReservoirConstraintWithActive(IntVar[] times, long[] demands,
      IntVar[] actives, long minLevel, long maxLevel) throws MismatchedArrayLengths {
    if (times.length != demands.length) {
      throw new MismatchedArrayLengths("addReservoirConstraint", "times", "demands");
    }
    if (times.length != actives.length) {
      throw new MismatchedArrayLengths("addReservoirConstraint", "times", "actives");
    }

    Constraint ct = new Constraint(modelBuilder);
    ReservoirConstraintProto.Builder reservoir = ct.getBuilder().getReservoirBuilder();
    for (IntVar var : times) {
      reservoir.addTimes(var.getIndex());
    }
    for (long d : demands) {
      reservoir.addDemands(d);
    }
    for (IntVar var : actives) {
      reservoir.addActives(var.getIndex());
    }
    reservoir.setMinLevel(minLevel);
    reservoir.setMaxLevel(maxLevel);
    return ct;
  }

  public Constraint addReservoirConstraintWithActive(IntVar[] times, int[] demands,
      IntVar[] actives, long minLevel, long maxLevel) throws MismatchedArrayLengths {
    return addReservoirConstraintWithActive(
        times, toLongArray(demands), actives, minLevel, maxLevel);
  }

  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(IntVar target, IntVar[] vars) {
    Constraint ct = new Constraint(modelBuilder);
    IntegerArgumentProto.Builder intMin = ct.getBuilder().getIntMinBuilder();
    intMin.setTarget(target.getIndex());
    for (IntVar var : vars) {
      intMin.addVars(var.getIndex());
    }
    return ct;
  }

  public Constraint addMaxEquality(IntVar target, IntVar[] vars) {
    Constraint ct = new Constraint(modelBuilder);
    IntegerArgumentProto.Builder intMax = ct.getBuilder().getIntMaxBuilder();
    intMax.setTarget(target.getIndex());
    for (IntVar var : vars) {
      intMax.addVars(var.getIndex());
    }
    return ct;
  }

  public Constraint addDivisionEquality(IntVar target, IntVar num, IntVar denom) {
    Constraint ct = new Constraint(modelBuilder);
    IntegerArgumentProto.Builder intDiv = ct.getBuilder().getIntDivBuilder();
    intDiv.setTarget(target.getIndex());
    intDiv.addVars(num.getIndex());
    intDiv.addVars(denom.getIndex());
    return ct;
  }

  public Constraint addAbsEquality(IntVar target, IntVar var) {
    Constraint ct = new Constraint(modelBuilder);
    IntegerArgumentProto.Builder intMax = ct.getBuilder().getIntMaxBuilder();
    intMax.setTarget(target.getIndex());
    intMax.addVars(var.getIndex());
    intMax.addVars(-var.getIndex() - 1);
    return ct;
  }

  public Constraint addModuloEquality(IntVar target, IntVar var, IntVar mod) {
    Constraint ct = new Constraint(modelBuilder);
    IntegerArgumentProto.Builder intMod = ct.getBuilder().getIntModBuilder();
    intMod.setTarget(target.getIndex());
    intMod.addVars(var.getIndex());
    intMod.addVars(mod.getIndex());
    return ct;
  }

  public Constraint addModuloEquality(IntVar target, IntVar var, long mod) {
    Constraint ct = new Constraint(modelBuilder);
    IntegerArgumentProto.Builder intMod = ct.getBuilder().getIntModBuilder();
    intMod.setTarget(target.getIndex());
    intMod.addVars(var.getIndex());
    intMod.addVars(indexFromConstant(mod));
    return ct;
  }

  public Constraint addProductEquality(IntVar target, IntVar[] vars) {
    Constraint ct = new Constraint(modelBuilder);
    IntegerArgumentProto.Builder intProd = ct.getBuilder().getIntProdBuilder();
    intProd.setTarget(target.getIndex());
    for (IntVar var : vars) {
      intProd.addVars(var.getIndex());
    }
    return ct;
  }

  // Scheduling support.

  public IntervalVar newIntervalVar(IntVar start, IntVar size, IntVar end, String name) {
    return new IntervalVar(modelBuilder, start.getIndex(), size.getIndex(), end.getIndex(), name);
  }

  public IntervalVar newIntervalVar(IntVar start, IntVar size, long end, String name) {
    return new IntervalVar(
        modelBuilder, start.getIndex(), size.getIndex(), indexFromConstant(end), name);
  }

  public IntervalVar newIntervalVar(IntVar start, long size, IntVar end, String name) {
    return new IntervalVar(
        modelBuilder, start.getIndex(), indexFromConstant(size), end.getIndex(), name);
  }

  public IntervalVar newIntervalVar(long start, IntVar size, IntVar end, String name) {
    return new IntervalVar(
        modelBuilder, indexFromConstant(start), size.getIndex(), end.getIndex(), name);
  }

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

  public IntervalVar newOptionalIntervalVar(
      IntVar start, IntVar size, IntVar end, Literal isPresent, String name) {
    return new IntervalVar(modelBuilder, start.getIndex(), size.getIndex(), end.getIndex(),
        isPresent.getIndex(), name);
  }

  public IntervalVar newOptionalIntervalVar(
      IntVar start, IntVar size, long end, Literal isPresent, String name) {
    return new IntervalVar(modelBuilder, start.getIndex(), size.getIndex(), indexFromConstant(end),
        isPresent.getIndex(), name);
  }

  public IntervalVar newOptionalIntervalVar(
      IntVar start, long size, IntVar end, Literal isPresent, String name) {
    return new IntervalVar(modelBuilder, start.getIndex(), indexFromConstant(size), end.getIndex(),
        isPresent.getIndex(), name);
  }

  public IntervalVar newOptionalIntervalVar(
      long start, IntVar size, IntVar end, Literal isPresent, String name) {
    return new IntervalVar(modelBuilder, indexFromConstant(start), size.getIndex(), end.getIndex(),
        isPresent.getIndex(), name);
  }

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

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

  public Constraint addNoOverlap2D(IntervalVar[] xIntervals, IntervalVar[] yIntervals) {
    Constraint ct = new Constraint(modelBuilder);
    NoOverlap2DConstraintProto.Builder noOverlap2d = ct.getBuilder().getNoOverlap2DBuilder();
    for (IntervalVar x : xIntervals) {
      noOverlap2d.addXIntervals(x.getIndex());
    }
    for (IntervalVar y : yIntervals) {
      noOverlap2d.addYIntervals(y.getIndex());
    }
    return ct;
  }

  public Constraint addCumulative(IntervalVar[] intervals, IntVar[] demands, IntVar capacity) {
    Constraint ct = new Constraint(modelBuilder);
    CumulativeConstraintProto.Builder cumul = ct.getBuilder().getCumulativeBuilder();
    for (IntervalVar interval : intervals) {
      cumul.addIntervals(interval.getIndex());
    }
    for (IntVar var : demands) {
      cumul.addDemands(var.getIndex());
    }
    cumul.setCapacity(capacity.getIndex());
    return ct;
  }

  public Constraint addCumulative(IntervalVar[] intervals, long[] demands, IntVar capacity) {
    Constraint ct = new Constraint(modelBuilder);
    CumulativeConstraintProto.Builder cumul = ct.getBuilder().getCumulativeBuilder();
    for (IntervalVar interval : intervals) {
      cumul.addIntervals(interval.getIndex());
    }
    for (long d : demands) {
      cumul.addDemands(indexFromConstant(d));
    }
    cumul.setCapacity(capacity.getIndex());
    return ct;
  }

  public Constraint addCumulative(IntervalVar[] intervals, int[] demands, IntVar capacity) {
    return addCumulative(intervals, toLongArray(demands), capacity);
  }

  public Constraint addCumulative(IntervalVar[] intervals, IntVar[] demands, long capacity) {
    Constraint ct = new Constraint(modelBuilder);
    CumulativeConstraintProto.Builder cumul = ct.getBuilder().getCumulativeBuilder();
    for (IntervalVar interval : intervals) {
      cumul.addIntervals(interval.getIndex());
    }
    for (IntVar var : demands) {
      cumul.addDemands(var.getIndex());
    }
    cumul.setCapacity(indexFromConstant(capacity));
    return ct;
  }

  public Constraint addCumulative(IntervalVar[] intervals, long[] demands, long capacity) {
    Constraint ct = new Constraint(modelBuilder);
    CumulativeConstraintProto.Builder cumul = ct.getBuilder().getCumulativeBuilder();
    for (IntervalVar interval : intervals) {
      cumul.addIntervals(interval.getIndex());
    }
    for (long d : demands) {
      cumul.addDemands(indexFromConstant(d));
    }
    cumul.setCapacity(indexFromConstant(capacity));
    return ct;
  }

  public Constraint addCumulative(IntervalVar[] intervals, int[] demands, long capacity) {
    return addCumulative(intervals, toLongArray(demands), capacity);
  }

  // Objective.

  public void minimize(LinearExpr expr) {
    CpObjectiveProto.Builder obj = modelBuilder.getObjectiveBuilder();
    for (int i = 0; i < expr.numElements(); ++i) {
      obj.addVars(expr.getVariable(i).getIndex());
      obj.addCoeffs(expr.getCoefficient(i));
    }
  }

  public void maximize(LinearExpr expr) {
    CpObjectiveProto.Builder obj = modelBuilder.getObjectiveBuilder();
    for (int i = 0; i < expr.numElements(); ++i) {
      obj.addVars(expr.getVariable(i).getIndex());
      obj.addCoeffs(-expr.getCoefficient(i));
    }
    obj.setScalingFactor(-1.0);
  }

  // DecisionStrategy

  public void addDecisionStrategy(IntVar[] variables,
      DecisionStrategyProto.VariableSelectionStrategy varStr,
      DecisionStrategyProto.DomainReductionStrategy domStr) {
    DecisionStrategyProto.Builder ds = modelBuilder.addSearchStrategyBuilder();
    for (IntVar var : variables) {
      ds.addVariables(var.getIndex());
    }
    ds.setVariableSelectionStrategy(varStr);
    ds.setDomainReductionStrategy(domStr);
  }

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

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

  // Helpers

  long[] toLongArray(int[] values) {
    long[] result = new long[values.length];
    for (int i = 0; i < values.length; ++i) {
      result[i] = values[i];
    }
    return result;
  }

  int indexFromConstant(long constant) {
    int index = modelBuilder.getVariablesCount();
    IntegerVariableProto.Builder cst = modelBuilder.addVariablesBuilder();
    cst.addDomain(constant);
    cst.addDomain(constant);
    return index;
  }

  // Getters.

  public CpModelProto model() {
    return modelBuilder.build();
  }

  public int negated(int index) {
    return -index - 1;
  }

  public CpModelProto.Builder getBuilder() {
    return modelBuilder;
  }

  private final CpModelProto.Builder modelBuilder;
}