Replacement rule candidates for single-occurrence variables

[chriseth]

Note that all the following rules have a non-local condition of the form "a variable does not occur in any other part of the system".

Candidate 1:

Pattern:
X * DI1 + Y * DI2 = C

Conditions:

1. DI1 and DI2 are two different variables that do not occur anywhere else in the system, also not inside X, Y or C (i.e. it would also be OK for them to be expressions as long as it is possible to assign any value to them. For example, any affine expression would work)
2. 0 <= X < MODULUS / 2, 0 <= Y < MODULUS / 2

Replacement:

(X + Y) * DI = C
[DI is a new variable]

Notes:

C can be an expression, so this can be iterated to apply it to larger sums

Candidate 2:

(square X if it is not non-negative)

Pattern:
X * DI1 + Y * DI2 = C

Conditions:

1. DI1 and DI2 are two different variables that do not occur anywhere else in the system, also not inside X, Y or C (i.e. it would also be OK for them to be expressions as long as it is possible to assign any value to them. For example, any affine expression would work)
2. -\sqrt(MODULUS) / 2 <= X < \sqrt(MODULUS) / 2,
3. 0 <= Y < MODULUS / 2

Replacement:

(X * X + Y) * DI = C
[DI is a new variable]

Note: We can iterate this if Y is the result of the previous run. But for that to work, we need to be able to reason that the
range constraint of a square is non-negatve.

Candidate 3:

(square both X and Y)

Pattern:
X * DI1 + Y * DI2 = C

Conditions:

1. DI1 and DI2 are two different variables that do not occur anywhere else in the system, also not inside X, Y or C (i.e. it would also be OK for them to be expressions as long as it is possible to assign any value to them. For example, any affine expression would work)
2. -\sqrt(MODULUS) / 2 <= X < \sqrt(MODULUS) / 2, -\sqrt(MODULUS) / 2 <= X < \sqrt(MODULUS) / 2

Replacement:

(X * X + Y * Y) * DI = C
[DI is a new variable]

Candidate 4:

Pattern:
(1 - C) * (A + B - A * B) = 0
V * (A + B - A * B) - C = 0

Conditions:

1. V only occurs here
2. A, B, C are binary

Replacement:
(1 - C) * (A + B - A * B) = 0
A + B - A * B - C = 0

Note: It would work the same way for an expression X such that we have (1 - C) * X = 0 and V * X - C = 0. The issue is that we crurrently cannot determine that A + B - A * B is boolean if A and B are boolean. Although this might be the case inside the solver after linearization.