diff --git a/src/org/sosy_lab/java_smt/api/InterpolatingProverEnvironment.java b/src/org/sosy_lab/java_smt/api/InterpolatingProverEnvironment.java index 11767bcf4d..6ac45b33e5 100644 --- a/src/org/sosy_lab/java_smt/api/InterpolatingProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/InterpolatingProverEnvironment.java @@ -24,7 +24,6 @@ * @param The type of the objects which can be used to select formulas for interpolant creation. */ public interface InterpolatingProverEnvironment extends BasicProverEnvironment { - /** * Get an interpolant for two groups of formulas. This should be called only immediately after an * {@link #isUnsat()} call that returned true. diff --git a/src/org/sosy_lab/java_smt/api/SolverContext.java b/src/org/sosy_lab/java_smt/api/SolverContext.java index 3fbd476c77..c697550852 100644 --- a/src/org/sosy_lab/java_smt/api/SolverContext.java +++ b/src/org/sosy_lab/java_smt/api/SolverContext.java @@ -53,7 +53,37 @@ enum ProverOptions { GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS, /** Whether the solver should enable support for formulae build in SL theory. */ - ENABLE_SEPARATION_LOGIC + ENABLE_SEPARATION_LOGIC, + + /** + * Enables Craig interpolation, using the model-based interpolation strategy. This strategy + * constructs interpolants based on the model provided by a solver, i.e. model generation must + * be enabled. This interpolation strategy is only usable for solvers supporting quantified + * solving over the theories interpolated upon. The solver does not need to support + * interpolation itself. + */ + GENERATE_PROJECTION_BASED_INTERPOLANTS, + + /** + * Enables (uniform) Craig interpolation, using the quantifier-based interpolation strategy + * utilizing quantifier-elimination in the forward direction. Forward means, that the set of + * formulas A, used to interpolate, interpolates towards the set of formulas B (B == all + * formulas that are currently asserted, but not in the given set of formulas A used to + * interpolate). This interpolation strategy is only usable for solvers supporting + * quantifier-elimination over the theories interpolated upon. The solver does not need to + * support interpolation itself. + */ + GENERATE_UNIFORM_FORWARD_INTERPOLANTS, + + /** + * Enables (uniform) Craig interpolation, using the quantifier-based interpolation strategy + * utilizing quantifier-elimination in the backward direction. Backward means, that the set of + * formulas B (B == all formulas that are currently asserted, but not in the given set of + * formulas A used to interpolate) interpolates towards the set of formulas A. This + * interpolation strategy is only usable for solvers supporting quantifier-elimination over the + * theories interpolated upon. The solver does not need to support interpolation itself. + */ + GENERATE_UNIFORM_BACKWARD_INTERPOLANTS } /** @@ -68,7 +98,6 @@ enum ProverOptions { /** * Create a fresh new {@link InterpolatingProverEnvironment} which encapsulates an assertion stack * and allows generating and retrieve interpolants for unsatisfiable formulas. If the SMT solver - * is able to handle satisfiability tests with assumptions please consider implementing the {@link * InterpolatingProverEnvironment} interface, and return an Object of this type here. * * @param options Options specified for the prover environment. All the options specified in diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 76523447d1..777bc8f2c6 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -19,6 +19,7 @@ import com.google.common.collect.Multimap; import com.google.errorprone.annotations.CanIgnoreReturnValue; import java.util.ArrayList; +import java.util.Collection; import java.util.LinkedHashSet; import java.util.List; import java.util.Map; @@ -227,6 +228,28 @@ protected ImmutableSet getAssertedFormulas() { return builder.build(); } + /** + * @param nativeFormulasOfA a group of formulas that has been asserted and is to be interpolated + * against. + * @return The de-duplicated collection of the 2 interpolation groups currently asserted as {@link + * BooleanFormula}s. + */ + protected InterpolationGroups getInterpolationGroups(Collection nativeFormulasOfA) { + ImmutableSet.Builder formulasOfA = ImmutableSet.builder(); + ImmutableSet.Builder formulasOfB = ImmutableSet.builder(); + for (Multimap assertedFormulasPerLevel : assertedFormulas) { + for (Entry assertedFormulaAndItpPoint : + assertedFormulasPerLevel.entries()) { + if (nativeFormulasOfA.contains(assertedFormulaAndItpPoint.getValue())) { + formulasOfA.add(assertedFormulaAndItpPoint.getKey()); + } else { + formulasOfB.add(assertedFormulaAndItpPoint.getKey()); + } + } + } + return InterpolationGroups.of(formulasOfA.build(), formulasOfB.build()); + } + protected ImmutableSet getAssertedConstraintIds() { ImmutableSet.Builder builder = ImmutableSet.builder(); for (Multimap level : assertedFormulas) { @@ -276,4 +299,31 @@ public void close() { closeAllEvaluators(); closed = true; } + + /** Provides the set of BooleanFormulas to interpolate on. */ + public static final class InterpolationGroups { + private final Collection formulasOfA; + private final Collection formulasOfB; + + private InterpolationGroups( + Collection pFormulasOfA, Collection pFormulasOfB) { + Preconditions.checkNotNull(pFormulasOfA); + Preconditions.checkNotNull(pFormulasOfB); + formulasOfA = pFormulasOfA; + formulasOfB = pFormulasOfB; + } + + public static InterpolationGroups of( + Collection pFormulasOfA, Collection pFormulasOfB) { + return new InterpolationGroups(pFormulasOfA, pFormulasOfB); + } + + public Collection getFormulasOfA() { + return formulasOfA; + } + + public Collection getFormulasOfB() { + return formulasOfB; + } + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java index f071b00d29..ae367bce61 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java @@ -8,12 +8,16 @@ package org.sosy_lab.java_smt.basicimpl; +import com.google.common.base.Joiner; import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableSet; +import java.util.ArrayList; import java.util.Collections; import java.util.EnumSet; import java.util.List; import java.util.Set; import java.util.function.Consumer; +import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; import org.sosy_lab.java_smt.api.OptimizationProverEnvironment; @@ -54,7 +58,7 @@ public final ProverEnvironment newProverEnvironment(ProverOptions... options) { public final InterpolatingProverEnvironment newProverEnvironmentWithInterpolation( ProverOptions... options) { - InterpolatingProverEnvironment out = newProverEnvironmentWithInterpolation0(toSet(options)); + InterpolatingProverEnvironment out = newProverEnvironmentWithInterpolation1(toSet(options)); if (!supportsAssumptionSolving()) { // In the case we do not already have a prover environment with assumptions, // we add a wrapper to it @@ -63,6 +67,32 @@ public final InterpolatingProverEnvironment newProverEnvironmentWithInterpola return out; } + @SuppressWarnings({"ResultOfMethodCallIgnored", "resource"}) + private InterpolatingProverEnvironment newProverEnvironmentWithInterpolation1( + Set options) { + InterpolatingProverEnvironment out; + // Try to get a new prover environment w native interpolation with the current options + try { + out = newProverEnvironmentWithInterpolation0(options); + } catch (UnsupportedOperationException e) { + // Check if QuantifiedFormulaManager is available before attempting independent interpolation + try { + getFormulaManager().getQuantifiedFormulaManager(); + } catch (UnsupportedOperationException error) { + e.addSuppressed(error); + throw e; + } + // If native interpolation is not available, we wrap a normal prover such that it returns + // interpolation points + ProverEnvironment normalProver = newProverEnvironment0(options); + // TODO: only allow this if there is a quantified formula manager available! + out = new InterpolatingSolverDelegate(normalProver, options); + } + + // TODO: do we need the assumptions inside of the interpolation delegate? + return new IndependentInterpolatingSolverDelegate<>(this, out, options); + } + protected abstract InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( Set pSet); @@ -93,6 +123,42 @@ protected abstract OptimizationProverEnvironment newOptimizationProverEnvironmen */ protected abstract boolean supportsAssumptionSolving(); + private static final Set ALL_INDEPENDENT_INTERPOLATION_STRATEGIES = + ImmutableSet.of( + ProverOptions.GENERATE_PROJECTION_BASED_INTERPOLANTS, + ProverOptions.GENERATE_UNIFORM_BACKWARD_INTERPOLANTS, + ProverOptions.GENERATE_UNIFORM_FORWARD_INTERPOLANTS); + + protected boolean useNativeInterpolation(Set options) { + return getIndependentInterpolationStrategy(options) == null; + } + + @SuppressWarnings("CheckReturnValue") + protected @Nullable ProverOptions getIndependentInterpolationStrategy( + Set options) { + List itpStrat = new ArrayList<>(options); + itpStrat.retainAll(ALL_INDEPENDENT_INTERPOLATION_STRATEGIES); + + if (itpStrat.isEmpty()) { + return null; + } else if (itpStrat.size() != 1) { + throw new IllegalArgumentException( + "Only a single independent interpolation strategy can be" + + " chosen for a prover, but chosen were: " + + Joiner.on(", ").join(options)); + } + + ProverOptions interpolationOption = itpStrat.get(0); + try { + fmgr.getQuantifiedFormulaManager(); + } catch (UnsupportedOperationException e) { + throw new UnsupportedOperationException( + "Solver does not support independent interpolation based on the current strategy, as" + + " it is lacking quantifier support."); + } + return interpolationOption; + } + private static Set toSet(ProverOptions... options) { Set opts = EnumSet.noneOf(ProverOptions.class); Collections.addAll(opts, options); diff --git a/src/org/sosy_lab/java_smt/basicimpl/IndependentInterpolatingSolverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/IndependentInterpolatingSolverDelegate.java new file mode 100644 index 0000000000..efcf364f36 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/IndependentInterpolatingSolverDelegate.java @@ -0,0 +1,274 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkState; + +import com.google.common.base.Preconditions; +import com.google.common.collect.Sets; +import java.util.Collection; +import java.util.List; +import java.util.Optional; +import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.common.UniqueIdGenerator; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.basicimpl.interpolation_techniques.AbstractInterpolationTechnique; +import org.sosy_lab.java_smt.basicimpl.interpolation_techniques.ModelBasedProjectionInterpolation; +import org.sosy_lab.java_smt.basicimpl.interpolation_techniques.QuantifierEliminationInterpolation; + +public class IndependentInterpolatingSolverDelegate extends AbstractProver + implements InterpolatingProverEnvironment { + + private final SolverContext solverContext; + + private final InterpolatingProverEnvironment delegate; + + private final @Nullable AbstractInterpolationTechnique interpolationTechnique; + + private final @Nullable ProverOptions interpolationStrategy; + + private final FormulaManager mgr; + private final BooleanFormulaManager bmgr; + + private static final String PREFIX = "javasmt_itp_term_"; // for term-names + private static final UniqueIdGenerator termIdGenerator = + new UniqueIdGenerator(); // for different term-names + + protected IndependentInterpolatingSolverDelegate( + AbstractSolverContext pSourceContext, + InterpolatingProverEnvironment pDelegate, + Set pOptions) { + super(checkNotNull(pOptions)); + solverContext = checkNotNull(pSourceContext); + delegate = checkNotNull(pDelegate); + interpolationStrategy = pSourceContext.getIndependentInterpolationStrategy(pOptions); + mgr = pSourceContext.getFormulaManager(); + bmgr = mgr.getBooleanFormulaManager(); + + if (interpolationStrategy == null) { + this.interpolationTechnique = null; + } else { + switch (interpolationStrategy) { + case GENERATE_PROJECTION_BASED_INTERPOLANTS: + this.interpolationTechnique = new ModelBasedProjectionInterpolation(solverContext); + break; + case GENERATE_UNIFORM_FORWARD_INTERPOLANTS: + case GENERATE_UNIFORM_BACKWARD_INTERPOLANTS: + this.interpolationTechnique = + new QuantifierEliminationInterpolation(mgr, interpolationStrategy); + break; + default: + throw new AssertionError("Unknown interpolation strategy: " + interpolationStrategy); + } + } + } + + // TODO: also present in SMTInterpol, generalize + protected static String generateTermName() { + return PREFIX + termIdGenerator.getFreshId(); + } + + @Override + public BooleanFormula getInterpolant(Collection identifiersForA) + throws SolverException, InterruptedException { + Preconditions.checkState(!closed); + checkArgument( + getAssertedConstraintIds().containsAll(identifiersForA), + "Interpolation can only be performed over previously asserted formulas."); + + if (identifiersForA.isEmpty()) { + return bmgr.makeTrue(); + } + + InterpolationGroups interpolationGroups = super.getInterpolationGroups(identifiersForA); + Collection formulasOfA = interpolationGroups.getFormulasOfA(); + Collection formulasOfB = interpolationGroups.getFormulasOfB(); + + if (formulasOfB.isEmpty()) { + return bmgr.makeFalse(); + } + + BooleanFormula conjugatedFormulasOfA = bmgr.and(formulasOfA); + BooleanFormula conjugatedFormulasOfB = bmgr.and(formulasOfB); + + if (bmgr.isFalse(conjugatedFormulasOfA)) { + return bmgr.makeFalse(); + } else if (bmgr.isFalse(conjugatedFormulasOfB)) { + return bmgr.makeTrue(); + } + + BooleanFormula interpolant; + + if (interpolationTechnique == null) { + interpolant = delegate.getInterpolant(identifiersForA); + } else { + interpolant = + interpolationTechnique.getInterpolant(conjugatedFormulasOfA, conjugatedFormulasOfB); + } + + assert satisfiesInterpolationCriteria( + interpolant, conjugatedFormulasOfA, conjugatedFormulasOfB); + + return interpolant; + } + + @Override + public List getTreeInterpolants( + List> partitionedFormulas, int[] startOfSubTree) + throws SolverException, InterruptedException { + if (interpolationStrategy == null) { + // Use native solver interpolation + return delegate.getTreeInterpolants(partitionedFormulas, startOfSubTree); + } + throw new UnsupportedOperationException( + "Tree interpolants are not supported for independent interpolation currently."); + } + + @Override + public List getSeqInterpolants(List> pPartitionedFormulas) + throws SolverException, InterruptedException { + if (interpolationStrategy == null) { + // Use native solver interpolation + return delegate.getSeqInterpolants(pPartitionedFormulas); + } + throw new UnsupportedOperationException( + "Sequential interpolants are not supported for independent interpolation currently."); + } + + /** + * Checks the following 3 criteria for Craig interpolants: + * + *

1. the implication A ⇒ interpolant holds, + * + *

2. the conjunction interpolant ∧ B is unsatisfiable, and + * + *

3. interpolant only contains symbols that occur in both A and B. + */ + private boolean satisfiesInterpolationCriteria( + BooleanFormula interpolant, + BooleanFormula conjugatedFormulasOfA, + BooleanFormula conjugatedFormulasOfB) + throws InterruptedException, SolverException { + + // checks that every Symbol of the interpolant appears either in A or B + Set interpolantSymbols = mgr.extractVariablesAndUFs(interpolant).keySet(); + Set interpolASymbols = mgr.extractVariablesAndUFs(conjugatedFormulasOfA).keySet(); + Set interpolBSymbols = mgr.extractVariablesAndUFs(conjugatedFormulasOfB).keySet(); + Set intersection = Sets.intersection(interpolASymbols, interpolBSymbols); + checkState( + intersection.containsAll(interpolantSymbols), + "Interpolant contains symbols %s that are not part of both input formula groups A and B.", + Sets.difference(interpolantSymbols, intersection)); + + try (ProverEnvironment validationSolver = getDistinctProver()) { + validationSolver.push(); + // A -> interpolant is SAT + validationSolver.addConstraint(bmgr.implication(conjugatedFormulasOfA, interpolant)); + checkState( + !validationSolver.isUnsat(), + "Invalid Craig interpolation: formula group A does not imply the interpolant."); + validationSolver.pop(); + + validationSolver.push(); + // interpolant AND B is UNSAT + validationSolver.addConstraint(bmgr.and(interpolant, conjugatedFormulasOfB)); + checkState( + validationSolver.isUnsat(), + "Invalid Craig interpolation: interpolant does not contradict formula group B."); + validationSolver.pop(); + } + return true; + } + + /** + * Create a new, distinct prover to interpolate on. Will be able to generate models. + * + * @return A new {@link ProverEnvironment} configured to generate models. + */ + private ProverEnvironment getDistinctProver() { + // TODO: we should include the possibility to choose from options here. E.g. CHC/Horn solvers. + return solverContext.newProverEnvironment(ProverOptions.GENERATE_MODELS); + } + + @Override + protected void popImpl() { + delegate.pop(); + } + + @Override + protected T addConstraintImpl(BooleanFormula constraint) throws InterruptedException { + return delegate.addConstraint(constraint); + } + + @Override + protected void pushImpl() throws InterruptedException { + delegate.push(); + } + + @Override + public int size() { + return delegate.size(); + } + + @Override + public boolean isUnsatImpl() throws SolverException, InterruptedException { + return delegate.isUnsat(); + } + + @Override + public boolean hasPersistentModel() { + return false; + } + + @Override + public boolean isUnsatWithAssumptions(Collection assumptions) + throws SolverException, InterruptedException { + return delegate.isUnsatWithAssumptions(assumptions); + } + + @Override + public Model getModel() throws SolverException { + return delegate.getModel(); + } + + @Override + public List getUnsatCore() { + return delegate.getUnsatCore(); + } + + @Override + public Optional> unsatCoreOverAssumptions( + Collection assumptions) throws SolverException, InterruptedException { + return delegate.unsatCoreOverAssumptions(assumptions); + } + + @Override + public void close() { + delegate.close(); + } + + @Override + public R allSat(AllSatCallback callback, List important) + throws InterruptedException, SolverException { + return delegate.allSat(callback, important); + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/InterpolatingSolverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingSolverDelegate.java new file mode 100644 index 0000000000..00e05a6866 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingSolverDelegate.java @@ -0,0 +1,121 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl; + +import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkState; +import static org.sosy_lab.java_smt.basicimpl.IndependentInterpolatingSolverDelegate.generateTermName; + +import java.util.Collection; +import java.util.List; +import java.util.Optional; +import java.util.Set; +import org.sosy_lab.java_smt.api.BasicProverEnvironment; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.SolverException; + +/** Delegate that wraps non-interpolating provers, allowing them to return itp tracking points. */ +public class InterpolatingSolverDelegate extends AbstractProver + implements InterpolatingProverEnvironment { + + private final BasicProverEnvironment delegate; + + protected InterpolatingSolverDelegate( + BasicProverEnvironment pDelegate, Set pOptions) { + super(checkNotNull(pOptions)); + // TODO: is the delegate also saving all info of AbstractProver additionally, or does VOID + // prevent that? + delegate = checkNotNull(pDelegate); + } + + @Override + public BooleanFormula getInterpolant(Collection formulasOfA) + throws SolverException, InterruptedException { + throw new UnsupportedOperationException("Solver does not support native interpolation."); + } + + @Override + public List getTreeInterpolants( + List> partitionedFormulas, int[] startOfSubTree) + throws SolverException, InterruptedException { + throw new UnsupportedOperationException( + "Tree interpolants are currently not supported using " + "independent interpolation"); + } + + @Override + protected void popImpl() { + delegate.pop(); + } + + @Override + protected String addConstraintImpl(BooleanFormula constraint) throws InterruptedException { + checkState(!closed); + delegate.addConstraint(constraint); + String termName = generateTermName(); + return termName; + } + + @Override + protected void pushImpl() throws InterruptedException { + delegate.push(); + } + + @Override + protected boolean hasPersistentModel() { + return false; + } + + @Override + public int size() { + return delegate.size(); + } + + @Override + public boolean isUnsatImpl() throws SolverException, InterruptedException { + return delegate.isUnsat(); + } + + @Override + public boolean isUnsatWithAssumptions(Collection assumptions) + throws SolverException, InterruptedException { + return delegate.isUnsatWithAssumptions(assumptions); + } + + @Override + public Model getModel() throws SolverException { + return delegate.getModel(); + } + + @Override + public List getUnsatCore() { + return delegate.getUnsatCore(); + } + + @Override + public Optional> unsatCoreOverAssumptions( + Collection assumptions) throws SolverException, InterruptedException { + return delegate.unsatCoreOverAssumptions(assumptions); + } + + @Override + public void close() { + delegate.close(); + } + + @Override + public R allSat(AllSatCallback callback, List important) + throws InterruptedException, SolverException { + return delegate.allSat(callback, important); + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java b/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java index d4db7d9956..bc2a40b2eb 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java +++ b/src/org/sosy_lab/java_smt/basicimpl/PackageSanityTest.java @@ -11,6 +11,9 @@ import com.google.common.testing.AbstractPackageSanityTests; import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.ShutdownNotifier; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.java_smt.SolverContextFactory; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.FormulaType; public class PackageSanityTest extends AbstractPackageSanityTests { @@ -18,5 +21,13 @@ public class PackageSanityTest extends AbstractPackageSanityTests { { setDistinctValues(FormulaType.class, FormulaType.BooleanType, FormulaType.IntegerType); setDefault(ShutdownNotifier.class, ShutdownManager.create().getNotifier()); + try { + // Use Princess as it is always available + setDefault( + AbstractSolverContext.class, + (AbstractSolverContext) SolverContextFactory.createSolverContext(Solvers.PRINCESS)); + } catch (InvalidConfigurationException e) { + throw new RuntimeException(e); + } } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/interpolation_techniques/AbstractInterpolationTechnique.java b/src/org/sosy_lab/java_smt/basicimpl/interpolation_techniques/AbstractInterpolationTechnique.java new file mode 100644 index 0000000000..ad8a9a2830 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/interpolation_techniques/AbstractInterpolationTechnique.java @@ -0,0 +1,57 @@ +/* + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl.interpolation_techniques; + +import com.google.common.collect.ImmutableList; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Set; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.SolverException; + +public abstract class AbstractInterpolationTechnique { + + protected final FormulaManager mgr; + protected final BooleanFormulaManager bmgr; + + protected AbstractInterpolationTechnique(FormulaManager pMgr) { + mgr = pMgr; + bmgr = mgr.getBooleanFormulaManager(); + } + + public abstract BooleanFormula getInterpolant( + BooleanFormula formulasOfA, BooleanFormula formulasOfB) + throws SolverException, InterruptedException; + + /** Extracts all variables (not UFs) from the given formula. */ + protected List getAllVariables(BooleanFormula formula) { + return mgr.extractVariables(formula).values().asList(); + } + + /** Returns common Formulas of the 2 given lists. */ + protected List getCommonFormulas( + List variables1, List variables2) { + Set set = new LinkedHashSet<>(variables1); + set.retainAll(variables2); + return ImmutableList.copyOf(set); + } + + /** Removes variablesToRemove from variablesToRemoveFrom. */ + protected List removeVariablesFrom( + List variablesToRemoveFrom, List variablesToRemove) { + ImmutableList.Builder builder = ImmutableList.builder(); + for (Formula var : variablesToRemoveFrom) { + if (!variablesToRemove.contains(var)) { + builder.add(var); + } + } + return builder.build(); + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/interpolation_techniques/ModelBasedProjectionInterpolation.java b/src/org/sosy_lab/java_smt/basicimpl/interpolation_techniques/ModelBasedProjectionInterpolation.java new file mode 100644 index 0000000000..1f6a93aff5 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/interpolation_techniques/ModelBasedProjectionInterpolation.java @@ -0,0 +1,83 @@ +/* + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl.interpolation_techniques; + +import static com.google.common.base.Preconditions.checkNotNull; + +import java.util.List; +import org.sosy_lab.common.UniqueIdGenerator; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.UFManager; + +public class ModelBasedProjectionInterpolation extends AbstractInterpolationTechnique { + + private final SolverContext solverContext; + private final UFManager ufmgr; + private final QuantifiedFormulaManager qfmgr; + + private static final UniqueIdGenerator termIdGenerator = new UniqueIdGenerator(); + + @Override + public BooleanFormula getInterpolant(BooleanFormula formulasOfA, BooleanFormula formulasOfB) + throws SolverException, InterruptedException { + + List variablesInA = getAllVariables(formulasOfA); + List variablesInB = getAllVariables(formulasOfB); + List sharedVars = getCommonFormulas(variablesInA, variablesInB); + + BooleanFormula itp = + ufmgr.declareAndCallUF( + "__itp_internal_javasmt_" + termIdGenerator.getFreshId(), + FormulaType.BooleanType, + sharedVars); + + BooleanFormula left; + BooleanFormula right; + + if (variablesInA.isEmpty()) { + left = bmgr.implication(formulasOfA, itp); + } else { + left = qfmgr.forall(variablesInA, bmgr.implication(formulasOfA, itp)); + } + + if (variablesInB.isEmpty()) { + right = bmgr.implication(itp, bmgr.not(formulasOfB)); + } else { + right = qfmgr.forall(variablesInB, bmgr.implication(itp, bmgr.not(formulasOfB))); + } + + BooleanFormula interpolant = bmgr.makeFalse(); + try (ProverEnvironment itpProver = + solverContext.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + itpProver.push(left); + itpProver.push(right); + + if (!itpProver.isUnsat()) { + try (Model model = itpProver.getModel()) { + interpolant = model.eval(itp); + } + checkNotNull(interpolant); + } + } + return mgr.simplify(interpolant); + } + + public ModelBasedProjectionInterpolation(SolverContext pContext) { + super(pContext.getFormulaManager()); + solverContext = pContext; + ufmgr = mgr.getUFManager(); + qfmgr = mgr.getQuantifiedFormulaManager(); + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/interpolation_techniques/QuantifierEliminationInterpolation.java b/src/org/sosy_lab/java_smt/basicimpl/interpolation_techniques/QuantifierEliminationInterpolation.java new file mode 100644 index 0000000000..541bc110e9 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/interpolation_techniques/QuantifierEliminationInterpolation.java @@ -0,0 +1,100 @@ +/* + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl.interpolation_techniques; + +import java.util.List; +import java.util.concurrent.atomic.AtomicBoolean; +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.QuantifiedFormulaManager; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; +import org.sosy_lab.java_smt.api.visitors.TraversalProcess; + +public class QuantifierEliminationInterpolation extends AbstractInterpolationTechnique { + + private final ProverOptions strategy; + private final QuantifiedFormulaManager qfmgr; + + public QuantifierEliminationInterpolation(FormulaManager pMgr, ProverOptions pStrategy) { + super(pMgr); + strategy = pStrategy; + qfmgr = mgr.getQuantifiedFormulaManager(); + } + + @Override + public BooleanFormula getInterpolant(BooleanFormula formulasOfA, BooleanFormula formulasOfB) + throws SolverException, InterruptedException { + + List variablesInA = getAllVariables(formulasOfA); + List variablesInB = getAllVariables(formulasOfB); + List sharedVariables = getCommonFormulas(variablesInA, variablesInB); + + BooleanFormula interpolant; + + if (strategy == ProverOptions.GENERATE_UNIFORM_FORWARD_INTERPOLANTS) { + // Forward: interpolate(A(x,y),B(y,z)) = ∃x.A(x,y) + List exclusiveVariablesInA = removeVariablesFrom(variablesInA, sharedVariables); + + if (exclusiveVariablesInA.isEmpty()) { + return formulasOfA; + } + + BooleanFormula itpForwardQuantified = qfmgr.exists(exclusiveVariablesInA, formulasOfA); + interpolant = qfmgr.eliminateQuantifiers(itpForwardQuantified); + + } else if (strategy == ProverOptions.GENERATE_UNIFORM_BACKWARD_INTERPOLANTS) { + // Backward: interpolate(A(x,y),B(y,z))=∀z.¬B(y,z) + List exclusiveVariablesInB = removeVariablesFrom(variablesInB, sharedVariables); + + if (exclusiveVariablesInB.isEmpty()) { + return bmgr.not(formulasOfB); + } + + BooleanFormula itpBackwardQuantified = + qfmgr.forall(exclusiveVariablesInB, bmgr.not(formulasOfB)); + interpolant = qfmgr.eliminateQuantifiers(itpBackwardQuantified); + + } else { + throw new AssertionError("Unknown interpolation strategy for QE: " + strategy); + } + + if (isQuantifiedFormula(interpolant)) { + throw new SolverException( + "Error when calculating uniform interpolant, quantifier elimination failed."); + } + + return mgr.simplify(interpolant); + } + + /** Checks the formula for a quantifier at an arbitrary position/depth. */ + private boolean isQuantifiedFormula(BooleanFormula maybeQuantifiedFormula) { + final AtomicBoolean isQuantified = new AtomicBoolean(false); + mgr.visitRecursively( + maybeQuantifiedFormula, + new DefaultFormulaVisitor<>() { + @Override + protected TraversalProcess visitDefault(Formula pF) { + return TraversalProcess.CONTINUE; + } + + @Override + public TraversalProcess visitQuantifier( + BooleanFormula pF, + Quantifier pQ, + List pBoundVariables, + BooleanFormula pBody) { + isQuantified.set(true); + return TraversalProcess.ABORT; + } + }); + return isQuantified.get(); + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/interpolation_techniques/package-info.java b/src/org/sosy_lab/java_smt/basicimpl/interpolation_techniques/package-info.java new file mode 100644 index 0000000000..4392fe8265 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/interpolation_techniques/package-info.java @@ -0,0 +1,11 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl.interpolation_techniques; diff --git a/src/org/sosy_lab/java_smt/example/IndependentInterpolation.java b/src/org/sosy_lab/java_smt/example/IndependentInterpolation.java new file mode 100644 index 0000000000..4ecc0c0ecb --- /dev/null +++ b/src/org/sosy_lab/java_smt/example/IndependentInterpolation.java @@ -0,0 +1,169 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.example; + +import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableList; +import java.util.logging.Level; +import org.sosy_lab.common.ShutdownNotifier; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.log.BasicLogManager; +import org.sosy_lab.common.log.LogManager; +import org.sosy_lab.java_smt.SolverContextFactory; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.IntegerFormulaManager; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.SolverException; + +public final class IndependentInterpolation { + + private IndependentInterpolation() { + // never called + } + + private static final ProverOptions STRATEGY = + ProverOptions.GENERATE_UNIFORM_BACKWARD_INTERPOLANTS; + + public static void main(String[] args) + throws InvalidConfigurationException, SolverException, InterruptedException { + + // set up a basic environment + Configuration config = Configuration.defaultConfiguration(); + LogManager logger = BasicLogManager.create(config); + ShutdownNotifier notifier = ShutdownNotifier.createDummy(); + + // choose solver + Solvers solver = Solvers.Z3; + + // setup context + try (SolverContext context = + SolverContextFactory.createSolverContext(config, logger, notifier, solver); + InterpolatingProverEnvironment prover = + context.newProverEnvironmentWithInterpolation(STRATEGY)) { + logger.log(Level.WARNING, "Using solver " + solver + " in version " + context.getVersion()); + logger.log(Level.INFO, "Interpolation strategy: " + STRATEGY); + + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager(); + + // example + prover.push(); + interpolateExample(prover, bmgr, imgr, logger); + prover.pop(); + + // another example + prover.push(); + interpolateExample2(prover, bmgr, imgr, logger); + prover.pop(); + + } catch (InvalidConfigurationException | UnsatisfiedLinkError e) { + + // on some machines we support only some solvers, + // thus we can ignore these errors. + logger.logUserException(Level.INFO, e, "Solver " + solver + " is not available."); + + } catch (UnsupportedOperationException e) { + logger.logUserException(Level.INFO, e, e.getMessage()); + } + } + + private static void interpolateExample( + InterpolatingProverEnvironment prover, + BooleanFormulaManager bmgr, + IntegerFormulaManager imgr, + LogManager logger) + throws InterruptedException, SolverException { + + // A: x = 1 && x = y + // B: y = z && z = 2 + // -> y = 1, y != 2 + + // create some variables + IntegerFormula x = imgr.makeVariable("x"); + IntegerFormula y = imgr.makeVariable("y"); + IntegerFormula z = imgr.makeVariable("z"); + IntegerFormula one = imgr.makeNumber(1); + IntegerFormula two = imgr.makeNumber(2); + + // create and assert some formulas + // instead of 'named' formulas, we return a 'handle' (of generic type T) + + BooleanFormula formulaB = bmgr.and(imgr.equal(y, z), imgr.equal(z, two)); + BooleanFormula formulaA = bmgr.and(imgr.equal(x, one), imgr.equal(y, x)); + prover.addConstraint(formulaB); + T ip1 = prover.addConstraint(formulaA); + + // check for satisfiability + boolean unsat = prover.isUnsat(); + Preconditions.checkState(unsat, "The example for interpolation should be UNSAT"); + + BooleanFormula itp = prover.getInterpolant(ImmutableList.of(ip1)); + logger.logf( + Level.INFO, + "Interpolation Result:%n" + + " Strategy: %s%n" + + " Formula A: %s%n" + + " Formula B: %s%n" + + " Interpolant: %s", + STRATEGY, + formulaA.toString().length() > 500 ? "Too large to display" : formulaA, + formulaB.toString().length() > 500 ? "Too large to display" : formulaB, + itp); + } + + private static void interpolateExample2( + InterpolatingProverEnvironment prover, + BooleanFormulaManager bmgr, + IntegerFormulaManager imgr, + LogManager logger) + throws InterruptedException, SolverException { + + // A: x > 0 && y = x + 1 + // B: y < 0 + // -> y > 0 + + // create some variables + IntegerFormula x = imgr.makeVariable("x"); + IntegerFormula y = imgr.makeVariable("y"); + IntegerFormula one = imgr.makeNumber(1); + IntegerFormula zero = imgr.makeNumber(0); + + BooleanFormula formulaB = imgr.lessThan(y, zero); + BooleanFormula formulaA = bmgr.and(imgr.greaterThan(x, zero), imgr.equal(y, imgr.add(x, one))); + + prover.addConstraint(formulaB); + T ip1 = prover.addConstraint(formulaA); + + // check for satisfiability + boolean unsat = prover.isUnsat(); + Preconditions.checkState(unsat, "The example for interpolation should be UNSAT"); + + BooleanFormula itp = prover.getInterpolant(ImmutableList.of(ip1)); + logger.log(Level.INFO, "Interpolants are:", itp); + logger.logf( + Level.INFO, + "Interpolation Result:%n" + + " Strategy: %s%n" + + " Formula A: %s%n" + + " Formula B: %s%n" + + " Interpolant: %s", + STRATEGY, + formulaA.toString().length() > 500 ? "Too large to display" : formulaA, + formulaB.toString().length() > 500 ? "Too large to display" : formulaB, + itp); + } +} diff --git a/src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java b/src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java index a9dc67113e..11eff19f8b 100644 --- a/src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java +++ b/src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java @@ -9,10 +9,12 @@ package org.sosy_lab.java_smt.test; import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkState; import static com.google.common.truth.Truth.assert_; import com.google.common.base.Joiner; import com.google.common.collect.FluentIterable; +import com.google.common.collect.Sets; import com.google.common.truth.Fact; import com.google.common.truth.FailureMetadata; import com.google.common.truth.SimpleSubjectBuilder; @@ -21,8 +23,10 @@ import com.google.common.truth.Truth; import java.util.ArrayList; import java.util.List; +import java.util.Set; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.ProverEnvironment; @@ -59,6 +63,14 @@ public static Subject.Factory booleanForm return (metadata, formula) -> new BooleanFormulaSubject(metadata, formula, context); } + /** + * Use this for checking assertions about BooleanFormulas with Truth: + * assertThatFormula(formula).is...(). + */ + public static BooleanFormulaSubject assertThat(BooleanFormula formula, SolverContext context) { + return assert_().about(booleanFormulasOf(context)).that(formula); + } + /** * Use this for checking assertions about BooleanFormulas (given the corresponding solver) with * Truth: assertUsing(context)).that(formula).is...(). @@ -255,4 +267,51 @@ public void implies(final BooleanFormula expected) throws SolverException, Inter checkIsUnsat(bmgr.not(implication), Fact.fact("expected to imply", expected)); } + + /** + * Checks if the subject is a valid Craig interpolant for the given formulas A and B. + * + *

Checks 3 properties: + * + *

    + *
  1. I is a subset of A\B + *
  2. A implies I + *
  3. I and B are mutually contradictory + *
+ */ + public void isValidInterpolant(BooleanFormula formulaA, BooleanFormula formulaB) + throws SolverException, InterruptedException { + isValidInterpolant(List.of(formulaA), List.of(formulaB)); + } + + /** Checks if the subject is a valid Craig interpolant for the lists of formulas A and B. */ + public void isValidInterpolant(List formulasA, List formulasB) + throws SolverException, InterruptedException { + + BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); + BooleanFormula conjugatedFormulasOfA = bmgr.and(formulasA); + BooleanFormula conjugatedFormulasOfB = bmgr.and(formulasB); + + // checks that every Symbol of the interpolant appears either in A or B + FormulaManager mgr = context.getFormulaManager(); + Set interpolantSymbols = mgr.extractVariablesAndUFs(formulaUnderTest).keySet(); + Set interpolASymbols = mgr.extractVariablesAndUFs(conjugatedFormulasOfA).keySet(); + Set interpolBSymbols = mgr.extractVariablesAndUFs(conjugatedFormulasOfB).keySet(); + Set intersection = Sets.intersection(interpolASymbols, interpolBSymbols); + + checkState( + intersection.containsAll(interpolantSymbols), + "Interpolant contains symbols %s that are not part of both input formula groups A and B.", + Sets.difference(interpolantSymbols, intersection)); + + checkIsUnsat( + bmgr.and(conjugatedFormulasOfA, bmgr.not(formulaUnderTest)), + Fact.simpleFact("Interpolant expected to be implied by A (A => I)"), + ProverOptions.GENERATE_MODELS); + + checkIsUnsat( + bmgr.and(formulaUnderTest, conjugatedFormulasOfB), + Fact.simpleFact("Interpolant expected to contradict B (I /\\ B => UNSAT)"), + ProverOptions.GENERATE_MODELS); + } } diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java index 1937ef3538..90da173ccd 100644 --- a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java +++ b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java @@ -28,13 +28,15 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.solvers.cvc5.CVC5BooleanFormulaManager; import org.sosy_lab.java_smt.solvers.opensmt.Logics; /** This class contains some simple Junit-tests to check the interpolation-API of our solvers. */ @SuppressWarnings({"resource", "LocalVariableName"}) -public class InterpolatingProverTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { +public class InterpolatingProverTest + extends SolverBasedTest0.ParameterizedInterpolatingSolverBasedTest0 { // INFO: OpenSmt only support interpolation for QF_LIA, QF_LRA and QF_UF @Override @@ -45,8 +47,14 @@ protected Logics logicToUse() { /** Generate a prover environment depending on the parameter above. */ @SuppressWarnings("unchecked") private InterpolatingProverEnvironment newEnvironmentForTest() { - requireInterpolation(); - return (InterpolatingProverEnvironment) context.newProverEnvironmentWithInterpolation(); + requireInterpolation(itpStrategyToUse()); + ProverOptions itpStrat = itpStrategyToUse(); + if (itpStrat == null) { + return (InterpolatingProverEnvironment) context.newProverEnvironmentWithInterpolation(); + } else { + return (InterpolatingProverEnvironment) + context.newProverEnvironmentWithInterpolation(itpStrat); + } } private static final UniqueIdGenerator index = new UniqueIdGenerator(); // to get different names @@ -54,10 +62,11 @@ private InterpolatingProverEnvironment newEnvironmentForTest() { @Test @SuppressWarnings("CheckReturnValue") public void simpleInterpolation() throws SolverException, InterruptedException { + requireIntegers(); assume() .withMessage("Solver %s runs into timeout on this test", solverToUse()) .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); + .isNotIn(ImmutableList.of(Solvers.CVC5, Solvers.Z3)); try (InterpolatingProverEnvironment prover = newEnvironmentForTest()) { IntegerFormula x = imgr.makeVariable("x"); @@ -88,6 +97,7 @@ public void simpleInterpolation() throws SolverException, InterruptedExcepti @SuppressWarnings("unchecked") public void emptyInterpolationGroup() throws SolverException, InterruptedException { try (InterpolatingProverEnvironment prover = newEnvironmentForTest()) { + requireIntegers(); IntegerFormula x = imgr.makeVariable("x"); IntegerFormula y = imgr.makeVariable("y"); /* INFO: Due to limitations in OpenSMT we need to use a simpler formula for this solver @@ -114,6 +124,8 @@ public void emptyInterpolationGroup() throws SolverException, InterruptedExc @Test public void binaryInterpolation() throws SolverException, InterruptedException { + requireBitvectors(); + requireIntegers(); InterpolatingProverEnvironment stack = newEnvironmentForTest(); int i = index.getFreshId(); @@ -243,6 +255,17 @@ public void illegalStateTest() throws InterruptedException, SolverException @Test public void binaryBVInterpolation1() throws SolverException, InterruptedException { + assume() + .withMessage("Solver %s is not supported or times out", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.BITWUZLA); + + assume() + .withMessage("Z3 with strategy %s is not supported or times out", itpStrategyToUse()) + .that( + solverToUse() == Solvers.Z3 + && itpStrategyToUse() == ProverOptions.GENERATE_PROJECTION_BASED_INTERPOLANTS) + .isFalse(); requireBitvectors(); InterpolatingProverEnvironment stack = newEnvironmentForTest(); @@ -290,16 +313,9 @@ public void binaryBVInterpolation1() throws SolverException, InterruptedExce checkItpSequence(ImmutableList.of(D, C, B, A), ImmutableList.of(itpD, itpDC, itpDCB)); } - private void requireTreeItp() { - requireInterpolation(); - assume() - .withMessage("Solver does not support tree-interpolation.") - .that(solver) - .isAnyOf(Solvers.SMTINTERPOL, Solvers.PRINCESS, Solvers.Z3_WITH_INTERPOLATION); - } - @Test public void sequentialInterpolation() throws SolverException, InterruptedException { + requireSeqItp(); InterpolatingProverEnvironment stack = newEnvironmentForTest(); requireIntegers(); @@ -352,6 +368,7 @@ public void sequentialInterpolation() throws SolverException, InterruptedExc public void sequentialInterpolationIsNotRepeatedIndividualInterpolation() throws SolverException, InterruptedException { InterpolatingProverEnvironment stack = newEnvironmentForTest(); + requireSeqItp(); requireIntegers(); IntegerFormula zero = imgr.makeNumber(0); @@ -387,6 +404,7 @@ public void sequentialInterpolationIsNotRepeatedIndividualInterpolation() public void sequentialInterpolationWithoutPartition() throws SolverException, InterruptedException { requireIntegers(); + requireSeqItp(); InterpolatingProverEnvironment stack = newEnvironmentForTest(); stack.push(imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1))); @@ -401,6 +419,7 @@ public void sequentialInterpolationWithoutPartition() public void sequentialInterpolationWithOnePartition() throws SolverException, InterruptedException { requireIntegers(); + requireSeqItp(); InterpolatingProverEnvironment stack = newEnvironmentForTest(); int i = index.getFreshId(); @@ -429,6 +448,7 @@ public void sequentialInterpolationWithOnePartition() public void sequentialInterpolationWithFewPartitions() throws SolverException, InterruptedException { requireIntegers(); + requireSeqItp(); InterpolatingProverEnvironment stack = newEnvironmentForTest(); int i = index.getFreshId(); @@ -461,6 +481,8 @@ public void sequentialInterpolationWithFewPartitions() @Test public void sequentialBVInterpolation() throws SolverException, InterruptedException { requireBitvectors(); + requireSeqItp(); + requireTreeItp(); InterpolatingProverEnvironment stack = newEnvironmentForTest(); @@ -1015,7 +1037,6 @@ public void treeInterpolationWithoutPartition() throws SolverException, Inte @Test public void treeInterpolationWithOnePartition() throws SolverException, InterruptedException { requireTreeItp(); - InterpolatingProverEnvironment stack = newEnvironmentForTest(); int i = index.getFreshId(); @@ -1045,6 +1066,8 @@ public void treeInterpolationWithOnePartition() throws SolverException, Inte public void bigSeqInterpolationTest() throws InterruptedException, SolverException { requireBitvectors(); requireInterpolation(); + requireSeqItp(); + requireTreeItp(); assume() .withMessage("Solver %s runs into timeout on this test", solverToUse()) @@ -1114,7 +1137,7 @@ public void bigSeqInterpolationTest() throws InterruptedException, SolverExc @Test public void testTrivialInterpolation() throws InterruptedException, SolverException { - requireInterpolation(); + requireIntegers(); InterpolatingProverEnvironment stack = newEnvironmentForTest(); IntegerFormula zero = imgr.makeNumber(0); IntegerFormula one = imgr.makeNumber(1); @@ -1161,7 +1184,7 @@ private void checkItpSequence(List formulas, List void testInvalidToken() throws InterruptedException, SolverException { - requireInterpolation(); + requireIntegers(); InterpolatingProverEnvironment stack = newEnvironmentForTest(); // create and push formulas and solve them @@ -1195,6 +1218,12 @@ public void testInvalidToken() throws InterruptedException, SolverException case SMTINTERPOL: p3 = "some string"; break; + case Z3: + p3 = 12345; + break; + case CVC4: + p3 = 12345; + break; case Z3_WITH_INTERPOLATION: p3 = 12350; break; @@ -1214,6 +1243,8 @@ public void testInvalidToken() throws InterruptedException, SolverException */ @Test public void issue381InterpolationTest1() throws InterruptedException, SolverException { + requireIntegers(); + requireSeqItp(); try (InterpolatingProverEnvironment prover = newEnvironmentForTest()) { var x = imgr.makeVariable("x"); var one = imgr.makeNumber(1); @@ -1240,6 +1271,8 @@ public void issue381InterpolationTest1() throws InterruptedException, Solver */ @Test public void issue381InterpolationTest2() throws InterruptedException, SolverException { + requireIntegers(); + requireSeqItp(); try (InterpolatingProverEnvironment prover = newEnvironmentForTest()) { var x = imgr.makeVariable("x"); var one = imgr.makeNumber(1); @@ -1266,6 +1299,7 @@ public void issue381InterpolationTest2() throws InterruptedException, Solver */ @Test public void issue381InterpolationTest3() throws InterruptedException, SolverException { + requireIntegers(); try (InterpolatingProverEnvironment prover = newEnvironmentForTest()) { var x = imgr.makeVariable("x"); var one = imgr.makeNumber(1); diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index e28c6823c2..7cd2421f21 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -10,11 +10,20 @@ import static com.google.common.truth.TruthJUnit.assume; import static org.sosy_lab.java_smt.api.FormulaType.getSinglePrecisionFloatingPointType; +import static org.sosy_lab.java_smt.api.SolverContext.ProverOptions.GENERATE_PROJECTION_BASED_INTERPOLANTS; +import static org.sosy_lab.java_smt.api.SolverContext.ProverOptions.GENERATE_UNIFORM_BACKWARD_INTERPOLANTS; +import static org.sosy_lab.java_smt.api.SolverContext.ProverOptions.GENERATE_UNIFORM_FORWARD_INTERPOLANTS; import static org.sosy_lab.java_smt.test.BooleanFormulaSubject.assertUsing; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableSet; import com.google.common.truth.Truth; +import java.util.ArrayList; +import java.util.Arrays; import java.util.Collection; +import java.util.List; +import java.util.Set; import org.checkerframework.checker.nullness.qual.Nullable; import org.junit.After; import org.junit.Before; @@ -79,8 +88,8 @@ * * * - * {@link #assertThatFormula(BooleanFormula)} can be used to easily write assertions about formulas - * using Truth. + *

{@link #assertThatFormula(BooleanFormula)} can be used to easily write assertions about + * formulas using Truth. * *

Test that rely on a theory that not all solvers support should call one of the {@code require} * methods at the beginning. @@ -132,6 +141,12 @@ protected ConfigurationBuilder createTestConfigBuilder() { return newConfig; } + private static final ImmutableList INDEPENDENT_INTERPOLATION_STRATEGIES = + ImmutableList.of( + GENERATE_UNIFORM_BACKWARD_INTERPOLANTS, + GENERATE_PROJECTION_BASED_INTERPOLANTS, + GENERATE_UNIFORM_FORWARD_INTERPOLANTS); + @Before public final void initSolver() throws InvalidConfigurationException { config = createTestConfigBuilder().build(); @@ -349,17 +364,83 @@ protected final void requireOptimization() { } } - protected final void requireInterpolation() { + protected final void requireInterpolation(ProverOptions... options) { + List optionList = + (options == null) ? ImmutableList.of() : Arrays.asList(options); + if (optionList.contains(null) || optionList.isEmpty()) { + assume() + .withMessage("Solver %s does not support native interpolation", solverToUse()) + .that(solverToUse()) + .isAnyOf( + Solvers.SMTINTERPOL, + Solvers.PRINCESS, + Solvers.OPENSMT, + Solvers.MATHSAT5, + Solvers.BOOLECTOR, + Solvers.CVC5, + Solvers.BITWUZLA); + } else if (optionList.contains(GENERATE_PROJECTION_BASED_INTERPOLANTS)) { + assume() + .withMessage("Only Z3 is enabled for projection-based interpolation") + .that(solverToUse()) + .isEqualTo(Solvers.Z3); + } else if (optionList.contains(GENERATE_UNIFORM_FORWARD_INTERPOLANTS) + || optionList.contains(GENERATE_UNIFORM_BACKWARD_INTERPOLANTS)) { + assume() + .withMessage("Solver %s does not support Quantifier Elimination", solverToUse()) + .that(solverToUse()) + .isNoneOf(Solvers.OPENSMT, Solvers.SMTINTERPOL, Solvers.YICES2); + } try { - context.newProverEnvironmentWithInterpolation().close(); + if (optionList.contains(null)) { + context.newProverEnvironmentWithInterpolation().close(); + } else { + context.newProverEnvironmentWithInterpolation(options).close(); + } } catch (UnsupportedOperationException e) { assume() - .withMessage("Solver %s does not support interpolation", solverToUse()) + .withMessage( + "Solver %s threw UnsupportedOperationException for options %s", + solverToUse(), Arrays.toString(options)) .that(e) .isNull(); } } + protected void requireSeqItp(ProverOptions... options) { + assume() + .withMessage( + "Solver independent interpolation strategy %s does not support sequential " + + "interpolation", + solverToUse()) + .that(options) + .asList() + .containsNoneIn(INDEPENDENT_INTERPOLATION_STRATEGIES); + } + + protected void requireTreeItp(ProverOptions... options) { + requireInterpolation(); + assume() + .withMessage( + "Solver independent interpolation strategy %s does not support tree " + "interpolation", + solverToUse()) + .that(options) + .asList() + .containsNoneIn(INDEPENDENT_INTERPOLATION_STRATEGIES); + assume() + .withMessage("Solver does not support tree-interpolation.") + .that(solverToUse()) + .isAnyOf(Solvers.SMTINTERPOL, Solvers.PRINCESS, Solvers.Z3_WITH_INTERPOLATION); + + assume() + .withMessage( + "Strategy %s does not support tree interpolation", + Arrays.toString(options)) // Optional: print the options for clarity + .that(options) + .asList() + .containsNoneIn(INDEPENDENT_INTERPOLATION_STRATEGIES); + } + protected void requireParser() { assume() .withMessage("Solver %s does not support parsing formulae", solverToUse()) @@ -506,4 +587,56 @@ protected Solvers solverToUse() { return solver; } } + + @RunWith(Parameterized.class) + public abstract static class ParameterizedInterpolatingSolverBasedTest0 + extends ParameterizedSolverBasedTest0 { + + // GENERATE_MODELS as stand-in for native + private static final Set ALL_INTERPOLATION_STRATEGIES = + ImmutableSet.of( + GENERATE_PROJECTION_BASED_INTERPOLANTS, + GENERATE_UNIFORM_BACKWARD_INTERPOLANTS, + GENERATE_UNIFORM_FORWARD_INTERPOLANTS); + + @Parameters(name = "solver {0} with interpolation strategy {1}") + public static List getAllSolversAndItpStrategies() { + List lst = new ArrayList<>(); + for (Solvers solver : Solvers.values()) { + // No arg for no option (== solver native interpolation) + lst.add(new Object[] {solver, null}); + for (ProverOptions itpStrat : ALL_INTERPOLATION_STRATEGIES) { + lst.add(new Object[] {solver, itpStrat}); + } + } + return lst; + } + + @Parameter(1) + public ProverOptions interpolationStrategy; + + protected ProverOptions itpStrategyToUse() { + return interpolationStrategy; + } + + @Override + protected void requireSeqItp(ProverOptions... options) { + List allOptions = new ArrayList<>(Arrays.asList(options)); + + if (itpStrategyToUse() != null) { + allOptions.add(itpStrategyToUse()); + } + + super.requireSeqItp(allOptions.toArray(new ProverOptions[0])); + } + + @Override + protected void requireTreeItp(ProverOptions... options) { + List allOptions = new ArrayList<>(Arrays.asList(options)); + if (itpStrategyToUse() != null) { + allOptions.add(itpStrategyToUse()); + } + super.requireTreeItp(allOptions.toArray(new ProverOptions[0])); + } + } }