From 097ce9df927ea0154388b3c2121e250d1471d8da Mon Sep 17 00:00:00 2001
From: Dmitry Ivanov <korifey@gmail.com>
Date: Mon, 3 Jul 2023 22:54:35 +0300
Subject: [PATCH] Fix problem when some variable is undefined and solver throw
 exception

---
 build.gradle.kts                         |  9 +--------
 gradle/wrapper/gradle-wrapper.properties |  2 +-
 src/commonMain/kotlin/org/kosat/CDCL.kt  | 18 ++++++++++++------
 src/input.txt                            |  0
 src/jvmMain/kotlin/org/kosat/Main.kt     |  6 +++++-
 src/jvmMain/kotlin/org/kosat/input.cnf   |  0
 src/jvmTest/kotlin/SmokeTest.kt          | 14 ++++++++++++++
 7 files changed, 33 insertions(+), 16 deletions(-)
 delete mode 100644 src/input.txt
 delete mode 100644 src/jvmMain/kotlin/org/kosat/input.cnf
 create mode 100644 src/jvmTest/kotlin/SmokeTest.kt

diff --git a/build.gradle.kts b/build.gradle.kts
index 87895563..38b89ec1 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -139,14 +139,7 @@ kotlin {
             }
         }
     }
-//    js(LEGACY) {
-//        binaries.executable()
-//        browser {
-//            commonWebpackConfig {
-//                cssSupport.enabled = true
-//            }
-//        }
-//    }
+
     sourceSets {
         val commonMain by getting {
             dependencies {
diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties
index 2e6e5897..8049c684 100644
--- a/gradle/wrapper/gradle-wrapper.properties
+++ b/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
diff --git a/src/commonMain/kotlin/org/kosat/CDCL.kt b/src/commonMain/kotlin/org/kosat/CDCL.kt
index a4e8302d..a59caa4c 100644
--- a/src/commonMain/kotlin/org/kosat/CDCL.kt
+++ b/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")
+//            }
         }
     }
 
diff --git a/src/input.txt b/src/input.txt
deleted file mode 100644
index e69de29b..00000000
diff --git a/src/jvmMain/kotlin/org/kosat/Main.kt b/src/jvmMain/kotlin/org/kosat/Main.kt
index bbf478c4..869a8b6a 100644
--- a/src/jvmMain/kotlin/org/kosat/Main.kt
+++ b/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()
     }
 }
diff --git a/src/jvmMain/kotlin/org/kosat/input.cnf b/src/jvmMain/kotlin/org/kosat/input.cnf
deleted file mode 100644
index e69de29b..00000000
diff --git a/src/jvmTest/kotlin/SmokeTest.kt b/src/jvmTest/kotlin/SmokeTest.kt
new file mode 100644
index 00000000..f31c35c8
--- /dev/null
+++ b/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()!! }
+    }
+}
\ No newline at end of file