Alternate equality logic theory solver. #199

matthiasgreen · 2025-09-12T13:17:59Z

An alternate equality logic theory solver. Less memory-intensive than the SplitEqTheory solver for sparse problems. Currently used in parallel with the STN. Can be activated using the ARIES_USE_EQ_LOGIC environment variable.

This branch is currently rebased onto the feature/coloring branch since I used it for profiling. I therefore opened the pull request onto the feature/coloring branch.

…rove propagation and checking

…ethod chaining api

solver/src/collections/ref_store.rs

solver/src/collections/set.rs

solver/src/core/state/domains.rs

solver/src/solver/solver_impl.rs

solver/src/reasoners/eq_alt/theory/mod.rs

matthiasgreen added 30 commits September 12, 2025 14:36

feat(eq): Add Directed Eq/Neq graph with specific algorithms

00c4dd1

feat(eq): Graph edge removal

7bea240

feat(eq): Implement eq propagation

b18484e

fix(eq): handle activation events

e4fc873

fix(eq): Fix and test backtracking

30c562c

fix(eq): Add inference causes

02b7278

refactor(eq): Refactor a couple functions

2caba47

feat(eq): Explain first draft

53c659f

fix(eq): Fix explanations and propagation, first working impl

c1f5ef6

fix(eq): Add stats, change dft to bft, switch to cycle propagation

5d26032

fix(eq): Small improvements

59dd5be

fix(eq): Add correct constraints in solver_impl for eq and neq

7aed0b5

fix(eq): Improve AltEqTheory unit tests

f598dc2

refactor(eq): Reorganize modules

5f607cd

feat(eq): Add propagation checking algorithm

6b0d34e

fix(eq): Improve propagation algorithm

8e2043f

fix(eq): fix infinite loop in path restitution

259c98f

fix(eq): Remove undecided graph, replace with constraint hashmap, imp…

a01c7f1

…rove propagation and checking

refactor(eq): Simplify generics, remove hashset of undecided props

7f213b1

perf(eq): Greatly improve paths_requiring algorithm

71e3864

perf(eq): Multiple smaller optimisations

59b4107

fix(eq): Fix error with Neq diff expr

1000e09

feat(eq): Replace HashMaps with RefMaps

450b0ca

feat(eq): Add graph statistics

1816877

perf(eq): Improve propagator addition

932637e

perf(ref): Improve ref collection allocation efficiency

cb34988

refactor(eq): Clean up theory

a9b7096

feat(eq): Add id to node map with union-find

80c7295

feat(eq): Rework graph traversal API and handle node groups

5c1651f

test(eq): Improve unit tests

c5bae7b

matthiasgreen added 7 commits September 12, 2025 14:36

refactor(eq): Simplify propagation

1d992a8

perf(eq): Improve propagator handling

c7849b4

refactor(eq): Replace graph subset + fold with graph transform, add m…

184c030

…ethod chaining api

perf(eq): Add reusable scratches for fast graph traversal

f7424b3

doc(eq): Lots of documentation

c0b0312

doc(eq): Finish documentation and clean up

c2933df

chore(eq): Fix CI failures

0e95f51

matthiasgreen requested a review from arbimo September 12, 2025 13:17

matthiasgreen added 2 commits September 15, 2025 13:36

feat(eq): Use BFS for explanations

b31629b

refactor(eq): Small improvements

970b67e