Solver independent interpolation by juliusbrehme · Pull Request #560 · sosy-lab/java-smt

juliusbrehme · 2025-12-20T17:56:06Z

Implemented independent interpolation strategies to support solvers lacking native interpolation features.

Features added:

Uniform Backward/Forward Interpolation.
Projection-based Interpolation

…of asserted formulas from our tracking of asserted formulas

…creation in AbstractSolverContext

…interpolation

…for solvers that do not allow interpolation

…dent interpolation (or native) depending on an option when asking for an interpolant (the techniques are unfinished!)

# Conflicts: # src/org/sosy_lab/java_smt/test/SolverBasedTest0.java

…rpolatingSolverBasedTest0 and block independent interpolation for tree interpolants properly for now

baierd

I found some minor things to improve, and opened some discussion points about how we want to handle things in general for this extension.

baierd · 2026-01-27T11:14:36Z

src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java

+        .withMessage(
+            "Solver %s with strategy %s is not supported or times out",
+            solverToUse(), itpStrategyToUse())
+        .that(


It might be better to split this assume statement into 2 for clarity.

baierd · 2026-01-27T11:16:08Z

src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java

  @Test
  public <T> void issue381InterpolationTest2() throws InterruptedException, SolverException {
+    requireIntegers();
+    requireSeqItp(itpStrategyToUse());


Can we just override requireSeqItp() in ParameterizedInterpolatingSolverBasedTest0 to always include the strategy for only this class?

I did this for requireTreeItp as well

baierd · 2026-01-27T12:11:07Z

src/org/sosy_lab/java_smt/test/SolverBasedTest0.java

+  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));


Could you look into adding this as an assertion function? Similar to the isUnsatisfiable() method (example: assertThatFormula(query).isUnsatisfiable();)

The new call would then need to interpolate as well of course.

src/org/sosy_lab/java_smt/example/IndependentInterpolation.java

baierd · 2026-01-27T12:13:02Z

src/org/sosy_lab/java_smt/example/IndependentInterpolation.java

+    Preconditions.checkState(unsat, "The example for interpolation should be UNSAT");
+
+    BooleanFormula itp = prover.getInterpolant(ImmutableList.of(ip1));
+    logger.log(Level.INFO, "Interpolants are:", itp);


We could add the interpolation technique used, as well as the interpolant (and the groups A and B if not too large) to the output.

I added this if the formulas are not longer than 500 chars

baierd · 2026-01-27T15:43:31Z

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

+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<String>


Maybe we need tests that involve the additional delegates as well, to check for problems when multiple are stacked.

baierd · 2026-01-27T15:44:20Z

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

+    if (interpolationStrategy == null) {
+      interpolant = delegate.getInterpolant(identifiersForA);
+
+    } else if (interpolationStrategy.equals(ProverOptions.GENERATE_PROJECTION_BASED_INTERPOLANTS)) {


This could be improved by making it a switch-case.

Added switch case, but the null can not be in a switch case

baierd · 2026-01-27T15:47:09Z

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

+  }
+
+  /** interpolate(A(x,y),B(y,z))=∀z.¬B(y,z). */
+  private BooleanFormula getUniformBackwardInterpolant(


Maybe it would be beneficial to separate the distinct techniques into their own package and classes, as if we add more techniques, especially techniques with more code, this class will end up very large and hard to read. E.g. a new package package org.sosy_lab.java_smt.basicimpl.interpolation_techniques; with a class for each technique?

baierd · 2026-01-27T15:49:56Z

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

+     * solving over the theories interpolated upon. The solver does not need to support
+     * interpolation itself.
+     */
+    GENERATE_PROJECTION_BASED_INTERPOLANTS,


@kfriedberger @PhilippWendler do you guys have feedback/ideas/proposals for how we want the user to be able to switch in between native and solver independent interpolation techniques? Currently we just ProverOptions, which is not ideal, as they can't be switched once a prover has been created.

Why would I want to switch the interpolation implementation for a prover instance and why would it be a problem to create a new prover instance instead? I don't really see a use case.

What I am interested in is to have the following 3 possibilities:

create an interpolating prover that guarantees that native solver interpolation is used (and creation fails if this is not possible)

create an interpolating prover that always uses the specific strategy implemented here

create an interpolating prover that prefers the solver native interpolation but falls back to a general implementation if the solver does not support interpolation

The third method could be done by catching the exception from the first case, but why not let JavaSMT provide it as well for the benefit of all its users?

OK that seems reasonable.

I thought it might be good to decide about a interpolation technique when asking for interpolants, as users can implement point 3 themselves (potentially even with more than one fallback.

Also interpolation is (usually) only possible after UNSAT has been returned. If a user wants to generate interpolants with multiple techniques in sequence, that would not be possible. E.g.: start with a technique like projection based interpolants that tends to return interpolants fast, but they also tend to be weak -> then use a stronger technique if that first interpolant is not useful. In your approach, a user would need to build a second (or n) new provers and then check satisfiability again.

(Just some thoughts. I want to provide the best possible API. I don't have a preference at the moment.)

@leventeBajczi you also use interpolation, maybe you have some thoughts?

I don't really have any further input to this -- as long as it's clear how I'm getting the interpolants, I don't mind if I need to create separate solver instances. We would probably always use point 3 if it was available, especially if it also handled the case when a solver returns an error for the interpolation query (although I'm not sure if the resulting solver state always stays usable). Failing that, we already have some support for using a portfolio of solvers, so we could easily implement the switching ourselves.

PhilippWendler · 2026-01-28T07:30:14Z

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

+     * solving over the theories interpolated upon. The solver does not need to support
+     * interpolation itself.
+     */
+    GENERATE_PROJECTION_BASED_INTERPOLANTS,


It might not be a good idea to add options that are only relevant for interpolating provers to the general ProverOptions class? What happens if I create a regular prover environment and tell it to generate interpolants?

I added this as a quick dummy. Hence the question about how we want to do it properly ;D

…ependent interpolation

…ontext to test the IndependentInterpolatingSolverDelegate

# Conflicts: # src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java # src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java

…sosy-lab/java-smt into solver_independent_interpolation2_arm64

baierd and others added 21 commits April 7, 2025 15:36

Add general implementation for retrieving the 2 interpolation groups …

733d43b

…of asserted formulas from our tracking of asserted formulas

Add the new interpolation options to the ProverOptions

8d35e69

Add a prover delegate for solver-independent interpolation to Prover …

eab70d4

…creation in AbstractSolverContext

Add options enum for interpolation

4d77924

Extend parameterized tests with possibility for second parameter for …

e2119ad

…interpolation

Remove options for interpolation from ProverOptions

f9d735c

Add InterpolatingProverDelegate that allows to use interpolation API …

8f87aec

…for solvers that do not allow interpolation

Add IndependentInterpolatingSolverDelegate that allows to use indepen…

a4769a4

…dent interpolation (or native) depending on an option when asking for an interpolant (the techniques are unfinished!)

Merge branch 'master' into solver_independent_interpolation2_arm64

993f400

# Conflicts: # src/org/sosy_lab/java_smt/test/SolverBasedTest0.java

First changes to get the independent interpolation method working

c256db9

added requirements for tests

d78e284

small fixes for independent interpolation

23ae59a

update independent interpolation logic and tests

2404f5c

Remove redundant variable present in super class in ParameterizedInte…

05864d6

…rpolatingSolverBasedTest0 and block independent interpolation for tree interpolants properly for now

Add TODO about restricting independent interpolation solver creation

a8eb472

add comments for interpolation options

9d74f92

updated code style

a3e98de

updated example for indepented interpolation

a587a83

updated requireInterpolation

70ccc55

updated to resolve spotbugs

d20c5f8

added supresswarning for building project successfully

a29d671

juliusbrehme requested a review from baierd December 20, 2025 17:56

juliusbrehme added 4 commits December 27, 2025 18:53

add trivial test for independent interpolation

74424f6

update requireInterpolation

89acfea

use class variable

6d7d488

remove isTrivialFalse

2fa4562

baierd requested changes Jan 27, 2026

View reviewed changes

PhilippWendler reviewed Jan 28, 2026

View reviewed changes

baierd added 2 commits January 29, 2026 10:43

Add CVC4 to interpolation test for invalid tokens, as it supports ind…

56168b4

…ependent interpolation

Extend PackageSanityTest for basicimpl package with a default SolverC…

788b408

…ontext to test the IndependentInterpolatingSolverDelegate

juliusbrehme added 6 commits January 31, 2026 12:10

us Immutablelist instead of Collection

52e6134

resolve checkstyle and check-format

e4f245c

Merge branch 'master' into solver_independent_interpolation2_arm64

316b747

# Conflicts: # src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java # src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java

format code

4b04456

resolved some comments from the pull request

995fa72

Merge branch 'solver_independent_interpolation2_arm64' of github.com:…

d2601d6

…sosy-lab/java-smt into solver_independent_interpolation2_arm64

Conversation

juliusbrehme commented Dec 20, 2025

Uh oh!

baierd left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

4 participants