mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-01-10 13:18:04 -05:00
7012abc5c8
Reproduces the issue that is blocking #2863. We should probably fix this in a separate PR, but here is some information about why it doesn't work: - At some point, the solver tries to do exhaustive search on the flags, as it should. Doing so, [this constraint](42f75af3b7/constraint-solver/tests/solver.rs (L410-L420)) fails for 10 / 14 possible assignments, so the number of possible assignments is reduced, but the assignment is not unique. - Currently, exhaustive search does nothing if the assignment is not unique ([source](42f75af3b7/constraint-solver/src/solver/exhaustive_search.rs (L97))). - If it had continued each of the 4 possible assignments, it would have figured out that in all of them [this constraint](42f75af3b7/constraint-solver/tests/solver.rs (L423-L430)) leads to `is_load = 1`. - Therefore, even though there is no unique assignment for the flags, there is a unique assignment for `is_load`. Ideas on how to make the test pass: - One (expensive) way to fix that is to do proper backtracking: Given the 4 possible assignments, we could run the solver on each of them and intersect the resulting assignments. This would leave us with the unique `is_load = 1` assignment. - For a more light-weight solution, notice that [this constraint](42f75af3b7/constraint-solver/tests/solver.rs (L423-L430)) is of the form `is_load = <expr>` where `expr` only depends on the flags. So given any of the 4 possible assignments, this constraint reduces to `is_valid = 1` immediately. So, instead of just asking if the constraint is conflicting, one could extract such "trivial" assignments and check if they are unique.