diff --git a/usvm-core/src/main/kotlin/org/usvm/PathNode.kt b/usvm-core/src/main/kotlin/org/usvm/PathNode.kt index d5ec1f786..ebbbe561d 100644 --- a/usvm-core/src/main/kotlin/org/usvm/PathNode.kt +++ b/usvm-core/src/main/kotlin/org/usvm/PathNode.kt @@ -3,46 +3,66 @@ package org.usvm import org.usvm.algorithms.findLcaLinear import org.usvm.merging.UMergeable +sealed interface PathSegment { + val statement: Statement + + data class Single( + override val statement: Statement, + ) : PathSegment { + override fun toString(): String = "$statement" + } + + data class Merged( + override val statement: Statement, + val left: List>, + val right: List>, + ) : PathSegment { + override fun toString(): String = buildString { + appendLine(statement) + val targetSize = kotlin.math.max(left.size, right.size) + val leftStrs = left.map { it.toString() } + List(targetSize - left.size) { "" } + val rightStrs = right.map { it.toString() } + List(targetSize - right.size) { "" } + val leftColumnnSize = (leftStrs.maxOfOrNull { it.length } ?: 0) + 8 + leftStrs.zip(rightStrs).forEach { (left, right) -> + append(left.padEnd(leftColumnnSize)) + appendLine(right) + } + } + } +} + class PathNode private constructor( val parent: PathNode?, - private val _statement: Statement?, + private val _segment: PathSegment?, depth: Int, ) : UMergeable, Unit> { var depth: Int = depth private set - val statement: Statement get() = requireNotNull(_statement) + val statement: Statement get() = requireNotNull(_segment).statement operator fun plus(statement: Statement): PathNode { - return PathNode(this, statement, depth + 1) + return PathNode(this, PathSegment.Single(statement), depth + 1) } val allStatements get(): Iterable = Iterable { object : Iterator { var cur = this@PathNode - override fun hasNext(): Boolean = cur._statement != null + override fun hasNext(): Boolean = cur._segment != null override fun next(): Statement { if (!hasNext()) { throw NoSuchElementException() } - val element = requireNotNull(cur._statement) + val element = requireNotNull(cur._segment) cur = requireNotNull(cur.parent) - return element + return element.statement } } } - companion object { - private val EMPTY = PathNode(parent = null, _statement = null, depth = 0) - - @Suppress("UNCHECKED_CAST") - fun root(): PathNode = EMPTY as PathNode - } - - /** * Check if this [PathNode] can be merged with [other] path node. * @@ -54,10 +74,32 @@ class PathNode private constructor( * @return the merged path node. */ override fun mergeWith(other: PathNode, by: Unit): PathNode? { - if (_statement != other._statement) { + if (_segment != other._segment) { return null } - val (lca, _, _) = findLcaLinear(this, other, { it.parent!! }, { it.depth }, { it.statement }) - return lca + statement + val (lca, suffixLeft, suffixRight) = findLcaLinear( + this, + other, + { it.parent!! }, + { it.depth }, + { it._segment!! } + ) + + val segment = PathSegment.Merged(statement, suffixLeft, suffixRight) + + return PathNode(lca, segment, lca.depth + 1) + } + + companion object { + private val EMPTY = PathNode(parent = null, _segment = null, depth = 0) + + @Suppress("UNCHECKED_CAST") + fun root(): PathNode = EMPTY as PathNode } + + override fun toString(): String = + buildString { + appendLine(_segment) + appendLine(parent) + } }