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 0e918fd6bb..d0127335ae 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -18,8 +18,10 @@ 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.Entry; import java.util.Set; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.java_smt.api.BasicProverEnvironment; @@ -126,6 +128,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) { @@ -158,4 +182,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..e5c1530728 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/IndependentInterpolatingSolverDelegate.java @@ -0,0 +1,432 @@ +/* + * 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.ImmutableList; +import com.google.common.collect.Sets; +import java.util.Collection; +import java.util.HashMap; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.Set; +import java.util.concurrent.atomic.AtomicBoolean; +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.Formula; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.FormulaType; +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.QuantifiedFormulaManager; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; +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; +import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; +import org.sosy_lab.java_smt.api.visitors.TraversalProcess; + +public class IndependentInterpolatingSolverDelegate extends AbstractProver + implements InterpolatingProverEnvironment { + + private final SolverContext solverContext; + + private final InterpolatingProverEnvironment delegate; + + private final @Nullable ProverOptions interpolationStrategy; + + private final FormulaManager mgr; + private final BooleanFormulaManager bmgr; + private final UFManager ufmgr; + + private static final String PREFIX = "javasmt_itp_term_"; // for term-names + private static final UniqueIdGenerator termIdGenerator = + new UniqueIdGenerator(); // for different term-names + + Map itpPointsMap = new HashMap<>(); + + 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(); + ufmgr = mgr.getUFManager(); + } + + // 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); + List variablesInA = getAllVariables(conjugatedFormulasOfA); + List variablesInB = getAllVariables(conjugatedFormulasOfB); + List sharedVariables = getCommonFormulas(variablesInA, variablesInB); + List exclusiveVariablesInA = removeVariablesFrom(variablesInA, sharedVariables); + List exclusiveVariablesInB = removeVariablesFrom(variablesInB, sharedVariables); + + BooleanFormula interpolant; + + if (bmgr.isFalse(conjugatedFormulasOfA)) { + return bmgr.makeFalse(); + } else if (bmgr.isFalse(conjugatedFormulasOfB)) { + return bmgr.makeTrue(); + } + + if (interpolationStrategy == null) { + interpolant = delegate.getInterpolant(identifiersForA); + + } else if (interpolationStrategy.equals(ProverOptions.GENERATE_PROJECTION_BASED_INTERPOLANTS)) { + interpolant = + getModelBasedProjectionInterpolant( + conjugatedFormulasOfA, + conjugatedFormulasOfB, + variablesInA, + variablesInB, + sharedVariables); + } else if (interpolationStrategy.equals(ProverOptions.GENERATE_UNIFORM_FORWARD_INTERPOLANTS)) { + // Will generate interpolants based on quantifier elimination + if (exclusiveVariablesInA.isEmpty()) { + return conjugatedFormulasOfA; + } + interpolant = getUniformForwardInterpolant(conjugatedFormulasOfA, exclusiveVariablesInA); + } else if (interpolationStrategy.equals(ProverOptions.GENERATE_UNIFORM_BACKWARD_INTERPOLANTS)) { + if (exclusiveVariablesInB.isEmpty()) { + return bmgr.not(conjugatedFormulasOfB); + } + // Note: uses the A -> i -> B is valid definition for Craig-Interpolants, so we negate B + interpolant = getUniformBackwardInterpolant(conjugatedFormulasOfB, exclusiveVariablesInB); + } else { + throw new AssertionError("Unknown interpolation strategy."); + } + + 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."); + } + + /** + * Extracts all variables (not UFs) from the given formula. There are no duplicates in the list. * + */ + private List getAllVariables(BooleanFormula formula) { + return mgr.extractVariables(formula).values().asList(); + } + + /** + * 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; + } + + /** interpolate(A(x,y),B(y,z))=∀z.¬B(y,z). */ + private BooleanFormula getUniformBackwardInterpolant( + BooleanFormula formulasOfB, List exclusiveVariables) + throws SolverException, InterruptedException { + + QuantifiedFormulaManager qfmgr = mgr.getQuantifiedFormulaManager(); + BooleanFormula itpBackwardQuantified = qfmgr.forall(exclusiveVariables, bmgr.not(formulasOfB)); + BooleanFormula itpBackward = qfmgr.eliminateQuantifiers(itpBackwardQuantified); + // Check that the top-level quantifier has been eliminated + if (isQuantifiedFormula(itpBackward)) { + throw new SolverException( + "Error when calculating uniform interpolant, quantifier elimination failed."); + } + + return mgr.simplify(itpBackward); + } + + /** 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(); + } + + /** + * Computes the uniform Craig interpolant, utilizing quantifier-elimination in the forward + * direction with: interpolate(A(x,y),B(y,z)) = ∃x.A(x,y) + * + *

Forward means, that the set of formulas A interpolates towards the set of formulas B. + * + * @param conjugatedFormulasOfA The set of formulas A, combined into one {@link BooleanFormula}. + * @param exclusiveVariables A list of shared variables found in both sets of formulas A and B. + * @return a uniform Craig interpolant or an exception is thrown. + */ + private BooleanFormula getUniformForwardInterpolant( + BooleanFormula conjugatedFormulasOfA, List exclusiveVariables) + throws SolverException, InterruptedException { + + QuantifiedFormulaManager qfmgr = mgr.getQuantifiedFormulaManager(); + BooleanFormula itpForwardQuantified = qfmgr.exists(exclusiveVariables, conjugatedFormulasOfA); + BooleanFormula itpForward = qfmgr.eliminateQuantifiers(itpForwardQuantified); + // Check that the top-level quantifier has been eliminated + if (isQuantifiedFormula(itpForward)) { + throw new SolverException( + "Error when calculating uniform interpolant, quantifier elimination failed."); + } + + return mgr.simplify(itpForward); + } + + private BooleanFormula getModelBasedProjectionInterpolant( + BooleanFormula conjugatedFormulasOfA, + BooleanFormula conjugatedFormulasOfB, + List variablesInA, + List variablesInB, + List sharedVars) + throws InterruptedException, SolverException { + + QuantifiedFormulaManager qfmgr = mgr.getQuantifiedFormulaManager(); + + BooleanFormula itp = + ufmgr.declareAndCallUF( + "__itp_internal_javasmt_" + termIdGenerator.getFreshId(), + FormulaType.BooleanType, + sharedVars); + BooleanFormula left; + BooleanFormula right; + if (variablesInA.isEmpty()) { + left = bmgr.implication(conjugatedFormulasOfA, itp); + } else { + left = qfmgr.forall(variablesInA, bmgr.implication(conjugatedFormulasOfA, itp)); + } + // BooleanFormula left = qfmgr.forall(variablesInA, bmgr.implication(conjugatedFormulasOfA, + // itp)); + if (variablesInB.isEmpty()) { + right = bmgr.implication(itp, bmgr.not(conjugatedFormulasOfB)); + } else { + right = qfmgr.forall(variablesInB, bmgr.implication(itp, bmgr.not(conjugatedFormulasOfB))); + } + + BooleanFormula interpolant = bmgr.makeFalse(); + try (ProverEnvironment itpProver = getDistinctProver()) { + + itpProver.push(left); + itpProver.push(right); + + if (!itpProver.isUnsat()) { + try (Model model = itpProver.getModel()) { + interpolant = model.eval(itp); + } + checkNotNull(interpolant); + } + } + return mgr.simplify(interpolant); + } + + /** + * 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); + } + + /** Returns common {@link org.sosy_lab.java_smt.api.Formula}s of the 2 given lists. * */ + private List getCommonFormulas( + List variables1, List variables2) { + Set set = new LinkedHashSet<>(variables1); + set.retainAll(variables2); + return ImmutableList.copyOf(set); + } + + /** + * Removes variablesToRemove from variablesToRemoveFrom and returns a new list without modifying + * the old lists. + */ + private 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(); + } + + @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 isUnsat() 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/InterpolatingSolverDelegate.java b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingSolverDelegate.java new file mode 100644 index 0000000000..59f78ea8e9 --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/InterpolatingSolverDelegate.java @@ -0,0 +1,116 @@ +/* + * 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 + public int size() { + return delegate.size(); + } + + @Override + public boolean isUnsat() 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/example/IndependentInterpolation.java b/src/org/sosy_lab/java_smt/example/IndependentInterpolation.java new file mode 100644 index 0000000000..e802219603 --- /dev/null +++ b/src/org/sosy_lab/java_smt/example/IndependentInterpolation.java @@ -0,0 +1,140 @@ +/* + * 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.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 + } + + 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( + ProverOptions.GENERATE_UNIFORM_BACKWARD_INTERPOLANTS)) { + logger.log(Level.WARNING, "Using solver " + solver + " in version " + context.getVersion()); + + 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) + prover.addConstraint(bmgr.and(imgr.equal(y, z), imgr.equal(z, two))); + T ip1 = prover.addConstraint(bmgr.and(imgr.equal(x, one), imgr.equal(y, x))); + + // 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); + } + + 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); + + prover.addConstraint(imgr.lessThan(y, zero)); + T ip1 = + prover.addConstraint(bmgr.and(imgr.greaterThan(x, zero), imgr.equal(y, imgr.add(x, one)))); + + // 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); + } +} diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java index 9287b00f67..820127722d 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(); @@ -197,6 +209,15 @@ public void binaryInterpolationWithConstantFalse() @Test public void binaryBVInterpolation1() throws SolverException, InterruptedException { + assume() + .withMessage( + "Solver %s with strategy %s is not supported or times out", + solverToUse(), itpStrategyToUse()) + .that( + (solverToUse() == Solvers.BITWUZLA) + || (solverToUse() == Solvers.Z3 + && itpStrategyToUse() == ProverOptions.GENERATE_PROJECTION_BASED_INTERPOLANTS)) + .isFalse(); requireBitvectors(); InterpolatingProverEnvironment stack = newEnvironmentForTest(); @@ -244,16 +265,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); - } - @Test public void sequentialInterpolation() throws SolverException, InterruptedException { + requireSeqItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); requireIntegers(); @@ -306,6 +320,7 @@ public void sequentialInterpolation() throws SolverException, InterruptedExc public void sequentialInterpolationIsNotRepeatedIndividualInterpolation() throws SolverException, InterruptedException { InterpolatingProverEnvironment stack = newEnvironmentForTest(); + requireSeqItp(itpStrategyToUse()); requireIntegers(); IntegerFormula zero = imgr.makeNumber(0); @@ -341,6 +356,7 @@ public void sequentialInterpolationIsNotRepeatedIndividualInterpolation() public void sequentialInterpolationWithoutPartition() throws SolverException, InterruptedException { requireIntegers(); + requireSeqItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); stack.push(imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1))); @@ -355,6 +371,7 @@ public void sequentialInterpolationWithoutPartition() public void sequentialInterpolationWithOnePartition() throws SolverException, InterruptedException { requireIntegers(); + requireSeqItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); int i = index.getFreshId(); @@ -383,6 +400,7 @@ public void sequentialInterpolationWithOnePartition() public void sequentialInterpolationWithFewPartitions() throws SolverException, InterruptedException { requireIntegers(); + requireSeqItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); int i = index.getFreshId(); @@ -415,6 +433,8 @@ public void sequentialInterpolationWithFewPartitions() @Test public void sequentialBVInterpolation() throws SolverException, InterruptedException { requireBitvectors(); + requireSeqItp(itpStrategyToUse()); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); @@ -464,7 +484,7 @@ public void sequentialBVInterpolation() throws SolverException, InterruptedE @Test public void treeInterpolation() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); int i = index.getFreshId(); @@ -634,7 +654,7 @@ private void testTreeInterpolants2( @Test public void treeInterpolation2() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); @@ -693,7 +713,7 @@ public void treeInterpolation2() throws SolverException, InterruptedExceptio @Test public void treeInterpolation3() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); @@ -749,7 +769,7 @@ public void treeInterpolation3() throws SolverException, InterruptedExceptio @Test public void treeInterpolation4() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); @@ -796,7 +816,7 @@ public void treeInterpolation4() throws SolverException, InterruptedExceptio @Test public void treeInterpolationForSequence() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); @@ -821,7 +841,7 @@ public void treeInterpolationForSequence() throws SolverException, Interrupt @Test public void treeInterpolationBranching() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); @@ -862,7 +882,7 @@ public void treeInterpolationBranching() throws SolverException, Interrupted @SuppressWarnings({"unchecked", "varargs"}) public void treeInterpolationMalFormed1() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); BooleanFormula A = imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1)); @@ -878,7 +898,7 @@ public void treeInterpolationMalFormed1() throws SolverException, Interrupte @SuppressWarnings({"unchecked", "varargs"}) public void treeInterpolationMalFormed2() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); BooleanFormula A = imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1)); @@ -894,7 +914,7 @@ public void treeInterpolationMalFormed2() throws SolverException, Interrupte @SuppressWarnings({"unchecked", "varargs"}) public void treeInterpolationMalFormed3() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); BooleanFormula A = imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1)); @@ -909,7 +929,7 @@ public void treeInterpolationMalFormed3() throws SolverException, Interrupte @Test public void treeInterpolationMalFormed4() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); BooleanFormula A = imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1)); @@ -924,7 +944,7 @@ public void treeInterpolationMalFormed4() throws SolverException, Interrupte @Test public void treeInterpolationMalFormed5() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); BooleanFormula A = imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1)); @@ -939,7 +959,7 @@ public void treeInterpolationMalFormed5() throws SolverException, Interrupte @Test public void treeInterpolationMalFormed6() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); BooleanFormula A = imgr.equal(imgr.makeNumber(0), imgr.makeNumber(1)); @@ -953,7 +973,7 @@ public void treeInterpolationMalFormed6() throws SolverException, Interrupte @Test public void treeInterpolationWithoutPartition() throws SolverException, InterruptedException { - requireTreeItp(); + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); @@ -968,8 +988,7 @@ public void treeInterpolationWithoutPartition() throws SolverException, Inte @Test public void treeInterpolationWithOnePartition() throws SolverException, InterruptedException { - requireTreeItp(); - + requireTreeItp(itpStrategyToUse()); InterpolatingProverEnvironment stack = newEnvironmentForTest(); int i = index.getFreshId(); @@ -999,6 +1018,8 @@ public void treeInterpolationWithOnePartition() throws SolverException, Inte public void bigSeqInterpolationTest() throws InterruptedException, SolverException { requireBitvectors(); requireInterpolation(); + requireSeqItp(itpStrategyToUse()); + requireTreeItp(itpStrategyToUse()); assume() .withMessage("Solver %s runs into timeout on this test", solverToUse()) @@ -1068,7 +1089,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); @@ -1115,7 +1136,7 @@ private void checkItpSequence(List formulas, List void testInvalidToken() throws InterruptedException, SolverException { - requireInterpolation(); + requireIntegers(); InterpolatingProverEnvironment stack = newEnvironmentForTest(); // create and push formulas and solve them @@ -1149,6 +1170,9 @@ public void testInvalidToken() throws InterruptedException, SolverException case SMTINTERPOL: p3 = "some string"; break; + case Z3: + p3 = 12345; + break; default: p3 = null; // unexpected solver for interpolation } @@ -1165,6 +1189,8 @@ public void testInvalidToken() throws InterruptedException, SolverException */ @Test public void issue381InterpolationTest1() throws InterruptedException, SolverException { + requireIntegers(); + requireSeqItp(itpStrategyToUse()); try (InterpolatingProverEnvironment prover = newEnvironmentForTest()) { var x = imgr.makeVariable("x"); var one = imgr.makeNumber(1); @@ -1191,6 +1217,8 @@ public void issue381InterpolationTest1() throws InterruptedException, Solver */ @Test public void issue381InterpolationTest2() throws InterruptedException, SolverException { + requireIntegers(); + requireSeqItp(itpStrategyToUse()); try (InterpolatingProverEnvironment prover = newEnvironmentForTest()) { var x = imgr.makeVariable("x"); var one = imgr.makeNumber(1); @@ -1217,6 +1245,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 2a975a3b24..31975367db 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -8,13 +8,25 @@ package org.sosy_lab.java_smt.test; +import static com.google.common.base.Preconditions.checkState; 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.collect.Sets; import com.google.common.truth.Truth; +import java.util.ArrayList; +import java.util.Arrays; import java.util.Collection; +import java.util.Collections; +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 +91,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 +144,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(); @@ -330,17 +348,83 @@ protected final void requireOptimization() { } } - protected final void requireInterpolation() { + protected final void requireInterpolation(ProverOptions... options) { + List optionList = + (options == null) ? Collections.emptyList() : Arrays.asList(options); + if (optionList.contains(null)) { + 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 final 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 final 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); + + 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()) @@ -405,6 +489,54 @@ protected final BooleanFormulaSubject assertThatFormula(BooleanFormula formula) return assertUsing(context).that(formula); } + /** Check that the interpolant in the subject is valid fot the formulas A and B. */ + public void isValidInterpolant(BooleanFormula interpolant, BooleanFormula a, BooleanFormula b) + throws SolverException, InterruptedException { + // TODO: move into assertion framework + isValidInterpolant(interpolant, ImmutableList.of(a), ImmutableList.of(b)); + } + + /** Check that the interpolant in the subject is valid fot the formulas A and B. */ + public void isValidInterpolant( + BooleanFormula interpolant, + List formulasOfA, + List formulasOfB) + throws SolverException, InterruptedException { + // TODO: move into assertion framework + + BooleanFormula conjugatedFormulasOfA = bmgr.and(formulasOfA); + BooleanFormula conjugatedFormulasOfB = bmgr.and(formulasOfB); + + // 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); + // TODO: assertThat is not available with message + 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 validationProver = context.newProverEnvironment()) { + validationProver.push(); + validationProver.addConstraint(bmgr.implication(conjugatedFormulasOfA, interpolant)); + // TODO: assertThat is not available with message + checkState( + !validationProver.isUnsat(), + "Invalid Craig interpolation: formula group A does not imply the interpolant."); + validationProver.pop(); + + validationProver.push(); + validationProver.addConstraint(bmgr.and(interpolant, conjugatedFormulasOfB)); + // TODO: assertThat is not available with message + checkState( + validationProver.isUnsat(), + "Invalid Craig interpolation: interpolant does not contradict formula group B."); + validationProver.pop(); + } + } + /** * Use this for checking assertions about ProverEnvironments with Truth: * assertThatEnvironment(stack).is...(). @@ -479,4 +611,36 @@ 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; + } + } }