Skip to content

Commit 7b01966

Browse files
kfriedbergerkfriedberger
authored
Merge pull request #409 from sosy-lab/dependency-update
update SMT solvers and libraries
2 parents 72b0691 + 5d85f66 commit 7b01966

File tree

10 files changed

+57
-83
lines changed

10 files changed

+57
-83
lines changed

‎lib/ivy.xml‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -84,14 +84,14 @@ SPDX-License-Identifier: Apache-2.0
8484

8585
<dependencies>
8686
<!-- SoSy-Lab Common Library -->
87-
<dependency org="org.sosy_lab" name="common" rev="0.3000-585-g7a5f95c1" conf="core->runtime; contrib->sources"/>
87+
<dependency org="org.sosy_lab" name="common" rev="0.3000-609-g90a352c" conf="core->runtime; contrib->sources"/>
8888

8989
<!-- Google Core Libraries for Java
9090
Contains a lot of helpful data structures. -->
91-
<dependency org="com.google.guava" name="guava" rev="33.2.1-jre" conf="core->default; contrib->sources"/>
91+
<dependency org="com.google.guava" name="guava" rev="33.3.1-jre" conf="core->default; contrib->sources"/>
9292

9393
<!-- Guava-testlib contains many useful testing utilities -->
94-
<dependency org="com.google.guava" name="guava-testlib" rev="33.2.1-jre" conf="test->default; contrib->sources"/>
94+
<dependency org="com.google.guava" name="guava-testlib" rev="33.3.1-jre" conf="test->default; contrib->sources"/>
9595

9696
<!-- Dependency on Ivy itself so that we can ugprade it easily.
9797
Change version number in build/build-ivy.xml for upgrading. -->
@@ -102,7 +102,7 @@ SPDX-License-Identifier: Apache-2.0
102102
<dependency org="com.google.auto.value" name="auto-value-annotations" rev="1.11.0" conf="build->default; contrib->sources"/>
103103

104104
<!-- Annotations we use for @Nullable etc. -->
105-
<dependency org="org.checkerframework" name="checker-qual" rev="3.44.0" conf="core->default; contrib->sources"/>
105+
<dependency org="org.checkerframework" name="checker-qual" rev="3.48.1" conf="core->default; contrib->sources"/>
106106

107107
<!-- JUnit
108108
Testing framework. -->
@@ -119,8 +119,8 @@ SPDX-License-Identifier: Apache-2.0
119119

120120
<!-- Truth
121121
Library for writing literal assertions. -->
122-
<dependency org="com.google.truth" name="truth" rev="1.4.2" conf="test->default; contrib->sources"/>
123-
<dependency org="com.google.truth.extensions" name="truth-java8-extension" rev="1.4.2" conf="test->default; contrib->sources"/>
122+
<dependency org="com.google.truth" name="truth" rev="1.4.4" conf="test->default; contrib->sources"/>
123+
<dependency org="com.google.truth.extensions" name="truth-java8-extension" rev="1.4.4" conf="test->default; contrib->sources"/>
124124

125125
<!-- Google error-prone
126126
Compiler adaptor with some useful checks for common errors. -->
@@ -129,11 +129,11 @@ SPDX-License-Identifier: Apache-2.0
129129

130130
<!-- Eclipse JDT Compiler
131131
For additional compiler warnings. -->
132-
<dependency org="org.eclipse.jdt.core.compiler" name="ecj" rev="4.29" conf="build->default"/>
132+
<dependency org="org.eclipse.jdt.core.compiler" name="ecj" rev="4.32-sosy0" conf="build->default"/>
133133

134134
<!-- google-java-format
135135
A source-code formatter for Java -->
136-
<dependency org="com.google.googlejavaformat" name="google-java-format" rev="1.22.0" conf="format-source->default"/>
136+
<dependency org="com.google.googlejavaformat" name="google-java-format" rev="1.24.0" conf="format-source->default"/>
137137

138138
<!-- SpotBugs -->
139139
<dependency org="com.github.spotbugs" name="spotbugs-ant" rev="4.8.6" conf="spotbugs->default"/>
@@ -143,7 +143,7 @@ SPDX-License-Identifier: Apache-2.0
143143

144144
<!-- Checkstyle -->
145145
<dependency org="com.github.sevntu-checkstyle" name="sevntu-checks" rev="1.44.1" conf="checkstyle->default"/>
146-
<dependency org="com.puppycrawl.tools" name="checkstyle" rev="10.17.0" conf="checkstyle->default"/>
146+
<dependency org="com.puppycrawl.tools" name="checkstyle" rev="10.19.0" conf="checkstyle->default"/>
147147

148148
<!-- SmtInterpol -->
149149
<dependency org="de.uni-freiburg.informatik.ultimate" name="smtinterpol" rev="2.5-1242-g5c50fb6d" conf="runtime-smtinterpol->master; contrib->sources"/>
@@ -160,14 +160,14 @@ SPDX-License-Identifier: Apache-2.0
160160
<dependency org="edu.tum.cs" name="java-cup" rev="11b-20160615" conf="runtime-princess->runtime"/>
161161

162162
<!-- Solver Binaries -->
163-
<dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.10" conf="runtime-mathsat->solver-mathsat" />
164-
<dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.12.5" conf="runtime-z3->solver-z3; contrib->sources,javadoc" />
163+
<dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.11-glibc2.27" conf="runtime-mathsat->solver-mathsat" />
164+
<dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.13.0" conf="runtime-z3->solver-z3; contrib->sources,javadoc" />
165165
<dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.6.0-g2f72cc0e" conf="runtime-opensmt->solver-opensmt; contrib->sources,javadoc" />
166166
<dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.1-sosy0" conf="runtime-optimathsat->solver-optimathsat" />
167167
<dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />
168168
<dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="1.0.5-g4cb2ab9eb" conf="runtime-cvc5->solver-cvc5" />
169169
<dependency org="org.sosy_lab" name="javasmt-solver-boolector" rev="3.2.2-g1a89c229" conf="runtime-boolector->solver-boolector" />
170-
<dependency org="org.sosy_lab" name="javasmt-solver-bitwuzla" rev="0.6.0-gab3db0e6" conf="runtime-bitwuzla->solver-bitwuzla; contrib->sources,javadoc"/>
170+
<dependency org="org.sosy_lab" name="javasmt-solver-bitwuzla" rev="0.6.0-g2b3d69a7" conf="runtime-bitwuzla->solver-bitwuzla; contrib->sources,javadoc"/>
171171

172172
<!-- additional JavaSMT components with Solver Binaries -->
173173
<dependency org="org.sosy_lab" name="javasmt-yices2" rev="4.1.1-734-g3732f7e08" conf="runtime-yices2->runtime; contrib->sources" />

‎src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ public final FormulaManager getFormulaManager() {
3535
return fmgr;
3636
}
3737

38+
@SuppressWarnings("resource")
3839
@Override
3940
public final ProverEnvironment newProverEnvironment(ProverOptions... options) {
4041
ProverEnvironment out = newProverEnvironment0(toSet(options));

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -294,7 +294,7 @@ public Integer visitFunction(
294294
nonLinearArithmetic = true;
295295
return allArgLevel + 1;
296296
}
297-
// $FALL-THROUGH$
297+
// $FALL-THROUGH$
298298
default:
299299
if (pFunctionDeclaration.getType().isBooleanType()) {
300300
if (EnumSet.of(

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

Lines changed: 14 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@
1010

1111
import static com.google.common.truth.Truth.assertThat;
1212
import static com.google.common.truth.Truth.assertWithMessage;
13-
import static com.google.common.truth.Truth.assert_;
1413
import static com.google.common.truth.TruthJUnit.assume;
1514
import static org.junit.Assert.assertThrows;
1615
import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
@@ -534,11 +533,9 @@ public void bvInRange() throws SolverException, InterruptedException {
534533
@SuppressWarnings("CheckReturnValue")
535534
public void bvOutOfRange() {
536535
for (int[] sizeAndValue : new int[][] {{4, 32}, {4, -9}, {8, 300}, {8, -160}}) {
537-
try {
538-
bvmgr.makeBitvector(sizeAndValue[0], sizeAndValue[1]);
539-
assert_().fail();
540-
} catch (IllegalArgumentException expected) {
541-
}
536+
assertThrows(
537+
IllegalArgumentException.class,
538+
() -> bvmgr.makeBitvector(sizeAndValue[0], sizeAndValue[1]));
542539
}
543540

544541
for (int size : new int[] {4, 6, 8, 10, 16, 32}) {
@@ -547,16 +544,9 @@ public void bvOutOfRange() {
547544
bvmgr.makeBitvector(size, -(1L << (size - 1)));
548545

549546
// forbitten values
550-
try {
551-
bvmgr.makeBitvector(size, 1L << size);
552-
assert_().fail();
553-
} catch (IllegalArgumentException expected) {
554-
}
555-
try {
556-
bvmgr.makeBitvector(size, -(1L << (size - 1)) - 1);
557-
assert_().fail();
558-
} catch (IllegalArgumentException expected) {
559-
}
547+
assertThrows(IllegalArgumentException.class, () -> bvmgr.makeBitvector(size, 1L << size));
548+
assertThrows(
549+
IllegalArgumentException.class, () -> bvmgr.makeBitvector(size, -(1L << (size - 1)) - 1));
560550
}
561551

562552
for (int size : new int[] {36, 40, 64, 65, 100, 128, 200, 250, 1000, 10000}) {
@@ -572,17 +562,14 @@ public void bvOutOfRange() {
572562
bvmgr.makeBitvector(size, BigInteger.ONE.shiftLeft(size - 1).negate());
573563

574564
// forbitten values
575-
try {
576-
bvmgr.makeBitvector(size, BigInteger.ONE.shiftLeft(size));
577-
assert_().fail();
578-
} catch (IllegalArgumentException expected) {
579-
}
580-
try {
581-
bvmgr.makeBitvector(
582-
size, BigInteger.ONE.shiftLeft(size - 1).negate().subtract(BigInteger.ONE));
583-
assert_().fail();
584-
} catch (IllegalArgumentException expected) {
585-
}
565+
assertThrows(
566+
IllegalArgumentException.class,
567+
() -> bvmgr.makeBitvector(size, BigInteger.ONE.shiftLeft(size)));
568+
assertThrows(
569+
IllegalArgumentException.class,
570+
() ->
571+
bvmgr.makeBitvector(
572+
size, BigInteger.ONE.shiftLeft(size - 1).negate().subtract(BigInteger.ONE)));
586573
}
587574
}
588575

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

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,8 @@
1010

1111
import static com.google.common.truth.Truth.assertThat;
1212
import static com.google.common.truth.Truth.assertWithMessage;
13-
import static com.google.common.truth.Truth.assert_;
1413
import static com.google.common.truth.TruthJUnit.assume;
14+
import static org.junit.Assert.assertThrows;
1515
import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
1616

1717
import com.google.common.collect.ImmutableList;
@@ -1024,11 +1024,9 @@ public void fpInterpolation() throws SolverException, InterruptedException {
10241024
}
10251025
}
10261026

1027-
@SuppressWarnings("CheckReturnValue")
1028-
@Test(expected = Exception.class)
1027+
@Test
10291028
public void failOnInvalidString() {
1030-
fpmgr.makeNumber("a", singlePrecType);
1031-
assert_().fail();
1029+
assertThrows(Exception.class, () -> fpmgr.makeNumber("a", singlePrecType));
10321030
}
10331031

10341032
@Test

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

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@
1111
import static com.google.common.collect.Iterables.getLast;
1212
import static com.google.common.truth.Truth.assertThat;
1313
import static com.google.common.truth.Truth.assertWithMessage;
14-
import static com.google.common.truth.Truth.assert_;
1514
import static com.google.common.truth.TruthJUnit.assume;
1615
import static org.junit.Assert.assertThrows;
1716
import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
@@ -362,8 +361,7 @@ public <T> void sequentialInterpolationIsNotRepeatedIndividualInterpolation()
362361
}
363362
}
364363

365-
@Test(expected = IllegalArgumentException.class)
366-
@SuppressWarnings("CheckReturnValue")
364+
@Test
367365
public <T> void sequentialInterpolationWithoutPartition()
368366
throws SolverException, InterruptedException {
369367
requireIntegers();
@@ -373,8 +371,8 @@ public <T> void sequentialInterpolationWithoutPartition()
373371
assertThat(stack).isUnsatisfiable();
374372

375373
// empty list of partition
376-
stack.getSeqInterpolants(ImmutableList.of());
377-
assert_().fail();
374+
assertThrows(
375+
IllegalArgumentException.class, () -> stack.getSeqInterpolants(ImmutableList.of()));
378376
}
379377

380378
@Test
@@ -973,8 +971,7 @@ public <T> void treeInterpolationMalFormed6() throws SolverException, Interrupte
973971
stack.getTreeInterpolants0(ImmutableList.of(TA, TA, TA), new int[] {0, 2, 0});
974972
}
975973

976-
@Test(expected = IllegalArgumentException.class)
977-
@SuppressWarnings("CheckReturnValue")
974+
@Test
978975
public <T> void treeInterpolationWithoutPartition() throws SolverException, InterruptedException {
979976
requireTreeItp();
980977

@@ -984,8 +981,9 @@ public <T> void treeInterpolationWithoutPartition() throws SolverException, Inte
984981
assertThat(stack).isUnsatisfiable();
985982

986983
// empty list of partition
987-
stack.getTreeInterpolants(ImmutableList.of(), new int[] {});
988-
assert_().fail();
984+
assertThrows(
985+
IllegalArgumentException.class,
986+
() -> stack.getTreeInterpolants(ImmutableList.of(), new int[] {}));
989987
}
990988

991989
@Test

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

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
import static com.google.common.truth.Truth.assertWithMessage;
1313
import static com.google.common.truth.Truth.assert_;
1414
import static com.google.common.truth.TruthJUnit.assume;
15+
import static org.junit.Assert.assertThrows;
1516
import static org.sosy_lab.java_smt.api.FormulaType.IntegerType;
1617
import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
1718

@@ -184,7 +185,7 @@ public void testGetRationals() throws SolverException, InterruptedException {
184185
/** Test that different names are no problem for Bools in the model. */
185186
@Test
186187
public void testGetBooleans() throws SolverException, InterruptedException {
187-
// Some names are specificly chosen to test the Boolector model
188+
// Some names are specifically chosen to test the Boolector model
188189
for (String name : VARIABLE_NAMES) {
189190
testModelGetters(bmgr.makeVariable(name), bmgr.makeBoolean(true), true, name);
190191
}
@@ -1207,12 +1208,12 @@ public void testGetArrays4() throws SolverException, InterruptedException {
12071208
ImmutableList.of(BigInteger.valueOf(5)));
12081209
}
12091210

1210-
@Test(expected = IllegalArgumentException.class)
1211-
@SuppressWarnings("CheckReturnValue")
1211+
@Test
12121212
public void testGetArrays4invalid() throws SolverException, InterruptedException {
12131213
requireParser();
12141214
requireArrays();
12151215
requireArrayModel();
1216+
requireIntegers();
12161217

12171218
// create formula for "arr[5]==x && x==123"
12181219
BooleanFormula f =
@@ -1229,7 +1230,9 @@ public void testGetArrays4invalid() throws SolverException, InterruptedException
12291230
assertThat(prover).isSatisfiable();
12301231

12311232
try (Model m = prover.getModel()) {
1232-
m.evaluate(amgr.makeArray("arr", ARRAY_TYPE_INT_INT));
1233+
assertThrows(
1234+
IllegalArgumentException.class,
1235+
() -> m.evaluate(amgr.makeArray("arr", ARRAY_TYPE_INT_INT)));
12331236
}
12341237
}
12351238
}
@@ -2306,22 +2309,19 @@ public void modelAfterSolverCloseTest() throws SolverException, InterruptedExcep
23062309
}
23072310
}
23082311

2309-
@SuppressWarnings("resource")
2310-
@Test(expected = IllegalStateException.class)
2312+
@Test
23112313
public void testGenerateModelsOption() throws SolverException, InterruptedException {
23122314
try (ProverEnvironment prover = context.newProverEnvironment()) { // no option
23132315
assertThat(prover).isSatisfiable();
2314-
prover.getModel();
2315-
assert_().fail();
2316+
assertThrows(IllegalStateException.class, () -> prover.getModel());
23162317
}
23172318
}
23182319

2319-
@Test(expected = IllegalStateException.class)
2320+
@Test
23202321
public void testGenerateModelsOption2() throws SolverException, InterruptedException {
23212322
try (ProverEnvironment prover = context.newProverEnvironment()) { // no option
23222323
assertThat(prover).isSatisfiable();
2323-
prover.getModelAssignments();
2324-
assert_().fail();
2324+
assertThrows(IllegalStateException.class, () -> prover.getModelAssignments());
23252325
}
23262326
}
23272327

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

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

1111
import static com.google.common.truth.Truth.assertThat;
12-
import static com.google.common.truth.Truth.assert_;
1312
import static com.google.common.truth.TruthJUnit.assume;
13+
import static org.junit.Assert.assertThrows;
1414

1515
import com.google.common.collect.Iterables;
1616
import java.util.HashSet;
@@ -139,10 +139,8 @@ protected Boolean visitDefault(Formula pF) {
139139
}
140140
}
141141

142-
@SuppressWarnings("CheckReturnValue")
143-
@Test(expected = Exception.class)
142+
@Test
144143
public void failOnInvalidString() {
145-
rmgr.makeNumber("a");
146-
assert_().fail();
144+
assertThrows(Exception.class, () -> rmgr.makeNumber("a"));
147145
}
148146
}

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

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

1111
import static com.google.common.truth.Truth.assertThat;
12-
import static com.google.common.truth.Truth.assert_;
12+
import static org.junit.Assert.assertThrows;
1313
import static org.sosy_lab.java_smt.api.FormulaType.BooleanType;
1414
import static org.sosy_lab.java_smt.api.FormulaType.IntegerType;
1515

@@ -199,7 +199,7 @@ public void ufEliminationNestedUfsTest() throws SolverException, InterruptedExce
199199
}
200200

201201
@Test
202-
public void ufEliminationNesteQuantifierTest() throws InterruptedException {
202+
public void ufEliminationNesteQuantifierTest() {
203203
requireIntegers();
204204
requireQuantifiers();
205205
// f := exists v1,v2v,v3,v4 : uf(v1, v3) == uf(v2, v4)
@@ -216,11 +216,7 @@ public void ufEliminationNesteQuantifierTest() throws InterruptedException {
216216
qmgr.exists(
217217
ImmutableList.of(variable1, variable2, variable3, variable4), bmgr.equivalence(f1, f2));
218218

219-
try {
220-
mgr.applyTactic(f, Tactic.ACKERMANNIZATION);
221-
assert_().fail();
222-
} catch (IllegalArgumentException expected) {
223-
}
219+
assertThrows(IllegalArgumentException.class, () -> mgr.applyTactic(f, Tactic.ACKERMANNIZATION));
224220
}
225221

226222
private static class CNFChecker implements BooleanFormulaVisitor<Void> {

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

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

99
package org.sosy_lab.java_smt.test;
1010

11-
import static com.google.common.truth.Truth.assert_;
1211
import static com.google.common.truth.TruthJUnit.assume;
12+
import static org.junit.Assert.assertThrows;
1313
import static org.sosy_lab.java_smt.api.FormulaType.BooleanType;
1414
import static org.sosy_lab.java_smt.api.FormulaType.IntegerType;
1515

@@ -238,11 +238,7 @@ public void quantifierTest() {
238238
qmgr.exists(
239239
ImmutableList.of(variable1, variable2, variable3, variable4), bmgr.equivalence(f1, f2));
240240

241-
try {
242-
ackermannization.eliminateUfs(f);
243-
assert_().fail();
244-
} catch (IllegalArgumentException expected) {
245-
}
241+
assertThrows(IllegalArgumentException.class, () -> ackermannization.eliminateUfs(f));
246242
}
247243

248244
@Test

0 commit comments

Comments
 (0)