Which method MiniZinc uses to decrease terms of degree > 2 to quadratic terms?

Question

I would like to know which methods/algorithms MiniZinc uses to decrease terms of degree > 2 to quadratic terms. For example in the following code

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

The flatzinc code is

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

As you can see two new variables a constraints were introduced here. Which methods/algorithms support this conversion? Is there any loss using those methods/algorithms?

Answer 1

It's not a particular method or algorithm. The reformulation just lifts out bilinear terms and replaces them with a new variable:

(x1*y1*z1) = 1.0

# into 

x1 * y1 = a
a  * z1 = b
b       = 1.0

The problems are equivalent, so it's not making the problem easier to solve (there is still non-convex quadratic equality constraints). The reformulation might be needed if the solver supports quadratic terms but not higher powers.

This is related to your other question: Why MiniZinc do not do convert to linear constraint a quadratic constraint?