Skip to content

fix(pumpkin-propagators): Make integer multiplication bounds(R) consistent - #517

Open
maartenflippo wants to merge 13 commits into
mainfrom
fix/bounds-consistency-multiplication
Open

fix(pumpkin-propagators): Make integer multiplication bounds(R) consistent#517
maartenflippo wants to merge 13 commits into
mainfrom
fix/bounds-consistency-multiplication

Conversation

@maartenflippo

Copy link
Copy Markdown
Contributor

Actually do the case-distinction to finally get our multiplication to be bounds(R) consistent.

@ImkoMarijnissen ImkoMarijnissen left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Overall, this looks good, but I have some questions. It would also be nice to see some experimentation with the impact on benchmarks.

Comment thread pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs Outdated
Comment thread pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs Outdated
Comment thread pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs Outdated
Comment thread pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs Outdated
Comment thread pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs Outdated
Comment thread pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs Outdated
Comment thread pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs Outdated
Comment thread pumpkin-crates/propagators/src/propagators/arithmetic/integer_multiplication.rs Outdated
@maartenflippo
maartenflippo force-pushed the fix/bounds-consistency-multiplication branch from 5a1e617 to dfae0bf Compare July 29, 2026 19:08
@github-actions
github-actions Bot dismissed ImkoMarijnissen’s stale review July 30, 2026 06:40

Review re-requested

@ImkoMarijnissen ImkoMarijnissen left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some small changes, but I think it can be merged

Comment on lines +137 to +138
/// In order, for each bound it is dropped if, when relaxing it, the `bound_fn` still justifies the
/// propagation we are explaining. Every bound that is deemed necessary is appended to `buffer`.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How about more something like this?

It is checked (in order) whether removing the bound from the explanation for the propagation still leads to a valid explanation (using bound_fn to calculate the possible bounds). The predicates necessary for a valid explanation are added to buffer.

Note - This leads to a subset minimal explanation (i.e., no element can be removed for it to still be a valid explanation), and not a cardinality minimum explanation.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants