Skip to content

Commit 71db611

Browse files
daniel-rafflerdaniel-raffler
committed
Move platform detection in example projects to a separate file
1 parent 713f7b2 commit 71db611

10 files changed

Lines changed: 395 additions & 289 deletions

File tree

‎doc/Example-Gradle-Project-Kotlin/src/test/kotlin/org/sosy_lab/java_smt_example/AppTest.kt‎

Lines changed: 1 addition & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ class AppTest {
8787

8888
@BeforeEach
8989
fun init() {
90-
assumeTrue(isSupportedOperatingSystemAndArchitecture(solver))
90+
assumeTrue(Platform.isSupported(solver))
9191
}
9292

9393
@Test
@@ -138,67 +138,6 @@ class AppTest {
138138
@JvmStatic
139139
fun getAllSolvers() = Solvers.entries.toTypedArray()
140140

141-
private val OS: String =
142-
StandardSystemProperty.OS_NAME.value()!!.lowercase(Locale.getDefault()).replace(" ", "")
143-
private val ARCH: String =
144-
StandardSystemProperty.OS_ARCH.value()!!.lowercase(Locale.getDefault()).replace(" ", "")
145-
146-
protected val IS_WINDOWS: Boolean = OS.startsWith("windows")
147-
private val IS_MAC: Boolean = OS.startsWith("macos")
148-
private val IS_LINUX: Boolean = OS.startsWith("linux")
149-
150-
private val IS_ARCH_ARM64 = ARCH == "aarch64"
151-
152-
private fun isSufficientVersionOfLibcxx(library: String): Boolean {
153-
try {
154-
NativeLibraries.loadLibrary(library)
155-
} catch (e: UnsatisfiedLinkError) {
156-
for (dependency in getRequiredLibcxx(library)) {
157-
if (e.message!!.contains("version `" + dependency + "' not found")) {
158-
return false
159-
}
160-
}
161-
}
162-
return true
163-
}
164-
165-
private fun getRequiredLibcxx(library: String): List<String> {
166-
return when (library) {
167-
"z3" -> listOf("GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29")
168-
"bitwuzlaj" -> listOf("GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29")
169-
"opensmtj" -> listOf("GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29")
170-
"mathsat5j" -> listOf("GLIBC_2.33", "GLIBC_2.38")
171-
"cvc5jni" -> listOf("GLIBC_2.32")
172-
"yices2java" -> listOf("GLIBC_2.34")
173-
else -> listOf()
174-
}
175-
}
176-
177-
/** Disable some checks on certain combinations of operating systems and solvers, because of missing dependencies. */
178-
private fun isSupportedOperatingSystemAndArchitecture(solver: Solvers): Boolean {
179-
return when (solver) {
180-
Solvers.SMTINTERPOL, Solvers.PRINCESS -> true
181-
Solvers.BOOLECTOR, Solvers.CVC4 -> IS_LINUX && !IS_ARCH_ARM64
182-
Solvers.YICES2 -> (IS_LINUX && !IS_ARCH_ARM64 && isSufficientVersionOfLibcxx("yices2java"))
183-
|| (IS_WINDOWS && !IS_ARCH_ARM64)
184-
185-
Solvers.CVC5 -> (IS_LINUX && isSufficientVersionOfLibcxx("cvc5jni"))
186-
|| IS_WINDOWS
187-
|| IS_MAC
188-
189-
Solvers.OPENSMT -> IS_LINUX && isSufficientVersionOfLibcxx("opensmtj")
190-
Solvers.BITWUZLA -> (IS_LINUX && isSufficientVersionOfLibcxx("bitwuzlaj"))
191-
|| (IS_WINDOWS && !IS_ARCH_ARM64)
192-
193-
Solvers.MATHSAT5 -> (IS_WINDOWS && !IS_ARCH_ARM64)
194-
Solvers.Z3 -> (IS_LINUX && isSufficientVersionOfLibcxx("z3"))
195-
|| IS_WINDOWS
196-
|| IS_MAC
197-
198-
Solvers.Z3_WITH_INTERPOLATION -> IS_LINUX && !IS_ARCH_ARM64
199-
}
200-
}
201-
202141
private val input = """
203142
|2..9.6..1
204143
|..6.4...9

‎doc/Example-Gradle-Project-Kotlin/src/test/kotlin/org/sosy_lab/java_smt_example/Platform.kt‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
// This file is part of JavaSMT,
2+
// an API wrapper for a collection of SMT solvers:
3+
// https://github.com/sosy-lab/java-smt
4+
//
5+
// SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
6+
//
7+
// SPDX-License-Identifier: Apache-2.0
8+
package org.sosy_lab.java_smt_example
9+
10+
import com.google.common.base.StandardSystemProperty
11+
import org.sosy_lab.common.NativeLibraries
12+
import org.sosy_lab.java_smt.SolverContextFactory
13+
import java.util.*
14+
15+
internal object Platform {
16+
private val OS: String = StandardSystemProperty.OS_NAME.value()!!.lowercase(Locale.getDefault()).replace(" ", "")
17+
private val ARCH: String = StandardSystemProperty.OS_ARCH.value()!!.lowercase(Locale.getDefault()).replace(" ", "")
18+
19+
private val IS_WINDOWS: Boolean = OS.startsWith("windows")
20+
private val IS_MAC: Boolean = OS.startsWith("macos")
21+
private val IS_LINUX: Boolean = OS.startsWith("linux")
22+
23+
private val IS_ARCH_ARM64: Boolean = ARCH.equals("aarch64")
24+
25+
private fun isSufficientVersionOfLibcxx(library: String): Boolean {
26+
try {
27+
NativeLibraries.loadLibrary(library)
28+
} catch (e: UnsatisfiedLinkError) {
29+
for (dependency in getRequiredLibcxx(library)) {
30+
if (e.message!!.contains("version `" + dependency + "' not found")) {
31+
return false
32+
}
33+
}
34+
}
35+
return true
36+
}
37+
38+
private fun getRequiredLibcxx(library: String): Array<out String?> {
39+
return when (library) {
40+
"z3" -> arrayOf<String>("GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29")
41+
"bitwuzlaj" -> arrayOf<String>("GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29")
42+
"opensmtj" -> arrayOf<String>("GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29")
43+
"mathsat5j" -> arrayOf<String>("GLIBC_2.33", "GLIBC_2.38")
44+
"cvc5jni" -> arrayOf<String>("GLIBC_2.32")
45+
"yices2java" -> arrayOf<String>("GLIBC_2.34")
46+
else -> arrayOf<String?>()
47+
}
48+
}
49+
50+
/**
51+
* `True` if the solver is supported on the current operating system and CPU
52+
* architecture
53+
*/
54+
fun isSupported(solver: SolverContextFactory.Solvers): Boolean {
55+
return when (solver) {
56+
SolverContextFactory.Solvers.SMTINTERPOL, SolverContextFactory.Solvers.PRINCESS ->
57+
// Any operating system and any architecture is allowed, Java is sufficient
58+
true
59+
60+
SolverContextFactory.Solvers.BOOLECTOR, SolverContextFactory.Solvers.CVC4 ->
61+
IS_LINUX && !IS_ARCH_ARM64
62+
63+
SolverContextFactory.Solvers.YICES2 ->
64+
(IS_LINUX && !IS_ARCH_ARM64 && isSufficientVersionOfLibcxx("yices2java")) || (IS_WINDOWS && !IS_ARCH_ARM64)
65+
66+
SolverContextFactory.Solvers.CVC5 ->
67+
(IS_LINUX && isSufficientVersionOfLibcxx("cvc5jni")) || IS_WINDOWS || IS_MAC
68+
69+
SolverContextFactory.Solvers.OPENSMT ->
70+
IS_LINUX && isSufficientVersionOfLibcxx("opensmtj")
71+
72+
SolverContextFactory.Solvers.BITWUZLA ->
73+
(IS_LINUX && isSufficientVersionOfLibcxx("bitwuzlaj")) || (IS_WINDOWS && !IS_ARCH_ARM64)
74+
75+
SolverContextFactory.Solvers.MATHSAT5 ->
76+
(IS_LINUX && isSufficientVersionOfLibcxx("mathsat5j")) || (IS_WINDOWS && !IS_ARCH_ARM64)
77+
78+
SolverContextFactory.Solvers.Z3 ->
79+
(IS_LINUX && isSufficientVersionOfLibcxx("z3")) || IS_WINDOWS || IS_MAC
80+
81+
SolverContextFactory.Solvers.Z3_WITH_INTERPOLATION ->
82+
IS_LINUX && !IS_ARCH_ARM64
83+
}
84+
}
85+
}

‎doc/Example-Gradle-Project/src/test/java/org/sosy_lab/java_smt_example/Platform.java‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
// This file is part of JavaSMT,
2+
// an API wrapper for a collection of SMT solvers:
3+
// https://github.com/sosy-lab/java-smt
4+
//
5+
// SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
6+
//
7+
// SPDX-License-Identifier: Apache-2.0
8+
9+
package org.sosy_lab.java_smt_example;
10+
11+
import com.google.common.base.StandardSystemProperty;
12+
import java.util.Locale;
13+
import org.sosy_lab.common.NativeLibraries;
14+
import org.sosy_lab.java_smt.SolverContextFactory;
15+
16+
class Platform {
17+
private static final String OS =
18+
StandardSystemProperty.OS_NAME.value().toLowerCase(Locale.getDefault()).replace(" ", "");
19+
private static final String ARCH =
20+
StandardSystemProperty.OS_ARCH.value().toLowerCase(Locale.getDefault()).replace(" ", "");
21+
22+
private static final boolean IS_WINDOWS = OS.startsWith("windows");
23+
private static final boolean IS_MAC = OS.startsWith("macos");
24+
private static final boolean IS_LINUX = OS.startsWith("linux");
25+
26+
private static final boolean IS_ARCH_ARM64 = ARCH.equals("aarch64");
27+
28+
private static boolean isSufficientVersionOfLibcxx(String library) {
29+
try {
30+
NativeLibraries.loadLibrary(library);
31+
} catch (UnsatisfiedLinkError e) {
32+
for (String dependency : getRequiredLibcxx(library)) {
33+
if (e.getMessage().contains("version `" + dependency + "' not found")) {
34+
return false;
35+
}
36+
}
37+
}
38+
return true;
39+
}
40+
41+
private static String[] getRequiredLibcxx(String library) {
42+
return switch (library) {
43+
case "z3" -> new String[] {"GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"};
44+
case "bitwuzlaj" -> new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"};
45+
case "opensmtj" -> new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"};
46+
case "mathsat5j" -> new String[] {"GLIBC_2.33", "GLIBC_2.38"};
47+
case "cvc5jni" -> new String[] {"GLIBC_2.32"};
48+
case "yices2java" -> new String[] {"GLIBC_2.34"};
49+
default -> new String[] {};
50+
};
51+
}
52+
53+
/**
54+
* <code>True</code> if the solver is supported on the current operating system and CPU
55+
* architecture
56+
*/
57+
static boolean isSupported(SolverContextFactory.Solvers solver) {
58+
return switch (solver) {
59+
case SMTINTERPOL, PRINCESS ->
60+
// Any operating system and any architecture is allowed, Java is sufficient
61+
true;
62+
case BOOLECTOR, CVC4 -> IS_LINUX && !IS_ARCH_ARM64;
63+
case YICES2 ->
64+
(IS_LINUX && !IS_ARCH_ARM64 && isSufficientVersionOfLibcxx("yices2java"))
65+
|| (IS_WINDOWS && !IS_ARCH_ARM64);
66+
case CVC5 -> (IS_LINUX && isSufficientVersionOfLibcxx("cvc5jni")) || IS_WINDOWS || IS_MAC;
67+
case OPENSMT -> IS_LINUX && isSufficientVersionOfLibcxx("opensmtj");
68+
case BITWUZLA ->
69+
(IS_LINUX && isSufficientVersionOfLibcxx("bitwuzlaj")) || (IS_WINDOWS && !IS_ARCH_ARM64);
70+
case MATHSAT5 ->
71+
(IS_LINUX && isSufficientVersionOfLibcxx("mathsat5j")) || (IS_WINDOWS && !IS_ARCH_ARM64);
72+
case Z3 -> (IS_LINUX && isSufficientVersionOfLibcxx("z3")) || IS_WINDOWS || IS_MAC;
73+
case Z3_WITH_INTERPOLATION -> IS_LINUX && !IS_ARCH_ARM64;
74+
};
75+
}
76+
}

‎doc/Example-Gradle-Project/src/test/java/org/sosy_lab/java_smt_example/SudokuTest.java‎

Lines changed: 1 addition & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -10,14 +10,12 @@
1010

1111
import com.google.common.base.Joiner;
1212
import com.google.common.base.Splitter;
13-
import com.google.common.base.StandardSystemProperty;
1413
import org.junit.jupiter.api.AfterEach;
1514
import org.junit.jupiter.api.BeforeEach;
1615
import org.junit.jupiter.api.Test;
1716
import org.junit.jupiter.params.Parameter;
1817
import org.junit.jupiter.params.ParameterizedClass;
1918
import org.junit.jupiter.params.provider.MethodSource;
20-
import org.sosy_lab.common.NativeLibraries;
2119
import org.sosy_lab.common.ShutdownNotifier;
2220
import org.sosy_lab.common.configuration.Configuration;
2321
import org.sosy_lab.common.configuration.InvalidConfigurationException;
@@ -32,7 +30,6 @@
3230

3331
import java.util.Arrays;
3432
import java.util.List;
35-
import java.util.Locale;
3633
import java.util.logging.Level;
3734

3835
import static org.junit.jupiter.api.Assertions.assertEquals;
@@ -89,17 +86,6 @@ public static List<Solvers> getAllSolvers() {
8986
@Parameter(0)
9087
public Solvers solver;
9188

92-
private static final String OS =
93-
StandardSystemProperty.OS_NAME.value().toLowerCase(Locale.getDefault()).replace(" ", "");
94-
private static final String ARCH =
95-
StandardSystemProperty.OS_ARCH.value().toLowerCase(Locale.getDefault()).replace(" ", "");
96-
97-
protected static final boolean IS_WINDOWS = OS.startsWith("windows");
98-
private static final boolean IS_MAC = OS.startsWith("macos");
99-
private static final boolean IS_LINUX = OS.startsWith("linux");
100-
101-
private static final boolean IS_ARCH_ARM64 = ARCH.equals("aarch64");
102-
10389
private Configuration config;
10490
private LogManager logger;
10591
private ShutdownNotifier notifier;
@@ -132,7 +118,7 @@ public static List<Solvers> getAllSolvers() {
132118

133119
@BeforeEach
134120
public void init() throws InvalidConfigurationException {
135-
assumeTrue(isSupportedOperatingSystemAndArchitecture(solver));
121+
assumeTrue(Platform.isSupported(solver));
136122

137123
config = Configuration.defaultConfiguration();
138124
logger = BasicLogManager.create(config);
@@ -149,48 +135,6 @@ public final void closeSolver() {
149135
}
150136
}
151137

152-
private boolean isSufficientVersionOfLibcxx(String library) {
153-
try {
154-
NativeLibraries.loadLibrary(library);
155-
} catch (UnsatisfiedLinkError e) {
156-
for (String dependency : getRequiredLibcxx(library)) {
157-
if (e.getMessage().contains("version `" + dependency + "' not found")) {
158-
return false;
159-
}
160-
}
161-
}
162-
return true;
163-
}
164-
165-
private String[] getRequiredLibcxx(String library) {
166-
return switch (library) {
167-
case "z3" -> new String[]{"GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"};
168-
case "bitwuzlaj" -> new String[]{"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"};
169-
case "opensmtj" -> new String[]{"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"};
170-
case "mathsat5j" -> new String[]{"GLIBC_2.33", "GLIBC_2.38"};
171-
case "cvc5jni" -> new String[]{"GLIBC_2.32"};
172-
case "yices2java" -> new String[]{"GLIBC_2.34"};
173-
default -> new String[]{};
174-
};
175-
}
176-
177-
private boolean isSupportedOperatingSystemAndArchitecture(Solvers solver) {
178-
return switch (solver) {
179-
case SMTINTERPOL, PRINCESS ->
180-
// Any operating system and any architecture is allowed, Java is sufficient
181-
true;
182-
case BOOLECTOR, CVC4 -> IS_LINUX && !IS_ARCH_ARM64;
183-
case YICES2 -> (IS_LINUX && !IS_ARCH_ARM64 && isSufficientVersionOfLibcxx("yices2java"))
184-
|| (IS_WINDOWS && !IS_ARCH_ARM64);
185-
case CVC5 -> (IS_LINUX && isSufficientVersionOfLibcxx("cvc5jni")) || IS_WINDOWS || IS_MAC;
186-
case OPENSMT -> IS_LINUX && isSufficientVersionOfLibcxx("opensmtj");
187-
case BITWUZLA -> (IS_LINUX && isSufficientVersionOfLibcxx("bitwuzlaj")) || (IS_WINDOWS && !IS_ARCH_ARM64);
188-
case MATHSAT5 -> (IS_LINUX && isSufficientVersionOfLibcxx("mathsat5j")) || (IS_WINDOWS && !IS_ARCH_ARM64);
189-
case Z3 -> (IS_LINUX && isSufficientVersionOfLibcxx("z3")) || IS_WINDOWS || IS_MAC;
190-
case Z3_WITH_INTERPOLATION -> IS_LINUX && !IS_ARCH_ARM64;
191-
};
192-
}
193-
194138
@Test
195139
public void checkSudoku()
196140
throws InvalidConfigurationException, InterruptedException, SolverException {

0 commit comments

Comments
 (0)