diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt index 4098e4f2a3..08e07417c4 100644 --- a/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt +++ b/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt @@ -94,8 +94,17 @@ open class UPathConstraints( typeConstraints.constraints() } + operator fun plusAssign(constraint: UBoolExpr) { + val queue = ArrayDeque() + queue.add(constraint) + while (queue.isNotEmpty()) { + val c = queue.removeFirst() + addConstraint(c, queue) + } + } + @Suppress("UNCHECKED_CAST") - open operator fun plusAssign(constraint: UBoolExpr): Unit = + protected open fun addConstraint(constraint: UBoolExpr, queue: ArrayDeque): Unit = with(constraint.uctx) { when { constraint == falseExpr -> contradiction(this) @@ -131,7 +140,7 @@ open class UPathConstraints( typeConstraints.addSubtype(constraint.ref, constraint.subtype as Type) } - constraint is UAndExpr -> constraint.args.forEach(::plusAssign) + constraint is UAndExpr -> queue.addAll(constraint.args) constraint is UNotExpr -> { val notConstraint = constraint.arg @@ -172,7 +181,7 @@ open class UPathConstraints( notConstraint in logicalConstraints -> contradiction(ctx) - notConstraint is UOrExpr -> notConstraint.args.forEach { plusAssign(ctx.mkNot(it)) } + notConstraint is UOrExpr -> queue.addAll(notConstraint.args.map(::mkNot)) else -> logicalConstraints.add(constraint, ownership) }