search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
131 stars 33 forks source link

fix(CP): Remove `ex` parameter from `Domain.intersect` #1112

Closed bclement-ocp closed 4 months ago

bclement-ocp commented 4 months ago

Adding an explicit ex parameter to the Domain.intersect signature was intended to make it behave more like an update and avoid issues such as #479. The other intent was to be a bit more efficient by avoiding additional add_explanation calls.

Given that I made this design yet have now introduced the same soundness issue twice because of it, it is now clear that this was not a good idea.

This patch reverts that design decision and the ex parameter in the Domain.intersect API, replacing it with explicit calls to add_explanation instead.

bclement-ocp commented 4 months ago

Given that I made this design yet have now introduced the same soundness issue twice because of it, it is now clear that this was not a good idea.

To clarify: this is what I am talking about.

Halbaroth commented 4 months ago

Is ADT theory exposed to same risk? Because we use the previous API for their domains.

bclement-ocp commented 4 months ago

We can make the same change in the enum/ADT theories yes.

(Note that I don't think there are soundness issues on next related to this currently; the soundness issue I mention is related to integration of the Intervals API that does not add explanations on intersection. But arguably the API here is weird: the explanation does not justify that "the intersection is valid" -- whatever that means -- ; rather it justifies that one of the domain applies to a specific variable and that should be reflected by a call to add_explanation).