Add possibility of divisor spanning zero

[snedeljkovic]

What language and solver does this apply to?
Python, CP-SAT

Describe the problem you are trying to solve.
I'm modelling abstract syntax trees for symbolic computation.

Describe the solution you'd like
As in the name of the request I'd like the possibility of the divisor to span across zero.

Describe alternatives you've considered

Additional context
Add any other context or screenshots about the feature request here.

[lperron]

Noted.

It will not happen soon.

You can emulate it by looking at:

or-tools/ortools/sat/cp_model_expand.cc

Line 255 in b37d9c7

void ExpandIntProdWithOneAcrossZero(int a_ref, int b_ref, int product_ref,

Roughly speaking,

divide the domain of the divisor in 2 (< 0, >0). Create one BoolVar b, link it to the 2 side of the domains.
Create 2 temp divisor variables (pos_div, neg_div), 2 temp target variable (pos_target, neg_target).

b implies divisor > 0
b implies pos_divisor == divisor
b implies neg_divisor == -1  # or max of the negative part of the divisor domain
add_division_equality(pos_target, numerator, pos_divisor)

not(b) implies divisor < 0
not(b) implies neg_divisor == divisor
not(b) implies pos_target == 1  # or min of the positive part of the divisor domain
add_division_equality(neg_target, numerator, neg_divisor)

link it all together

b implies target == pos_target
not(b) implies target == neg_target

[snedeljkovic]

Thanks, Laurent!

[lperron]

I have just pushed the code for that.

Never too late :-)