Linearity and Nonlinear Residues

The clp(Q,R) system is restricted to deal with linear constraints because the decision algorithms for general nonlinear constraints are prohibitively expensive to run. If you need this functionality badly, you should look into symbolic algebra packages. Although the clp(Q,R) system cannot solve nonlinear constraints, it will collect them faithfully in the hope that through the addition of further (linear) constraints they might get simple enough to solve eventually. If an answer contains nonlinear constraints, you have to be aware of the fact that success is qualified modulo the existence of a solution to the system of residual (nonlinear) constraints:

     clp(r) ?- {sin(X) = cos(X)}.
     
     clpr:{sin(X)-cos(X)=0.0}
     
There are indeed infinitely many solutions to this constraint (X = 0.785398 + n*Pi), but clp(Q,R) has no direct means to find and represent them.

The systems goes through some lengths to recognize linear expressions as such. The method is based on a normal form for multivariate polynomials. In addition, some simple isolation axioms, that can be used in equality constraints, have been added. The current major limitation of the method is that full polynomial division has not been implemented. Examples:

This is an example where the isolation axioms are sufficient to determine the value of X.

     clp(r) ?- {sin(cos(X)) = 1/2}.
     
     X = 1.0197267436954502
     

If we change the equation into an inequation, clp(Q,R) gives up:

     clp(r) ?- {sin(cos(X)) < 1/2}.
     
     clpr:{sin(cos(X))-0.5<0.0}
     

The following is easy again:

     clp(r) ?- {sin(X+2+2)/sin(4+X) = Y}.
     
     Y = 1.0
     

And so is this:

     clp(r) ?- {(X+Y)*(Y+X)/X = Y*Y/X+99}.
     
     {Y=49.5-0.5*X}
     

An ancient symbol manipulation benchmark consists in rising the expression X+Y+Z+1 to the 15th power:

     clp(q) ?- {exp(X+Y+Z+1,15)=0}.
     clpq:{Z^15+Z^14*15+Z^13*105+Z^12*455+Z^11*1365+Z^10*3003+...
            ... polynomial continues for a few pages ...
            =0}
     

Computing its roots is another story.