[CP-SAT] add BoolVar class to the java modelling layer

ortools/java/com/google/ortools/sat/BoolVar.java

@@ -0,0 +1,51 @@
+// Copyright 2010-2021 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.CpModelProto;
+import com.google.ortools.util.Domain;
+
+/** An Boolean variable. */
+public final class BoolVar extends IntVar implements Literal {
+  BoolVar(CpModelProto.Builder builder, Domain domain, String name) {
+    super(builder, domain, name);
+    this.negation_ = null;
+  }
+
+  BoolVar(CpModelProto.Builder builder, int index) {
+    super(builder, index);
+    this.negation_ = null;
+  }
+
+  /** Returns the negation of a boolean variable. */
+  @Override
+  public Literal not() {
+    if (negation_ == null) {
+      negation_ = new NotBooleanVariable(this);
+    }
+    return negation_;
+  }
+
+  @Override
+  public BoolVar getBoolVar() {
+    return this;
+  }
+
+  @Override
+  public boolean negated() {
+    return false;
+  }
+
+  private NotBooleanVariable negation_ = null;
+}

ortools/java/com/google/ortools/sat/ConstantExpression.java

@@ -14,10 +14,10 @@
 package com.google.ortools.sat;
 
 /** A specialized constant linear expression. */
-public final class Constant implements LinearExpr {
+public final class ConstantExpression implements LinearExpr {
   private final long offset;
 
-  public Constant(long offset) {
+  public ConstantExpression(long offset) {
     this.offset = offset;
   }
 

ortools/java/com/google/ortools/sat/CpModel.java

@@ -85,28 +85,38 @@ public final class CpModel {
   }
 
   /** Creates a Boolean variable with the given name. */
-  public IntVar newBoolVar(String name) {
-    return new IntVar(modelBuilder, new Domain(0, 1), name);
+  public BoolVar newBoolVar(String name) {
+    return new BoolVar(modelBuilder, new Domain(0, 1), name);
   }
 
   /** Creates a constant variable. */
   public IntVar newConstant(long value) {
     if (constantMap.containsKey(value)) {
-      return constantMap.get(value);
+      return new IntVar(modelBuilder, constantMap.get(value));
     }
     IntVar cste = new IntVar(modelBuilder, new Domain(value), ""); // bounds and name.
-    constantMap.put(value, cste);
+    constantMap.put(value, cste.getIndex());
     return cste;
   }
 
   /** Returns the true literal. */
   public Literal trueLiteral() {
-    return newConstant(1);
+    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;
   }
 
   /** Returns the false literal. */
   public Literal falseLiteral() {
-    return newConstant(0);
+    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;
   }
 
   // Boolean Constraints.
@@ -268,8 +278,8 @@ public final class CpModel {
   /** Adds {@code left == right}. */
   public Constraint addEquality(LinearExpr left, LinearExpr right) {
     LinearExprBuilder difference = LinearExpr.newBuilder();
-    difference.addExpression(left, 1);
-    difference.addExpression(right, -1);
+    difference.addTerm(left, 1);
+    difference.addTerm(right, -1);
     return addLinearExpressionInDomain(difference.build(), new Domain(0));
   }
 
@@ -281,8 +291,8 @@ public final class CpModel {
   /** Adds {@code left <= right}. */
   public Constraint addLessOrEqual(LinearExpr left, LinearExpr right) {
     LinearExprBuilder difference = LinearExpr.newBuilder();
-    difference.addExpression(left, 1);
-    difference.addExpression(right, -1);
+    difference.addTerm(left, 1);
+    difference.addTerm(right, -1);
     return addLinearExpressionInDomain(difference.build(), new Domain(Long.MIN_VALUE, 0));
   }
 
@@ -294,8 +304,8 @@ public final class CpModel {
   /** Adds {@code left < right}. */
   public Constraint addLessThan(LinearExpr left, LinearExpr right) {
     LinearExprBuilder difference = LinearExpr.newBuilder();
-    difference.addExpression(left, 1);
-    difference.addExpression(right, -1);
+    difference.addTerm(left, 1);
+    difference.addTerm(right, -1);
     return addLinearExpressionInDomain(difference.build(), new Domain(Long.MIN_VALUE, -1));
   }
 
@@ -307,8 +317,8 @@ public final class CpModel {
   /** Adds {@code left >= right}. */
   public Constraint addGreaterOrEqual(LinearExpr left, LinearExpr right) {
     LinearExprBuilder difference = LinearExpr.newBuilder();
-    difference.addExpression(left, 1);
-    difference.addExpression(right, -1);
+    difference.addTerm(left, 1);
+    difference.addTerm(right, -1);
     return addLinearExpressionInDomain(difference.build(), new Domain(0, Long.MAX_VALUE));
   }
 
@@ -320,8 +330,8 @@ public final class CpModel {
   /** Adds {@code left > right}. */
   public Constraint addGreaterThan(LinearExpr left, LinearExpr right) {
     LinearExprBuilder difference = LinearExpr.newBuilder();
-    difference.addExpression(left, 1);
-    difference.addExpression(right, -1);
+    difference.addTerm(left, 1);
+    difference.addTerm(right, -1);
     return addLinearExpressionInDomain(difference.build(), new Domain(1, Long.MAX_VALUE));
   }
 
@@ -335,8 +345,8 @@ public final class CpModel {
   /** Adds {@code left != right}. */
   public Constraint addDifferent(LinearExpr left, LinearExpr right) {
     LinearExprBuilder difference = LinearExpr.newBuilder();
-    difference.addExpression(left, 1);
-    difference.addExpression(right, -1);
+    difference.addTerm(left, 1);
+    difference.addTerm(right, -1);
     return addLinearExpressionInDomain(difference.build(),
         Domain.fromFlatIntervals(new long[] {Long.MIN_VALUE, -1, 1, Long.MAX_VALUE}));
   }
@@ -798,10 +808,7 @@ public final class CpModel {
    */
   public IntervalVar newIntervalVar(
       LinearExpr start, LinearExpr size, LinearExpr end, String name) {
-    LinearExprBuilder expr = LinearExpr.newBuilder();
-    expr.addExpression(start);
-    expr.addExpression(size);
-    addEquality(expr.build(), end);
+    addEquality(LinearExpr.newBuilder().add(start).add(size).build(), end);
     return new IntervalVar(modelBuilder,
         getLinearExpressionProtoBuilderFromLinearExpr(start, /*negate=*/false),
         getLinearExpressionProtoBuilderFromLinearExpr(size, /*negate=*/false),
@@ -824,7 +831,7 @@ public final class CpModel {
         getLinearExpressionProtoBuilderFromLinearExpr(start, /*negate=*/false),
         getLinearExpressionProtoBuilderFromLong(size),
         getLinearExpressionProtoBuilderFromLinearExpr(
-            LinearExpr.newBuilder().addExpression(start).add(size).build(), /*negate=*/false),
+            LinearExpr.newBuilder().add(start).add(size).build(), /*negate=*/false),
         name);
   }
 
@@ -855,8 +862,7 @@ public final class CpModel {
    */
   public IntervalVar newOptionalIntervalVar(
       LinearExpr start, LinearExpr size, LinearExpr end, Literal isPresent, String name) {
-    addEquality(LinearExpr.newBuilder().addExpression(start).addExpression(size).build(), end)
-        .onlyEnforceIf(isPresent);
+    addEquality(LinearExpr.newBuilder().add(start).add(size).build(), end).onlyEnforceIf(isPresent);
     return new IntervalVar(modelBuilder,
         getLinearExpressionProtoBuilderFromLinearExpr(start, /*negate=*/false),
         getLinearExpressionProtoBuilderFromLinearExpr(size, /*negate=*/false),
@@ -883,7 +889,7 @@ public final class CpModel {
         getLinearExpressionProtoBuilderFromLinearExpr(start, /*negate=*/false),
         getLinearExpressionProtoBuilderFromLong(size),
         getLinearExpressionProtoBuilderFromLinearExpr(
-            LinearExpr.newBuilder().addExpression(start).add(size).build(), /*negate=*/false),
+            LinearExpr.newBuilder().add(start).add(size).build(), /*negate=*/false),
         isPresent.getIndex(), name);
   }
 
@@ -1124,5 +1130,5 @@ public final class CpModel {
   }
 
   private final CpModelProto.Builder modelBuilder;
-  private final Map<Long, IntVar> constantMap;
+  private final Map<Long, Integer> constantMap;
 }

ortools/java/com/google/ortools/sat/IntVar.java

@@ -18,7 +18,7 @@ import com.google.ortools.sat.IntegerVariableProto;
 import com.google.ortools.util.Domain;
 
 /** An integer variable. */
-public final class IntVar implements Literal, LinearExpr {
+public class IntVar implements LinearExpr {
   IntVar(CpModelProto.Builder builder, Domain domain, String name) {
     this.modelBuilder = builder;
     this.variableIndex = modelBuilder.getVariablesCount();
@@ -27,14 +27,12 @@ public final class IntVar implements Literal, LinearExpr {
     for (long b : domain.flattenedIntervals()) {
       this.varBuilder.addDomain(b);
     }
-    this.negation_ = null;
   }
 
   IntVar(CpModelProto.Builder builder, int index) {
     this.modelBuilder = builder;
     this.variableIndex = index;
     this.varBuilder = modelBuilder.getVariablesBuilder(index);
-    this.negation_ = null;
   }
 
   @Override
@@ -48,7 +46,6 @@ public final class IntVar implements Literal, LinearExpr {
   }
 
   /** Internal, returns the index of the variable in the underlying CpModelProto. */
-  @Override
   public int getIndex() {
     return variableIndex;
   }
@@ -66,13 +63,17 @@ public final class IntVar implements Literal, LinearExpr {
 
   @Override
   public IntVar getVariable(int index) {
-    assert (index == 0);
+    if (index != 0) {
+      throw new IllegalArgumentException("wrong index in LinearExpr.getVariable(): " + index);
+    }
     return this;
   }
 
   @Override
   public long getCoefficient(int index) {
-    assert (index == 0);
+    if (index != 0) {
+      throw new IllegalArgumentException("wrong index in LinearExpr.getCoefficient(): " + index);
+    }
     return 1;
   }
 
@@ -81,20 +82,6 @@ public final class IntVar implements Literal, LinearExpr {
     return 0;
   }
 
-  /** Returns a short string describing the variable. */
-  @Override
-  public String getShortString() {
-    if (varBuilder.getName().isEmpty()) {
-      if (varBuilder.getDomainCount() == 2 && varBuilder.getDomain(0) == varBuilder.getDomain(1)) {
-        return String.format("%d", varBuilder.getDomain(0));
-      } else {
-        return String.format("var_%d(%s)", getIndex(), displayBounds());
-      }
-    } else {
-      return String.format("%s(%s)", getName(), displayBounds());
-    }
-  }
-
   /** Returns the domain as a string without the enclosing []. */
   public String displayBounds() {
     String out = "";
@@ -111,22 +98,25 @@ public final class IntVar implements Literal, LinearExpr {
     return out;
   }
 
-  /** Returns the negation of a boolean variable. */
-  @Override
-  public Literal not() {
-    if (negation_ == null) {
-      negation_ = new NotBooleanVariable(this);
-    }
-    return negation_;
-  }
-
   /** Returns the domain of the variable. */
   public Domain getDomain() {
     return CpSatHelper.variableDomain(varBuilder.build());
   }
 
-  private final CpModelProto.Builder modelBuilder;
-  private final int variableIndex;
-  private final IntegerVariableProto.Builder varBuilder;
-  private NotBooleanVariable negation_ = null;
+  /** Returns a short string describing the variable. */
+  public String getShortString() {
+    if (varBuilder.getName().isEmpty()) {
+      if (varBuilder.getDomainCount() == 2 && varBuilder.getDomain(0) == varBuilder.getDomain(1)) {
+        return String.format("%d", varBuilder.getDomain(0));
+      } else {
+        return String.format("var_%d(%s)", getIndex(), displayBounds());
+      }
+    } else {
+      return String.format("%s(%s)", getName(), displayBounds());
+    }
+  }
+
+  protected final CpModelProto.Builder modelBuilder;
+  protected final int variableIndex;
+  protected final IntegerVariableProto.Builder varBuilder;
 }

ortools/java/com/google/ortools/sat/LinearExpr.java

@@ -45,6 +45,11 @@ public interface LinearExpr {
     return newBuilder().addTerm(var, coeff).build();
   }
 
+  /** Shortcut for newBuilder().addTerm(expr, coeff).build() */
+  static LinearExpr term(LinearExpr expr, long coeff) {
+    return newBuilder().addTerm(expr, coeff).build();
+  }
+
   /** Shortcut for newBuilder().addTerm(literal, coeff).build() */
   static LinearExpr term(Literal literal, long coeff) {
     return newBuilder().addTerm(literal, coeff).build();
@@ -55,26 +60,36 @@ public interface LinearExpr {
     return newBuilder().addSum(vars).build();
   }
 
+  /** Shortcut for newBuilder().addSum(exprs).build() */
+  static LinearExpr sum(LinearExpr[] exprs) {
+    return newBuilder().addSum(exprs).build();
+  }
+
   /** Shortcut for newBuilder().addSum(literals).build() */
   static LinearExpr sum(Literal[] literals) {
     return newBuilder().addSum(literals).build();
   }
 
-  /** Shortcut for newBuilder().addScalProd(vars, coeffs).build() */
-  static LinearExpr scalProd(IntVar[] vars, long[] coeffs) {
-    return newBuilder().addScalProd(vars, coeffs).build();
+  /** Shortcut for newBuilder().addWeightedSum(vars, coeffs).build() */
+  static LinearExpr weightedSum(IntVar[] vars, long[] coeffs) {
+    return newBuilder().addWeightedSum(vars, coeffs).build();
   }
 
-  /** Shortcut for newBuilder().addScalProd(literals, coeffs).build() */
-  static LinearExpr scalProd(Literal[] literals, long[] coeffs) {
-    return newBuilder().addScalProd(literals, coeffs).build();
+  /** Shortcut for newBuilder().addWeightedSum(literals, coeffs).build() */
+  static LinearExpr weightedSum(Literal[] literals, long[] coeffs) {
+    return newBuilder().addWeightedSum(literals, coeffs).build();
+  }
+
+  /** Shortcut for newBuilder().addWeightedSum(exprs, coeffs).build() */
+  static LinearExpr weightedSum(LinearExpr[] exprs, long[] coeffs) {
+    return newBuilder().addWeightedSum(exprs, coeffs).build();
   }
 
   static LinearExpr rebuildFromLinearExpressionProto(
       LinearExpressionProto proto, CpModelProto.Builder builder) {
     int numElements = proto.getVarsCount();
     if (numElements == 0) {
-      return new Constant(proto.getOffset());
+      return new ConstantExpression(proto.getOffset());
     } else if (numElements == 1) {
       return new AffineExpression(
           new IntVar(builder, proto.getVars(0)), proto.getCoeffs(0), proto.getOffset());
@@ -91,9 +106,9 @@ public interface LinearExpr {
         }
       }
       if (allOnes) {
-        return new SumOfVariables(vars, offset);
+        return new SumExpression(vars, offset);
       } else {
-        return new ScalProd(vars, coeffs, offset);
+        return new WeightedSumExpression(vars, coeffs, offset);
       }
     }
   }

ortools/java/com/google/ortools/sat/LinearExprBuilder.java

@@ -28,19 +28,13 @@ public final class LinearExprBuilder {
     this.offset = 0;
   }
 
-  public LinearExprBuilder add(IntVar var) {
-    coefficients.merge(var, 1L, Long::sum);
+  public LinearExprBuilder add(LinearExpr expr) {
+    addTerm(expr, 1);
     return this;
   }
 
   public LinearExprBuilder add(Literal literal) {
-    final int index = literal.getIndex();
-    if (index >= 0) {
-      coefficients.merge((IntVar) literal, 1L, Long::sum);
-    } else {
-      offset = offset + 1;
-      coefficients.merge((IntVar) literal.not(), -1L, Long::sum);
-    }
+    addTerm(literal, 1);
     return this;
   }
 
@@ -49,79 +43,87 @@ public final class LinearExprBuilder {
     return this;
   }
 
-  public LinearExprBuilder addTerm(IntVar var, long coeff) {
-    coefficients.merge(var, coeff, Long::sum);
+  public LinearExprBuilder addTerm(LinearExpr expr, long coeff) {
+    final int numElements = expr.numElements();
+    for (int i = 0; i < numElements; ++i) {
+      coefficients.merge(expr.getVariable(i), expr.getCoefficient(i) * coeff, Long::sum);
+    }
+    offset = offset + expr.getOffset() * coeff;
     return this;
   }
 
   public LinearExprBuilder addTerm(Literal literal, long coeff) {
-    final int index = literal.getIndex();
-    if (index >= 0) {
-      coefficients.merge((IntVar) literal, coeff, Long::sum);
-    } else {
+    final BoolVar boolVar = literal.getBoolVar();
+    if (literal.negated()) {
+      coefficients.merge(boolVar, -coeff, Long::sum);
       offset = offset + coeff;
-      coefficients.merge((IntVar) literal.not(), -coeff, Long::sum);
+    } else {
+      coefficients.merge(boolVar, coeff, Long::sum);
     }
     return this;
   }
 
   public LinearExprBuilder addSum(IntVar[] vars) {
     for (final IntVar var : vars) {
-      add(var);
+      addTerm(var, 1);
     }
     return this;
   }
 
   public LinearExprBuilder addSum(Literal[] literals) {
     for (final Literal literal : literals) {
-      add(literal);
+      addTerm(literal, 1);
     }
     return this;
   }
 
-  public LinearExprBuilder addScalProd(IntVar[] vars, long[] coeffs) {
+  public LinearExprBuilder addSum(LinearExpr[] exprs) {
+    for (final LinearExpr expr : exprs) {
+      addTerm(expr, 1);
+    }
+    return this;
+  }
+
+  public LinearExprBuilder addWeightedSum(IntVar[] vars, long[] coeffs) {
     for (int i = 0; i < vars.length; ++i) {
       addTerm(vars[i], coeffs[i]);
     }
-
     return this;
   }
 
-  public LinearExprBuilder addScalProd(IntVar[] vars, int[] coeffs) {
+  public LinearExprBuilder addWeightedSum(IntVar[] vars, int[] coeffs) {
     for (int i = 0; i < vars.length; ++i) {
       addTerm(vars[i], coeffs[i]);
     }
-
     return this;
   }
 
-  public LinearExprBuilder addScalProd(Literal[] literals, long[] coeffs) {
+  public LinearExprBuilder addWeightedSum(Literal[] literals, long[] coeffs) {
     for (int i = 0; i < literals.length; ++i) {
       addTerm(literals[i], coeffs[i]);
     }
-
     return this;
   }
 
-  public LinearExprBuilder addScalProd(Literal[] literals, int[] coeffs) {
+  public LinearExprBuilder addWeightedSum(Literal[] literals, int[] coeffs) {
     for (int i = 0; i < literals.length; ++i) {
       addTerm(literals[i], coeffs[i]);
     }
-
     return this;
   }
 
-  public LinearExprBuilder addExpression(LinearExpr expr, long coeff) {
-    final int numElements = expr.numElements();
-    for (int i = 0; i < numElements; ++i) {
-      addTerm(expr.getVariable(i), expr.getCoefficient(i) * coeff);
+  public LinearExprBuilder addWeightedSum(LinearExpr[] exprs, long[] coeffs) {
+    for (int i = 0; i < exprs.length; ++i) {
+      addTerm(exprs[i], coeffs[i]);
     }
-    add(expr.getOffset());
     return this;
   }
 
-  public LinearExprBuilder addExpression(LinearExpr expr) {
-    return addExpression(expr, 1);
+  public LinearExprBuilder addWeightedSum(LinearExpr[] exprs, int[] coeffs) {
+    for (int i = 0; i < exprs.length; ++i) {
+      addTerm(exprs[i], coeffs[i]);
+    }
+    return this;
   }
 
   public LinearExpr build() {
@@ -140,7 +142,7 @@ public final class LinearExprBuilder {
       }
     }
     if (numElements == 0) {
-      return new Constant(offset);
+      return new ConstantExpression(offset);
     } else if (numElements == 1) {
       return new AffineExpression(lastVar, lastCoeff, offset);
     } else if (allOnes) {
@@ -152,7 +154,7 @@ public final class LinearExprBuilder {
           index++;
         }
       }
-      return new SumOfVariables(vars, offset);
+      return new SumExpression(vars, offset);
     } else {
       IntVar[] vars = new IntVar[numElements];
       long[] coeffs = new long[numElements];
@@ -164,7 +166,7 @@ public final class LinearExprBuilder {
           index++;
         }
       }
-      return new ScalProd(vars, coeffs, offset);
+      return new WeightedSumExpression(vars, coeffs, offset);
     }
   }
 }

ortools/java/com/google/ortools/sat/Literal.java

@@ -14,7 +14,7 @@
 package com.google.ortools.sat;
 
 /** Interface to describe a boolean variable or its negation. */
-public interface Literal {
+public interface Literal extends LinearExpr {
   public int getIndex();
 
   /** Returns the Boolean negation of the current literal. */
@@ -22,4 +22,10 @@ public interface Literal {
 
   /** Returns a short string to describe the literal. */
   public String getShortString();
+
+  /** Returns the underlying BoolVar */
+  public BoolVar getBoolVar();
+
+  /** Returns true if the literal is the negation of a Boolean variable */
+  public boolean negated();
 }

ortools/java/com/google/ortools/sat/NotBooleanVariable.java

@@ -18,7 +18,7 @@ package com.google.ortools.sat;
  * instead.
  */
 public final class NotBooleanVariable implements Literal {
-  public NotBooleanVariable(IntVar boolVar) {
+  public NotBooleanVariable(BoolVar boolVar) {
     this.boolVar = boolVar;
   }
 
@@ -34,11 +34,48 @@ public final class NotBooleanVariable implements Literal {
     return boolVar;
   }
 
+  @Override
+  public BoolVar getBoolVar() {
+    return boolVar;
+  }
+
+  @Override
+  public boolean negated() {
+    return true;
+  }
+
+  // LinearExpr interface.
+  @Override
+  public int numElements() {
+    return 1;
+  }
+
+  @Override
+  public IntVar getVariable(int index) {
+    if (index != 0) {
+      throw new IllegalArgumentException("wrong index in LinearExpr.getVariable(): " + index);
+    }
+    return boolVar;
+  }
+
+  @Override
+  public long getCoefficient(int index) {
+    if (index != 0) {
+      throw new IllegalArgumentException("wrong index in LinearExpr.getCoefficient(): " + index);
+    }
+    return -1;
+  }
+
+  @Override
+  public long getOffset() {
+    return 1;
+  }
+
   /** Returns a short string describing this literal. */
   @Override
   public String getShortString() {
     return "not(" + boolVar.getShortString() + ")";
   }
 
-  private final IntVar boolVar;
+  private final BoolVar boolVar;
 }

ortools/java/com/google/ortools/sat/SumExpression.java

@@ -14,11 +14,11 @@
 package com.google.ortools.sat;
 
 /** A specialized linear expression: sum(xi) + b. */
-public final class SumOfVariables implements LinearExpr {
+public final class SumExpression implements LinearExpr {
   private final IntVar[] variables;
   private final long offset;
 
-  public SumOfVariables(IntVar[] variables, long offset) {
+  public SumExpression(IntVar[] variables, long offset) {
     this.variables = variables;
     this.offset = offset;
   }

ortools/java/com/google/ortools/sat/WeightedSumExpression.java

@@ -14,12 +14,12 @@
 package com.google.ortools.sat;
 
 /** A specialized linear expression: sum(ai * xi) + b. */
-public final class ScalProd implements LinearExpr {
+public final class WeightedSumExpression implements LinearExpr {
   private final IntVar[] variables;
   private final long[] coefficients;
-  private long offset;
+  private final long offset;
 
-  public ScalProd(IntVar[] variables, long[] coefficients, long offset) {
+  public WeightedSumExpression(IntVar[] variables, long[] coefficients, long offset) {
     this.variables = variables;
     this.coefficients = coefficients;
     this.offset = offset;

ortools/sat/doc/README.md

@@ -14,6 +14,8 @@ https://developers.google.com/optimization/cp/cp_solver
          * [C   code samples](#c-code-samples)
          * [Java code samples](#java-code-samples)
          * [C# code samples](#c-code-samples-1)
+
+
 <!--te-->
 
 

ortools/sat/doc/boolean_logic.md

@@ -26,6 +26,8 @@ https://developers.google.com/optimization/
          * [C# code](#c-code-5)
       * [Product of two Boolean Variables](#product-of-two-boolean-variables)
          * [Python code](#python-code-3)
+
+
 <!--te-->
 
 
@@ -93,17 +95,17 @@ int main() {
 ```java
 package com.google.ortools.sat.samples;
 
-import com.google.ortools.Loader;
+import com.google.ortools.sat.BoolVar;
 import com.google.ortools.sat.CpModel;
-import com.google.ortools.sat.IntVar;
 import com.google.ortools.sat.Literal;
+import com.google.ortools.Loader;
 
 /** Code sample to demonstrate Boolean variable and literals. */
 public class LiteralSampleSat {
   public static void main(String[] args) throws Exception {
     Loader.loadNativeLibraries();
     CpModel model = new CpModel();
-    IntVar x = model.newBoolVar("x");
+    BoolVar x = model.newBoolVar("x");
     Literal notX = x.not();
     System.out.println(notX.getShortString());
   }
@@ -192,8 +194,8 @@ int main() {
 package com.google.ortools.sat.samples;
 
 import com.google.ortools.Loader;
+import com.google.ortools.sat.BoolVar;
 import com.google.ortools.sat.CpModel;
-import com.google.ortools.sat.IntVar;
 import com.google.ortools.sat.Literal;
 
 /** Code sample to demonstrates a simple Boolean constraint. */
@@ -201,8 +203,8 @@ public class BoolOrSampleSat {
   public static void main(String[] args) throws Exception {
     Loader.loadNativeLibraries();
     CpModel model = new CpModel();
-    IntVar x = model.newBoolVar("x");
-    IntVar y = model.newBoolVar("y");
+    BoolVar x = model.newBoolVar("x");
+    BoolVar y = model.newBoolVar("y");
     model.addBoolOr(new Literal[] {x, y.not()});
   }
 }
@@ -319,8 +321,8 @@ int main() {
 package com.google.ortools.sat.samples;
 
 import com.google.ortools.Loader;
+import com.google.ortools.sat.BoolVar;
 import com.google.ortools.sat.CpModel;
-import com.google.ortools.sat.IntVar;
 import com.google.ortools.sat.Literal;
 
 /**
@@ -338,9 +340,9 @@ public class ReifiedSampleSat {
     Loader.loadNativeLibraries();
     CpModel model = new CpModel();
 
-    IntVar x = model.newBoolVar("x");
-    IntVar y = model.newBoolVar("y");
-    IntVar b = model.newBoolVar("b");
+    BoolVar x = model.newBoolVar("x");
+    BoolVar y = model.newBoolVar("y");
+    BoolVar b = model.newBoolVar("b");
 
     // Version 1: a half-reified boolean and.
     model.addBoolAnd(new Literal[] {x, y.not()}).onlyEnforceIf(b);

ortools/sat/doc/channeling.md

@@ -17,6 +17,8 @@ https://developers.google.com/optimization/
          * [C   code](#c-code-2)
          * [Java code](#java-code-1)
          * [C# code](#c-code-3)
+
+
 <!--te-->
 
 
@@ -178,6 +180,7 @@ package com.google.ortools.sat.samples;
 import com.google.ortools.Loader;
 import com.google.ortools.sat.DecisionStrategyProto;
 import com.google.ortools.sat.SatParameters;
+import com.google.ortools.sat.BoolVar;
 import com.google.ortools.sat.CpModel;
 import com.google.ortools.sat.CpSolver;
 import com.google.ortools.sat.CpSolverSolutionCallback;
@@ -195,7 +198,7 @@ public class ChannelingSampleSat {
     IntVar[] vars = new IntVar[] {model.newIntVar(0, 10, "x"), model.newIntVar(0, 10, "y")};
 
     // Declare our intermediate boolean variable.
-    IntVar b = model.newBoolVar("b");
+    BoolVar b = model.newBoolVar("b");
 
     // Implement b == (x >= 5).
     model.addGreaterOrEqual(vars[0], 5).onlyEnforceIf(b);
@@ -514,6 +517,7 @@ import com.google.ortools.sat.CpSolver;
 import com.google.ortools.sat.IntVar;
 import com.google.ortools.sat.LinearExpr;
 import com.google.ortools.sat.LinearExprBuilder;
+import com.google.ortools.sat.Literal;
 
 /** Solves a bin packing problem with the CP-SAT solver. */
 public class BinPackingProblemSat {
@@ -546,7 +550,7 @@ public class BinPackingProblemSat {
     }
 
     // Slack variables.
-    IntVar[] slacks = new IntVar[numBins];
+    Literal[] slacks = new Literal[numBins];
     for (int b = 0; b < numBins; ++b) {
       slacks[b] = model.newBoolVar("slack_" + b);
     }

ortools/sat/doc/integer_arithmetic.md

@@ -33,6 +33,8 @@ https://developers.google.com/optimization/
          * [C   code](#c-code-4)
          * [Java code](#java-code-2)
          * [C# code](#c-code-5)
+
+
 <!--te-->
 
 

ortools/sat/doc/model.md

@@ -16,6 +16,8 @@ https://developers.google.com/optimization/
       * [Model copy](#model-copy)
          * [Python code](#python-code-1)
          * [C   code](#c-code-2)
+
+
 <!--te-->
 
 
@@ -204,7 +206,7 @@ public class SolutionHintingSampleSat {
     // Create the constraints.
     model.addDifferent(x, y);
 
-    model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {1, 2, 3}));
+    model.maximize(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {1, 2, 3}));
 
     // Solution hinting: x <- 1, y <- 2
     model.addHint(x, 1);

ortools/sat/doc/scheduling.md

@@ -38,6 +38,8 @@ https://developers.google.com/optimization/
       * [Precedences between intervals](#precedences-between-intervals)
       * [Convex hull of a set of intervals](#convex-hull-of-a-set-of-intervals)
       * [Reservoir constraint](#reservoir-constraint)
+
+
 <!--te-->
 
 
@@ -991,6 +993,7 @@ package com.google.ortools.sat.samples;
 
 import com.google.ortools.Loader;
 import com.google.ortools.sat.CpSolverStatus;
+import com.google.ortools.sat.BoolVar;
 import com.google.ortools.sat.CpModel;
 import com.google.ortools.sat.CpSolver;
 import com.google.ortools.sat.IntVar;
@@ -1006,9 +1009,10 @@ public class RankingSampleSat {
   /**
    * This code takes a list of interval variables in a noOverlap constraint, and a parallel list of
    * integer variables and enforces the following constraint
+   *
    * <ul>
-   * <li>rank[i] == -1 iff interval[i] is not active.
-   * <li>rank[i] == number of active intervals that precede interval[i].
+   *   <li>rank[i] == -1 iff interval[i] is not active.
+   *   <li>rank[i] == number of active intervals that precede interval[i].
    * </ul>
    */
   static void rankTasks(CpModel model, IntVar[] starts, Literal[] presences, IntVar[] ranks) {
@@ -1021,7 +1025,7 @@ public class RankingSampleSat {
         if (i == j) {
           precedences[i][i] = presences[i];
         } else {
-          IntVar prec = model.newBoolVar(String.format("%d before %d", i, j));
+          BoolVar prec = model.newBoolVar(String.format("%d before %d", i, j));
           precedences[i][j] = prec;
           // Ensure that task i precedes task j if prec is true.
           model.addLessThan(starts[i], starts[j]).onlyEnforceIf(prec);
@@ -1079,7 +1083,7 @@ public class RankingSampleSat {
     Literal[] presences = new Literal[numTasks];
     IntVar[] ranks = new IntVar[numTasks];
 
-    IntVar trueVar = model.newConstant(1);
+    Literal trueLiteral = model.trueLiteral();
 
     // Creates intervals, half of them are optional.
     for (int t = 0; t < numTasks; ++t) {
@@ -1090,7 +1094,7 @@ public class RankingSampleSat {
         intervals[t] =
             model.newIntervalVar(
                 starts[t], LinearExpr.constant(duration), ends[t], "interval_" + t);
-        presences[t] = trueVar;
+        presences[t] = trueLiteral;
       } else {
         presences[t] = model.newBoolVar("presence_" + t);
         intervals[t] =

ortools/sat/doc/solver.md

@@ -27,6 +27,8 @@ https://developers.google.com/optimization/
          * [C   code](#c-code-4)
          * [Java code](#java-code-2)
          * [C# code](#c-code-5)
+
+
 <!--te-->
 
 
@@ -368,7 +370,7 @@ public class SolveAndPrintIntermediateSolutionsSampleSat {
     model.addDifferent(x, y);
 
     // Maximize a linear combination of variables.
-    model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {1, 2, 3}));
+    model.maximize(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {1, 2, 3}));
 
     // Create a solver and solve the model.
     CpSolver solver = new CpSolver();

ortools/sat/samples/BinPackingProblemSat.java

@@ -20,6 +20,7 @@ import com.google.ortools.sat.CpSolverStatus;
 import com.google.ortools.sat.IntVar;
 import com.google.ortools.sat.LinearExpr;
 import com.google.ortools.sat.LinearExprBuilder;
+import com.google.ortools.sat.Literal;
 
 /** Solves a bin packing problem with the CP-SAT solver. */
 public class BinPackingProblemSat {
@@ -52,7 +53,7 @@ public class BinPackingProblemSat {
     }
 
     // Slack variables.
-    IntVar[] slacks = new IntVar[numBins];
+    Literal[] slacks = new Literal[numBins];
     for (int b = 0; b < numBins; ++b) {
       slacks[b] = model.newBoolVar("slack_" + b);
     }

ortools/sat/samples/BoolOrSampleSat.java

@@ -14,8 +14,8 @@
 package com.google.ortools.sat.samples;
 
 import com.google.ortools.Loader;
+import com.google.ortools.sat.BoolVar;
 import com.google.ortools.sat.CpModel;
-import com.google.ortools.sat.IntVar;
 import com.google.ortools.sat.Literal;
 
 /** Code sample to demonstrates a simple Boolean constraint. */
@@ -23,8 +23,8 @@ public class BoolOrSampleSat {
   public static void main(String[] args) throws Exception {
     Loader.loadNativeLibraries();
     CpModel model = new CpModel();
-    IntVar x = model.newBoolVar("x");
-    IntVar y = model.newBoolVar("y");
+    BoolVar x = model.newBoolVar("x");
+    BoolVar y = model.newBoolVar("y");
     model.addBoolOr(new Literal[] {x, y.not()});
   }
 }

ortools/sat/samples/ChannelingSampleSat.java

@@ -14,6 +14,7 @@
 package com.google.ortools.sat.samples;
 
 import com.google.ortools.Loader;
+import com.google.ortools.sat.BoolVar;
 import com.google.ortools.sat.CpModel;
 import com.google.ortools.sat.CpSolver;
 import com.google.ortools.sat.CpSolverSolutionCallback;
@@ -33,7 +34,7 @@ public class ChannelingSampleSat {
     IntVar[] vars = new IntVar[] {model.newIntVar(0, 10, "x"), model.newIntVar(0, 10, "y")};
 
     // Declare our intermediate boolean variable.
-    IntVar b = model.newBoolVar("b");
+    BoolVar b = model.newBoolVar("b");
 
     // Implement b == (x >= 5).
     model.addGreaterOrEqual(vars[0], 5).onlyEnforceIf(b);

ortools/sat/samples/CpIsFunSat.java

@@ -77,7 +77,7 @@ public final class CpIsFunSat {
     model.addAllDifferent(letters);
 
     // CP + IS + FUN = TRUE
-    model.addEquality(LinearExpr.scalProd(new IntVar[] {c, p, i, s, f, u, n, t, r, u, e},
+    model.addEquality(LinearExpr.weightedSum(new IntVar[] {c, p, i, s, f, u, n, t, r, u, e},
                           new long[] {base, 1, base, 1, base * base, base, 1, -base * base * base,
                               -base * base, -base, -1}),
         0);

ortools/sat/samples/CpSatExample.java

@@ -44,13 +44,13 @@ public final class CpSatExample {
 
     // Create the constraints.
     // [START constraints]
-    model.addLessOrEqual(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {2, 7, 3}), 50);
-    model.addLessOrEqual(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {3, -5, 7}), 45);
-    model.addLessOrEqual(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {5, 2, -6}), 37);
+    model.addLessOrEqual(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {2, 7, 3}), 50);
+    model.addLessOrEqual(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {3, -5, 7}), 45);
+    model.addLessOrEqual(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {5, 2, -6}), 37);
     // [END constraints]
 
     // [START objective]
-    model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {2, 2, 3}));
+    model.maximize(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {2, 2, 3}));
     // [END objective]
 
     // Create a solver and solve the model.

ortools/sat/samples/LiteralSampleSat.java

@@ -14,8 +14,8 @@
 package com.google.ortools.sat.samples;
 
 import com.google.ortools.Loader;
+import com.google.ortools.sat.BoolVar;
 import com.google.ortools.sat.CpModel;
-import com.google.ortools.sat.IntVar;
 import com.google.ortools.sat.Literal;
 
 /** Code sample to demonstrate Boolean variable and literals. */
@@ -23,7 +23,7 @@ public class LiteralSampleSat {
   public static void main(String[] args) throws Exception {
     Loader.loadNativeLibraries();
     CpModel model = new CpModel();
-    IntVar x = model.newBoolVar("x");
+    BoolVar x = model.newBoolVar("x");
     Literal notX = x.not();
     System.out.println(notX.getShortString());
   }

ortools/sat/samples/RankingSampleSat.java

@@ -14,6 +14,7 @@
 package com.google.ortools.sat.samples;
 
 import com.google.ortools.Loader;
+import com.google.ortools.sat.BoolVar;
 import com.google.ortools.sat.CpModel;
 import com.google.ortools.sat.CpSolver;
 import com.google.ortools.sat.CpSolverStatus;
@@ -30,9 +31,10 @@ public class RankingSampleSat {
   /**
    * This code takes a list of interval variables in a noOverlap constraint, and a parallel list of
    * integer variables and enforces the following constraint
+   *
    * <ul>
-   * <li>rank[i] == -1 iff interval[i] is not active.
-   * <li>rank[i] == number of active intervals that precede interval[i].
+   *   <li>rank[i] == -1 iff interval[i] is not active.
+   *   <li>rank[i] == number of active intervals that precede interval[i].
    * </ul>
    */
   static void rankTasks(CpModel model, IntVar[] starts, Literal[] presences, IntVar[] ranks) {
@@ -45,7 +47,7 @@ public class RankingSampleSat {
         if (i == j) {
           precedences[i][i] = presences[i];
         } else {
-          IntVar prec = model.newBoolVar(String.format("%d before %d", i, j));
+          BoolVar prec = model.newBoolVar(String.format("%d before %d", i, j));
           precedences[i][j] = prec;
           // Ensure that task i precedes task j if prec is true.
           model.addLessThan(starts[i], starts[j]).onlyEnforceIf(prec);
@@ -103,7 +105,7 @@ public class RankingSampleSat {
     Literal[] presences = new Literal[numTasks];
     IntVar[] ranks = new IntVar[numTasks];
 
-    IntVar trueVar = model.newConstant(1);
+    Literal trueLiteral = model.trueLiteral();
 
     // Creates intervals, half of them are optional.
     for (int t = 0; t < numTasks; ++t) {
@@ -113,7 +115,7 @@ public class RankingSampleSat {
       if (t < numTasks / 2) {
         intervals[t] = model.newIntervalVar(
             starts[t], LinearExpr.constant(duration), ends[t], "interval_" + t);
-        presences[t] = trueVar;
+        presences[t] = trueLiteral;
       } else {
         presences[t] = model.newBoolVar("presence_" + t);
         intervals[t] = model.newOptionalIntervalVar(

ortools/sat/samples/ReifiedSampleSat.java

@@ -14,8 +14,8 @@
 package com.google.ortools.sat.samples;
 
 import com.google.ortools.Loader;
+import com.google.ortools.sat.BoolVar;
 import com.google.ortools.sat.CpModel;
-import com.google.ortools.sat.IntVar;
 import com.google.ortools.sat.Literal;
 
 /**
@@ -33,9 +33,9 @@ public class ReifiedSampleSat {
     Loader.loadNativeLibraries();
     CpModel model = new CpModel();
 
-    IntVar x = model.newBoolVar("x");
-    IntVar y = model.newBoolVar("y");
-    IntVar b = model.newBoolVar("b");
+    BoolVar x = model.newBoolVar("x");
+    BoolVar y = model.newBoolVar("y");
+    BoolVar b = model.newBoolVar("b");
 
     // Version 1: a half-reified boolean and.
     model.addBoolAnd(new Literal[] {x, y.not()}).onlyEnforceIf(b);

ortools/sat/samples/SolutionHintingSampleSat.java

@@ -45,7 +45,7 @@ public class SolutionHintingSampleSat {
     // [END constraints]
 
     // [START objective]
-    model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {1, 2, 3}));
+    model.maximize(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {1, 2, 3}));
     // [END objective]
 
     // Solution hinting: x <- 1, y <- 2

ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.java

@@ -71,7 +71,7 @@ public class SolveAndPrintIntermediateSolutionsSampleSat {
 
     // Maximize a linear combination of variables.
     // [START objective]
-    model.maximize(LinearExpr.scalProd(new IntVar[] {x, y, z}, new long[] {1, 2, 3}));
+    model.maximize(LinearExpr.weightedSum(new IntVar[] {x, y, z}, new long[] {1, 2, 3}));
     // [END objective]
 
     // Create a solver and solve the model.