SWI-Prolog stack limit exceeded with tiny problem space using clpfd

Question

I try to show a minimal example for this behaviour. This is the code I load:

:- use_module(library(clpfd)).

gcd(A, 0, A) :- !.
gcd(0, B, B) :- !.
gcd(A, B, C) :- A #> B, !, A1 #= A mod B, gcd(A1, B, C).
gcd(A, B, C) :- A #=< B, A1 #= B mod A, gcd(A1, A, C).

ncalc(N, X, Y) :-
    Y #=< N,
    X*X #= (Y),
    X #< Y,
    X #> 0,
    gcd(X, Y, 1).

Querying ncalc(9, X, Y). I get:

ERROR: Stack limit (1.0Gb) exceeded
ERROR:   Stack sizes: local: 1Kb, global: 0.7Gb, trail: 9Kb
ERROR:   Stack depth: 1,548,057, last-call: 100%, Choice points: 5
ERROR:   In:
ERROR:     [1,548,057] clpfd:pop_queue(_176712142, <compound fast_slow/2>, 1)
ERROR:     [1,548,056] clpfd:pop_queue(_176712170)
ERROR:     [1,548,055] clpfd:fetch_propagator(_176712188)
ERROR:     [1,548,054] clpfd:do_queue
ERROR:     [1,548,052] clpfd:parse_clpfd('<garbage_collected>', _176712222)
ERROR:
ERROR: Use the --stack_limit=size[KMG] command line option or
ERROR: ?- set_prolog_flag(stack_limit, 2_147_483_648). to double the limit.

Querying ncalc(8, X, Y). immediatley returns false.. Querying ncalc(9, 1, Y). through ncalc(9, 8, Y). (all possible valid ranges for X) too. Why does it only work for the simpler cases? Is there a workaround for this? Thanks!

PS: I'm new to prolog and what I plan to do is more complex, but knowing a workaround for this I can probably adapt the solution.

Answer 1

(Let's ignore programming style, see @Capelli's comment for that.)

The actual source of non-termination is due to a weakness in SWI's CLP(FD) system. Here is the actual culprit:

?- X in 2..3, Y in 4..9, Y mod X#=X1.
X in 2..3,
Y mod X#=X1,
Y in 4..9.

So the system is not capable of deducing any useful information for X1. Contrast this to SICStus:

| ?- X in 2..3, Y in 4..9, Y mod X#=X1.
Y mod X#=X1,
X in 2..3,
Y in 4..9,
X1 in 0..2 

Here SICStus deduced that X1 must be within 0..2 and thus not negative. This in turn avoids the loop in question in the next inference.

You can help the system a bit by insisting on non-negative numbers and thus the module is always smaller than the operands.

A1 #>= 0, A1 #=< B, A1 #=< A

In the meantime fixed in CLP(Z).