In this section, we outline how the output is obtained to give a flavor of the kinds of simplifications and reductions that are possible in the answer constraints.
Functor equations are handled first, and in much the same way as in PROLOG. The constraints are stored in solved form using bindings, and printing the simplest form of each target variable simply involves printing their term representation. For example
?- X = f(Y, Z), Z = g(a, Y), dump([X, Y]).
results in the output
X = f(Y, g(a, Y)).
Note that there is no equation for Y since it is its own term representation. With functor equations, it is not always possible to present the output in terms of target variables alone, and some non-target variables are printed out using an internal name. For example,
?- X = f(Y, Z), Z = g(a, Y), dump([X]).
results in an output such as
X = f(_h6, g(a, _h6)).
Linear equations are used to substitute out non-target variables in the following manner. If E is a linear equation containing non-target variable X, then we rewrite E into the form X = t and substitute t for X in all the other constraints (including functor equations, inequalities and non-linear equations). Consider, for example
?- T = 3 + Y, X = 2 * Y + U, Z = 3 * U + Y, dump([X, T, Z]).
First, we eliminate Y using the first equation Y = 3 - T and obtain
X = 2 * T - 6 + U, Z = 3 * U + T - 3.
Then we eliminate U using the the first equation and obtain
Z = 3*X - 5*T + 15.
This is the final answer since only the variables X, T and Z remain.
Linear inequalities are more difficult to handle than linear equations. We will not go into the details of how variables can be eliminated from inequalities except to mention that a variation of Fourier-Motzkin elimination [19] with some improvements is used (see [11] for more details). In general, eliminating variables from inequalities can be expensive and the projection can contain an exponential number of inequalities.
We finally deal with the nonlinear equations.
In general, the algorithm here simply outputs each
nonlinear equation unless it has been used as a substitution.
We will not define formally what exactly constitutes a substitution,
but will discuss some examples.
Recall that each non-linear constraint takes the form
or X = abs(Y). Each of these equations can be used
to substitute for X if X is a non-target variable.
For example,
?- Y = sin(X), Y = cos(Z), dump([X,Z]).
leads to the output
sin(X) = cos(Z).
As in the case for functor equations, we cannot in practice eliminate all non-target variables appearing in non-linear constraints. As before, we display any non-target variable using an internal name.
A Complete Example
Consider the goal
?- X = f(V, M), V = a, N = 2 * T, Y = 4 * T, Z = R + T, M = N * R,
Y + Z >= U, U > T, U >= R + N,
dump([X, Y, Z]).
First we eliminate V by substitution obtaining
X = f(a, M), N = 2 * T, Y = 4 * T, Z = R + T, M = N * R,
Y + Z >= U, U > T, U >= R + N
Next we eliminate N using the second constraint obtaining
X = f(a, M), Y = 4 * T, Z = R + T, M = (2 * T) * R,
Y + Z >= U, U > T, U >= R + 2 * T
Next we eliminate T using the second constraint obtaining
X = f(a, M), Z = R + 0.25 * Y, M = (0.5 * Y) * R,
Y + Z >= U, U > 0.25 * Y, U >= R + 0.5 * Y
Next we eliminate R using the second constraint obtaining
X = f(a, M), M = (0.5 * Y) * (Z - 0.25 * Y),
Y + Z >= U, U > 0.25 * Y, U >= Z + 0.25 * Y
Next we eliminate U from the inequalities (and here the individual steps taken may not be so obvious), obtaining
X = f(a, M), M = (0.5 * Y) * (Z - 0.25 * Y),
0.75 * Y + Z > 0, 0.75 * Y >= 0
Finally, we eliminate M using the second constraint, and as output we obtain (after performing some straightforward scaling) the constraints
X = f(a, (0.5 * Y) * (Z - 0.25 * Y)),
0 < Z + 0.75 * Y,
0 <= Y
We finally remark that we can obtain an empty output using the algorithm just outlined. This indicates that there are no restrictions on the values that the target variables can take. For example,
?- T = 3 + Y, X = 2 * Y + U, Z = 3 * U + Y, dump([X, Z]).
results in no constraints at all. In such cases, the distinguished predicate real/1 is then used to indicate that certain variables are arithmetic, and that no further constraints are upon them. In this example, we will output the constraints
real(X), real(Z).