Skip to content

Commit 34850fa

Browse files
kfriedbergerkfriedberger
committed
replace all usages of "List.of" with more readable "ImmutableList.of/copyOf" to directly show the immutability.
 This might optimise internal operations, e.g., avoid copies from List to other Lists, if all are ImmutableLists.
1 parent d344e3a commit 34850fa

13 files changed

+32
-30
lines changed

‎src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88

99
package org.sosy_lab.java_smt.api;
1010

11+
import com.google.common.collect.ImmutableList;
1112
import java.math.BigInteger;
1213
import java.util.List;
1314
import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
@@ -415,6 +416,6 @@ default BitvectorFormula extract(BitvectorFormula number, int msb, int lsb, bool
415416
BooleanFormula distinct(List<BitvectorFormula> pBits);
416417

417418
default BooleanFormula distinct(BitvectorFormula... pBits) {
418-
return distinct(List.of(pBits));
419+
return distinct(ImmutableList.copyOf(pBits));
419420
}
420421
}

‎src/org/sosy_lab/java_smt/api/BooleanFormulaManager.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,9 @@
88

99
package org.sosy_lab.java_smt.api;
1010

11+
import com.google.common.collect.ImmutableList;
1112
import com.google.errorprone.annotations.CanIgnoreReturnValue;
1213
import java.util.Collection;
13-
import java.util.List;
1414
import java.util.Set;
1515
import java.util.stream.Collector;
1616
import org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor;
@@ -113,7 +113,7 @@ default BooleanFormula makeBoolean(boolean value) {
113113
* @see #and(BooleanFormula, BooleanFormula)
114114
*/
115115
default BooleanFormula and(BooleanFormula... bits) {
116-
return and(List.of(bits));
116+
return and(ImmutableList.copyOf(bits));
117117
}
118118

119119
/** Return a stream {@link Collector} that creates a conjunction of all elements in the stream. */
@@ -137,7 +137,7 @@ default BooleanFormula and(BooleanFormula... bits) {
137137
* @see #or(BooleanFormula, BooleanFormula)
138138
*/
139139
default BooleanFormula or(BooleanFormula... bits) {
140-
return or(List.of(bits));
140+
return or(ImmutableList.copyOf(bits));
141141
}
142142

143143
/** Return a stream {@link Collector} that creates a disjunction of all elements in the stream. */

‎src/org/sosy_lab/java_smt/api/UFManager.java‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88

99
package org.sosy_lab.java_smt.api;
1010

11+
import com.google.common.collect.ImmutableList;
1112
import java.util.List;
1213

1314
/** Manager for dealing with uninterpreted functions (UFs). */
@@ -20,7 +21,7 @@ <T extends Formula> FunctionDeclaration<T> declareUF(
2021
/** Declare an uninterpreted function. */
2122
default <T extends Formula> FunctionDeclaration<T> declareUF(
2223
String name, FormulaType<T> returnType, FormulaType<?>... args) {
23-
return declareUF(name, returnType, List.of(args));
24+
return declareUF(name, returnType, ImmutableList.copyOf(args));
2425
}
2526

2627
/**
@@ -38,7 +39,7 @@ default <T extends Formula> FunctionDeclaration<T> declareUF(
3839
* @see #callUF(FunctionDeclaration, List)
3940
*/
4041
default <T extends Formula> T callUF(FunctionDeclaration<T> funcType, Formula... args) {
41-
return callUF(funcType, List.of(args));
42+
return callUF(funcType, ImmutableList.copyOf(args));
4243
}
4344

4445
/**
@@ -58,6 +59,6 @@ <T extends Formula> T declareAndCallUF(
5859
*/
5960
default <T extends Formula> T declareAndCallUF(
6061
String name, FormulaType<T> pReturnType, Formula... pArgs) {
61-
return declareAndCallUF(name, pReturnType, List.of(pArgs));
62+
return declareAndCallUF(name, pReturnType, ImmutableList.copyOf(pArgs));
6263
}
6364
}

‎src/org/sosy_lab/java_smt/delegate/debugging/DebuggingAssertions.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
package org.sosy_lab.java_smt.delegate.debugging;
1010

1111
import com.google.common.base.Preconditions;
12-
import java.util.List;
12+
import com.google.common.collect.ImmutableList;
1313
import org.sosy_lab.common.configuration.Configuration;
1414
import org.sosy_lab.common.configuration.InvalidConfigurationException;
1515
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
@@ -54,7 +54,7 @@ public void addFunctionDeclaration(FunctionDeclaration<?> pFunctionDeclaration)
5454

5555
/** Assert that the function declaration belongs to this context. */
5656
public void assertDeclarationInContext(FunctionDeclaration<?> pFunctionDeclaration) {
57-
if (List.of(FunctionDeclarationKind.VAR, FunctionDeclarationKind.UF)
57+
if (ImmutableList.of(FunctionDeclarationKind.VAR, FunctionDeclarationKind.UF)
5858
.contains(pFunctionDeclaration.getKind())) {
5959
Preconditions.checkArgument(
6060
debugInfo.getDeclaredFunctions().contains(pFunctionDeclaration),

‎src/org/sosy_lab/java_smt/example/Binoxxo.java‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
package org.sosy_lab.java_smt.example;
1010

1111
import com.google.common.base.Preconditions;
12+
import com.google.common.collect.ImmutableList;
1213
import java.io.IOException;
1314
import java.math.BigInteger;
1415
import java.nio.charset.Charset;
@@ -95,7 +96,7 @@ public static void main(String... args)
9596
SolverContextFactory.createSolverContext(config, logger, notifier, solver)) {
9697

9798
for (BinoxxoSolver<?> binoxxo :
98-
List.of(
99+
ImmutableList.of(
99100
new IntegerBasedBinoxxoSolver(context), new BooleanBasedBinoxxoSolver(context))) {
100101
long start = System.currentTimeMillis();
101102

@@ -300,7 +301,7 @@ List<BooleanFormula> getRules(IntegerFormula[][] symbols) {
300301
for (int row = 0; row < size; row++) {
301302
for (int col = 0; col < size - 2; col++) {
302303
List<IntegerFormula> lst =
303-
List.of(symbols[row][col], symbols[row][col + 1], symbols[row][col + 2]);
304+
ImmutableList.of(symbols[row][col], symbols[row][col + 1], symbols[row][col + 2]);
304305
IntegerFormula sum = imgr.sum(lst);
305306
rules.add(bmgr.or(imgr.equal(one, sum), imgr.equal(two, sum)));
306307
}
@@ -310,7 +311,7 @@ List<BooleanFormula> getRules(IntegerFormula[][] symbols) {
310311
for (int col = 0; col < size; col++) {
311312
for (int row = 0; row < size - 2; row++) {
312313
List<IntegerFormula> lst =
313-
List.of(symbols[row][col], symbols[row + 1][col], symbols[row + 2][col]);
314+
ImmutableList.of(symbols[row][col], symbols[row + 1][col], symbols[row + 2][col]);
314315
IntegerFormula sum = imgr.sum(lst);
315316
rules.add(bmgr.or(imgr.equal(one, sum), imgr.equal(two, sum)));
316317
}
@@ -398,7 +399,7 @@ List<BooleanFormula> getRules(BooleanFormula[][] symbols) {
398399
for (int row = 0; row < size; row++) {
399400
for (int col = 0; col < size - 2; col++) {
400401
List<BooleanFormula> lst =
401-
List.of(symbols[row][col], symbols[row][col + 1], symbols[row][col + 2]);
402+
ImmutableList.of(symbols[row][col], symbols[row][col + 1], symbols[row][col + 2]);
402403
rules.add(bmgr.not(bmgr.and(lst)));
403404
rules.add(bmgr.or(lst));
404405
}
@@ -408,7 +409,7 @@ List<BooleanFormula> getRules(BooleanFormula[][] symbols) {
408409
for (int col = 0; col < size; col++) {
409410
for (int row = 0; row < size - 2; row++) {
410411
List<BooleanFormula> lst =
411-
List.of(symbols[row][col], symbols[row + 1][col], symbols[row + 2][col]);
412+
ImmutableList.of(symbols[row][col], symbols[row + 1][col], symbols[row + 2][col]);
412413
rules.add(bmgr.not(bmgr.and(lst)));
413414
rules.add(bmgr.or(lst));
414415
}

‎src/org/sosy_lab/java_smt/example/Sudoku.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -108,7 +108,7 @@ public static void main(String... args)
108108
SolverContextFactory.createSolverContext(config, logger, notifier, solver)) {
109109

110110
for (SudokuSolver<?> sudoku :
111-
List.of(
111+
ImmutableList.of(
112112
new IntegerBasedSudokuSolver(context),
113113
new EnumerationBasedSudokuSolver(context),
114114
new BooleanBasedSudokuSolver(context))) {

‎src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
import static org.junit.Assert.assertThrows;
1515
import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
1616

17+
import com.google.common.collect.ImmutableList;
1718
import java.math.BigInteger;
1819
import java.util.ArrayList;
1920
import java.util.LinkedHashMap;
@@ -392,9 +393,9 @@ public void bvVarDistinct() throws SolverException, InterruptedException {
392393
BitvectorFormula a = bvmgr.makeVariable(4, "a");
393394
BitvectorFormula num3 = bvmgr.makeBitvector(4, 3);
394395

395-
assertThatFormula(bvmgr.distinct(List.of(a, num3))).isSatisfiable();
396-
assertThatFormula(bvmgr.distinct(List.of(a, a))).isUnsatisfiable();
397-
assertThatFormula(bvmgr.distinct(List.of(num3, num3))).isUnsatisfiable();
396+
assertThatFormula(bvmgr.distinct(ImmutableList.of(a, num3))).isSatisfiable();
397+
assertThatFormula(bvmgr.distinct(ImmutableList.of(a, a))).isUnsatisfiable();
398+
assertThatFormula(bvmgr.distinct(ImmutableList.of(num3, num3))).isUnsatisfiable();
398399
}
399400

400401
@Test

‎src/org/sosy_lab/java_smt/test/DebugModeTest.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ public void noSharedFormulasTest()
149149
BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE);
150150

151151
// We expect debug mode to throw an exception for all solvers, except CVC4, CVC5 and Yices
152-
if (!List.of(Solvers.CVC4, Solvers.YICES2).contains(solverToUse())) {
152+
if (!ImmutableList.of(Solvers.CVC4, Solvers.YICES2).contains(solverToUse())) {
153153
assertThrows(IllegalArgumentException.class, () -> checkFormulaInDebugContext(formula));
154154
} else {
155155
checkFormulaInDebugContext(formula);

‎src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -344,7 +344,7 @@ public <T> void sequentialInterpolationIsNotRepeatedIndividualInterpolation()
344344

345345
// sequential interpolation should always work as expected
346346
checkItpSequence(ImmutableList.of(A, B, C), itpSeq);
347-
checkItpSequence(ImmutableList.of(A, B, C), List.of(itp1, itp2));
347+
checkItpSequence(ImmutableList.of(A, B, C), ImmutableList.of(itp1, itp2));
348348
}
349349

350350
@Test

‎src/org/sosy_lab/java_smt/test/MixedArithmeticsTest.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@
1616
import com.google.common.collect.ImmutableList;
1717
import java.math.BigDecimal;
1818
import java.math.BigInteger;
19-
import java.util.List;
2019
import java.util.function.BiFunction;
2120
import java.util.function.Function;
2221
import org.junit.Before;
@@ -69,7 +68,7 @@ private void testIntegerOperation(
6968
public void createIntegerNumberTest() throws SolverException, InterruptedException {
7069
IntegerFormula num1 = imgr.makeNumber(1.0);
7170
for (IntegerFormula num2 :
72-
List.of(
71+
ImmutableList.of(
7372
imgr.makeNumber(1.0),
7473
imgr.makeNumber("1"),
7574
imgr.makeNumber(1),
@@ -86,7 +85,7 @@ public void createIntegerNumberTest() throws SolverException, InterruptedExcepti
8685
public void createRationalNumberTest() throws SolverException, InterruptedException {
8786
RationalFormula num1 = rmgr.makeNumber(1.0);
8887
for (RationalFormula num2 :
89-
List.of(
88+
ImmutableList.of(
9089
rmgr.makeNumber(1.0),
9190
rmgr.makeNumber("1"),
9291
rmgr.makeNumber(1),
@@ -103,7 +102,7 @@ public void createRationalNumberTest() throws SolverException, InterruptedExcept
103102
public void createRational2NumberTest() throws SolverException, InterruptedException {
104103
RationalFormula num1 = rmgr.makeNumber(1.5);
105104
for (RationalFormula num2 :
106-
List.of(
105+
ImmutableList.of(
107106
rmgr.makeNumber(1.5),
108107
rmgr.makeNumber("1.5"),
109108
rmgr.makeNumber(BigDecimal.valueOf(1.5)),

0 commit comments

Comments
 (0)