ConSol-Lab / Pumpkin

A lazy clause generation constraint solver written in Rust.
Apache License 2.0
18 stars 5 forks source link

feat: adding option to force incremental cumulative propagators to find the same trace as non-incremental #86

Closed ImkoMarijnissen closed 3 weeks ago

ImkoMarijnissen commented 3 weeks ago

It is difficult to compare the different types of changes made to the cumulative due to the fact that traces oftentimes diverge due to differences in the explanation(s)

This PR addresses this issue by creating a synchronisation between the incremental and the non-incremental version of the time-tabling propagators by ensuring that the explanations for the conflicts and the propagations are the same as would be found by the non-incremental propagator and the incremental version of the propagator.

For both the per-point reasoning and the over-interval reasoning, a synchronisation module is created which finds the correct conflicts and orders the profile tasks in the profile in the correct order!

Edit: After discussion with @maartenflippo, this PR now also contains a new crate which contains procedural macros; these are currently used to create test cases for the cumulative where we want to test a lot of combinations of tests!