# Why MiniZinc do not do convert to linear constraint a quadratic constraint?

I would like to know which are the advantage to do not convert quadratic expressions into linear expression in MiniZinc. For example let be the following simple MiniZinc code

var -1.0..1.0:  x1;
var -1.0..1.0:  y1;
constraint (x1*y1) = 1.0;
solve satisfy;


The flatzinc code of that portion of code is

var -1.0..1.0: x1:: output_var;
var -1.0..1.0: y1:: output_var;
var -1.0..1.0: X_INTRODUCED_0_ ::var_is_introduced :: is_defined_var;
constraint float_eq(X_INTRODUCED_0_,1.0);
constraint float_times(x1,y1,X_INTRODUCED_0_):: defines_var(X_INTRODUCED_0_);
solve  satisfy;


As you can see, the quadratic term x1*y1 is still quadratic float_times(x1,y1,X_INTRODUCED_0_). Why MiniZinc does not convert x1*y1 to linear constraints?

MiniZinc does not convert x1 * y1 = 1 to a linear constraint because x1 * y1 = 1 cannot be represented by a linear constraint.
• +1 If you allow an addition binary variable, I believe you can linearize the constraint given the variables are required to be between -1 and 1: $x_1+y_1=4z-2$ where $z$ is binary. If the product of $x_1$ and $y_1$ should be one, they should both be 1 or $-1$. Hence, their sum should be either $2$ or $-2$.