fixed tests for mac and win

ftsrg · Jul 8, 2024 · a28db70 · a28db70
1 parent 515cd4a
commit a28db70
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 14 deletions.
diff --git a/...solver/solver-smtlib/src/test/java/hu/bme/mit/theta/solver/smtlib/SmtLibHornSolverTest.kt b/...solver/solver-smtlib/src/test/java/hu/bme/mit/theta/solver/smtlib/SmtLibHornSolverTest.kt
@@ -30,6 +30,7 @@ import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
 import hu.bme.mit.theta.core.type.inttype.IntType
 import hu.bme.mit.theta.solver.SolverFactory
 import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstallerException
+import org.junit.Assume
 import org.junit.jupiter.api.*
 import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.Arguments
@@ -51,7 +52,7 @@ class SmtLibHornSolverTest {
 
         @JvmStatic
         fun solvers(): List<Arguments> {
-            return solverFactories.map { Arguments.of(it.key, it.value) }
+            return SOLVERS.map { Arguments.of(it) }
         }
 
         @BeforeAll
@@ -94,7 +95,8 @@ class SmtLibHornSolverTest {
 
     @ParameterizedTest(name = "[{index}] {0}")
     @MethodSource("solvers")
-    fun testSolvable(name: Pair<String, String>, solverFactory: SolverFactory) {
+    fun testSolvable(name: Pair<String, String>) {
+        val solverFactory = solverFactories[name]!!
         val solver = solverFactory.createHornSolver()
         solver.use { hornSolver ->
             val p = ParamHolder(Int())
@@ -137,7 +139,8 @@ class SmtLibHornSolverTest {
 
     @ParameterizedTest(name = "[{index}] {0}")
     @MethodSource("solvers")
-    fun testUnsolvable(name: Pair<String, String>, solverFactory: SolverFactory) {
+    fun testUnsolvable(name: Pair<String, String>) {
+        val solverFactory = solverFactories[name]!!
         val solver = solverFactory.createHornSolver()
 
         solver.use { hornSolver ->
@@ -165,7 +168,8 @@ class SmtLibHornSolverTest {
 
     @ParameterizedTest(name = "[{index}] {0}")
     @MethodSource("solvers")
-    fun testNonlinearUnsolvable(name: Pair<String, String>, solverFactory: SolverFactory) {
+    fun testNonlinearUnsolvable(name: Pair<String, String>) {
+        val solverFactory = solverFactories[name]!!
         val solver = solverFactory.createHornSolver()
 
         solver.use { hornSolver ->

diff --git a/subprojects/xcfa/xcfa2chc/src/test/java/hu/bme/mit/theta/xcfa2chc/TestChcUtils.kt b/subprojects/xcfa/xcfa2chc/src/test/java/hu/bme/mit/theta/xcfa2chc/TestChcUtils.kt
@@ -34,7 +34,9 @@ import hu.bme.mit.theta.solver.SolverFactory
 import hu.bme.mit.theta.solver.SolverStatus
 import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager
 import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstallerException
-import org.junit.jupiter.api.*
+import org.junit.jupiter.api.AfterAll
+import org.junit.jupiter.api.Assertions
+import org.junit.jupiter.api.BeforeAll
 import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.Arguments
 import org.junit.jupiter.params.provider.MethodSource
@@ -56,8 +58,8 @@ class TestChcUtils {
         )
 
         @JvmStatic
-        fun solvers(): List<Arguments> {
-            return solverFactories.map { Arguments.of(it.key, it.value) }
+        fun solvers(): List<Arguments?> {
+            return SOLVERS.map { Arguments.of(it) }
         }
 
         @BeforeAll
@@ -93,14 +95,10 @@ class TestChcUtils {
         }
     }
 
-    @BeforeEach
-    fun before() {
-        Assumptions.assumeTrue(OsHelper.getOs() == OsHelper.OperatingSystem.LINUX)
-    }
-
     @ParameterizedTest(name = "[{index}] {0}")
     @MethodSource("solvers")
-    fun testPetersonManualCounting(name: Pair<String, String>, solverFactory: SolverFactory) {
+    fun testPetersonManualCounting(name: Pair<String, String>) {
+        val solverFactory = solverFactories[name]!!
         val i2i = ArrayType.of(Int(), Int())
 
         val pI = ParamHolder(Int())
@@ -400,7 +398,8 @@ class TestChcUtils {
 
     @ParameterizedTest(name = "[{index}] {0}")
     @MethodSource("solvers")
-    fun testPetersonNoCounting(name: Pair<String, String>, solverFactory: SolverFactory) {
+    fun testPetersonNoCounting(name: Pair<String, String>) {
+        val solverFactory = solverFactories[name]!!
         val i2i = ArrayType.of(Int(), Int())
 
         val pI = ParamHolder(Int())