Optimization API and Resource Management Improvements Needed

[shivammm21]

Inconsistent Optimization Support Across Solvers

Description

The optimization API in JavaSMT has inconsistent implementation across different solvers, leading to unpredictable behavior when applications switch between solver backends. Currently, only Z3 and MathSAT5 (via OptiMathSAT) properly support optimization capabilities, while other solvers simply throw exceptions without providing alternative functionality.

Observed Issues

Evidence in Implementation Code:

Z3 provides full implementation:

// In Z3SolverContext.java
public OptimizationProverEnvironment newOptimizationProverEnvironment0(
    Set<ProverOptions> options) {
  Z3SolverContext.ExtraOptions extraOptions = new Z3SolverContext.ExtraOptions(config);
  return new Z3OptimizationProver(
      creator,
      logger,
      (Z3FormulaManager) getFormulaManager(),
      options,
      ImmutableMap.<String, Object>builder()
          .put(OPT_ENGINE_CONFIG_KEY, extraOptions.optimizationEngine)
          .put(OPT_PRIORITY_CONFIG_KEY, extraOptions.objectivePrioritizationMode)
          .build(),
      logfile,
      shutdownNotifier);
}

While other solvers throw exceptions:

// In YicesSolverContext.java
protected OptimizationProverEnvironment newOptimizationProverEnvironment0(
    Set<ProverOptions> options) {
  throw new UnsupportedOperationException("Yices does not support optimization");
}

// In SMTInterpolSolverContext.java
public OptimizationProverEnvironment newOptimizationProverEnvironment0(
    Set<ProverOptions> options) {
  throw new UnsupportedOperationException("SMTInterpol does not support optimization");
}

// In PrincessSolverContext.java
public OptimizationProverEnvironment newOptimizationProverEnvironment0(
    Set<ProverOptions> pOptions) {
  throw new UnsupportedOperationException("Princess does not support optimization");
}

Test Code Shows Special Handling:

Tests must skip optimization tests for most solvers:

// In OptimizationTest.java
@Before
public void skipUnsupportedSolvers() {
  requireOptimization();
}

// In SolverBasedTest0.java
protected final void requireOptimization() {
  try {
    context.newOptimizationProverEnvironment().close();
  } catch (UnsupportedOperationException e) {
    assume()
        .withMessage("Solver %s does not support optimization", solverToUse())
        .that(e)
        .isNull();
  }
}

Even between supported solvers, behavior differs:

// From OptimizationTest.java - MathSAT5 specific workaround
if (solverToUse() == Solvers.MATHSAT5) {
  // see https://github.com/sosy-lab/java-smt/issues/233
  assume()
      .withMessage("OptiMathSAT 1.7.2 has a bug with switching objectives")
      .that(context.getVersion())
      .doesNotContain("MathSAT5 version 1.7.2");
  assume()
      .withMessage("OptiMathSAT 1.7.3 has a bug with switching objectives")
      .that(context.getVersion())
      .doesNotContain("MathSAT5 version 1.7.3");
}

// Different precision handling between solvers
// OptiMathSAT5 has at least an epsilon of 1/1000000. It does not allow larger values.
assume()
    .withMessage("Solver %s does not support large epsilons", solverToUse())
    .that(solver)
    .isNotEqualTo(Solvers.MATHSAT5);

Impact

• Applications using optimization features cannot easily switch between solvers
• Code must handle UnsupportedOperationExceptions and provide fallbacks
• Optimization functionality is effectively limited to Z3 in many cases
• Testing is incomplete due to varying solver capabilities

[shivammm21]

I'd like to assign myself to work on fixing the inconsistent optimization support issue. Based on my analysis.

1. I understand the core problem is that optimization is fully implemented only in Z3 and partially in MathSAT5, while other solvers throw UnsupportedOperationException.

2. I have experience with the JavaSMT codebase and am familiar with the solver interfaces.

3. My approach would be to:

   • Create a fallback optimization implementation for solvers without native support
   • Standardize error handling and documentation across all solvers
   • Add better test coverage for mixed solver environments

I can submit an initial PR within 5 days that addresses the core inconsistencies.

Please let me know if there are any specific aspects you'd like me to prioritize.

[kfriedberger]

Thanks for your interest in tackling this issue! We really appreciate your initiative and willingness to dive into the inconsistent optimization support problem.

Optimization techniques can indeed be quite complex. Full support exists only in Z3, and a partial implementation in MathSAT5, while other solvers just do not have this feature. It’s worth noting that even MathSAT doesn’t include optimization in its main library - it's actually only available in its fork called OptiMathSAT, which is maybe inactive in development.

I would assume that the UnsupportedOperationException for an unsupported feature it thrown consistently across all solvers. If you see a way of improving this, feel free to provide a PR as quick-win for JavaSMT. Additionally, you might want to deeply go into the problem of optimization techniques to come with a valid solver-independent fallback mechanism that can be used if there is missing native support in a solver.

Looking forward to seeing your contribution—thanks again for stepping up!

[shivammm21]

Hi, I'd like to take on this issue. Please assign it to me.

I've already started researching the current state of optimization support in the various solvers integrated with JavaSMT, including how UnsupportedOperationException is being handled. I'm also looking into potential improvements and exploring ideas for a solver-independent fallback mechanism when native optimization support is missing.

It would be great if you could also add relevant labels such as enhancement or good first issue, if applicable.

Thanks for the helpful context and for encouraging community contributions. I am looking forward to working on this.

[kfriedberger]

Please make sure that you really understand the problem of optimization support before starting your implementation. There are reasons why several solvers do not support this feature, and one reason might be the complexity of this task: Finding an optimum for a specific constraint in SMT is considered a "hard problem".

[shivammm21]

Thank you for your feedback, @kfriedberger. I appreciate the caution about the complexity of optimization in SMT.

I understand optimization is inherently a "hard problem" in SMT, which explains why many solvers don't support it. My intention isn't to implement optimization algorithms from scratch for each solver, but rather to:

1. Create better standardization of the existing optimization API
2. Implement consistent error handling across solvers
3. Potentially create a basic fallback for simpler optimization cases using iterative solving approaches

Before proceeding, I'd like to better understand the specific limitations of different solvers. Would it be helpful to start with a survey of the current state and documentation improvements, before proposing any implementation changes?

[kfriedberger]

Your task list sounds reasonable.

1. Create better standardization of the existing optimization API
2. Implement consistent error handling across solvers

Please document the inconsistencies in the current API and error handling, e.g., is there more than just "unsupported" for now regarding the API of JavaSMT. Please consider to minimize API changes due to the requirement of backwards-compatibility. . Any reasonable pull request is appreciated.

3. Potentially create a basic fallback for simpler optimization cases using iterative solving approaches

Feel free to provide a fallback if there is a general solution. Please note that JavaSMT as such is only considered a "simple wrapper library" and as such any fallback should also be maintainable with reasonable effort in the future. Even larger SMT solver dismiss features that are not required by a larger group of users or have higher development effort as expected. A prominent example for such a feature is Craig interpolation that was removed from Z3 some years ago.