Solver independent interpolation

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

@@ -24,7 +24,6 @@
  * @param <T> The type of the objects which can be used to select formulas for interpolant creation.
  */
 public interface InterpolatingProverEnvironment<T> extends BasicProverEnvironment<T> {
-
   /**
    * Get an interpolant for two groups of formulas. This should be called only immediately after an
    * {@link #isUnsat()} call that returned <code>true</code>.

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

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<BooleanFormula> 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<T> nativeFormulasOfA) {
+    ImmutableSet.Builder<BooleanFormula> formulasOfA = ImmutableSet.builder();
+    ImmutableSet.Builder<BooleanFormula> formulasOfB = ImmutableSet.builder();
+    for (Multimap<BooleanFormula, T> assertedFormulasPerLevel : assertedFormulas) {
+      for (Entry<BooleanFormula, T> 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<T> getAssertedConstraintIds() {
     ImmutableSet.Builder<T> builder = ImmutableSet.builder();
     for (Multimap<BooleanFormula, T> 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<BooleanFormula> formulasOfA;
+    private final Collection<BooleanFormula> formulasOfB;
+
+    private InterpolationGroups(
+        Collection<BooleanFormula> pFormulasOfA, Collection<BooleanFormula> pFormulasOfB) {
+      Preconditions.checkNotNull(pFormulasOfA);
+      Preconditions.checkNotNull(pFormulasOfB);
+      formulasOfA = pFormulasOfA;
+      formulasOfB = pFormulasOfB;
+    }
+
+    public static InterpolationGroups of(
+        Collection<BooleanFormula> pFormulasOfA, Collection<BooleanFormula> pFormulasOfB) {
+      return new InterpolationGroups(pFormulasOfA, pFormulasOfB);
+    }
+
+    public Collection<BooleanFormula> getFormulasOfA() {
+      return formulasOfA;
+    }
+
+    public Collection<BooleanFormula> getFormulasOfB() {
+      return formulasOfB;
+    }
+  }
 }

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<ProverOptions> 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<ProverOptions> pSet);
 
@@ -93,6 +123,42 @@ protected abstract OptimizationProverEnvironment newOptimizationProverEnvironmen
    */
   protected abstract boolean supportsAssumptionSolving();
 
+  private static final Set<ProverOptions> 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<ProverOptions> options) {
+    return getIndependentInterpolationStrategy(options) == null;
+  }
+
+  @SuppressWarnings("CheckReturnValue")
+  protected @Nullable ProverOptions getIndependentInterpolationStrategy(
+      Set<ProverOptions> options) {
+    List<ProverOptions> 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<ProverOptions> toSet(ProverOptions... options) {
     Set<ProverOptions> opts = EnumSet.noneOf(ProverOptions.class);
     Collections.addAll(opts, options);