fix(arith): Do not overly tighten bounds over infinite domains

[bclement-ocp]

Model generation for arithmetic constraints proceeds in two stages:

• In the first stage, we only choose a value for variables that are within a finite domain (i.e. integer variables bounded from both above and below). This is the behavior of regular case splits, and happens in function default_case_split.

• In the second stage, which we only reach if model generation is enabled, we must select a value for all variables. In this case, we select one interval for variables that can have multiple intervals (recall that we model arithmetic domains using unions of intervals). This happens in function case_split_union_of_intervals. If the selected interval is finite, we go back to the first stage in the next case split.

• In the final stage, all remaining variables have infinite intervals as domains, and we must now pick a value for these. This happens in model_from_unbounded_domains -- even though for rational variables, the domain can still be bounded. For integers however, infinite intervals mean that they lack either a finite lower or upper bound (or both). For integers, we create a new simplex environment in fm_simplex_unbounded_integers_encoding where we adjust the bounds by a factor of half the sum of the absolute values of the coefficients. This means that an inequality 0 < 3x + 4y becomes 0 + (3 + 4) / 2 < 3x + 4y, i.e. 3.5 < 3x + 4y. This removes x = 1, y = 0 from the domain. On its own, this would be correct (albeit strange) because after removing a finite number of elements from an infinite domain there is still an infinite number of elements to choose from. But within a larger system this can (and is) problematic.

This patch removes the "adjustment" of the bounds which is not justified and actually causes unsoundness.

Fixes #1022

[bclement-ocp]

Great, we don't have the same model for OCaml 4.14.0 and 5.0.1… or with/without the weak table :/

@Halbaroth any progress on #790 ? 😅

(Although I don't really understand what is impacted by the weak table here… there are no disjunctions or quantifiers in the problem, and yet we choose x1 first with --disable-weak and x3 first without?)

[Halbaroth]

#790 is stuck because we use custom function as ae.round in our models and Dolmen rejects them because it doesn't know this value.

I also implemented get-value but it doesn't work with optimization because of #1023 :D

[bclement-ocp]

#790 is stuck because we use custom function as ae.round in our models and Dolmen rejects them because it doesn't know this value.

There are no ae.round in the expected models though, so that shouldn't be an issue?

I also implemented get-value but it doesn't work with optimization because of #1023 :D

👍 although that shouldn't block using Dolmen to check the models on CI

(I am now thinking that maybe I did not link the correct issue, I was thinking of the one about using Dolmen to check models on the CI instead of comparing models textually)

[bclement-ocp]

OK, the main cause of the discrepancy is because we use hash_cmp to define the simplex variables here which in turn means that the weak table impact the solution we get from the simplex, which can cause large discrepancies in the output.

Using str_cmp here stabilizes the result for this new test case, and it might improve stability generally — hopefully without impacting performance too much. I will do a test run with str_cmp for the simplex variables to see what happens.

[Halbaroth]

There are no ae.round in the expected models though, so that shouldn't be an issue?

You're right. I meant there is such functions in the input problem, thus Dolmen cannot evaluate them to check the model because it doesn't know an interpretation of these functions.

[Halbaroth]

I think we should rename model_from_unbounded_domains to model_from_infinite_domains ;)

But within a larger system this can (and is) problematic.

Can you explain? It look sound to remove finitely many elements of an infinite set. Besides, do you have any clue on the reason of this strange code?

[bclement-ocp]

I think we should rename model_from_unbounded_domains to model_from_infinite_domains ;)

Done.

Can you explain? It look sound to remove finitely many elements of an infinite set. Besides, do you have any clue on the reason of this strange code?

The propagators are not complete. Assume you have x > 0 and also x ** 1 = 1; the exponentiation is not a linear function and so we cannot reason about it within the simplex; removing 1 from the domain of x would be unsound because x = 1 is the only solution of x ** 1 = 1.

[bclement-ocp]

do you have any clue on the reason of this strange code?

Also: not really, unfortunately :( We discussed it with @Gbury but could not figure out either a logical justification or practical interest for doing this, it just looks like a misguided attempt to do an (incorrect) simplifying cut.

[Halbaroth]

Ok, I'll merge your PR if the benchmarks are okay after changing the comparison function ;)

[bclement-ocp]

Removed the additional tests after the discussion at the dev meeting (see also here); should be ready for a 2nd round.