clpfd: incompleteness

[UWN]

ulrich@p0:/opt/gupu/scryer-prolog$ /opt/gupu/scryer-prolog/target/release/scryer-prolog --version
Scryer
"v0.8.123-146-g10ba6fb"
ulrich@p0:/opt/gupu/scryer-prolog$ /opt/gupu/scryer-prolog/target/release/scryer-prolog 
Scryer
?- E = -2, F = -3, F in -3..1,1#> -3 mod (-3 mod (E mod F)).
   E = -2, F = -3
;  false.
?-                 F in -3..1,1#> -3 mod (-3 mod (E mod F)).
false.

What is it?

For your consolation: Same with clpz in SICStus 4.4.1. (Native SICStus is OK here)

[UWN]

... and why the unnecessary internal non-determinism?

[UWN]

Cost: 2318mim

[triska]

Here is a simpler test case that exhibits the problem:

?- F = 1, F in -3..1, X #= Y mod F.
   F = 1, X = 0, clpz:(Y in inf..sup)
;  false.

But a generalization fails (using library(debug)):

?- *F = 1, F in -3..1, X #= Y mod F.
false.

This problem was introduced with triska/clpz@cf8db7e.

@notoria, since you have already made excellent contributions via various considerations involving stronger (and correct) bounds, are you interested in taking a look? I would strongly appreciate your input in this area, since I easily introduce wrong computations in this propagator. The challenge here is to have correct, strong and fast propagation for common cases involving mod, for example in cases as cited in the commit that introduced the problem.

[triska]

... and why the unnecessary internal non-determinism?

Regarding the non-determinism, many goals that ought to succeed deterministically are currently not deterministic, most notably involving the frequently used maplist/N and foldl/[4,5] family of predicates. For instance, we have:

?- maplist(=(a), [X]).
   X = a
;  false.

At least for maplist/1, this can be easily improved via an auxiliary predicate that exchanges the arguments in order to benefit from first-argument indexing. However, for the other predicates, a more general improvement would be preferable, I have filed #192 for this, please see the discussion.

[ghost]

Yes, this is an interesting challenge. I will look into it.

[UWN]

Regarding the non-determinism, many goals that ought to succeed deterministically are currently not deterministic, ...

And thus testing is less effective.

[ghost]

This is a new implementation for mod but I don't know a good way to test it. The implementation seems strong and correct but I can't do benchmark for speed.

[UWN]

Please put it into the masterbranch.

[ghost]

The change is too big to go in master, it might take some time to get it merged.

[UWN]

??

[UWN]

Anyway, so I will test, if this is merged.

[UWN]

#675