Fix problem when some variable is undefined and solver throw exception

build.gradle.kts

@@ -139,14 +139,7 @@ kotlin {
             }
         }
     }
-//    js(LEGACY) {
-//        binaries.executable()
-//        browser {
-//            commonWebpackConfig {
-//                cssSupport.enabled = true
-//            }
-//        }
-//    }
+
     sourceSets {
         val commonMain by getting {
             dependencies {

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-7.3.3-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-7.5-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

src/commonMain/kotlin/org/kosat/CDCL.kt

@@ -5,6 +5,12 @@ import org.kosat.heuristics.VSIDS
 import org.kosat.heuristics.VariableSelector
 
 // CDCL
+/**
+ * Solves [cnf] and returns
+ * `null` if request unsatisfiable
+ * [emptyList] is request is tautology
+ * assignments of literals otherwise
+ */
 fun solveCnf(cnf: CnfRequest): List<Int>? {
     val clauses = (cnf.clauses.map { it.lits }).toMutableList()
     return CDCL(clauses.map { Clause(it) }.toMutableList(), cnf.vars).solve()
@@ -330,13 +336,13 @@ class CDCL(private val solverType: SolverType = SolverType.INCREMENTAL) {
     // return current assignment of variables
     private fun getModel(): List<Int> = vars.mapIndexed { index, v ->
         when (v.value) {
-            VarValue.TRUE -> index + 1
+            VarValue.TRUE, VarValue.UNDEFINED -> index + 1
             VarValue.FALSE -> -index - 1
-            VarValue.UNDEFINED -> {
-                println(vars)
-                println(trail)
-                throw Exception("Unexpected unassigned variable")
-            }
+//            VarValue.UNDEFINED -> {
+//                println(vars)
+//                println(trail)
+//                throw Exception("Unexpected unassigned variable")
+//            }
         }
     }
 

src/jvmMain/kotlin/org/kosat/Main.kt

@@ -20,7 +20,11 @@ fun main(args: Array<String>) {
 
     when (args.size) {
         0 -> run(System.`in`.bufferedReader().readText())
-        2 -> if (args[0] == "--file") run(File(args[1]).readText()) else usage()
+        2 ->
+            if (args[0] == "--file")
+                run(File(args[1]).readText())
+            else
+                usage()
         else -> usage()
     }
 }

src/jvmTest/kotlin/SmokeTest.kt

@@ -0,0 +1,14 @@
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.TestInstance
+import org.kosat.CDCL
+import kotlin.test.assertTrue
+
+@TestInstance(TestInstance.Lifecycle.PER_CLASS)
+internal class SmokeTest {
+    @Test
+    fun `test one variable`() {
+        val solver = CDCL()
+        solver.addVariable()
+        assertTrue { solver.solve()?.isNotEmpty()!! }
+    }
+}