Compact sets in RelationAnalysis

[xeren]

• Adds IndexedDomain<T>, a list of distinct elements with a hashtable-powered indexOf method.
• Adds IndexedSet<T>, an implementation of Set<T> that uses IndexedDomain<T> and a bit array to describe its contents.
• Memoizes the results of ExecutionAnalysis (EA) with IndexedSet.
• Replaces usages HashSet<T> with IndexedSet<T> in RelationAnalysis (RA) and ActiveSetAnalysis (ASA).
• Adds VisibilityAnalysis RelationEventDomains to allow using a smaller domain on most relations in RelationAnalysis.
• Enhances the precision of the Extended Relation Analysis (XRA):
  Given a transitive closure $r\mathrel{:=}s^+$. The event pair set $\delta$ has previously been disabled in $s$, such that $\mathsf{may}(s)\cap\delta$ is empty.
  The bottom-up propagation should compute $\mathsf{may}(r)\setminus\mathsf{may}(s)^+$.
  In development, the result was smaller $(\delta\cup(\delta\mathrel;\mathsf{may}(r)))\setminus\mathsf{may}(s)^+$.
  Without this, XRA and ASA produce the same results as development in all tests.
• Edit: Adds EventDomainRepository to create domains to be used by analyses.

Table 1 - Performance for suite benchmarks/challenging in seconds (only the mentioned analyses). For each pair of rows, the upper describes development and the lower describes this PR.

Benchmark	EA	RA	XRA	ASA	Total
cna.c rc11.cat	0.0	2.2	2.0	6.6	10.8
	0.1	0.2	0.5	0.3	1.1
cna.c imm.cat	0.0	1.4	1.3	5.0	7.7
	0.1	0.3	0.3	0.3	1.0
harris-3.c rc11.cat	0.0	86	159	381	626
	1.9	1.8	6.1	5.7	15.5
harris-3.c imm.cat	0.0	58	68	395	521
	2.0	1.9	3.7	5.0	12.6
wsq.c rc11.cat	0.0	4.0	16.8	8.2	29.0
	0.2	0.2	1.0	0.6	2.0
wsq.c imm.cat	0.0	4.5	12.6	6.7	23.8
	0.2	0.3	0.7	0.5	1.7

[hernanponcedeleon]

I get the following error

> java -jar dartagnan/target/dartagnan.jar cat/imm.cat benchmarks/locks/ttas.c --wmm.analysis.relationAnalysis=lazy
Test: benchmarks/locks/ttas.c
Result: ERROR
Reason: ClassCastException
Details:
        class com.dat3m.dartagnan.wmm.utils.graph.immutable.ImmutableMapEventGraph cannot be cast to class com.dat3m.dartagnan.wmm.utils.graph.mutable.IndexedEventGraph (com.dat3m.dartagnan.wmm.utils.graph.immutable.ImmutableMapEventGraph and com.dat3m.dartagnan.wmm.utils.graph.mutable.IndexedEventGraph are in unnamed module of loader 'app')

[hernanponcedeleon]

First pass up to IndexedSet.java

[xeren]

I get the following error

> java -jar dartagnan/target/dartagnan.jar cat/imm.cat benchmarks/locks/ttas.c --wmm.analysis.relationAnalysis=lazy
Test: benchmarks/locks/ttas.c
Result: ERROR
Reason: ClassCastException
Details:
        class com.dat3m.dartagnan.wmm.utils.graph.immutable.ImmutableMapEventGraph cannot be cast to class com.dat3m.dartagnan.wmm.utils.graph.mutable.IndexedEventGraph (com.dat3m.dartagnan.wmm.utils.graph.immutable.ImmutableMapEventGraph and com.dat3m.dartagnan.wmm.utils.graph.mutable.IndexedEventGraph are in unnamed module of loader 'app')

Fixed that now.

LazyRelationAnalysis does not yet benefit from the compact sets. Once it does, it may still out-perform NativeRelationAnalysis in some large benchmarks. Otherwise, we could remove it.

[hernanponcedeleon]

dartagnan cat/svcomp.cat --method=eager ../sv-benchmarks/c/pthread-complex/elimination_backoff_stack-race.c --wmm.analysis.relationAnalysis=lazy
Test: ../sv-benchmarks/c/pthread-complex/elimination_backoff_stack-race.c
Result: ERROR
Reason: IllegalArgumentException
Details:
        Missing domain for intersection.

[hernanponcedeleon]

I haven't yet checked in detail what you changed in the LAZY RA but there is a regression

> dartagnan -DlogLevel=info cat/svcomp.cat --method=eager ../sv-benchmarks/c/pthread-complex/elimination_backoff_stack-race.c --wmm.analysis.relationAnalysis=lazy
[02.07.2026] 15:10:57 [INFO] EnvironmentInfo.logEnvironmentInfo - Git branch: development
[02.07.2026] 15:10:57 [INFO] EnvironmentInfo.logEnvironmentInfo - Git commit ID: a7e3e4843359dde3a0e29500a821030e2433e316
...
[02.07.2026] 15:11:11 [INFO] RelationAnalysis.fromConfig - Finished regular analysis in 12.988 secs

vs

> dartagnan -DlogLevel=info cat/svcomp.cat --method=eager ../sv-benchmarks/c/pthread-complex/elimination_backoff_stack-race.c --wmm.analysis.relationAnalysis=lazy
[02.07.2026] 15:14:26 [INFO] GitInfo.logGitInfo - Git branch: indexedset
[02.07.2026] 15:14:26 [INFO] GitInfo.logGitInfo - Git commit ID: 9551006b0e8ea81be5b1cb809eccb654e1ec62d5
...
[02.07.2026] 15:15:07 [INFO] RelationAnalysis.fromConfig - Finished regular analysis in 39.260 secs

EDIT: actually, I do not think is a good idea to touch the lazy analysis. The performance of the native one now is so good that probably the main use case for lazy is to check both analyses compute the same results. For that, the current implementation of lazy should be good enough

[xeren]

dartagnan cat/svcomp.cat --method=eager ../sv-benchmarks/c/pthread-complex/elimination_backoff_stack-race.c --wmm.analysis.relationAnalysis=lazy
Test: ../sv-benchmarks/c/pthread-complex/elimination_backoff_stack-race.c
Result: ERROR
Reason: IllegalArgumentException
Details:
        Missing domain for intersection.

Caused by ActiveSetAnalysis, where the new sets were expected. I added some operations to SetUtil, where IndexedSet is preferred, but other sets still work.

I haven't yet checked in detail what you changed in the LAZY RA but there is a regression

> dartagnan -DlogLevel=info cat/svcomp.cat --method=eager ../sv-benchmarks/c/pthread-complex/elimination_backoff_stack-race.c --wmm.analysis.relationAnalysis=lazy
[02.07.2026] 15:10:57 [INFO] EnvironmentInfo.logEnvironmentInfo - Git branch: development
[02.07.2026] 15:10:57 [INFO] EnvironmentInfo.logEnvironmentInfo - Git commit ID: a7e3e4843359dde3a0e29500a821030e2433e316
...
[02.07.2026] 15:11:11 [INFO] RelationAnalysis.fromConfig - Finished regular analysis in 12.988 secs

vs

> dartagnan -DlogLevel=info cat/svcomp.cat --method=eager ../sv-benchmarks/c/pthread-complex/elimination_backoff_stack-race.c --wmm.analysis.relationAnalysis=lazy
[02.07.2026] 15:14:26 [INFO] GitInfo.logGitInfo - Git branch: indexedset
[02.07.2026] 15:14:26 [INFO] GitInfo.logGitInfo - Git commit ID: 9551006b0e8ea81be5b1cb809eccb654e1ec62d5
...
[02.07.2026] 15:15:07 [INFO] RelationAnalysis.fromConfig - Finished regular analysis in 39.260 secs

EDIT: actually, I do not think is a good idea to touch the lazy analysis. The performance of the native one now is so good that probably the main use case for lazy is to check both analyses compute the same results. For that, the current implementation of lazy should be good enough

I reverted the latest changes.

[xeren]

I do not plan any feature additions to this MR. Something like IndexedMap, more fine-grained event domains, or infix-based compatibility can be added later, if the need arises.

[hernanponcedeleon]

These are the latest results on SVCOMP benchmarks

Category	Branch	Total CPU Time (s)	Total Solved Tasks	Avg Time per Task (s)	Performance Improvement (%)
unreach-call	MR	15700	470	33.40	13.78%
unreach-call	Development	17900	462	38.74	-
no-data-race	MR	19300	699	27.61	15.80%
no-data-race	Development	22300	680	32.79	-
valid-memsafety	MR	16700	480	34.79	14.04%
valid-memsafety	Development	19100	472	40.47	-
no-overflow	MR	14900	431	34.57	15.77%
no-overflow	Development	17400	424	41.04	-

I am fine with the current version of the code, so unless @ThomasHaas has further comments, I think we can merge

[ThomasHaas]

I haven't checked the code in detail, but I think it is fine overall and the tests show it is correct as well. We can merge.