Feature request: add OMT (Optimization Modulo Theories) support

[yeicor]

Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) by enabling solvers to find optimal solutions based on a defined objective function after verifying formula satisfiability. Adding OMT capabilities to the library would significantly enhance its ability to solve optimization problems directly.

I have implemented a prototype using Z3’s APIs. The solution is functional but hacky. I’m unsure if it’s the correct approach and it is inefficient because it copies all constraints to the optimizer. I’m also uncertain whether other SMT solvers support OMT, as my experience with SMT is limited.

data class MinimizingSolverZ3(val impl: KZ3Solver) : MinimizingSolver<KZ3SolverConfiguration>,
    KSolver<KZ3SolverConfiguration> by impl {
    val z3Ctx: KZ3Context =
        impl::class.java.getDeclaredField("z3Ctx").apply { isAccessible = true }.get(impl) as KZ3Context
    val exprInternalizer = impl::class.java.getDeclaredMethod("getExprInternalizer")
        .apply { isAccessible = true }.invoke(impl) as KZ3ExprInternalizer
    val exprCreate = Expr::class.java.getDeclaredMethod("create", Context::class.java, Long::class.java)
        .apply { isAccessible = true } as Method

    override fun <K : KArithSort> modelMinimizing(
        expr: KExpr<K>,
        maxIterations: Int,
        timeout: Duration,
    ): KModel {
        // Sadly, we need to create an Optimize object and copy all Solver constraints to it
        val opt: Optimize = z3Ctx.nativeContext.mkOptimize()
        applyTimeout(opt, timeout)
        for (c in impl.nativeSolver().assertions) opt.Assert(c)

        // Add the expression to minimize
        val exprId = with(exprInternalizer) { expr.internalizeExpr() }
        val convertedExpr = exprCreate.invoke(null, z3Ctx.nativeContext, exprId) as Expr<*>
        opt.MkMinimize(convertedExpr)

        // Normal check, but using the optimizer
        opt.Check()

        // Extract the model and return it
        return KZ3Model(opt.model, expr.ctx, z3Ctx, exprInternalizer)
    }

    private fun applyTimeout(opt: Optimize, timeout: Duration) {
        val z3Timeout = if (timeout == Duration.INFINITE) UInt.MAX_VALUE.toInt()
        else timeout.toInt(DurationUnit.MILLISECONDS)
        opt.setParameters(z3Ctx.nativeContext.mkParams().apply { add("timeout", z3Timeout) })
    }
}