Solver independent interpolation

build/ivysettings.xml

@@ -10,7 +10,6 @@ SPDX-FileCopyrightText: 2018-2020 Dirk Beyer <https://www.sosy-lab.org>
 SPDX-License-Identifier: Apache-2.0
 -->
 
-<!DOCTYPE ivysettings> <!-- generic AcceptAllDTD to make the Eclipse Warning go away -->
 <ivysettings>
     <!-- DO NOT EDIT LOCALLY!
          Keep this file synchronized with

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

@@ -52,6 +52,36 @@ enum ProverOptions {
      */
     GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS,
 
+    /**
+     * 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_MODEL_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,
+
     /** Whether the solver should enable support for formulae build in SL theory. */
     ENABLE_SEPARATION_LOGIC
   }

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

@@ -17,8 +17,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;
@@ -133,6 +135,27 @@ protected ImmutableSet<T> getAssertedConstraintIds() {
     return builder.build();
   }
 
+  /**
+   * Returns a tuple, consisting of 2 sets, that combined form the set of all formulas on the stack.
+   * The set of formulas A is the formulas identified by the set of input interpolation points. The
+   * set of formulas B is the rest of the current asserted formulas.
+   */
+  protected InterpolationFormulas getInterpolationGroups(Collection<T> pFormulasOfA) {
+    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 (pFormulasOfA.contains(assertedFormulaAndItpPoint.getValue())) {
+          formulasOfA.add(assertedFormulaAndItpPoint.getKey());
+        } else {
+          formulasOfB.add(assertedFormulaAndItpPoint.getKey());
+        }
+      }
+    }
+    return InterpolationFormulas.of(formulasOfA.build(), formulasOfB.build());
+  }
+
   /**
    * This method registers the Evaluator to be cleaned up before the next change on the prover
    * stack.
@@ -157,4 +180,31 @@ public void close() {
     closeAllEvaluators();
     closed = true;
   }
+
+  /** Provides the set of formulas to interpolate on a distinct prover. */
+  public static class InterpolationFormulas {
+    private final Collection<BooleanFormula> formulasForA;
+    private final Collection<BooleanFormula> formulasForB;
+
+    private InterpolationFormulas(
+        Collection<BooleanFormula> pFormulasOfA, Collection<BooleanFormula> pFormulasOfB) {
+      Preconditions.checkNotNull(pFormulasOfA);
+      Preconditions.checkNotNull(pFormulasOfB);
+      formulasForA = pFormulasOfA;
+      formulasForB = pFormulasOfB;
+    }
+
+    protected static InterpolationFormulas of(
+        Collection<BooleanFormula> pFormulasOfA, Collection<BooleanFormula> pFormulasOfB) {
+      return new InterpolationFormulas(pFormulasOfA, pFormulasOfB);
+    }
+
+    protected Collection<BooleanFormula> gotFormulasForA() {
+      return formulasForA;
+    }
+
+    protected Collection<BooleanFormula> gotFormulasForB() {
+      return formulasForB;
+    }
+  }
 }

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

@@ -18,6 +18,7 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.BooleanFormulaManager;
 import org.sosy_lab.java_smt.api.Evaluator;
+import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
 
@@ -32,11 +33,9 @@ public abstract class AbstractProverWithAllSat<T> extends AbstractProver<T> {
   private final BooleanFormulaManager bmgr;
 
   protected AbstractProverWithAllSat(
-      Set<ProverOptions> pOptions,
-      BooleanFormulaManager pBmgr,
-      ShutdownNotifier pShutdownNotifier) {
+      Set<ProverOptions> pOptions, FormulaManager pMgr, ShutdownNotifier pShutdownNotifier) {
     super(pOptions);
-    bmgr = pBmgr;
+    bmgr = pMgr.getBooleanFormulaManager();
     shutdownNotifier = pShutdownNotifier;
   }