Boolean linear expression results in `int_lin_le`

[Dekker1]

The following MiniZinc model

array[1..3] of var bool: bs;

constraint sum(i in 1..3) ( i * bs[i] ) < 5;

results in the following FlatZinc model when compiled using the standard library:

array [1..3] of int: X_INTRODUCED_11_ = [1,2,3];
var bool: X_INTRODUCED_0_;
var bool: X_INTRODUCED_1_;
var bool: X_INTRODUCED_2_;
var 0..1: X_INTRODUCED_3_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_4_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_7_ ::var_is_introduced :: is_defined_var;
array [1..3] of var bool: bs:: output_array([1..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_];
constraint int_lin_le(X_INTRODUCED_11_,[X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_7_],4);
constraint bool2int(X_INTRODUCED_0_,X_INTRODUCED_3_):: defines_var(X_INTRODUCED_3_);
constraint bool2int(X_INTRODUCED_1_,X_INTRODUCED_4_):: defines_var(X_INTRODUCED_4_);
constraint bool2int(X_INTRODUCED_2_,X_INTRODUCED_7_):: defines_var(X_INTRODUCED_7_);
solve  satisfy;

Instead I would have expected bool_lin_le instead of int_lin_le. Making the integer variable and their bool2int channeling constraint redundant.

[MaxOstrowski]

I think to be complete, you would need to add:

predicate bool_lin_eq(array [int] of int: as, array [int] of var bool: bs, var int: c);
predicate bool_lin_ne(array [int] of int: as, array [int] of var bool: bs, var int: c);
predicate bool_lin_le(array [int] of int: as, array [int] of var bool: bs, var int: c);

Currently, I do not think that there is a way to express r -> (a_1*b_1 + ... + a_n*b_n != c where r, b[] are var bool, a[] is int and c is var int.

This should then be translated to bool_lin_ne_imp

[Dekker1]

I'm not sure if that should be part of this Issue. There is something to be said for a special case when only one variable is integer, but in the current scheme the idea would just be that we would create integer linear expression in that case. So

r -> (a[1]*b[1] + ... + a[n]*b[n] != c) where r, b[] are var bool, a[] is int and c is var int. Would become int_lin_ne_imp(a++[-1], b++[c], 0, r)`.

It would then be up to the solver library to detect that there is only 1 real integer variable and use special handling. If there are enough solvers that could benefit from this special handling, then maybe we can adjust the compiler to output these special forms.

According to the FlatZinc spec, these would also need different names since FlatZinc functions should not be overloaded.

[MaxOstrowski]

There is something to be said for a special case when only one variable is integer, but in the current scheme the idea would just be that we would create integer linear expression in that case.

But this is already the case with the following predicate, described here

predicate bool_lin_eq(array [int] of int: as,
                      array [int] of var bool: bs,
                      var int: c)

I just wondered why you have this special case with eq and not with ne and le.

Edit: And I agree, we should have this special case only for Boolean variables. Edit2: The following cases should be supported

array[1..3] of var bool: bs;
var bool: a;
var bool: b;
var bool: c;
var bool: d;

constraint a -> sum(i in 1..3) ( i * bs[i] ) < 5;
constraint b -> sum(i in 1..3) ( i * bs[i] ) > 5;
constraint c -> sum(i in 1..3) ( i * bs[i] ) = 5;
constraint d -> sum(i in 1..3) ( i * bs[i] ) != 5;