Safening of partial functions

[IgnaceBleukx]

Started on a safening transformation for partial functions.
Largely based on

Frisch, Alan M., and Peter J. Stuckey. "The proper treatment of undefinedness in constraint languages." International Conference on Principles and Practice of Constraint Programming. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009.

but some trickery was required for div as we do not allow domains with a hole in it.

For now, this is quite dumb: no care is taken to the context of an expression, nor whether it is top-level.

For example, arr[x] == 2 will be safened and thus introduce a bunch of extra variables/constraints.
I think it's reasonable to leave this expression "unsafe" and just let the solver to its thing with it (TODO).

BUT, in the case of division it's more tricky, as the actual API of e.g., OR-Tools does not accept 0 in the denominator's domain.
So for that one, we actually do need safening at toplevel... (hence I did it this way for now)
A solution to this is to also introduce a supported list for this transformation but it feels quite hacky...

This PR only includes safening for div and Element, but the same can be implemented for mod I believe.

[tias]

@IgnaceBleukx @Wout4
I've rewritten the function documentation to structurally describe why, what and how we do this.

Please revise just the text in the comment, see if we can get that right.

(small clean-ups/renamings/reorderings to the code will follow from getting the description right)

[tias]

I wrote out the 'why' part a bit more explicitly.

Following the text, I think we should not 'safen' top-level expressions. If solvers like ortools want to be picky and not even allow a '0' in the domain for div, then within the solver interface we should detect that and call the relevant safen function there (or safen that specific constraint there knowing that the nearest boolean context is true)?
All other solvers will simply implement strict semantics and propagate the unsafe value away, correct?

[tias]

I restructured the code following the explanation in comments.

There is one mismatch... in the explanation, I wrote about a 'guard'; however, in the safen functions, we don't really introduce a guard/guard conditions... its more like a flag, and we use that flag for multiple things.
e.g. in safen_range, we write ((unsafe_arg >= lb) & (unsafe_arg <= ub)).implies(is_safe), so implication so not the definition of a 'guard' more a 'condition'... is this on purpose? should we rewrite the explanation? or the code? (e.g. the is_safe == (safe_arg == unsafe_arg) part?)

[tias]

The alternative would be:

    toplevel = [is_safe == ((safe_lb <= unsafe_arg) & (unsafe_arg <= safe_ub)),  # the guard
                       is_safe.implies(safe_arg == unsafe_arg),
                       # avoid additional solutions when new var is unconstrained (should always work because newly defined?)
                       (~is_safe).implies(safe_arg == safe_lb)]

which seems intuitive, but some (even toplevel) tests are failing with this.

(some tests were already failing before too)

[tias]

I went through the Frisch and Stuckey paper again. Ignace implementation followed that paper's rewrite faithfully. But they didn't provide much of a constructive explanation of why this is the right rewrite.
I now rewrote the explanation at the top and the implementation with an (imho) intuitive explanation of the rewrite rule, also giving all the newly introduced variables a semantic name. It differs slightly from the rewrite of Frisch and Stuckey but should be logically equivalent.

Please proofread.

I also added an intuitive example and explanation of the side-effects of this transformation, that b <-> ~(partial==5) and `b <-> (partial!=5) mean different things. Wrt impact on us I think this exposes one thing: in the fuzztester, we are not allowed to do semantic fusion on partial functions... because it changes the semantics (e.g. if we fuze a toplevel expression with a partial expression used in a reified context, we are changing the semantics of both...)
@Wout4 do you agree? That means we either need to make sure our 'seeds' are totalized first; or we need to check in semantic fusion that the selected numerical exprs are not partial...

Also, I think the implementation for toplevel partials was incomplete, nbc was not added to toplevel. However, I believe we should NOT do the rewrite for toplevel exprs, as for that case its the strict semantics anyway (unless all solvers don't accept 0 in div/mod like ortools does? seems to be more its design choice?)

[Wout4]

good point on the fuzzing, I think we can do a check to only fuse safe expressions.
Although our fusion functions are non-boolean, so we are not changing any of the boolean contexts that contain the partial functions. Maybe there won't be a problem

[IgnaceBleukx]

Took me a while to get the more elaborate code of safen_hole. In my version the Boolean variables were not created explicitly but logically it seems equivalent and probably avoids generation of extra variables downstream.

(Side thought: when we do CSE, we should also test whether the negated expr already exists in the store!)

Toplevelness

I modified the behaviour of the transformation to act differently when toplevel. Essentially, we don't safen whenever the neirest Boolean context is toplevel, except when asked for it explicitly in the function args.

This was needed for both OR-Tools (due to the API) and Z3 (due to underspecification of div)
https://microsoft.github.io/z3guide/docs/theories/Arithmetic/#division
so -1 / 0 == 1 would have been allowed...

Fuzz testing

Regarding the semantic fusion in our fuzz-tester, we certainly cannot fuse unsafe expressions...
Assume we have two constraints b == (x / 0 == 3) and max(p,q,r) == 10 and we fuse x / 0 and pto a new variablezwithz = (x / 0) + p`. Then the resulting constraints will become:

b == ((z - p) / 0)  == 3 # fine
max(z - (x / 0), q,r) == 10) # NOT FINE

So the model will always be UNSAT... So here we are changing the Boolean context of the unsafe expression...