Portfolio solver cancellation

[niyaznigmatullin]

I have a suggestion (probably I can make a PR, but I'm not very familiar with the code).

KSolverRunner unlike KPortfolioSolver allowed us to cancel suspending methods from the outside, for KPortfolioSolver it doesn't work as far as I tried to investigate the reason is awaitFirstSolver function.

This line throws an exception on cancellation https://github.com/UnitTestBot/ksmt/blob/6803209da1c54a995de9ba4f92f8633bbb421cb8/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt#L319, and the exception is not handled.

I suggest to catch the exception inside awaitFirstSolver and kill all active inner solvers.

(If you think this is doable and can be done straightforwardly, I will create a PR)

[Saloed]

Can you provide an example with expected behaviour? It is unclear, why it is inappropriate to catch the exception it the user code and invoke close. Is it ok to wrap the cancellation exception into KSolverException?

[niyaznigmatullin]

The expected behaviour is when I cancel the KPortfolioSolver's async method it cancels the inner solvers as well.

The issue is KPortfolioSolver's close waits for them to finish (I don't know why exactly, but it is blocking).

I've run the following test in PortfolioSolverTest.kt

    @Test
    fun testCancellation(): Unit {
        val query = with(context) {
            val x = intSort.mkConst("x")
            val y = intSort.mkConst("y")
            val z = intSort.mkConst("z")
            (x gt 0.expr) and (y gt 0.expr) and (z gt 0.expr) and (x * x * x + y * y * y eq z * z * z)
        }
        val result = runBlocking {
            withTimeoutOrNull(500.milliseconds) {
                solver.assertAsync(query)
                solver.checkAsync(Duration.INFINITE)
            }
        }
        assertEquals(null, result)
    }

It runs in 10 seconds, it hangs in close method (in clearResources), waiting for the inner solvers to finish in hardTimeout as I understand.

If I change:

        return resultFuture.await()

into

        try {
            return resultFuture.await()
        } catch (ex: CancellationException) {
            activeSolvers.forEach { _, solverOperationState ->
                solverOperationState.operationScope.cancel(ex)
            }
            throw ex
        }

it starts running in 0.5 seconds.

[Saloed]

In your solution you just cancel the coroutine and skip deleteSolver leaving the solver process pool in the incorrect state. The issue with close can be fixed with #129

Does this fix works in your cases or maybe you have more complex scenarios?

[niyaznigmatullin]

Yes, I've checked, it works in my case. Thanks