Use integers for assertion ids by daniel-raffler · Pull Request #706 · sosy-lab/java-smt

daniel-raffler · 2026-08-15T08:17:54Z

Hello,

this PR adds integer formula ids for all solvers with interpolation support. Internal solver ids will be mapped to theses integer ids. This helps when rebuilding a prover stack, possible with a different solver, by allowing existing ids to be reused by other provers

The ids returned are simply the position of the asserted formula on the stack. They start at 1 and go up to the size of the assertion stack, while 0 can be used to mark an invalid id. When popping a solver frame, and then pushing new formulas, old ids are reassigned

kfriedberger

The change is small and might not harm existing implementations. lgtm.

However, I doubt that reuse across solvers will be a use-case.

kfriedberger · 2026-08-15T10:56:27Z

  @Override
  public void pop() {
    itpProver.pop();
+    lastId = getDelegateAsAbstractProver().getAssertedConstraintIds().size();


no cleanup/deletion of the popped id?

Thanks for the fast review! I've now added some code to remove outdated ids when a frame is popped

PhilippWendler · 2026-08-17T05:52:58Z

I value JavaSMT as a layer that provides direct access to solvers without introducing unnecessary indirections and performance / memory overhead while abstracting over the different solvers.

The current implementation of interpolation ids achieves this, and why should there now be additional overhead added?

Reusing interpolation ids across contexts or solvers would first require to expose the concrete type in the API. But this would be bad, because Integer is a such general type that it can easily be mixed up with other values. Furthermore, right now it is possible to write code that handles more than one interpolation environment and where the compiler guarantees that the interpolation ids are not mixed up across the solvers. This would no longer be possible.

That for every new interpolation environment (and even after a pop) old ids are reused and their values become valid again also makes the API much more error prone.

Furthermore, I also think it is a bad idea to tell users of JavaSMT that interpolation ids can and should be reused across contexts and solvers. This goes directly against what users of JavaSMT need to know and follow for other objects, in particular formulas, possibly leading to confusion and more accidental reuse of formula objects.

Besides these problems, I also don't think there is much value in reusing interpolation ids. And users who want this can easily add such a mapping themselves.

baierd · 2026-08-17T10:25:16Z

I think that the general idea of this is a good thing, if done right. This means that this layer needs to be cheap and follow consistent rules with clear benefits over what the solvers do.

That being said; we need to tackle this problem in a structured way. This is by no means a small change!

We already have Id solutions for some solvers (due to inconsistencies in how they handle them). This solutions needs to be able to replace the old ones in my opinion, otherwise we start piling multiple solutions on top of each other, reducing maintainability and increasing our own work in the future.

I think what we need is a structured investigation into:

what is current solver behavior, including differences between them? For example, what is solver behavior if we have 2 formulas that are distinct structurally, but are simplified to the same formula. Do these get the same IDs?
what behavior do we want to guarantee? What problems do we want to fix? Is it even possible to fix all of this in a way that is acceptable? We need figure this out first, and then document it properly for users (We give no proper guarantees/limits on the IDs currently)

Also, we need to test and evaluate this, making sure it works as intended, and does not cause a big overhead!
I recommend starting with a test that models the problem that we want to solve first.

Also, I agree with Philipp in most points (besides that we should not do this. I am a big fan of solver independent and/or convenience features):

we want interpolation IDs to represent the same formula. Even if we re-build the formula, it should represent the same ID. Or, if we push a formula, then pop it again, then push it again, it should represent the same ID as before. And i currently see no easy and cheap way of guaranteeing this across multiple contexts. The current solution is dependent on the order used to push formulae, and does not guarantee this at all.
can the IDs clash? The solution is clearly to build this in a way that IDs are not re-used, with the exception of equal formulas that have been used before. Instead of using some custom solution, why not use what we define in SoSy-Commons with UniqueIdGenerator?
type safety is a HUGE issue here. Nobody stops me from using a arbitrary integer, or another solvers IDs. The IDs should clearly be a unique type that is overridden on a per solver basis. Inside this type, we can use whatever, as long as we don't get clashes.
what about formulas? I can't re-use the formulas, but the IDs?

I have little hopes of finding a general solution for this to be honest. We should focus on the actual problem that you try to tackle here; re-building a context, with formulas and prover states. Because that is much easier. I would start this way:

figure out which solvers guarantee consistent interpolation IDs across multiple contexts. Adding tests for this seems to be a good start. Please make sure that the formulas are not trivial enough that solvers give them the same IDs by chance. You can also change the order of pushing them.
add a new method importStateFrom(InterpolatingProver) for InterpolatingProver, that imports the state of a existing InterpolatingProver into the current prover. I.e.: this re-builds the stack of the given prover in the current prover, including translating the IDs in the way you started here.
- Take the prover stack of the source prover and translate all (use the translate method, as it may be more efficient) formulas to the new prover.
- Find the diff of the source provers stack formulas and their IDs to the target provers.
- Add a mapping of formulas and Ids from the old prover to their new counterparts, but only if you can't re-use the old ones. The target prover should accept the source provers formulas and IDs and translate them to the target prover formulas, but also directly accept the formulas and IDs originating from the target prover.
- Return the formulas that have been added to the target prover from the translate() method, including a mapping of the old formulae to the new ones. This allows users to know which formulas have been added, and replace theirs with new ones if they want to.
- The translation should work only in 1 direction (source prover -> target prover), i.e. the source prover is not changed.
- Only map IDs and formulae that are not equal between the provers.
- I recommend throwing an exception if the current prover stack is not a strict subset of the imported one, or any inconsistency is encountered.
- document this well! Including use-cases and don'ts.

baierd · 2026-08-17T08:22:14Z

    // TODO: do we want a common method to calculate partition B out of the asserted formulas
    //  efficiently? We currently have several distinct solutions.
-    return itpProver.getInterpolant(formulasOfA);
+    return itpProver.getInterpolant(formulaIds);


This should be formulaIdsOfA.

baierd · 2026-08-17T08:42:14Z

  public void pop() {
    itpProver.pop();
+    lastId = getDelegateAsAbstractProver().getAssertedConstraintIds().size();
+    assertionIds = new HashMap<>(Maps.filterKeys(assertionIds, k -> k <= lastId));


This re-builds the map from the filtered view. In general; either use ImmutableMap, as it would be cleaner here and communicate how we use the map, or use the mutability of the map, which would be more efficient.

Since CPAchecker (as an example) has cases in which it holds 20.000+ formulas, meaning we need to copy all of them here in the worst case, we should use a mutable data-structure with O(1) access, addition and deletion, i.e. HashMap.

Since CPAchecker (as an example) has cases in which it holds 20.000+ formulas

Ok, that's a lot more than I was excpecting 😅

If performance is an issue, we could simply use an ArrayList here. I don't think it necessarily needs to be updated either when frames are popped from the prover. Outdated ids in the list are invalid, and should throw an exception in InterpolatingProverDelegate when used. It just seemed like a good idea to have this check as early as possible

baierd · 2026-08-17T08:45:40Z

-  public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException {
-    return itpProver.addConstraint(constraint);
+  public @Nullable Integer addConstraint(BooleanFormula constraint) throws InterruptedException {
+    var newId = ++lastId;


var for Integer?

baierd · 2026-08-17T10:25:57Z

  private final InterpolatingProverEnvironment<T> itpProver;

+  private Map<Integer, T> assertionIds = new HashMap<>();
+  private int lastId = 0;


Why not use our UniqueIdGenerator?

UniqueIdGenerator creates fresh ids for every assertion that is pushed. However, if we want to rebuild solver stack, popped ids need to be reused. Otherwise we may end up with non-consecutive ids:

push(f1) // [id1 = f1] push(f2) // [id1 = f1, id2 = f2] pop() // [id1 = f1] push(f3) // [id1 = f1, id3 = f3]

These "gaps" are skipped when rebuilding the prover:

push(f1) // [id1 = f1] push(f3) // [id1 = f1, id2 = f3]

As a result, we can no longer use the old id for f3 with the new prover

PhilippWendler · 2026-08-17T10:44:27Z

figure out which solvers guarantee consistent interpolation IDs across multiple contexts.

Why do you think that is the case at all?

I would hope that IDs are recycled as rarely as possible, even for the same formula, because this helps to detect bugs when one accidentally reuses old interpolation ids.

we want interpolation IDs to represent the same formula.

I disagree, for the mentioned reasons.

The IDs should clearly be a unique type that is overridden on a per solver basis.

This would still be worse then the current solution, which does not only prevent mixing ids between solvers, but also between mixing them between instances of interpolation environments.

Several of your goals actually contradict each other and would be unsolvable together. I would not bother with attempting to do this.

baierd · 2026-08-17T11:48:53Z

figure out which solvers guarantee consistent interpolation IDs across multiple contexts.

Why do you think that is the case at all?

I don't. That is why i want it investigated.

I would hope that IDs are recycled as rarely as possible, even for the same formula, because this helps to detect bugs when one accidentally reuses old interpolation ids.

we want interpolation IDs to represent the same formula.

I disagree, for the mentioned reasons.

This view is certainly valid. But are you sure that using IDs from a distinct context lead to errors in all cases immediately?

The IDs should clearly be a unique type that is overridden on a per solver basis.

This would still be worse then the current solution, which does not only prevent mixing ids between solvers, but also between mixing them between instances of interpolation environments.

The goal here is to allow this.

But i think it is clear that there are multiple views on this. So we should close this PR for now and discuss this critically before implementing something!

daniel-raffler added 2 commits August 14, 2026 20:09

Use integers for formula ids on all solvers

7c6092d

Suppress "resource" warning

230c073

daniel-raffler requested review from baierd and kfriedberger August 15, 2026 08:17

daniel-raffler self-assigned this Aug 15, 2026

daniel-raffler added the enhancement label Aug 15, 2026

kfriedberger previously approved these changes Aug 15, 2026

View reviewed changes

Remove outdated assertion ids from the mapping when a frame is popped

22ca820

daniel-raffler dismissed kfriedberger’s stale review via 22ca820 August 16, 2026 09:55

baierd requested changes Aug 17, 2026

View reviewed changes

Navigation Menu

Uh oh!

Use integers for assertion ids - #706

Use integers for assertion ids#706
daniel-raffler wants to merge 3 commits into
masterfrom
generic-assertion-ids

daniel-raffler commented Aug 15, 2026

Uh oh!

kfriedberger left a comment

Uh oh!

kfriedberger Aug 15, 2026

Uh oh!

daniel-raffler Aug 16, 2026

Uh oh!

PhilippWendler commented Aug 17, 2026

Uh oh!

baierd commented Aug 17, 2026

Uh oh!

baierd Aug 17, 2026

Uh oh!

baierd Aug 17, 2026

Uh oh!

daniel-raffler Aug 18, 2026

Uh oh!

baierd Aug 17, 2026

Uh oh!

baierd Aug 17, 2026

Uh oh!

daniel-raffler Aug 18, 2026

Uh oh!

PhilippWendler commented Aug 17, 2026

Uh oh!

baierd commented Aug 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

daniel-raffler commented Aug 15, 2026

Uh oh!

kfriedberger 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!

PhilippWendler commented Aug 17, 2026

Uh oh!

baierd commented Aug 17, 2026

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!

PhilippWendler commented Aug 17, 2026

Uh oh!

baierd commented Aug 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

4 participants