clpz: new loop

[UWN]

?- B=3, C in 1..3,A#=abs(max(B^A,C)),labeling([],[B,C]).
   B = 3, C = 1, clpz:(A in 27..sup), clpz:(A#=abs(_A)), clpz:(3^A#=_A), clpz:(_A in 7625597484987..sup)
;   loops, unexpected.
?- C in 2..3,A#=abs(max(3^A,C)),labeling([],[C]).
   C = 2, clpz:(A in 19683..sup), clpz:(A#=abs(_A)), clpz:(3^A#=_A), clpz:(_A in 1505416___617859227..sup)
;  ... .

(The three _ (underscores) stand for a page full of digits)

To be fair, that is not that much a correctness problem. SICStus just barfs a representation error which is also a not-incorrect response. I am not sure what to do in such a situation, except that I would like to "carry on" my tests.

[UWN]

The manual states

Labeling is always complete, always terminates, and yields no redundant solutions.

Is this still the case here?

[notoria]

By limiting the amount of memory, it crashes. Can you interrupt it (ctrl-C)?

It's possible to make abs/1 a bit stronger but it isn't clear what's the tradeoff.

?- X in 1..sup, Y #= abs(X).
   clpz:(X in 1..sup), clpz:(Y#=abs(X)), clpz:(Y in 1..sup). % old
   X = Y, clpz:(X in 1..sup). % new
?- X in inf.. -1, Y #= abs(X).
   clpz:(X in inf.. -1), clpz:(Y#=abs(X)), clpz:(Y in 1..sup). % old
   clpz:(X in inf.. -1), clpz:(Y+X#=0), clpz:(Y in 1..sup). % new
?-

[notoria]

Similar issue and related to #2279:

?- Y in 1..sup, Z #= 2^Y, Z #< Y.
   clpz:(Y in 9..sup), clpz:(Z#=<Y+ -1), clpz:(2^Y#=Z), clpz:(Z in 512..sup).
?- Y in 1..sup, Z #= 2^Y, Z #< Y, Z #< Y.
thread 'main' panicked at /home/begin/.cargo/registry/src/index.crates.io-6f17d22bba15001f/dashu-int-0.4.0/src/error.rs:15:5:
out of memory
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Nonlinear computation that grows too fast maybe should be avoided (the bound of Z).

[UWN]

The inference limit does not help much, space is out much too early:

?- call_with_inference_limit((A#=max(2,max(A,A^A))),8500,R).
Killed
5.235u 12.181s 0:25.13 69.2%    0+0k 15816+16io 113pf+0w

Yes, a clean resource error would help, #16

[notoria]

But putting a bound on Z helps:

?- ZU #= 2^1024, Z #= B^A, Z in 0..ZU, B=3, C in 1..3,A#=abs(max(Z,C)),labeling([],[B,C]).
   false.
?- ZU #= 2^1024, Z #= A^A, Z in 0..ZU, A#=max(2,max(A,Z)).
   false.
?-

The only part that could change to help the first query is abs/1.

[UWN]

There are so many cases where everything works as expected, even

?- A#>max(2,A^A^A).
   clpz:(A in 3..sup), clpz:(A#>=_A), clpz:(A^_B#=_C), clpz:(A^A#=_B), clpz:(_A in 7625597484988..sup), clpz:(_C+1#=_A), clpz:(_C in 7625597484987..sup), clpz:(_B in 27..sup).

Note that here clpz stops for the sake of preferring termination over consistency. SICStus here produces its representation error which tells us also nothing about the truth. But hey, at least are not incorrect.

The original motivation for favoring termination were simple beginners' programs that did not terminate and where a failure slice was used to explain non-termination. In fact, a minimal failure slice is searched for. So programs involving X #= X-1 and some X#>0. In the meantime systems (= SICStus and clpz) are bit smarter, but not everywhere.