Change command and file args to lambdas

Lipen · Nov 30, 2020 · ee97085 · ee97085
1 parent af1d94b
commit ee97085
Show file tree

Hide file tree

Showing 5 changed files with 22 additions and 28 deletions.
diff --git a/kotlin-satlib-core/src/main/kotlin/com/github/lipen/satlib/solver/DimacsFileSolver.kt b/kotlin-satlib-core/src/main/kotlin/com/github/lipen/satlib/solver/DimacsFileSolver.kt
@@ -11,8 +11,8 @@ import java.io.File
 
 @Suppress("MemberVisibilityCanBePrivate")
 class DimacsFileSolver @JvmOverloads constructor(
-    val command: String,
-    val file: File = createTempFile(),
+    val file: () -> File = { createTempFile() },
+    val command: (File) -> String,
 ) : AbstractSolver() {
     private var _model: Model? = null
 
@@ -41,8 +41,9 @@ class DimacsFileSolver @JvmOverloads constructor(
     override fun _addClause(literals: List<Lit>) {}
 
     override fun _solve(): Boolean {
+        val file = file()
         dumpDimacs(file)
-        val process = Runtime.getRuntime().exec(command.format(file))
+        val process = Runtime.getRuntime().exec(command(file))
         val processOutput = process.inputStream.source().buffer()
         _model = parseDimacsOutput(processOutput)
         return _model != null
@@ -64,20 +65,16 @@ class DimacsFileSolver @JvmOverloads constructor(
         return _model ?: error("Model is null because the solver is not in the SAT state")
     }
 
-    override fun toString(): String {
-        return "${this::class.java.simpleName}(\"$command\", \"$file\")"
-    }
-
     companion object {
-        private val ASSUMPTIONS_NOT_SUPPORTED: String =
-            "${DimacsFileSolver::class.java.simpleName} does not support solving with assumptions"
-        private val INTERRUPTION_NOT_SUPPORTED: String =
-            "${DimacsFileSolver::class.java.simpleName} does not support interruption"
+        private const val ASSUMPTIONS_NOT_SUPPORTED: String =
+            "DimacsFileSolver does not support solving with assumptions"
+        private const val INTERRUPTION_NOT_SUPPORTED: String =
+            "DimacsFileSolver does not support interruption"
     }
 }
 
 private fun main() {
-    DimacsFileSolver("cryptominisat5 %s", File("dimacs.cnf")).useWith {
+    DimacsFileSolver({ File("dimacs.cnf") }, { "cryptominisat5 $it" }).useWith {
         testSolverWithoutAssumptions()
     }
 }
diff --git a/kotlin-satlib-core/src/main/kotlin/com/github/lipen/satlib/solver/DimacsStreamSolver.kt b/kotlin-satlib-core/src/main/kotlin/com/github/lipen/satlib/solver/DimacsStreamSolver.kt
@@ -11,7 +11,7 @@ import okio.source
 
 @Suppress("MemberVisibilityCanBePrivate")
 class DimacsStreamSolver(
-    val command: String,
+    val command: () -> String,
 ) : AbstractSolver() {
     private var _model: Model? = null
 
@@ -40,6 +40,7 @@ class DimacsStreamSolver(
     override fun _addClause(literals: List<Lit>) {}
 
     override fun _solve(): Boolean {
+        val command = command()
         val process = Runtime.getRuntime().exec(command)
         val processInput = process.outputStream.sink().buffer()
         dumpDimacs(processInput)
@@ -66,20 +67,16 @@ class DimacsStreamSolver(
         return _model ?: error("Model is null because the solver is not in the SAT state")
     }
 
-    override fun toString(): String {
-        return "${this::class.java.simpleName}(\"$command\")"
-    }
-
     companion object {
-        private val ASSUMPTIONS_NOT_SUPPORTED: String =
-            "${DimacsStreamSolver::class.java.simpleName} does not support solving with assumptions"
-        private val INTERRUPTION_NOT_SUPPORTED: String =
-            "${DimacsStreamSolver::class.java.simpleName} does not support interruption"
+        private const val ASSUMPTIONS_NOT_SUPPORTED: String =
+            "DimacsStreamSolver does not support solving with assumptions"
+        private const val INTERRUPTION_NOT_SUPPORTED: String =
+            "DimacsStreamSolver does not support interruption"
     }
 }
 
 private fun main() {
-    DimacsStreamSolver("cryptominisat5").useWith {
+    DimacsStreamSolver { "cryptominisat5" }.useWith {
         testSolverWithoutAssumptions()
     }
 }
diff --git a/kotlin-satlib-core/src/test/kotlin/com/github/lipen/satlib/solver/DimacsFileSolverTest.kt b/kotlin-satlib-core/src/test/kotlin/com/github/lipen/satlib/solver/DimacsFileSolverTest.kt
@@ -10,7 +10,7 @@ import org.junit.jupiter.api.assertThrows
 @TestInstance(TestInstance.Lifecycle.PER_METHOD)
 class DimacsFileSolverTest {
     private val solverCmd = "cryptominisat5 %s"
-    private val solver: Solver = DimacsFileSolver(solverCmd, createTempFile())
+    private val solver: Solver = DimacsFileSolver({ createTempFile() }, { solverCmd.format(it) })
 
     @Test
     fun `simple SAT`(): Unit = with(solver) {

diff --git a/kotlin-satlib-core/src/test/kotlin/com/github/lipen/satlib/solver/DimacsStreamSolverTest.kt b/kotlin-satlib-core/src/test/kotlin/com/github/lipen/satlib/solver/DimacsStreamSolverTest.kt
@@ -10,7 +10,7 @@ import org.junit.jupiter.api.assertThrows
 @TestInstance(TestInstance.Lifecycle.PER_METHOD)
 class DimacsStreamSolverTest {
     private val solverCmd = "cryptominisat5"
-    private val solver: Solver = DimacsStreamSolver(solverCmd)
+    private val solver: Solver = DimacsStreamSolver { solverCmd }
 
     @Test
     fun `simple SAT`(): Unit = with(solver) {

diff --git a/kotlin-satlib-core/src/test/kotlin/com/github/lipen/satlib/solver/SolversTest.kt b/kotlin-satlib-core/src/test/kotlin/com/github/lipen/satlib/solver/SolversTest.kt
@@ -80,17 +80,17 @@ class SolversTest {
             listOf(
                 MiniSatSolver(),
                 GlucoseSolver(),
-                DimacsFileSolver("cryptominisat5 %s"),
-                DimacsStreamSolver("cryptominisat5"),
+                DimacsFileSolver { "cryptominisat5 $it" },
+                DimacsStreamSolver { "cryptominisat5" },
             )
         } else {
             listOf(
                 MiniSatSolver(),
                 GlucoseSolver(),
                 CadicalSolver(),
                 CryptoMiniSatSolver(),
-                DimacsFileSolver("cryptominisat5 %s"),
-                DimacsStreamSolver("cryptominisat5"),
+                DimacsFileSolver { "cryptominisat5 $it" },
+                DimacsStreamSolver { "cryptominisat5" },
             )
         }
 }