search

plaans / aries

Toolbox for automated planning and combinatorial solving.
MIT License
43 stars 7 forks source link

Feat: up plus & minus #111

Closed Shi-Raida closed 10 months ago

Shi-Raida commented 10 months ago

Add support for up:plus and up:minus operators.

Converts IntCst from i32 into i64 in order to fix overflow issues on LinearSumLeq propagation. The bounds of the sum's terms are clamped into the set_ub method.

NOTE: It was not possible to have INT_CST_MIN = i64::from(i32::MIN) - 1 (same for INT_CST_MAX) since the result is not a constant anymore. Therefore, I hard coded the value of the i32::MIN constant.

arbimo commented 10 months ago

@Shi-Raida It looks for the first part but the change to use i64 should only be internal to the linear propagator. So domains should still be represented with 32 bits (IntCst does not change) but your local copy should be 64 bits. When updating the domains, the 64bits numerals should be clamped and converted to i32.

As implemented, this would have drastic performance implications as the size of a literal would be 128bits (instead of 64), which means it cannot be manipulated as a single machine word. It would also ~double the memory footprint of the solver and negatively impact cache behavior.

Shi-Raida commented 10 months ago

@Shi-Raida It looks for the first part but the change to use i64 should only be internal to the linear propagator. So domains should still be represented with 32 bits (IntCst does not change) but your local copy should be 64 bits. When updating the domains, the 64bits numerals should be clamped and converted to i32.

As implemented, this would have drastic performance implications as the size of a literal would be 128bits (instead of 64), which means it cannot be manipulated as a single machine word. It would also ~double the memory footprint of the solver and negatively impact cache behavior.

Everything should be fine now.