From d3c1744507d5a49fb89236d3eb1ccec168e05f77 Mon Sep 17 00:00:00 2001 From: Rainbowcat13 Date: Tue, 24 Mar 2026 10:35:05 +0300 Subject: [PATCH] Add ksmt-noodler first version --- ksmt-noodler/build.gradle.kts | 28 ++ .../io/ksmt/solver/noodler/KNoodlerSolver.kt | 153 +++++++++ .../solver/noodler/automaton/Automaton.kt | 179 +++++++++++ .../solver/noodler/automaton/BaseAutomata.kt | 56 ++++ .../io/ksmt/solver/noodler/automaton/DFA.kt | 153 +++++++++ .../io/ksmt/solver/noodler/automaton/NFA.kt | 196 ++++++++++++ .../io/ksmt/solver/noodler/automaton/Node.kt | 118 +++++++ .../io/ksmt/solver/noodler/automaton/Regex.kt | 162 ++++++++++ .../io/ksmt/solver/noodler/core/Noodler.kt | 299 ++++++++++++++++++ .../solver/noodler/core/NoodlerStatements.kt | 38 +++ .../solver/noodler/core/NoodlerZ3Example.kt | 47 +++ .../solver/noodler/core/SolverInteractor.kt | 53 ++++ .../noodler/automaton/AutomatonPictureTest.kt | 83 +++++ .../noodler/automaton/BaseAutomataTest.kt | 66 ++++ .../noodler/automaton/DFAMinimizeTest.kt | 58 ++++ .../ksmt/solver/noodler/automaton/DFATest.kt | 61 ++++ .../noodler/automaton/NFAExtendedTest.kt | 123 +++++++ .../ksmt/solver/noodler/automaton/NFATest.kt | 238 ++++++++++++++ .../noodler/automaton/RegexToNFATest.kt | 176 +++++++++++ .../noodler/automaton/TransformToDFATest.kt | 75 +++++ .../ksmt/solver/noodler/core/NoodlerTest.kt | 105 ++++++ settings.gradle.kts | 1 + 22 files changed, 2468 insertions(+) create mode 100644 ksmt-noodler/build.gradle.kts create mode 100644 ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/KNoodlerSolver.kt create mode 100644 ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/Automaton.kt create mode 100644 ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/BaseAutomata.kt create mode 100644 ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/DFA.kt create mode 100644 ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/NFA.kt create mode 100644 ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/Node.kt create mode 100644 ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/Regex.kt create mode 100644 ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/Noodler.kt create mode 100644 ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/NoodlerStatements.kt create mode 100644 ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/NoodlerZ3Example.kt create mode 100644 ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/SolverInteractor.kt create mode 100644 ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/AutomatonPictureTest.kt create mode 100644 ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/BaseAutomataTest.kt create mode 100644 ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/DFAMinimizeTest.kt create mode 100644 ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/DFATest.kt create mode 100644 ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/NFAExtendedTest.kt create mode 100644 ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/NFATest.kt create mode 100644 ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/RegexToNFATest.kt create mode 100644 ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/TransformToDFATest.kt create mode 100644 ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/core/NoodlerTest.kt diff --git a/ksmt-noodler/build.gradle.kts b/ksmt-noodler/build.gradle.kts new file mode 100644 index 000000000..56c606255 --- /dev/null +++ b/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("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("maven") { + from(components["java"]) + + addKsmtPom() + addSourcesAndJavadoc(project) + signKsmtPublication(project) + } + } +} diff --git a/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/KNoodlerSolver.kt b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/KNoodlerSolver.kt new file mode 100644 index 000000000..48781d6da --- /dev/null +++ b/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, + private val alphabet: List = ALL_CHAR_ALPHABET +) : KSolver { + private val assertions = arrayListOf>() + private val assertionSet = linkedSetOf>() + private val scopeMarks = ArrayDeque() + + private var lastStatus = KSolverStatus.UNKNOWN + private var lastReason: String? = null + + @Suppress("UNCHECKED_CAST") + override fun configure(configurator: KSolverConfiguration.() -> Unit) { + (baseSolver as KSolver).configure(configurator) + } + + override fun assert(expr: KExpr) { + ctx.ensureContextMatch(expr) + + if (!assertionSet.add(expr)) { + return + } + + assertions += expr + baseSolver.assert(expr) + } + + override fun assertAndTrack(expr: KExpr) = 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>, + 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> { + 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>): Boolean { + var hasFreshConstraints = false + + for (constraint in constraints) { + if (!assertionSet.add(constraint)) { + continue + } + + assertions += constraint + baseSolver.assert(constraint) + hasFreshConstraints = true + } + + return hasFreshConstraints + } +} diff --git a/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/Automaton.kt b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/Automaton.kt new file mode 100644 index 000000000..7409fdee2 --- /dev/null +++ b/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, A: Automaton>( + val start: N, + var alphabet: List, +) { + var terminal: List = listNodes(start, { it.terminal }) + + protected abstract fun newAutomaton(start: N, alphabet: List): Automaton + protected abstract fun scanExtraSymbols(visited: MutableSet) + + open fun check(word: String): Boolean { + var visited = mutableSetOf(start) + scanExtraSymbols(visited) + for (letter in word) { + val newVisited = mutableSetOf() + 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 { + 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>() + 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 { + val ordered = LinkedHashSet() + val queue = ArrayDeque() + + 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) + } + } +} diff --git a/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/BaseAutomata.kt b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/BaseAutomata.kt new file mode 100644 index 000000000..70f8f44a3 --- /dev/null +++ b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/BaseAutomata.kt @@ -0,0 +1,56 @@ +package io.ksmt.solver.noodler.automaton + +val ALL_CHAR_ALPHABET = CharRange(Char(1), Char(255)).toList() + +class BaseAutomata( + val alphabet: List = ALL_CHAR_ALPHABET, +) { + internal fun epsilon(): NFA { + val base = NFANode(true, mutableMapOf()) + base.put(EPS, base) + return NFA(base, alphabet) + } + + internal fun allChar(): NFA { + val start = NFANode(false, mutableMapOf()) + val finish = NFANode(true, mutableMapOf()) + for (letter in alphabet) { + start.put(letter, finish) + } + return NFA(start, alphabet) + } + + internal fun allWord(): NFA { + val base = NFANode(true, mutableMapOf()) + for (letter in alphabet) { + base.put(letter, base) + } + return NFA(base, alphabet) + } + + internal fun word(word: String): NFA { + val start = NFANode(false, mutableMapOf()) + var current = start + for (letter in word) { + val next = NFANode(false, mutableMapOf()) + current.put(letter, next) + current = next + } + current.terminal = true + return NFA(start, alphabet) + } + + internal fun range(from: Char, to: Char): NFA { + val start = NFANode(false, mutableMapOf()) + val finish = NFANode(true, mutableMapOf()) + for (letter in CharRange(from, to)) { + start.put(letter, finish) + } + return NFA(start, alphabet) + } + + internal fun empty(): NFA { + val start = NFANode(false, mutableMapOf()) + return NFA(start, alphabet) + } +} diff --git a/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/DFA.kt b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/DFA.kt new file mode 100644 index 000000000..891eefec9 --- /dev/null +++ b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/DFA.kt @@ -0,0 +1,153 @@ +package io.ksmt.solver.noodler.automaton + +class DFA(start: DFANode, alphabet: List) : + Automaton(start, alphabet) { + + override fun newAutomaton( + start: DFANode, + alphabet: List + ): DFA { + return DFA(start, alphabet) + } + + override fun scanExtraSymbols(visited: MutableSet) { + // Really does nothing + } + + fun complement(): DFA { + val nodes = listNodes(start, { true }) + val newNodes = HashMap(nodes.size) + for (old in nodes) { + newNodes[old] = DFANode(!old.terminal, mutableMapOf()) + } + + val sink = DFANode(true, mutableMapOf()) + for (letter in alphabet) { + sink.put(letter, sink) + } + + for (old in nodes) { + val current = newNodes[old]!! + for (letter in alphabet) { + val next = old.get(letter) + val mapped = if (next == null) sink else newNodes[next]!! + current.put(letter, mapped) + } + } + + return DFA(newNodes[start]!!, alphabet) + } + + fun asNFA(): NFA { + val nodes = listNodes(start, { true }) + val newNodes = HashMap(nodes.size) + for (old in nodes) { + newNodes[old] = NFANode(old.terminal, mutableMapOf()) + } + for (old in nodes) { + val current = newNodes[old]!! + for ((letter, next) in old.getAll()) { + current.put(letter, newNodes[next]!!) + } + } + return NFA(newNodes[start]!!, alphabet) + } + + fun minimize(): DFA { + val q = ArrayDeque, Char>>() + + val nonTerminalSet = listNodes(start, { !it.terminal }).toMutableSet() + val terminalSet = terminal.toMutableSet() + val currentClasses = mutableSetOf(terminalSet, nonTerminalSet) + + fun addSplitters(splitters: List>) { + for (c in alphabet) { + q.addAll( + splitters.map { + Pair(it, c) + } + ) + } + } + + addSplitters(listOf(terminalSet, nonTerminalSet)) + + while (q.isNotEmpty()) { + val (splitter, c) = q.removeFirst() + val toRemove = HashSet>() + val toAdd = HashSet>() + + for (cls in currentClasses) { + val withTransitionToSplitter = HashSet() + val withoutTransitionToSplitter = HashSet() + + for (state in cls) { + if (splitter.contains(state.get(c))) { + withTransitionToSplitter.add(state) + } else { + withoutTransitionToSplitter.add(state) + } + } + + if ( + withoutTransitionToSplitter.isNotEmpty() && + withTransitionToSplitter.isNotEmpty() + ) { + toRemove.add(cls) + toAdd.addAll( + listOf( + withTransitionToSplitter, + withoutTransitionToSplitter + ) + ) + + addSplitters( + listOf(withTransitionToSplitter, + withoutTransitionToSplitter) + ) + } + } + + currentClasses.removeAll(toRemove) + currentClasses.addAll(toAdd) + } + + if (currentClasses.all { it.size == 1 } ) { + // Already minimized + return this + } + + return constructDFAFromStateSets(currentClasses.toList()) + } + + private fun constructDFAFromStateSets(stateSets: List>): DFA { + val setsToNewNodes = HashMap, DFANode>() + val oldNodesToSets = HashMap>() + + val oldNodes = listNodes(start, { true }) + + for (stateSet in stateSets) { + for (state in stateSet) { + oldNodesToSets[state] = stateSet + } + + setsToNewNodes[stateSet] = DFANode( + stateSet.any { it.terminal }, + mutableMapOf() + ) + } + + for (state in oldNodes) { + val currentNewState = setsToNewNodes[oldNodesToSets[state]]!! + for ((c, next) in state.getAll()) { + val nextNewState = setsToNewNodes[oldNodesToSets[next]]!! + currentNewState.put(c, nextNewState) + } + } + + val startSet = stateSets.find { it.contains(start) } + val newStartNode = setsToNewNodes[startSet]!! + + return DFA(newStartNode, alphabet) + } +} diff --git a/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/NFA.kt b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/NFA.kt new file mode 100644 index 000000000..d5de39a16 --- /dev/null +++ b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/NFA.kt @@ -0,0 +1,196 @@ +package io.ksmt.solver.noodler.automaton + + +val EPS = Char(0) + + +class NFA(start: NFANode, alphabet: List) : + Automaton(start, alphabet) { + + fun concat(other: NFA): NFA { + val thisCopy = copy() as NFA + val otherCopy = other.copy() as NFA + for (state in thisCopy.terminal) { + state.put(EPS, otherCopy.start) + } + thisCopy.alphabet = thisCopy.alphabet.toSet().union(otherCopy.alphabet.toSet()).toList() + val allNodes = listNodes(thisCopy.start, { true }) + for (node in allNodes) { + node.terminal = false + } + for (node in otherCopy.terminal) { + node.terminal = true + } + thisCopy.terminal = otherCopy.terminal + return thisCopy + } + + fun product(other: NFA): NFA { + val newAlphabet = alphabet.toSet().union(other.alphabet).toList() + + val q = ArrayDeque>() + + val productStart = product(start, other.start) + val pairsToProduct = mutableMapOf, NFANode>() + pairsToProduct[Pair(start, other.start)] = productStart + + q.add(Triple(start, other.start, productStart)) + + while (q.isNotEmpty()) { + val (currentThis, currentOther, currentProduct) = q.removeFirst() + + fun processProductNode(one: NFANode, other: NFANode): NFANode { + val pair = Pair(one, other) + val existing = pairsToProduct[pair] + if (existing != null) { + return existing + } + val newProductNode = product(one, other) + pairsToProduct[pair] = newProductNode + q.add(Triple(one, other, newProductNode)) + return newProductNode + } + + fun addEdge(letter: Char, one: NFANode, other: NFANode) { + val next = processProductNode(one, other) + currentProduct.put(letter, next) + } + + for (ths in currentThis.getList(EPS)) { + addEdge(EPS, ths, currentOther) + } + for (oth in currentOther.getList(EPS)) { + addEdge(EPS, currentThis, oth) + } + + for (letter in currentProduct.getAllList().keys) { + if (letter == EPS) { + continue + } + for (ths in currentThis.getList(letter)) { + for (oth in currentOther.getList(letter)) { + addEdge(letter, ths, oth) + } + } + } + } + + return NFA(productStart, newAlphabet) + } + + fun union(other: NFA): NFA { + val newStart = NFANode(start.terminal || other.start.terminal, mutableMapOf()) + val newAlphabet = alphabet.toSet().union(other.alphabet.toSet()).toList() + newStart.put(EPS, start) + newStart.put(EPS, other.start) + return NFA(newStart, newAlphabet) + } + + fun kleeneClosure(): NFA { + val result = copy() + + for (node in result.terminal) { + node.put(EPS, result.start) + } + result.start.terminal = true + result.terminal = listNodes(result.start, { it.terminal }) + + return result as NFA + } + + fun power(a: Int): NFA { + require(a >= 0) { "power must be non-negative" } + if (a == 0) { + val start = NFANode(true, mutableMapOf()) + return NFA(start, alphabet) + } + + var result = copy() as NFA + repeat(a - 1) { + result = result.concat(copy() as NFA) + } + return result + } + + fun difference(other: NFA): NFA { + val unionAlphabet = alphabet.toSet().union(other.alphabet).toList() + + val left = (copy() as NFA).apply { alphabet = unionAlphabet } + val right = (other.copy() as NFA).apply { alphabet = unionAlphabet } + + val rightComplement = transformToDFA(right).complement().asNFA() + return left.product(rightComplement) + } + + fun loop(from: Int, to: Int): NFA { + require(from >= 0) { "from must be non-negative" } + require(to >= from) { "to must be >= from" } + + var currentPower = power(from) + var result = currentPower.copy() as NFA + for (i in (from + 1)..to) { + currentPower = currentPower.concat(copy() as NFA) + result = result.union(currentPower) + } + return result + } + + override fun newAutomaton( + start: NFANode, + alphabet: List + ): Automaton { + return NFA(start, alphabet) + } + + override fun scanExtraSymbols(visited: MutableSet) { + epsilonClosure(visited) + } +} + +fun transformToDFA(a: NFA): DFA { + val symbols = a.alphabet.filter { it != EPS } + val startSet = mutableSetOf(a.start) + epsilonClosure(startSet) + val newStart = DFANode(startSet.any { it.terminal }, mutableMapOf()) + + val q = ArrayDeque, DFANode>>() + val visited: MutableMap, DFANode> = mutableMapOf() + visited[startSet] = newStart + q.add(Pair(startSet, newStart)) + + while (q.isNotEmpty()) { + val (currentStateSet, currentDFANode) = q.removeFirst() + + for (c in symbols) { + val newStateSet = LinkedHashSet() + for (state in currentStateSet) { + newStateSet.addAll(state.getList(c)) + } + epsilonClosure(newStateSet) + + val nextDFANode = visited[newStateSet] ?: run { + val node = DFANode(newStateSet.any { it.terminal }, mutableMapOf()) + visited[newStateSet] = node + q.add(Pair(newStateSet, node)) + node + } + currentDFANode.put(c, nextDFANode) + } + } + + return DFA(newStart, symbols) +} + +fun epsilonClosure(visited: MutableSet) { + val queue = ArrayDeque() + queue.addAll(visited) + + while (queue.isNotEmpty()) { + val state = queue.removeFirst() + for (next in state.getList(EPS)) { + if (visited.add(next)) { + queue.add(next) + } + } + } +} diff --git a/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/Node.kt b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/Node.kt new file mode 100644 index 000000000..6eb2596b3 --- /dev/null +++ b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/Node.kt @@ -0,0 +1,118 @@ +package io.ksmt.solver.noodler.automaton + + +abstract class Node>( + var terminal: Boolean, +) { + override fun equals(other: Any?): Boolean = this === other + override fun hashCode(): Int = System.identityHashCode(this) + + abstract fun copy(): N + abstract fun put(letter: Char, v: N) + abstract fun getList(letter: Char): List + abstract fun getAllList(): Map> + abstract fun newEmpty(terminal: Boolean): N + abstract fun remove(letter: Char) +} + +class DFANode(terminal: Boolean, val next: MutableMap) : Node(terminal) { + override fun copy(): DFANode { + return DFANode(terminal, mutableMapOf()) + } + + override fun put(letter: Char, v: DFANode) { + next[letter] = v + } + + override fun getList(letter: Char): List { + val v = next[letter] ?: return emptyList() + return listOf(v) + } + + override fun getAllList(): Map> { + return next.mapValues { listOf(it.value) } + } + + override fun newEmpty(terminal: Boolean): DFANode { + return DFANode(terminal, mutableMapOf()) + } + + override fun remove(letter: Char) { + next.remove(letter) + } + + fun get(letter: Char): DFANode? { + return next[letter] + } + + fun getAll(): Map { + return next + } +} + +class NFANode(terminal: Boolean, val next: MutableMap>) : Node(terminal) { + override fun copy(): NFANode { + return NFANode(terminal, mutableMapOf()) + } + + override fun put(letter: Char, v: NFANode) { + next.getOrPut(letter) { mutableListOf() }.add(v) + } + + override fun getList(letter: Char): List { + return next[letter] ?: emptyList() + } + + override fun getAllList(): Map> { + return next + } + + override fun newEmpty(terminal: Boolean): NFANode { + return NFANode(terminal, mutableMapOf()) + } + + override fun remove(letter: Char) { + next.remove(letter) + } +} + +fun > copy(v: N, copies: MutableMap = mutableMapOf()): N { + val copied = v.copy() + copies[v] = copied + for ((letter, children) in v.getAllList()) { + for (u in children) { + var cu = copies[u] + if (u == v) { + cu = copied + } else if (cu == null) { + cu = copy(u, copies) + copies[u] = cu + } + copied.put(letter, cu) + } + } + return copied +} + +fun > listNodes(v: N, predicate: (N) -> Boolean, visited: MutableSet = mutableSetOf()): List { + val result = HashSet() + visited.add(v) + if (predicate(v)) { + result.add(v) + } + for (u in v.getAllList().values.flatten()) { + if (!visited.contains(u)) { + result.addAll(listNodes(u, predicate, visited)) + } + } + return result.toList() +} + +fun > product(one: N, other: N): N { + val new = one.newEmpty(one.terminal && other.terminal) + val keep = one.getAllList().keys.intersect(other.getAllList().keys) + for (letter in keep) { + new.put(letter, one.newEmpty(false)) + } + return new +} diff --git a/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/Regex.kt b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/Regex.kt new file mode 100644 index 000000000..324c9b909 --- /dev/null +++ b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/automaton/Regex.kt @@ -0,0 +1,162 @@ +package io.ksmt.solver.noodler.automaton + +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.expr.KRegexAll +import io.ksmt.expr.KRegexAllChar +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexEpsilon +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexLoopExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KStringLiteralExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.sort.KRegexSort + +fun fromRegex(expr: KExpr, alphabet: List = ALL_CHAR_ALPHABET): NFA { + val base = BaseAutomata(alphabet) + return when (expr) { + is KRegexEpsilon -> base.empty() + is KRegexAll -> base.allWord() + is KRegexAllChar -> base.allChar() + is KRegexConcatExpr -> fromRegex(expr.arg0, alphabet).concat(fromRegex(expr.arg1, alphabet)) + is KRegexUnionExpr -> fromRegex(expr.arg0, alphabet).union(fromRegex(expr.arg1, alphabet)) + is KRegexIntersectionExpr -> fromRegex(expr.arg0, alphabet).product(fromRegex(expr.arg1, alphabet)) + is KRegexStarExpr -> fromRegex(expr.arg, alphabet).kleeneClosure() + is KRegexCrossExpr -> { + val a = fromRegex(expr.arg, alphabet) + a.concat(a.kleeneClosure()) + } + is KRegexDifferenceExpr -> fromRegex(expr.arg0, alphabet).difference(fromRegex(expr.arg1, alphabet)) + is KRegexComplementExpr -> transformToDFA(fromRegex(expr.arg, alphabet)).complement().asNFA() + is KRegexOptionExpr -> fromRegex(expr.arg, alphabet).union(base.epsilon()) + is KRegexRangeExpr -> rangeFromLiterals(expr, base) + is KRegexPowerExpr -> fromRegex(expr.arg, alphabet).power(expr.power) + is KRegexLoopExpr -> fromRegex(expr.arg, alphabet).loop(expr.from, expr.to) + is KStringToRegexExpr -> fromString(expr, base) + else -> unsupported(expr, "unknown expression type") + } +} + +private fun fromString(expr: KStringToRegexExpr, base: BaseAutomata): NFA { + return when (val arg = expr.arg) { + is KStringLiteralExpr -> base.word(arg.value) + else -> unsupported(expr, "not a string literal in regex") + } +} + +private fun rangeFromLiterals(expr: KRegexRangeExpr, base: BaseAutomata): NFA { + val from = expr.arg0 as? KStringLiteralExpr + val to = expr.arg1 as? KStringLiteralExpr + if (from == null || to == null || + from.value.length != 1 || to.value.length != 1) { + unsupported(expr, "range values are invalid") + } + return base.range(from.value[0], to.value[0]) +} + +private fun unsupported(expr: KExpr<*>, reason: String): Nothing = + error("fromRegex: unsupported expression: ${expr::class.simpleName} because of: $reason") + +fun NFA.toRegex(ctx: KContext): KExpr { + val nodes = listNodes(start, { true }) + val n = nodes.size + val startId = n + val finalId = n + 1 + + val emptyLang = ctx.mkRegexEpsilon() + val epsilon = ctx.mkStringToRegex(ctx.mkStringLiteral("")) + + val idOf = nodes.withIndex().associate { it.value to it.index } + val R = HashMap>>() + + fun getR(i: Int, j: Int): KExpr = + R[i]?.get(j) ?: emptyLang + + fun setR(i: Int, j: Int, expr: KExpr) { + if (expr == emptyLang) return + R.getOrPut(i) { HashMap() }[j] = expr + } + + fun regexUnion(a: KExpr, b: KExpr): KExpr = + when { + a == emptyLang -> b + b == emptyLang -> a + else -> ctx.mkRegexUnion(a, b) + } + + fun regexConcat(a: KExpr, b: KExpr): KExpr = + when { + a == emptyLang || b == emptyLang -> emptyLang + a == epsilon -> b + b == epsilon -> a + else -> ctx.mkRegexConcat(a, b) + } + + fun regexStar(a: KExpr): KExpr = + when (a) { + emptyLang, epsilon -> epsilon + else -> ctx.mkRegexStar(a) + } + + for (u in nodes) { + val i = idOf.getValue(u) + for ((letter, nexts) in u.getAllList()) { + val label = if (letter == EPS) { + epsilon + } else { + ctx.mkStringToRegex(ctx.mkStringLiteral(letter.toString())) + } + for (v in nexts) { + val j = idOf.getValue(v) + val prev = getR(i, j) + setR(i, j, regexUnion(prev, label)) + } + } + } + + // New start -> old start + setR(startId, idOf.getValue(start), epsilon) + // Old terminals -> new final + for (t in terminal) { + setR(idOf.getValue(t), finalId, epsilon) + } + + val allIds = (0 until n).toMutableList() + allIds.add(startId) + allIds.add(finalId) + + for (k in allIds.toList()) { + if (k == startId || k == finalId) continue + val rkk = getR(k, k) + val rkkStar = regexStar(rkk) + + for (i in allIds) { + if (i == k) continue + val rik = getR(i, k) + if (rik == emptyLang) continue + for (j in allIds) { + if (j == k) continue + val rkj = getR(k, j) + if (rkj == emptyLang) continue + val rij = getR(i, j) + val through = regexConcat(rik, regexConcat(rkkStar, rkj)) + setR(i, j, regexUnion(rij, through)) + } + } + + R.remove(k) + for (m in R.values) { + m.remove(k) + } + } + + return getR(startId, finalId) +} diff --git a/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/Noodler.kt b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/Noodler.kt new file mode 100644 index 000000000..c2809d3f8 --- /dev/null +++ b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/Noodler.kt @@ -0,0 +1,299 @@ +@file:Suppress("UNCHECKED_CAST") + +package io.ksmt.solver.noodler.core + +import io.ksmt.expr.KConst +import io.ksmt.expr.KEqExpr +import io.ksmt.expr.KExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.solver.noodler.automaton.ALL_CHAR_ALPHABET +import io.ksmt.solver.noodler.automaton.BaseAutomata +import io.ksmt.solver.noodler.automaton.EPS +import io.ksmt.solver.noodler.automaton.NFA +import io.ksmt.solver.noodler.automaton.NFANode +import io.ksmt.solver.noodler.automaton.fromRegex +import io.ksmt.solver.noodler.automaton.toRegex +import io.ksmt.solver.noodler.automaton.transformToDFA +import io.ksmt.sort.KStringSort + +class Noodler( + statements: List>, + val alphabet: List +) { + val equations: List> + val regularConstraints: List + val regularConstraintsByVariable: Map + + init { + val collectedEquations = mutableListOf>() + val collectedRegularConstraints = mutableListOf() + val collectedRegularConstraintsByVariable = linkedMapOf() + + statements.forEachIndexed { index, statement -> + when { + statement is KStringInRegexExpr -> { + collectedRegularConstraints.add(statement) + + val variableName = statement.extractVariableName(index) + val automaton = fromRegex(statement.arg1, alphabet) + val a2 = transformToDFA(automaton).minimize() + println(a2.alphabet) + + collectedRegularConstraintsByVariable.compute(variableName) { _, oldAutomaton -> + oldAutomaton?.product(automaton) ?: automaton + } + } + + statement is KEqExpr<*> && + statement.lhs.sort is KStringSort && + statement.rhs.sort is KStringSort -> { + val lhs = statement.lhs as KExpr + val rhs = statement.rhs as KExpr + require(lhs.isConcatOfStringVariables()) { + "Equation at index $index has unsupported left side. " + + "Only concatenations of string variables are allowed." + } + require(rhs.isConcatOfStringVariables()) { + "Equation at index $index has unsupported right side. " + + "Only concatenations of string variables are allowed." + } + + collectedEquations.add(statement) + } + + else -> throw IllegalArgumentException( + "Unsupported statement at index $index: " + + "${statement::class.simpleName}. " + + "Only string equations and regular constraints are allowed." + ) + } + } + + equations = collectedEquations + regularConstraints = collectedRegularConstraints + regularConstraintsByVariable = collectedRegularConstraintsByVariable + } + + fun solve(): Pair> { + val baseAutomata = BaseAutomata(alphabet) + val refinedByVariable = linkedMapOf() + val variablesByName = linkedMapOf>() + + fun rememberVariable(variable: KConst<*>) { + if (variable.sort is KStringSort) { + variablesByName.putIfAbsent(variable.decl.name, variable as KExpr) + } + } + + equations.forEach { equation -> + flattenConcatVariables(equation.lhs as KExpr).forEach(::rememberVariable) + flattenConcatVariables(equation.rhs as KExpr).forEach(::rememberVariable) + } + regularConstraints.forEach { constraint -> + val variable = constraint.arg0 as? KConst<*> ?: return@forEach + rememberVariable(variable) + } + + fun areEquivalent(lhs: NFA, rhs: NFA): Boolean { + return lhs.difference(rhs).isEmpty() && rhs.difference(lhs).isEmpty() + } + + if (regularConstraintsByVariable.values.any { it.isEmpty() }) { + return false to emptyList() + } + + for (equation in equations) { + val (ok, refined) = processEquation(equation) + if (!ok) { + return false to emptyList() + } + + for ((variableName, automaton) in refined) { + if (automaton.isEmpty()) { + return false to emptyList() + } + refinedByVariable.compute(variableName) { _, old -> + old?.product(automaton) ?: automaton + } + } + } + + val additionalConstraints = mutableListOf() + for ((variableName, automaton) in refinedByVariable) { + val baseConstraint = regularConstraintsByVariable[variableName] ?: baseAutomata.allWord() + val strengthened = baseConstraint.product(automaton) + if (strengthened.isEmpty()) { + return false to emptyList() + } + if (areEquivalent(baseConstraint, strengthened)) { + continue + } + + val variable = variablesByName[variableName] ?: continue + val regex = strengthened.toRegex(variable.ctx) + additionalConstraints.add(variable.ctx.mkStringInRegexNoSimplify(variable, regex)) + } + + return true to additionalConstraints + } + + private fun processEquation(equation: KEqExpr<*>): Pair> { + fun transformConcatenationToNFASequence(expr: KExpr<*>): List { + return flattenConcatVariables( + expr as KExpr + ).map { + regularConstraintsByVariable[it.decl.name] ?: BaseAutomata().allWord() + } + } + + val rhsVariables = flattenConcatVariables(equation.rhs as KExpr) + val leftNFASequence = transformConcatenationToNFASequence(equation.lhs) + val rightNFASequence = transformConcatenationToNFASequence(equation.rhs) + + val leftAutomaton = transformToDFA(leftNFASequence.drop(1).fold(leftNFASequence.first()) { acc, nfa -> + acc.concat(nfa) + }).minimize().asNFA() + + val rightAutomaton = rightNFASequence.drop(1).fold(rightNFASequence.first()) { acc, nfa -> + acc.concat(nfa) + } + + leftAutomaton.picture("left.png") + rightAutomaton.picture("right.png") + + val grid = leftAutomaton.product(rightAutomaton) + + if (grid.isEmpty()) { + return false to emptyMap() + } + + val noodles = makeNoodles(grid) + val result = mutableMapOf() + for (noodle in noodles) { + val resultInNoodle = mutableMapOf() + + val segments = noodle.map { + makeSegmentNFA(it) + } + val segmentCount = minOf(rhsVariables.size, segments.size) + for (i in 0 until segmentCount) { + val variableName = rhsVariables[i].decl.name + val automaton = segments[i] + + resultInNoodle.compute(variableName) { _, old -> + old?.product(automaton) ?: automaton + } + } + + for ((variableName, automaton) in resultInNoodle) { + result.compute(variableName) { _, old -> + old?.union(automaton) ?: automaton + } + } + } + + return true to result + } + + private fun makeNoodles(grid: NFA): List>> { + val allNoodles = mutableListOf>>() + + fun dfs( + v: NFANode, + currentSegment: MutableList, + currentSegmentSet: MutableSet, + currentNoodle: MutableList>, + stagePathNodes: MutableSet + ) { + currentSegment.add(v) + currentSegmentSet.add(v) + + for ((letter, nextNodes) in v.getAllList()) { + if (letter == EPS) { + continue + } + + for (next in nextNodes) { + if (next !in currentSegmentSet) { + dfs(next, currentSegment, currentSegmentSet, currentNoodle, stagePathNodes) + } + } + } + + val nextStageNodes = v.getList(EPS) + currentNoodle.add(currentSegment.toList()) + + if (nextStageNodes.isEmpty()) { + if (currentSegment.any { it.terminal }) { + allNoodles.add(currentNoodle.map { it.toList() }) + } + } else { + for (nextStageNode in nextStageNodes) { + if (!stagePathNodes.add(nextStageNode)) { + continue + } + dfs( + v = nextStageNode, + currentSegment = mutableListOf(), + currentSegmentSet = mutableSetOf(), + currentNoodle = currentNoodle, + stagePathNodes = stagePathNodes + ) + stagePathNodes.remove(nextStageNode) + } + } + + currentNoodle.removeLast() + currentSegment.removeLast() + currentSegmentSet.remove(v) + } + + dfs( + v = grid.start, + currentSegment = mutableListOf(), + currentSegmentSet = mutableSetOf(), + currentNoodle = mutableListOf(), + stagePathNodes = mutableSetOf(grid.start) + ) + return allNoodles + } + + private fun makeSegmentNFA(nodes: List): NFA { + val nodeSet = nodes.toSet() + + for (node in nodes) { + val edges = node.getAllList().map { (letter, nextNodes) -> + letter to nextNodes.toList() + } + for ((letter, nextNodes) in edges) { + val newNextNodes = nextNodes.filter { nodeSet.contains(it) } + node.remove(letter) + newNextNodes.forEach { node.put(letter, it) } + } + } + + nodes.last().terminal = true + return NFA(nodes.first(), ALL_CHAR_ALPHABET) + } +} + +private fun KStringInRegexExpr.extractVariableName(index: Int): String { + val variable = arg0 as? KConst<*> + require(variable != null && variable.sort is KStringSort) { + "Regular constraint at index $index must use a string variable on the left-hand side" + } + return variable.decl.name +} + +private fun flattenConcatVariables(expr: KExpr<*>): List> { + return when (expr) { + is KStringConcatExpr -> flattenConcatVariables(expr.arg0) + flattenConcatVariables(expr.arg1) + is KConst<*> -> { + require(expr.sort is KStringSort) { "Expected string variable in equation side" } + listOf(expr) + } + + else -> error("Expected concatenation of string variables") + } +} diff --git a/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/NoodlerStatements.kt b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/NoodlerStatements.kt new file mode 100644 index 000000000..c76213fe9 --- /dev/null +++ b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/NoodlerStatements.kt @@ -0,0 +1,38 @@ +package io.ksmt.solver.noodler.core + +import io.ksmt.expr.KConst +import io.ksmt.expr.KEqExpr +import io.ksmt.expr.KExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.sort.KBoolSort +import io.ksmt.sort.KStringSort + +internal fun KExpr.toNoodlerStatementOrNull(): KExpr<*>? = when (this) { + is KStringInRegexExpr -> { + val variable = arg0 as? KConst<*> + if (variable != null && variable.sort is KStringSort) { + this + } else { + null + } + } + + is KEqExpr<*> -> { + if (lhs.sort is KStringSort && rhs.sort is KStringSort && + lhs.isConcatOfStringVariables() && rhs.isConcatOfStringVariables() + ) { + this + } else { + null + } + } + + else -> null +} + +internal fun KExpr<*>.isConcatOfStringVariables(): Boolean = when (this) { + is KStringConcatExpr -> arg0.isConcatOfStringVariables() && arg1.isConcatOfStringVariables() + is KConst<*> -> sort is KStringSort + else -> false +} diff --git a/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/NoodlerZ3Example.kt b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/NoodlerZ3Example.kt new file mode 100644 index 000000000..49e034be6 --- /dev/null +++ b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/NoodlerZ3Example.kt @@ -0,0 +1,47 @@ +package io.ksmt.solver.noodler.core + +import io.ksmt.KContext + +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration + +fun main() = with(KContext()) { + val z = mkConst("z", stringSort) + val y = mkConst("y", stringSort) + + // zy = z + // y in a+b+ + // z in b+ + val equation = mkEq(mkStringConcat(z, y), z) + + val aPlus = mkRegexCross(mkStringToRegex(mkStringLiteral("a"))) + val bPlus = mkRegexCross(mkStringToRegex(mkStringLiteral("b"))) + val yConstraint = mkStringInRegex(y, mkRegexConcat(aPlus, bPlus)) + val zConstraint = mkStringInRegex(z, bPlus) + + val assertions = listOf(equation, yConstraint, zConstraint) + + val n = Noodler(assertions, listOf('a', 'b')) + + val (sat, extra) = n.solve() + println(sat) + for (a in extra) { + println(a) + } + + val interactor = SolverInteractor(assertions, + listOf('a', 'b'), createZ3SolverOrNull(this)!!) + + println("Interactor result: ${interactor.solve()}") +} + +private fun createZ3SolverOrNull(ctx: KContext): KSolver? { + return try { + val solverClass = Class.forName("io.ksmt.solver.z3.KZ3Solver") + val ctor = solverClass.getConstructor(KContext::class.java) + @Suppress("UNCHECKED_CAST") + ctor.newInstance(ctx) as KSolver + } catch (_: Throwable) { + null + } +} diff --git a/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/SolverInteractor.kt b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/SolverInteractor.kt new file mode 100644 index 000000000..dc6eeecc9 --- /dev/null +++ b/ksmt-noodler/src/main/kotlin/io/ksmt/solver/noodler/core/SolverInteractor.kt @@ -0,0 +1,53 @@ +package io.ksmt.solver.noodler.core + +import io.ksmt.expr.KExpr +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus +import io.ksmt.sort.KBoolSort +import kotlin.time.Duration +import kotlin.time.Duration.Companion.minutes + +class SolverInteractor( + statements: List>, + val alphabet: List, + val solver: KSolver +) { + private val noodler = Noodler(statements, alphabet) + + fun solve(maxRounds: Int = 1, solverTimeout: Duration = 1.minutes): KSolverStatus { + for (roundCount in 1..maxRounds) { + // Из-за того, что при запуске решателя с таймаутом я не смог + // вытащить дополнительные ограничения, которые он генерирует, + // пока что цикл по раундам бесполезный + System.err.println("Executing round $roundCount") + + val result = oneRound(solverTimeout) + if (result != KSolverStatus.UNKNOWN) { + System.err.println("Found result: $result") + return result + } + } + System.err.println("Cannot find definite result") + return KSolverStatus.UNKNOWN + } + + private fun oneRound(solverTimeout: Duration): KSolverStatus { + val (result, extraConstraints) = launchNoodler() + + if (!result) { + return KSolverStatus.UNSAT + } + solver.assert(extraConstraints) + + return launchExternalSolver(solverTimeout) + } + + private fun launchExternalSolver(solverTimeout: Duration): KSolverStatus { + return solver.check(timeout = solverTimeout) + } + + private fun launchNoodler(): Pair>> { + return noodler.solve() + } +} diff --git a/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/AutomatonPictureTest.kt b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/AutomatonPictureTest.kt new file mode 100644 index 000000000..5b9a1b4df --- /dev/null +++ b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/AutomatonPictureTest.kt @@ -0,0 +1,83 @@ +package io.ksmt.solver.noodler.automaton + +import org.junit.jupiter.api.Assumptions +import java.nio.file.Files +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertTrue + +class AutomatonPictureTest { + + @Test + fun testToDotProducesDeterministicGraphvizDescription() { + val terminal = NFANode(true, mutableMapOf()) + val start = NFANode(false, mutableMapOf()) + start.put('a', terminal) + start.put(EPS, terminal) + + val nfa = NFA(start, alphabet = listOf('a')) + + val expected = """ + digraph Automaton { + rankdir=LR; + start [shape=point]; + start -> q0; + q0 [shape=circle, label="q0"]; + q1 [shape=doublecircle, label="q1"]; + q0 -> q1 [label="eps, a"]; + } + """.trimIndent() + + assertEquals(expected, nfa.toDot().trim()) + } + + @Test + fun testPictureCreatesSvgFile() { + Assumptions.assumeTrue(isGraphvizAvailable(), "Graphviz 'dot' is not installed") + + val terminal = NFANode(true, mutableMapOf()) + val start = NFANode(false, mutableMapOf()) + start.put('a', terminal) + start.put(EPS, terminal) + + val nfa = NFA(start, alphabet = listOf('a')) + val tempDir = Files.createTempDirectory("automaton-picture") + + try { + val output = tempDir.resolve("nfa.svg") + nfa.picture(output.toString()) + + assertTrue(Files.exists(output)) + assertTrue(Files.size(output) > 0) + + val svg = String(Files.readAllBytes(output), Charsets.UTF_8) + assertTrue(svg.contains("q0")) + assertTrue(svg.contains("q1")) + assertTrue(svg.contains("eps, a")) + } finally { + tempDir.toFile().deleteRecursively() + } + } + + @Test + fun testPictureRequiresFilenameExtension() { + val nfa = NFA(NFANode(true, mutableMapOf()), alphabet = emptyList()) + + val error = assertFailsWith { + nfa.picture("automaton") + } + + assertTrue(error.message.orEmpty().contains("extension")) + } + + private fun isGraphvizAvailable(): Boolean = runCatching { + val process = ProcessBuilder("dot", "-V") + .redirectErrorStream(true) + .start() + + process.outputStream.close() + process.inputStream.use { it.readBytes() } + process.waitFor() == 0 + }.getOrDefault(false) +} diff --git a/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/BaseAutomataTest.kt b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/BaseAutomataTest.kt new file mode 100644 index 000000000..19fa03ad9 --- /dev/null +++ b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/BaseAutomataTest.kt @@ -0,0 +1,66 @@ +package io.ksmt.solver.noodler.automaton + +import kotlin.test.Test +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class BaseAutomataTest { + + @Test + fun testEpsilonAcceptsOnlyEmptyWord() { + val base = BaseAutomata(alphabet = listOf('a')) + val epsilon = base.epsilon() + + assertTrue(epsilon.check("")) + assertFalse(epsilon.check("a")) + assertFalse(epsilon.check("aa")) + } + + @Test + fun testAllCharAcceptsSingleAlphabetChar() { + val base = BaseAutomata(alphabet = listOf('a', 'b')) + val allChar = base.allChar() + + assertTrue(allChar.check("a")) + assertTrue(allChar.check("b")) + assertFalse(allChar.check("")) + assertFalse(allChar.check("ab")) + assertFalse(allChar.check("c")) + } + + @Test + fun testAllWordAcceptsAnyWordOverAlphabet() { + val base = BaseAutomata(alphabet = listOf('a', 'b')) + val allWord = base.allWord() + + assertTrue(allWord.check("")) + assertTrue(allWord.check("a")) + assertTrue(allWord.check("ba")) + assertTrue(allWord.check("abba")) + assertFalse(allWord.check("c")) + } + + @Test + fun testWordAcceptsOnlyExactWord() { + val base = BaseAutomata(alphabet = listOf('a', 'b')) + val word = base.word("ab") + + assertTrue(word.check("ab")) + assertFalse(word.check("")) + assertFalse(word.check("a")) + assertFalse(word.check("aba")) + assertFalse(word.check("bb")) + } + + @Test + fun testRangeAcceptsOnlyCharsInRange() { + val base = BaseAutomata(alphabet = listOf('a', 'b', 'c', 'd')) + val range = base.range('b', 'c') + + assertTrue(range.check("b")) + assertTrue(range.check("c")) + assertFalse(range.check("a")) + assertFalse(range.check("d")) + assertFalse(range.check("bc")) + } +} diff --git a/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/DFAMinimizeTest.kt b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/DFAMinimizeTest.kt new file mode 100644 index 000000000..b5f6fe446 --- /dev/null +++ b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/DFAMinimizeTest.kt @@ -0,0 +1,58 @@ +package io.ksmt.solver.noodler.automaton + +import kotlin.test.Test +import kotlin.test.assertEquals + +class DFAMinimizeTest { + + @Test + fun testMinimizeMergesEquivalentTerminalStates() { + val start = node(terminal = false) + val terminalA = node(terminal = true) + val terminalB = node(terminal = true) + + start.put('a', terminalA) + start.put('b', terminalB) + terminalA.put('a', terminalA) + terminalA.put('b', terminalA) + terminalB.put('a', terminalB) + terminalB.put('b', terminalB) + + val dfa = DFA(start, alphabet = listOf('a', 'b')) + val minimized = dfa.minimize() + + assertEquals(3, listNodes(dfa.start, { true }).size) + assertEquals(2, listNodes(minimized.start, { true }).size) + + val samples = listOf("", "a", "b", "ab", "ba", "bbb") + for (word in samples) { + assertEquals(dfa.check(word), minimized.check(word), "Mismatch on '$word'") + } + } + + @Test + fun testMinimizeKeepsDistinctNonEquivalentStates() { + val start = node(terminal = false) + val terminalA = node(terminal = true) + val terminalB = node(terminal = true) + val sink = node(terminal = false) + + start.put('a', terminalA) + start.put('b', terminalB) + terminalA.put('a', terminalA) + terminalA.put('b', sink) + terminalB.put('a', sink) + terminalB.put('b', terminalB) + sink.put('a', sink) + sink.put('b', sink) + + val dfa = DFA(start, alphabet = listOf('a', 'b')) + val minimized = dfa.minimize() + + assertEquals(4, listNodes(minimized.start, { true }).size) + } + + private fun node(terminal: Boolean): DFANode { + return DFANode(terminal, mutableMapOf()) + } +} diff --git a/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/DFATest.kt b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/DFATest.kt new file mode 100644 index 000000000..799f50a64 --- /dev/null +++ b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/DFATest.kt @@ -0,0 +1,61 @@ +package io.ksmt.solver.noodler.automaton + +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFalse + +class DFATest { + + @Test + fun testComplementHandlesMissingTransitions() { + val start = node(terminal = false) + val accept = node(terminal = true) + start.put('a', accept) + accept.put('a', accept) + + val dfa = DFA(start, alphabet = listOf('a', 'b')) + val complement = dfa.complement() + + val samples = listOf("", "a", "aa", "b", "ab", "ba") + for (word in samples) { + assertEquals(!dfa.check(word), complement.check(word), "Mismatch on '$word'") + } + } + + @Test + fun testAsNfaPreservesLanguage() { + val start = node(terminal = false) + val accept = node(terminal = true) + + start.put('a', accept) + start.put('b', start) + accept.put('a', accept) + accept.put('b', start) + + val dfa = DFA(start, alphabet = listOf('a', 'b')) + val nfa = dfa.asNFA() + + val samples = listOf("", "a", "b", "ba", "ab", "bb", "aba", "abba") + for (word in samples) { + assertEquals(dfa.check(word), nfa.check(word), "Mismatch on '$word'") + } + } + + @Test + fun testComplementOfUniversalLanguage() { + val start = node(terminal = true) + start.put('a', start) + + val dfa = DFA(start, alphabet = listOf('a')) + val complement = dfa.complement() + + val samples = listOf("", "a", "aa", "aaa") + for (word in samples) { + assertFalse(complement.check(word), "Expected complement to reject '$word'") + } + } + + private fun node(terminal: Boolean): DFANode { + return DFANode(terminal, mutableMapOf()) + } +} diff --git a/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/NFAExtendedTest.kt b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/NFAExtendedTest.kt new file mode 100644 index 000000000..e0e809435 --- /dev/null +++ b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/NFAExtendedTest.kt @@ -0,0 +1,123 @@ +package io.ksmt.solver.noodler.automaton + +import kotlin.test.Test +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class NFAExtendedTest { + + @Test + fun testUnionAcceptsEitherLanguage() { + val nfaA = literal('a', listOf('a')) + val nfaB = literal('b', listOf('b')) + + val union = nfaA.union(nfaB) + + assertTrue(union.check("a")) + assertTrue(union.check("b")) + assertFalse(union.check("")) + assertFalse(union.check("ab")) + assertTrue(union.alphabet.contains('a')) + assertTrue(union.alphabet.contains('b')) + } + + @Test + fun testKleeneClosureAcceptsRepetitionAndEmpty() { + val nfa = literal('a', listOf('a', 'b')) + val closure = nfa.kleeneClosure() + + assertTrue(closure.check("")) + assertTrue(closure.check("a")) + assertTrue(closure.check("aa")) + assertFalse(closure.check("b")) + } + + @Test + fun testPowerBuildsExactRepetition() { + val nfa = literal('a', listOf('a')) + + val pow0 = nfa.power(0) + assertTrue(pow0.check("")) + assertFalse(pow0.check("a")) + + val pow1 = nfa.power(1) + assertTrue(pow1.check("a")) + assertFalse(pow1.check("")) + + val pow2 = nfa.power(2) + assertTrue(pow2.check("aa")) + assertFalse(pow2.check("a")) + assertFalse(pow2.check("aaa")) + } + + @Test + fun testLoopAcceptsRangeInclusive() { + val nfa = literal('a', listOf('a')) + val loop = nfa.loop(1, 3) + + assertTrue(loop.check("a")) + assertTrue(loop.check("aa")) + assertTrue(loop.check("aaa")) + assertFalse(loop.check("")) + assertFalse(loop.check("aaaa")) + } + + @Test + fun testLoopFromZeroIncludesEmpty() { + val nfa = literal('a', listOf('a')) + val loop = nfa.loop(0, 0) + + assertTrue(loop.check("")) + assertFalse(loop.check("a")) + } + + @Test + fun testDifferenceRemovesLanguage() { + val base = literal('a', listOf('a')) + val star = base.kleeneClosure() + + val diff = star.difference(base) + + assertTrue(diff.check("")) + assertFalse(diff.check("a")) + assertTrue(diff.check("aa")) + assertTrue(diff.check("aaa")) + } + + @Test + fun testDifferenceUsesAlphabetUnion() { + val a = literal('a', listOf('a')) + val b = literal('b', listOf('b')) + + val diff = a.difference(b) + + assertTrue(diff.check("a")) + assertFalse(diff.check("")) + assertFalse(diff.check("b")) + } + + @Test + fun testPowerRejectsNegative() { + val nfa = literal('a', listOf('a')) + assertFailsWith { nfa.power(-1) } + } + + @Test + fun testLoopValidatesBounds() { + val nfa = literal('a', listOf('a')) + assertFailsWith { nfa.loop(-1, 2) } + assertFailsWith { nfa.loop(2, 1) } + } + + private fun literal(ch: Char, alphabet: List): NFA { + val start = node(terminal = false) + val terminal = node(terminal = true) + start.put(ch, terminal) + return NFA(start, alphabet) + } + + private fun node(terminal: Boolean): NFANode { + return NFANode(terminal, mutableMapOf()) + } +} diff --git a/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/NFATest.kt b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/NFATest.kt new file mode 100644 index 000000000..d502301c7 --- /dev/null +++ b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/NFATest.kt @@ -0,0 +1,238 @@ +package io.ksmt.solver.noodler.automaton + +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class NFATest { + + @Test + fun testAcceptsEmptyWordWhenStartIsTerminal() { + val start = node(terminal = true) + val nfa = NFA(start = start, alphabet = listOf('a')) + + assertTrue(nfa.check("")) + assertFalse(nfa.check("a")) + } + + @Test + fun testAcceptsSingleLetter() { + val terminalNode = node(terminal = true) + val start = node(terminal = false) + start.put('a', terminalNode) + + val nfa = NFA(start = start, alphabet = listOf('a', 'b')) + + assertTrue(nfa.check("a")) + assertFalse(nfa.check("")) + assertFalse(nfa.check("b")) + } + + @Test + fun testAcceptsViaEpsilonTransition() { + val terminalNode = node(terminal = true) + val mid = node(terminal = false) + val start = node(terminal = false) + mid.put('b', terminalNode) + start.put(EPS, mid) + + val nfa = NFA(start = start, alphabet = listOf('a', 'b')) + + assertTrue(nfa.check("b")) + assertFalse(nfa.check("")) + assertFalse(nfa.check("a")) + } + + @Test + fun testRejectsUnreachableTerminal() { + val start = node(terminal = false) + node(terminal = true) + val nfa = NFA(start = start, alphabet = listOf('a')) + + assertFalse(nfa.check("")) + assertFalse(nfa.check("a")) + } + + @Test + fun testMultipleTransitionsSameChar() { + val terminalNode = node(terminal = true) + val deadEnd = node(terminal = false) + val start = node(terminal = false) + start.put('a', deadEnd) + start.put('a', terminalNode) + + val nfa = NFA(start = start, alphabet = listOf('a', 'b')) + + assertTrue(nfa.check("a")) + assertFalse(nfa.check("")) + assertFalse(nfa.check("b")) + } + + @Test + fun testListNodesFindsAllTerminalStates() { + val t1 = node(terminal = true) + val t2 = node(terminal = true) + val mid = node(terminal = false) + val start = node(terminal = false) + + mid.put('a', t1) + mid.put('b', t2) + start.put('x', mid) + start.put('y', t2) + + val terminals = listNodes(start, { it.terminal }) + assertEquals(2, terminals.size) + assertTrue(terminals.any { it === t1 }) + assertTrue(terminals.any { it === t2 }) + } + + @Test + fun testNodeCopyPreservesStructure() { + val terminalNode = node(terminal = true) + val start = node(terminal = false) + start.put('a', terminalNode) + + val copied = copy(start) + assertTrue(copied !== start) + val copiedChildren = copied.getList('a') + assertTrue(copiedChildren.isNotEmpty(), "Copied start has no 'a' transition") + val firstChild = copiedChildren[0] + assertTrue(firstChild !== terminalNode) + assertTrue(firstChild.terminal) + } + + @Test + fun testNfaCopyPreservesLanguageOnSamples() { + val terminalNode = node(terminal = true) + val start = node(terminal = false) + start.put('a', terminalNode) + + val nfa = NFA(start = start, alphabet = listOf('a')) + val copied = nfa.copy() + + assertTrue(nfa.check("a")) + assertTrue(copied.check("a")) + assertFalse(nfa.check("")) + assertFalse(copied.check("")) + } + + @Test + fun testConcatAcceptsConcatenation() { + val aTerminal = node(terminal = true) + val aStart = node(terminal = false) + aStart.put('a', aTerminal) + + val bTerminal = node(terminal = true) + val bStart = node(terminal = false) + bStart.put('b', bTerminal) + + val nfaA = NFA(start = aStart, alphabet = listOf('a', 'b')) + val nfaB = NFA(start = bStart, alphabet = listOf('a', 'b')) + + val concatenated = nfaA.concat(nfaB) + + assertTrue(concatenated.check("ab")) + assertFalse(concatenated.check("a")) + assertFalse(concatenated.check("b")) + + // original automata remain unchanged + assertTrue(nfaA.check("a")) + assertTrue(nfaB.check("b")) + } + + @Test + fun testProductKeepsCyclesBetweenVisitedPairs() { + val universal = node(terminal = true) + universal.put('a', universal) + universal.put('b', universal) + val nfaAll = NFA(start = universal, alphabet = listOf('a', 'b')) + + val first = node(terminal = true) + val second = node(terminal = true) + first.put('a', second) + second.put('b', first) + val nfaPattern = NFA(start = first, alphabet = listOf('a', 'b')) + + val product = nfaAll.product(nfaPattern) + + assertTrue(product.check("")) + assertTrue(product.check("a")) + assertTrue(product.check("ab")) + assertTrue(product.check("aba")) + assertTrue(product.check("abab")) + assertFalse(product.check("b")) + assertFalse(product.check("aa")) + assertFalse(product.check("abb")) + } + + @Test + fun testProductHandlesEpsilonTransitionsFromSingleSide() { + val terminalA = node(terminal = true) + val midA = node(terminal = false) + val startA = node(terminal = false) + startA.put(EPS, midA) + midA.put('a', terminalA) + val nfaA = NFA(start = startA, alphabet = listOf('a', 'b')) + + val terminalB = node(terminal = true) + val startB = node(terminal = false) + startB.put('a', terminalB) + val nfaB = NFA(start = startB, alphabet = listOf('a', 'b')) + + val product = nfaA.product(nfaB) + + assertTrue(product.check("a")) + assertFalse(product.check("")) + assertFalse(product.check("b")) + } + + @Test + fun testProductEpsilonAllowsEmptyWord() { + val terminalA = node(terminal = true) + val startA = node(terminal = false) + startA.put(EPS, terminalA) + val nfaA = NFA(start = startA, alphabet = listOf('a')) + + val startB = node(terminal = true) + val nfaB = NFA(start = startB, alphabet = listOf('a')) + + val product = nfaA.product(nfaB) + + assertTrue(product.check("")) + assertFalse(product.check("a")) + } + + @Test + fun testEpsilonClosureExpandsReachableNodes() { + val first = node(terminal = false) + val second = node(terminal = false) + val third = node(terminal = true) + first.put(EPS, second) + second.put(EPS, third) + + val visited = mutableSetOf(first) + epsilonClosure(visited) + + assertTrue(visited.contains(first)) + assertTrue(visited.contains(second)) + assertTrue(visited.contains(third)) + } + + @Test + fun testEpsilonClosureIgnoresNonEpsilonTransitions() { + val first = node(terminal = false) + val second = node(terminal = true) + first.put('a', second) + + val visited = mutableSetOf(first) + epsilonClosure(visited) + + assertTrue(visited.contains(first)) + assertFalse(visited.contains(second)) + } + + private fun node(terminal: Boolean): NFANode { + return NFANode(terminal, mutableMapOf()) + } +} diff --git a/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/RegexToNFATest.kt b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/RegexToNFATest.kt new file mode 100644 index 000000000..196e884e3 --- /dev/null +++ b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/RegexToNFATest.kt @@ -0,0 +1,176 @@ +package io.ksmt.solver.noodler.automaton + +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.sort.KRegexSort +import kotlin.test.Test +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class RegexToNFATest { + + @Test + fun testRangeStar() = with(KContext()) { + val range = mkRegexRange(mkStringLiteral("a"), mkStringLiteral("t")) + val star = mkRegexStar(range) + + val nfa = fromRegex(star, alphabet = ('a'..'u').toList()) + + assertAccepts(nfa, "", "a", "t", "abc", "ttt") + assertRejects(nfa, "u", "az", "A") + } + + @Test + fun testAbPlusC() = with(KContext()) { + val a = lit("a") + val b = lit("b") + val c = lit("c") + val bPlus = mkRegexCross(b) + val regex = mkRegexConcat(mkRegexConcat(a, bPlus), c) + + val nfa = fromRegex(regex, alphabet = listOf('a', 'b', 'c')) + + assertAccepts(nfa, "abc", "abbc", "abbbbbc") + assertRejects(nfa, "ac", "ab", "abcc", "aabc") + } + + @Test + fun testXyStarZPlusAbc() = with(KContext()) { + val x = lit("x") + val y = lit("y") + val z = lit("z") + val dot = mkRegexAllChar() + + val yStar = mkRegexStar(y) + val zPlus = mkRegexCross(z) + val abc = mkRegexUnion(mkRegexUnion(lit("a"), lit("b")), lit("c")) + + // xy*.z+(a|b|c) + val regex = mkRegexConcat( + mkRegexConcat( + mkRegexConcat(mkRegexConcat(x, yStar), dot), + zPlus + ), + abc + ) + + val nfa = fromRegex(regex, alphabet = listOf('a', 'b', 'c', 'x', 'y', 'z', 'q')) + + assertAccepts(nfa, "xzza", "xyyzzb", "xyazc", "xqza") + assertRejects(nfa, "xza", "xyya", "xyzzd", "xqz") + } + + @Test + fun testLiteralPupa() = with(KContext()) { + val regex = lit("pupa") + val nfa = fromRegex(regex, alphabet = listOf('p', 'u', 'a')) + + assertAccepts(nfa, "pupa") + assertRejects(nfa, "", "pup", "pupaa") + } + + @Test + fun testOperationsCoverage() = with(KContext()) { + val a = lit("a") + val b = lit("b") + val c = lit("c") + + // Epsilon (empty language) + val empty = fromRegex(mkRegexEpsilon(), alphabet = listOf('a')) + assertRejects(empty, "", "a") + + // All / AllChar + val all = fromRegex(mkRegexAll(), alphabet = listOf('a', 'b')) + assertAccepts(all, "", "a", "ab", "bba") + assertRejects(all, "c") + + val allChar = fromRegex(mkRegexAllChar(), alphabet = listOf('a', 'b')) + assertAccepts(allChar, "a", "b") + assertRejects(allChar, "", "ab", "c") + + // Concat / Union + val concat = fromRegex(mkRegexConcat(a, b), alphabet = listOf('a', 'b')) + assertAccepts(concat, "ab") + assertRejects(concat, "a", "b", "") + + val union = fromRegex(mkRegexUnion(a, b), alphabet = listOf('a', 'b')) + assertAccepts(union, "a", "b") + assertRejects(union, "ab", "") + + // Intersection + val inter = fromRegex(mkRegexIntersection(mkRegexUnion(a, b), mkRegexUnion(b, c)), alphabet = listOf('a', 'b', 'c')) + assertAccepts(inter, "b") + assertRejects(inter, "a", "c", "bb") + + // Star / Cross + val star = fromRegex(mkRegexStar(a), alphabet = listOf('a')) + assertAccepts(star, "", "a", "aa") + assertRejects(star, "b") + + val plus = fromRegex(mkRegexCross(a), alphabet = listOf('a')) + assertAccepts(plus, "a", "aa") + assertRejects(plus, "") + + // Difference / Complement + val diff = fromRegex(mkRegexDifference(mkRegexUnion(a, b), b), alphabet = listOf('a', 'b')) + assertAccepts(diff, "a") + assertRejects(diff, "b", "ab", "") + + val comp = fromRegex(mkRegexComplement(a), alphabet = listOf('a', 'b')) + assertAccepts(comp, "", "b", "bb", "ab") + assertRejects(comp, "a") + + // Option + val opt = fromRegex(mkRegexOption(a), alphabet = listOf('a')) + assertAccepts(opt, "", "a") + assertRejects(opt, "aa", "b") + + // Range + val range = fromRegex(mkRegexRange(mkStringLiteral("b"), mkStringLiteral("d")), alphabet = listOf('a', 'b', 'c', 'd')) + assertAccepts(range, "b", "c", "d") + assertRejects(range, "a", "e", "bc") + + // Power + val pow = fromRegex(mkRegexPower(3, a), alphabet = listOf('a')) + assertAccepts(pow, "aaa") + assertRejects(pow, "", "a", "aa", "aaaa") + + // Loop + val loop = fromRegex(mkRegexLoop(1, 2, a), alphabet = listOf('a')) + assertAccepts(loop, "a", "aa") + assertRejects(loop, "", "aaa") + + // StringToRegex + val strRe = fromRegex(mkStringToRegex(mkStringLiteral("ab")), alphabet = listOf('a', 'b')) + assertAccepts(strRe, "ab") + assertRejects(strRe, "", "a", "aba") + } + + @Test + fun testDotAnyChar() = with(KContext()) { + val x = lit("x") + val z = lit("z") + val dot = mkRegexAllChar() + val regex = mkRegexConcat(mkRegexConcat(x, dot), z) + + val nfa = fromRegex(regex, alphabet = listOf('x', 'z', 'a', 'b')) + + assertAccepts(nfa, "xaz", "xbz", "xzz") + assertRejects(nfa, "xz", "xazz", "xcz") + } + + private fun KContext.lit(value: String): KExpr = + mkStringToRegex(mkStringLiteral(value)) + + private fun assertAccepts(nfa: NFA, vararg words: String) { + for (word in words) { + assertTrue(nfa.check(word), "Expected to accept '$word'") + } + } + + private fun assertRejects(nfa: NFA, vararg words: String) { + for (word in words) { + assertFalse(nfa.check(word), "Expected to reject '$word'") + } + } +} diff --git a/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/TransformToDFATest.kt b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/TransformToDFATest.kt new file mode 100644 index 000000000..2c2fba232 --- /dev/null +++ b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/automaton/TransformToDFATest.kt @@ -0,0 +1,75 @@ +package io.ksmt.solver.noodler.automaton + +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class TransformToDFATest { + + @Test + fun testTransformToDfaUsesEpsilonClosureOnStart() { + val terminal = node(terminal = true) + val start = node(terminal = false) + start.put(EPS, terminal) + + val nfa = NFA(start = start, alphabet = listOf('a')) + val dfa = transformToDFA(nfa) + + assertTrue(dfa.check("")) + assertFalse(dfa.check("a")) + } + + @Test + fun testTransformToDfaUsesEpsilonClosureAfterMove() { + val terminal = node(terminal = true) + val mid = node(terminal = false) + val start = node(terminal = false) + start.put(EPS, mid) + mid.put('a', terminal) + + val nfa = NFA(start = start, alphabet = listOf('a')) + val dfa = transformToDFA(nfa) + + assertTrue(dfa.check("a")) + assertFalse(dfa.check("")) + assertFalse(dfa.check("b")) + } + + @Test + fun testTransformToDfaPreservesNondeterministicChoices() { + val acceptA = node(terminal = true) + val mid = node(terminal = false) + val acceptAB = node(terminal = true) + val start = node(terminal = false) + start.put('a', acceptA) + start.put('a', mid) + mid.put('b', acceptAB) + + val nfa = NFA(start = start, alphabet = listOf('a', 'b')) + val dfa = transformToDFA(nfa) + + val samples = listOf("", "a", "ab", "b", "aa", "abb") + for (word in samples) { + assertEquals(nfa.check(word), dfa.check(word), "Mismatch on '$word'") + } + } + + @Test + fun testTransformToDfaDropsEpsilonFromAlphabet() { + val terminal = node(terminal = true) + val start = node(terminal = false) + start.put(EPS, terminal) + start.put('a', terminal) + + val nfa = NFA(start = start, alphabet = listOf(EPS, 'a')) + val dfa = transformToDFA(nfa) + + assertFalse(dfa.alphabet.contains(EPS)) + assertTrue(dfa.alphabet.contains('a')) + } + + private fun node(terminal: Boolean): NFANode { + return NFANode(terminal, mutableMapOf()) + } +} diff --git a/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/core/NoodlerTest.kt b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/core/NoodlerTest.kt new file mode 100644 index 000000000..53105cbdf --- /dev/null +++ b/ksmt-noodler/src/test/kotlin/io/ksmt/solver/noodler/core/NoodlerTest.kt @@ -0,0 +1,105 @@ +package io.ksmt.solver.noodler.core + +import io.ksmt.KContext +import io.ksmt.expr.KConst +import io.ksmt.solver.noodler.automaton.fromRegex +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertFailsWith +import kotlin.test.assertTrue + +class NoodlerTest { + private val binaryAlphabet = listOf('a', 'b') + + @Test + fun testSplitStatementsAndBuildRegularConstraintMap() = with(KContext()) { + val x = mkConst("x", stringSort) + val y = mkConst("y", stringSort) + val t = mkConst("t", stringSort) + + val equation = mkEq(mkStringConcat(x, y), t) + val xConstraint = mkStringInRegex(x, mkRegexCross(mkStringToRegex(mkStringLiteral("a")))) + val yConstraint = mkStringInRegex(y, mkRegexStar(mkStringToRegex(mkStringLiteral("b")))) + + val noodler = Noodler(listOf(equation, xConstraint, yConstraint), binaryAlphabet) + + assertEquals(1, noodler.equations.size) + assertEquals(2, noodler.regularConstraints.size) + assertEquals(setOf("x", "y"), noodler.regularConstraintsByVariable.keys) + + val xRegexNfa = noodler.regularConstraintsByVariable.getValue("x") + assertTrue(xRegexNfa.check("a")) + assertTrue(xRegexNfa.check("aa")) + } + + @Test + fun testDuplicateRegularConstraintMergesByIntersection() = with(KContext()) { + val x = mkConst("x", stringSort) + val constraint1 = mkStringInRegex(x, mkRegexCross(mkStringToRegex(mkStringLiteral("a")))) + val constraint2 = mkStringInRegex(x, mkRegexStar(mkStringToRegex(mkStringLiteral("b")))) + + val noodler = Noodler(listOf(constraint1, constraint2), binaryAlphabet) + val merged = noodler.regularConstraintsByVariable.getValue("x") + assertTrue(!merged.check("")) + assertTrue(!merged.check("a")) + assertTrue(!merged.check("b")) + } + + @Test + fun testRegularConstraintOnNonVariableFails(): Unit = with(KContext()) { + val x = mkConst("x", stringSort) + val y = mkConst("y", stringSort) + val nonVariable = mkStringConcat(x, y) + val constraint = mkStringInRegex(nonVariable, mkRegexAll()) + + assertFailsWith { + Noodler(listOf(constraint), binaryAlphabet) + } + } + + @Test + fun testEquationWithLiteralFails(): Unit = with(KContext()) { + val x = mkConst("x", stringSort) + val y = mkConst("y", stringSort) + val equation = mkEq(mkStringConcat(x, mkStringLiteral("a")), y) + + assertFailsWith { + Noodler(listOf(equation), binaryAlphabet) + } + } + + @Test + fun testSolveDerivesAdditionalConstraintForTargetVariable() = with(KContext()) { + val x = mkConst("x", stringSort) + val y = mkConst("y", stringSort) + val t = mkConst("t", stringSort) + + val equation = mkEq(mkStringConcat(x, y), t) + val xConstraint = mkStringInRegex(x, mkStringToRegex(mkStringLiteral("a"))) + val yConstraint = mkStringInRegex(y, mkStringToRegex(mkStringLiteral("b"))) + + val (isSat, additionalConstraints) = Noodler( + listOf(equation, xConstraint, yConstraint), + binaryAlphabet + ).solve() + + assertTrue(isSat) + assertTrue(additionalConstraints.all { constraint -> + val variableName = (constraint.arg0 as KConst<*>).decl.name + variableName in setOf(x.decl.name, y.decl.name, t.decl.name) + }) + + val tConstraint = additionalConstraints.firstOrNull { + val variableName = (it.arg0 as KConst<*>).decl.name + variableName == t.decl.name + } + if (tConstraint != null) { + val derivedAutomaton = fromRegex(tConstraint.arg1, binaryAlphabet) + assertTrue(derivedAutomaton.check("ab")) + assertFalse(derivedAutomaton.check("a")) + assertFalse(derivedAutomaton.check("b")) + } + } + +} diff --git a/settings.gradle.kts b/settings.gradle.kts index 887d3798c..af7ae51f8 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -22,6 +22,7 @@ include("ksmt-runner:solver-generator") include("ksmt-test") include("ksmt-symfpu") +include("ksmt-noodler") pluginManagement { resolutionStrategy {