Add ksmt-noodler solver

ksmt-noodler/build.gradle.kts

@@ -0,0 +1,28 @@
+plugins {
+    id("io.ksmt.ksmt-base")
+}
+
+dependencies {
+    implementation(project(":ksmt-core"))
+    runtimeOnly(project(":ksmt-z3"))
+}
+
+tasks.register<JavaExec>("runNoodlerZ3Example") {
+    group = "application"
+    description = "Run Noodler ping-pong example with Z3 backend"
+    classpath = sourceSets["main"].runtimeClasspath
+    mainClass.set("io.ksmt.solver.noodler.core.NoodlerZ3ExampleKt")
+    jvmArgs("-Xss8m")
+}
+
+publishing {
+    publications {
+        create<MavenPublication>("maven") {
+            from(components["java"])
+
+            addKsmtPom()
+            addSourcesAndJavadoc(project)
+            signKsmtPublication(project)
+        }
+    }
+}

ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/KNoodlerSolver.kt

@@ -0,0 +1,153 @@
+package io.ksmt.solver.noodler
+
+import io.ksmt.KContext
+import io.ksmt.expr.KExpr
+import io.ksmt.solver.KModel
+import io.ksmt.solver.KSolver
+import io.ksmt.solver.KSolverConfiguration
+import io.ksmt.solver.KSolverStatus
+import io.ksmt.solver.KSolverUnsupportedFeatureException
+import io.ksmt.solver.noodler.automaton.ALL_CHAR_ALPHABET
+import io.ksmt.solver.noodler.core.Noodler
+import io.ksmt.solver.noodler.core.toNoodlerStatementOrNull
+import io.ksmt.sort.KBoolSort
+import kotlin.time.Duration
+
+class KNoodlerSolver(
+    private val ctx: KContext,
+    private val baseSolver: KSolver<out KSolverConfiguration>,
+    private val alphabet: List<Char> = ALL_CHAR_ALPHABET
+) : KSolver<KSolverConfiguration> {
+    private val assertions = arrayListOf<KExpr<KBoolSort>>()
+    private val assertionSet = linkedSetOf<KExpr<KBoolSort>>()
+    private val scopeMarks = ArrayDeque<Int>()
+
+    private var lastStatus = KSolverStatus.UNKNOWN
+    private var lastReason: String? = null
+
+    @Suppress("UNCHECKED_CAST")
+    override fun configure(configurator: KSolverConfiguration.() -> Unit) {
+        (baseSolver as KSolver<KSolverConfiguration>).configure(configurator)
+    }
+
+    override fun assert(expr: KExpr<KBoolSort>) {
+        ctx.ensureContextMatch(expr)
+
+        if (!assertionSet.add(expr)) {
+            return
+        }
+
+        assertions += expr
+        baseSolver.assert(expr)
+    }
+
+    override fun assertAndTrack(expr: KExpr<KBoolSort>) = assert(expr)
+
+    override fun push() {
+        baseSolver.push()
+        scopeMarks.addLast(assertions.size)
+    }
+
+    override fun pop(n: UInt) {
+        require(n.toInt() <= scopeMarks.size) {
+            "Can not pop $n scope levels because current scope level is ${scopeMarks.size}"
+        }
+
+        repeat(n.toInt()) {
+            baseSolver.pop()
+
+            val scopeMark = scopeMarks.removeLast()
+            while (assertions.size > scopeMark) {
+                val removed = assertions.removeAt(assertions.lastIndex)
+                assertionSet.remove(removed)
+            }
+        }
+    }
+
+    override fun check(timeout: Duration): KSolverStatus {
+        lastStatus = KSolverStatus.UNKNOWN
+        lastReason = null
+
+        while (true) {
+            val noodlerAssertions = assertions.mapNotNull { it.toNoodlerStatementOrNull() }
+            if (noodlerAssertions.isEmpty()) {
+                lastStatus = baseSolver.check(timeout)
+                if (lastStatus == KSolverStatus.UNKNOWN) {
+                    lastReason = baseSolver.reasonOfUnknown()
+                }
+                return lastStatus
+            }
+
+            val (isSat, extraConstraints) = Noodler(noodlerAssertions, alphabet).solve()
+            if (!isSat) {
+                lastStatus = KSolverStatus.UNSAT
+                return lastStatus
+            }
+
+            val hasFreshConstraints = assertFreshConstraints(extraConstraints)
+
+            val baseStatus = baseSolver.check(timeout)
+            if (baseStatus != KSolverStatus.SAT) {
+                lastStatus = baseStatus
+                if (baseStatus == KSolverStatus.UNKNOWN) {
+                    lastReason = baseSolver.reasonOfUnknown()
+                }
+                return lastStatus
+            }
+
+            if (!hasFreshConstraints) {
+                lastStatus = KSolverStatus.SAT
+                return lastStatus
+            }
+        }
+    }
+
+    override fun checkWithAssumptions(
+        assumptions: List<KExpr<KBoolSort>>,
+        timeout: Duration
+    ): KSolverStatus {
+        ctx.ensureContextMatch(assumptions)
+
+        push()
+        try {
+            assumptions.forEach(::assert)
+            return check(timeout)
+        } finally {
+            pop()
+        }
+    }
+
+    override fun model(): KModel {
+        require(lastStatus == KSolverStatus.SAT) {
+            "Model is only available after SAT checks, current solver status: $lastStatus"
+        }
+
+        return baseSolver.model()
+    }
+
+    override fun unsatCore(): List<KExpr<KBoolSort>> {
+        throw KSolverUnsupportedFeatureException("Unsat core is not supported by KNoodlerSolver")
+    }
+
+    override fun reasonOfUnknown(): String = lastReason ?: "unknown"
+
+    override fun interrupt() = baseSolver.interrupt()
+
+    override fun close() = baseSolver.close()
+
+    private fun assertFreshConstraints(constraints: List<KExpr<KBoolSort>>): Boolean {
+        var hasFreshConstraints = false
+
+        for (constraint in constraints) {
+            if (!assertionSet.add(constraint)) {
+                continue
+            }
+
+            assertions += constraint
+            baseSolver.assert(constraint)
+            hasFreshConstraints = true
+        }
+
+        return hasFreshConstraints
+    }
+}

ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/Automaton.kt

@@ -0,0 +1,179 @@
+package io.ksmt.solver.noodler.automaton
+
+import java.io.IOException
+import java.nio.file.Files
+import java.nio.file.Paths
+
+abstract class Automaton<N: Node<N>, A: Automaton<N, A>>(
+    val start: N,
+    var alphabet: List<Char>,
+) {
+    var terminal: List<N> = listNodes(start, { it.terminal })
+
+    protected abstract fun newAutomaton(start: N, alphabet: List<Char>): Automaton<N, A>
+    protected abstract fun scanExtraSymbols(visited: MutableSet<N>)
+
+    open fun check(word: String): Boolean {
+        var visited = mutableSetOf(start)
+        scanExtraSymbols(visited)
+        for (letter in word) {
+            val newVisited = mutableSetOf<N>()
+            for (current in visited) {
+                for (new in current.getList(letter)) {
+                    if (!newVisited.contains(new)) {
+                        newVisited.add(new)
+                    }
+                }
+            }
+            visited = newVisited
+            scanExtraSymbols(visited)
+        }
+        return visited.intersect(terminal.toSet()).isNotEmpty()
+    }
+
+    open fun isEmpty(): Boolean {
+        return listNodes(start, { true }).all { !it.terminal}
+    }
+
+    open fun isNotEmpty(): Boolean {
+        return !isEmpty()
+    }
+
+    fun copy(): Automaton<N, A> {
+        val root = copy(start)
+        return newAutomaton(root, alphabet)
+    }
+
+    fun picture(filename: String) {
+        val output = Paths.get(filename).toAbsolutePath()
+        val format = graphvizFormat(output.fileName.toString())
+
+        output.parent?.let(Files::createDirectories)
+
+        val process = try {
+            ProcessBuilder("dot", "-T$format", "-o", output.toString())
+                .redirectErrorStream(true)
+                .start()
+        } catch (ex: IOException) {
+            throw IllegalStateException(
+                "Failed to start Graphviz 'dot'. Make sure Graphviz is installed and available on PATH.",
+                ex
+            )
+        }
+
+        process.outputStream.bufferedWriter(Charsets.UTF_8).use { writer ->
+            writer.write(toDot())
+        }
+
+        val graphvizOutput = process.inputStream.bufferedReader(Charsets.UTF_8).use { reader ->
+            reader.readText().trim()
+        }
+        val exitCode = process.waitFor()
+
+        check(exitCode == 0) {
+            val details = if (graphvizOutput.isEmpty()) "" else ": $graphvizOutput"
+            "Graphviz failed to render automaton$details"
+        }
+        check(Files.exists(output) && Files.size(output) > 0) {
+            "Graphviz did not create output file '$output'"
+        }
+    }
+
+    internal fun toDot(): String {
+        val nodes = orderedNodes()
+        val nodeIds = nodes.mapIndexed { index, node -> node to "q$index" }.toMap()
+
+        return buildString {
+            fun appendDotLine(line: String) {
+                append(line)
+                append('\n')
+            }
+
+            appendDotLine("digraph Automaton {")
+            appendDotLine("    rankdir=LR;")
+            appendDotLine("    start [shape=point];")
+            appendDotLine("    start -> ${nodeIds.getValue(start)};")
+
+            for (node in nodes) {
+                val nodeId = nodeIds.getValue(node)
+                val shape = if (node.terminal) "doublecircle" else "circle"
+                appendDotLine("    $nodeId [shape=$shape, label=\"${escapeGraphviz(nodeId)}\"];")
+            }
+
+            for (node in nodes) {
+                val groupedTransitions = linkedMapOf<N, MutableSet<Char>>()
+                for ((letter, children) in node.getAllList().entries.sortedBy { it.key.code }) {
+                    for (child in children.sortedBy { nodeIds.getValue(it) }) {
+                        groupedTransitions.getOrPut(child) { linkedSetOf() }.add(letter)
+                    }
+                }
+
+                for ((child, letters) in groupedTransitions.entries.sortedBy { nodeIds.getValue(it.key) }) {
+                    val label = letters
+                        .sortedBy { it.code }
+                        .joinToString(", ") { graphvizLabel(it) }
+
+                    appendDotLine(
+                        "    ${nodeIds.getValue(node)} -> ${nodeIds.getValue(child)} " +
+                            "[label=\"${escapeGraphviz(label)}\"];"
+                    )
+                }
+            }
+
+            appendDotLine("}")
+        }
+    }
+
+    private fun orderedNodes(): List<N> {
+        val ordered = LinkedHashSet<N>()
+        val queue = ArrayDeque<N>()
+
+        ordered.add(start)
+        queue.add(start)
+
+        while (queue.isNotEmpty()) {
+            val current = queue.removeFirst()
+            for ((_, children) in current.getAllList().entries.sortedBy { it.key.code }) {
+                for (child in children) {
+                    if (ordered.add(child)) {
+                        queue.add(child)
+                    }
+                }
+            }
+        }
+
+        return ordered.toList()
+    }
+}
+
+private fun graphvizFormat(filename: String): String {
+    val extension = filename.substringAfterLast('.', "")
+    require(extension.isNotBlank()) {
+        "filename must have an extension supported by Graphviz, for example '.png' or '.svg'"
+    }
+
+    return when (extension.lowercase()) {
+        "jpg" -> "jpeg"
+        else -> extension.lowercase()
+    }
+}
+
+private fun graphvizLabel(symbol: Char): String = when (symbol) {
+    EPS -> "eps"
+    ' ' -> "space"
+    else -> if (Character.isISOControl(symbol)) {
+        "U+" + symbol.code.toString(16).uppercase().padStart(4, '0')
+    } else {
+        symbol.toString()
+    }
+}
+
+private fun escapeGraphviz(value: String): String = buildString {
+    for (symbol in value) {
+        when (symbol) {
+            '\\' -> append("\\\\")
+            '"' -> append("\\\"")
+            else -> append(symbol)
+        }
+    }
+}