diff --git a/doc/Optimization.md b/doc/Optimization.md new file mode 100644 index 0000000000..0519ecba6e --- /dev/null +++ b/doc/Optimization.md @@ -0,0 +1 @@ + \ No newline at end of file diff --git a/src/org/sosy_lab/java_smt/SolverContextFactory.java b/src/org/sosy_lab/java_smt/SolverContextFactory.java index 576285424d..55ecfbebc0 100644 --- a/src/org/sosy_lab/java_smt/SolverContextFactory.java +++ b/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 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); + } + } } diff --git a/src/org/sosy_lab/java_smt/api/SolverOptimizationException.java b/src/org/sosy_lab/java_smt/api/SolverOptimizationException.java new file mode 100644 index 0000000000..7dc869c1bf --- /dev/null +++ b/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; + } +} \ No newline at end of file diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractOptimizationProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractOptimizationProver.java new file mode 100644 index 0000000000..d524f259f4 --- /dev/null +++ b/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 upper(int handle, Rational epsilon) { + if (!isOptimizationSupported()) { + throw new UnsupportedOperationException( + "Optimization not supported by " + getSolverName()); + } + return upperInternal(handle, epsilon); + } + + @Override + public Optional lower(int handle, Rational epsilon) { + if (!isOptimizationSupported()) { + throw new UnsupportedOperationException( + "Optimization not supported by " + getSolverName()); + } + return lowerInternal(handle, epsilon); + } + + protected abstract Optional upperInternal(int handle, Rational epsilon); + protected abstract Optional lowerInternal(int handle, Rational epsilon); +} \ No newline at end of file diff --git a/src/org/sosy_lab/java_smt/basicimpl/FallbackOptimizationProver.java b/src/org/sosy_lab/java_smt/basicimpl/FallbackOptimizationProver.java new file mode 100644 index 0000000000..9cd08964d1 --- /dev/null +++ b/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 objectives; + private int nextHandle; + + public FallbackOptimizationProver( + SolverContext pContext, + LogManager pLogger, + FormulaManager pMgr, + Set 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 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 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(); + } +} \ No newline at end of file diff --git a/src/org/sosy_lab/java_smt/basicimpl/SolverVersionChecker.java b/src/org/sosy_lab/java_smt/basicimpl/SolverVersionChecker.java new file mode 100644 index 0000000000..71ad89631b --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/SolverVersionChecker.java @@ -0,0 +1,49 @@ +package org.sosy_lab.java_smt.basicimpl; + +import org.sosy_lab.java_smt.api.SolverOptimizationException; +import org.sosy_lab.java_smt.api.Solvers; + +/** + * Utility class for checking solver versions and compatibility. + */ +public final class SolverVersionChecker { + private SolverVersionChecker() {} + + /** + * Check if the given MathSAT5 version has known optimization bugs. + * @param version The solver version string + * @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")) { + throw new SolverOptimizationException( + Solvers.MATHSAT5.name(), + "optimization", + "version " + version + " has known optimization bugs"); + } + } + + /** + * Check if optimization is supported for the given solver. + * @param solver The solver to check + * @return true if optimization is supported + */ + public static boolean isOptimizationSupported(Solvers solver) { + return solver == Solvers.Z3 || solver == Solvers.MATHSAT5; + } + + /** + * Get a descriptive message about optimization support for a solver. + * @param solver The solver to check + * @return A message describing optimization support + */ + public static String getOptimizationSupportMessage(Solvers solver) { + 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)"; + } else { + return solver.name() + " does not support optimization"; + } + } +} \ No newline at end of file diff --git a/src/org/sosy_lab/java_smt/test/FallbackOptimizationTest.java b/src/org/sosy_lab/java_smt/test/FallbackOptimizationTest.java new file mode 100644 index 0000000000..9d7a51a5cb --- /dev/null +++ b/src/org/sosy_lab/java_smt/test/FallbackOptimizationTest.java @@ -0,0 +1,86 @@ +package org.sosy_lab.java_smt.test; + +import org.junit.Before; +import org.junit.Test; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.IntegerFormulaManager; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +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.java_smt.basicimpl.FallbackOptimizationProver; +import org.sosy_lab.java_smt.basicimpl.SolverVersionChecker; + +import java.util.Optional; +import java.util.Set; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertTrue; + +public class FallbackOptimizationTest extends SolverBasedTest0 { + + private SolverContext context; + private IntegerFormulaManager imgr; + private OptimizationProverEnvironment prover; + + @Before + public void setUp() throws Exception { + context = SolverContextFactory.createSolverContext( + config, logger, shutdownNotifier, Solvers.PRINCESS); + imgr = context.getFormulaManager().getIntegerFormulaManager(); + prover = new FallbackOptimizationProver( + context, logger, context.getFormulaManager(), Set.of()); + } + + @Test + public void testMaximize() throws SolverException, InterruptedException { + // Create variables + IntegerFormula x = imgr.makeVariable("x"); + IntegerFormula y = imgr.makeVariable("y"); + + // Add constraints: x + y <= 10, x >= 0, y >= 0 + BooleanFormula constraint1 = imgr.lessOrEquals( + imgr.add(x, y), imgr.makeNumber(10)); + BooleanFormula constraint2 = imgr.greaterOrEquals(x, imgr.makeNumber(0)); + BooleanFormula constraint3 = imgr.greaterOrEquals(y, imgr.makeNumber(0)); + + prover.addConstraint(constraint1); + prover.addConstraint(constraint2); + prover.addConstraint(constraint3); + + // Maximize x + y + int handle = prover.maximize(imgr.add(x, y)); + + // Check result + Optional upper = prover.upper(handle, Rational.ofLong(1)); + assertTrue(upper.isPresent()); + assertEquals(Rational.ofLong(10), upper.get()); + } + + @Test + public void testMinimize() throws SolverException, InterruptedException { + // Create variables + IntegerFormula x = imgr.makeVariable("x"); + IntegerFormula y = imgr.makeVariable("y"); + + // Add constraints: x + y >= 5, x >= 0, y >= 0 + BooleanFormula constraint1 = imgr.greaterOrEquals( + imgr.add(x, y), imgr.makeNumber(5)); + BooleanFormula constraint2 = imgr.greaterOrEquals(x, imgr.makeNumber(0)); + BooleanFormula constraint3 = imgr.greaterOrEquals(y, imgr.makeNumber(0)); + + prover.addConstraint(constraint1); + prover.addConstraint(constraint2); + prover.addConstraint(constraint3); + + // Minimize x + y + int handle = prover.minimize(imgr.add(x, y)); + + // Check result + Optional lower = prover.lower(handle, Rational.ofLong(1)); + assertTrue(lower.isPresent()); + assertEquals(Rational.ofLong(5), lower.get()); + } +} \ No newline at end of file