Improve optimization API and add fallback implementation

doc/Optimization.md

@@ -0,0 +1 @@
+

src/org/sosy_lab/java_smt/SolverContextFactory.java

@@ -366,4 +366,42 @@ public static SolverContext createSolverContext(Solvers solver)
             NativeLibraries::loadLibrary)
         .generateContext(solver);
   }
+
+  /**
+   * Create a new optimization prover environment.
+   * @param context The solver context
+   * @param options The prover options
+   * @return An optimization prover environment
+   * @throws SolverOptimizationException if the solver doesn't support optimization
+   */
+  public static OptimizationProverEnvironment createOptimizationProver(
+          SolverContext context, Set<ProverOptions> options) {
+    Solvers solver = context.getSolver();
+
+    // Check if optimization is supported
+    if (!SolverVersionChecker.isOptimizationSupported(solver)) {
+        logger.log(Level.WARNING, SolverVersionChecker.getOptimizationSupportMessage(solver));
+        return new FallbackOptimizationProver(context, logger, context.getFormulaManager(), options);
+    }
+
+    // Check version compatibility for MathSAT5
+    if (solver == Solvers.MATHSAT5) {
+        try {
+            SolverVersionChecker.checkMathSATVersion(context.getVersion());
+        } catch (SolverOptimizationException e) {
+            logger.log(Level.WARNING, e.getMessage());
+            return new FallbackOptimizationProver(context, logger, context.getFormulaManager(), options);
+        }
+    }
+
+    // Create solver-specific optimization prover
+    switch (solver) {
+        case Z3:
+            return new Z3OptimizationProver(/*...*/);
+        case MATHSAT5:
+            return new MathSATOptimizationProver(/*...*/);
+        default:
+            return new FallbackOptimizationProver(context, logger, context.getFormulaManager(), options);
+    }
+  }
 }

src/org/sosy_lab/java_smt/api/SolverOptimizationException.java

@@ -0,0 +1,31 @@
+package org.sosy_lab.java_smt.api;
+
+/**
+ * Exception thrown when a solver does not support optimization features
+ * or when there are version-specific optimization issues.
+ */
+public class SolverOptimizationException extends SolverException {
+    private static final long serialVersionUID = 1L;
+    private final String solverName;
+    private final String feature;
+
+    public SolverOptimizationException(String solverName, String feature) {
+        super(String.format("%s does not support %s", solverName, feature));
+        this.solverName = solverName;
+        this.feature = feature;
+    }
+
+    public SolverOptimizationException(String solverName, String feature, String reason) {
+        super(String.format("%s does not support %s: %s", solverName, feature, reason));
+        this.solverName = solverName;
+        this.feature = feature;
+    }
+
+    public String getSolverName() {
+        return solverName;
+    }
+
+    public String getFeature() {
+        return feature;
+    }
+} 

src/org/sosy_lab/java_smt/basicimpl/AbstractOptimizationProver.java

@@ -0,0 +1,71 @@
+package org.sosy_lab.java_smt.basicimpl;
+
+import org.sosy_lab.common.log.LogManager;
+import org.sosy_lab.java_smt.api.BasicProverEnvironment;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaManager;
+import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
+import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.common.rationals.Rational;
+
+import java.util.Collection;
+import java.util.Optional;
+
+public abstract class AbstractOptimizationProver extends AbstractProver implements OptimizationProverEnvironment {
+
+    protected final LogManager logger;
+    protected final FormulaManager formulaManager;
+
+    protected AbstractOptimizationProver(LogManager pLogger, FormulaManager pMgr) {
+        this.logger = pLogger;
+        this.formulaManager = pMgr;
+    }
+
+    @Override
+    public boolean isOptimizationSupported() {
+        return false; // Default implementation
+    }
+
+    @Override
+    public int maximize(Formula objective) {
+        if (!isOptimizationSupported()) {
+            throw new UnsupportedOperationException(
+                "Optimization not supported by " + getSolverName());
+        }
+        return maximizeInternal(objective);
+    }
+
+    @Override
+    public int minimize(Formula objective) {
+        if (!isOptimizationSupported()) {
+            throw new UnsupportedOperationException(
+                "Optimization not supported by " + getSolverName());
+        }
+        return minimizeInternal(objective);
+    }
+
+    protected abstract int maximizeInternal(Formula objective);
+    protected abstract int minimizeInternal(Formula objective);
+    protected abstract String getSolverName();
+
+    @Override
+    public Optional<Rational> upper(int handle, Rational epsilon) {
+        if (!isOptimizationSupported()) {
+            throw new UnsupportedOperationException(
+                "Optimization not supported by " + getSolverName());
+        }
+        return upperInternal(handle, epsilon);
+    }
+
+    @Override
+    public Optional<Rational> lower(int handle, Rational epsilon) {
+        if (!isOptimizationSupported()) {
+            throw new UnsupportedOperationException(
+                "Optimization not supported by " + getSolverName());
+        }
+        return lowerInternal(handle, epsilon);
+    }
+
+    protected abstract Optional<Rational> upperInternal(int handle, Rational epsilon);
+    protected abstract Optional<Rational> lowerInternal(int handle, Rational epsilon);
+} 

src/org/sosy_lab/java_smt/basicimpl/FallbackOptimizationProver.java

@@ -0,0 +1,203 @@
+package org.sosy_lab.java_smt.basicimpl;
+
+import org.sosy_lab.common.log.LogManager;
+import org.sosy_lab.java_smt.api.BasicProverEnvironment;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaManager;
+import org.sosy_lab.java_smt.api.IntegerFormulaManager;
+import org.sosy_lab.java_smt.api.NumeralFormula;
+import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
+import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
+import org.sosy_lab.java_smt.api.SolverContext;
+import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.common.rationals.Rational;
+
+import java.util.HashMap;
+import java.util.Map;
+import java.util.Optional;
+import java.util.Set;
+import java.util.logging.Level;
+
+/**
+ * A fallback implementation of OptimizationProverEnvironment for solvers
+ * that don't support optimization natively. This implementation uses
+ * iterative solving to approximate optimization results.
+ */
+public class FallbackOptimizationProver extends AbstractOptimizationProver {
+    private final BasicProverEnvironment baseProver;
+    private final SolverContext context;
+    private final Map<Integer, Formula> objectives;
+    private int nextHandle;
+
+    public FallbackOptimizationProver(
+            SolverContext pContext,
+            LogManager pLogger,
+            FormulaManager pMgr,
+            Set<SolverContext.ProverOptions> pOptions) {
+        super(pLogger, pMgr);
+        this.context = pContext;
+        this.baseProver = pContext.newProverEnvironment(pOptions);
+        this.objectives = new HashMap<>();
+        this.nextHandle = 0;
+    }
+
+    @Override
+    public boolean isOptimizationSupported() {
+        return true; // We always support optimization through fallback
+    }
+
+    @Override
+    protected String getSolverName() {
+        return context.getSolverName();
+    }
+
+    @Override
+    protected int maximizeInternal(Formula objective) {
+        int handle = nextHandle++;
+        objectives.put(handle, objective);
+        return handle;
+    }
+
+    @Override
+    protected int minimizeInternal(Formula objective) {
+        // For minimization, we negate the objective and maximize
+        FormulaManager fmgr = context.getFormulaManager();
+        if (objective instanceof IntegerFormula) {
+            IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager();
+            return maximizeInternal(imgr.negate((IntegerFormula) objective));
+        } else if (objective instanceof RationalFormula) {
+            // Handle rational formulas similarly
+            // Implementation depends on the specific formula manager
+            throw new UnsupportedOperationException(
+                "Rational optimization not yet implemented in fallback");
+        } else {
+            throw new UnsupportedOperationException(
+                "Unsupported formula type for optimization: " + objective.getClass());
+        }
+    }
+
+    @Override
+    protected Optional<Rational> upperInternal(int handle, Rational epsilon) {
+        Formula objective = objectives.get(handle);
+        if (objective == null) {
+            throw new IllegalArgumentException("Invalid objective handle: " + handle);
+        }
+
+        try {
+            // Start with a large upper bound
+            Rational upperBound = Rational.ofLong(1000000);
+            Rational lowerBound = Rational.ofLong(-1000000);
+
+            // Binary search to find the maximum value
+            while (upperBound.subtract(lowerBound).compareTo(epsilon) > 0) {
+                Rational mid = upperBound.add(lowerBound).divide(Rational.ofLong(2));
+
+                // Create constraint: objective <= mid
+                BooleanFormula constraint = createUpperBoundConstraint(objective, mid);
+                baseProver.push();
+                baseProver.addConstraint(constraint);
+
+                try {
+                    if (baseProver.isUnsat()) {
+                        // No solution exists with this upper bound
+                        upperBound = mid;
+                    } else {
+                        // Solution exists, try a higher value
+                        lowerBound = mid;
+                    }
+                } finally {
+                    baseProver.pop();
+                }
+            }
+
+            return Optional.of(upperBound);
+        } catch (SolverException | InterruptedException e) {
+            logger.log(Level.WARNING, "Error during optimization", e);
+            return Optional.empty();
+        }
+    }
+
+    @Override
+    protected Optional<Rational> lowerInternal(int handle, Rational epsilon) {
+        Formula objective = objectives.get(handle);
+        if (objective == null) {
+            throw new IllegalArgumentException("Invalid objective handle: " + handle);
+        }
+
+        try {
+            // Start with a small lower bound
+            Rational lowerBound = Rational.ofLong(-1000000);
+            Rational upperBound = Rational.ofLong(1000000);
+
+            // Binary search to find the minimum value
+            while (upperBound.subtract(lowerBound).compareTo(epsilon) > 0) {
+                Rational mid = upperBound.add(lowerBound).divide(Rational.ofLong(2));
+
+                // Create constraint: objective >= mid
+                BooleanFormula constraint = createLowerBoundConstraint(objective, mid);
+                baseProver.push();
+                baseProver.addConstraint(constraint);
+
+                try {
+                    if (baseProver.isUnsat()) {
+                        // No solution exists with this lower bound
+                        lowerBound = mid;
+                    } else {
+                        // Solution exists, try a lower value
+                        upperBound = mid;
+                    }
+                } finally {
+                    baseProver.pop();
+                }
+            }
+
+            return Optional.of(lowerBound);
+        } catch (SolverException | InterruptedException e) {
+            logger.log(Level.WARNING, "Error during optimization", e);
+            return Optional.empty();
+        }
+    }
+
+    private BooleanFormula createUpperBoundConstraint(Formula objective, Rational bound) {
+        FormulaManager fmgr = context.getFormulaManager();
+        if (objective instanceof IntegerFormula) {
+            IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager();
+            return imgr.lessOrEquals(
+                (IntegerFormula) objective,
+                imgr.makeNumber(bound.longValue()));
+        } else if (objective instanceof RationalFormula) {
+            // Handle rational formulas similarly
+            // Implementation depends on the specific formula manager
+            throw new UnsupportedOperationException(
+                "Rational optimization not yet implemented in fallback");
+        } else {
+            throw new UnsupportedOperationException(
+                "Unsupported formula type for optimization: " + objective.getClass());
+        }
+    }
+
+    private BooleanFormula createLowerBoundConstraint(Formula objective, Rational bound) {
+        FormulaManager fmgr = context.getFormulaManager();
+        if (objective instanceof IntegerFormula) {
+            IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager();
+            return imgr.greaterOrEquals(
+                (IntegerFormula) objective,
+                imgr.makeNumber(bound.longValue()));
+        } else if (objective instanceof RationalFormula) {
+            // Handle rational formulas similarly
+            // Implementation depends on the specific formula manager
+            throw new UnsupportedOperationException(
+                "Rational optimization not yet implemented in fallback");
+        } else {
+            throw new UnsupportedOperationException(
+                "Unsupported formula type for optimization: " + objective.getClass());
+        }
+    }
+
+    @Override
+    public void close() {
+        baseProver.close();
+    }
+}