Improve optimization API and add fallback implementation #477
Conversation
This commit addresses issue sosy-lab#476 by: 1. Creating a standardized optimization API with AbstractOptimizationProver 2. Adding a fallback implementation for solvers without native optimization support 3. Implementing version compatibility checks for MathSAT5 4. Adding comprehensive tests for optimization features 5. Improving error handling with SolverOptimizationException 6. Adding documentation for optimization features The changes provide consistent optimization support across all solvers, with a graceful fallback for unsupported solvers. The implementation uses binary search to approximate optimization results for solvers without native support.
There was a problem hiding this comment.
Please split your implementation on "API consistency" from "default fallback algorithm".
For API consistency, I do not yet seen any benefit. It looks to become even worse.
For the fallback algorithm, the initial approach looks quite simple and could work for most use-cases on Integer theory.
There are some further comments above.
| * Exception thrown when a solver does not support optimization features | ||
| * or when there are version-specific optimization issues. | ||
| */ | ||
| public class SolverOptimizationException extends SolverException { |
There was a problem hiding this comment.
This looks like a complex way of throwing an UnsupportedOperationException, as it is done for other unsupported features, too, such as Interpolation in several solvers (see https://github.com/sosy-lab/java-smt/blob/master/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java#L308). A possible benefit is that this exception class extends SolverException, but this makes it inconsistent to other unsupported features.
| * @return An optimization prover environment | ||
| * @throws SolverOptimizationException if the solver doesn't support optimization | ||
| */ | ||
| public static OptimizationProverEnvironment createOptimizationProver( |
There was a problem hiding this comment.
The SolverContextFactory is intended to construct a SolverContext. This method violates this constraint, as it constructs a ProverEnvironment.
| if (solver == Solvers.Z3) { | ||
| return "Z3 provides full optimization support"; | ||
| } else if (solver == Solvers.MATHSAT5) { | ||
| return "MathSAT5 provides partial optimization support (versions > 1.7.3)"; |
There was a problem hiding this comment.
This message is incorrect. MathSAT5 (original version) does not support optimization, only OptiMathSAT does.
| * @return true if optimization is supported | ||
| */ | ||
| public static boolean isOptimizationSupported(Solvers solver) { | ||
| return solver == Solvers.Z3 || solver == Solvers.MATHSAT5; |
There was a problem hiding this comment.
This check is redundant. The same "feature" was already implemented in the solver-specific code when constructing a OptimizationProverEnvironment. The prover throws an UnsupportedOperationException if unsupported, or constructs a OptimizationProverEnvironment if supported.
| * @throws SolverOptimizationException if the version has known issues | ||
| */ | ||
| public static void checkMathSATVersion(String version) { | ||
| if (version.startsWith("1.7.2") || version.startsWith("1.7.3")) { |
There was a problem hiding this comment.
We avoid hard-coded versions, because this blocks users from simply replacing solver binaries and test on their own. We try to provide as much from the solver as possible and useful for the user, and do not create artificial boundaries.
| } | ||
| } | ||
|
|
||
| return Optional.of(upperBound); |
There was a problem hiding this comment.
Binary search is a valid idea and it should work in most applications. As a first prototype, this might work for several use cases. The performance overhead is not that large, e.g., several SAT checks are required (which is ok) and the number of them is logarithmic in the bounding window size (which is good).
There are some open points:
- We need to think about upper/lower bounds on unbounded theories like Integer or Rational.
- Maybe keep the prover content if the next contraint it stricter than the previous. This might improve reuse and perfomance on larger queries.
Optimization API and Resource Management Improvements
Description
This PR addresses the inconsistent optimization support across SMT solvers by implementing a robust fallback mechanism and standardizing the optimization API. The changes provide a consistent interface for optimization features across all supported solvers.
Changes
AbstractOptimizationProverbase class for standardizationFallbackOptimizationProverfor solvers without native supportSolverVersionCheckerfor version compatibility checksKey Features
Fixes #476