Scryer-prolog: clpz: unexpected failure

[UWN]

ulrich@p0:/opt/gupu/scryer-prolog$ /opt/gupu/scryer-prolog/target/release/scryer-prolog --version
"v0.8.123-165-g79a7403-modified"
ulrich@p0:/opt/gupu/scryer-prolog$ /opt/gupu/scryer-prolog/target/release/scryer-prolog
?- use_module(library(clpz)).
   true.
?- C = -1, C in -2.. -1,1#>0 mod C.
   C = -1
;  false.
?-         C in -2.. -1,1#>0 mod C.
false.               % inattendu

[notoria]

This also fails:

?- Y in -2.. -1, Z#= 0 mod Y.
false.
?-

It's happening here. On that condition, YL = -2, YU = -1, so YU < 0 and ZMax is -2 + 1, ZMax = -1. In the end Z must verify Z in -1..0.

Using queue_goal//1 at this line seems to solve the issue.

[UWN]

Update?

[notoria]

@triska , should queue_goal//1 be used? Or is there a way around that?

Update?

There could be other places that need the same treatment, replace fd_put/3 with queue_goal//1.

[triska]

queue_goal//1 is slower than using fd_put/3, since it involves queuing a goal, fetching it, and interpreting it.

The advantage of queue_goal//1 is that it is less error-prone. So, you must decide what you want to prioritize: speed, convenience, correctness, etc.

In this concrete case, one suspect issue is definitely that variables like YU are reused in different parts of the code, for instance YU is used also here, and is not necessarily the same bound as in other places, so a different variable should be used!

[notoria]

So Z = X is enough to change Y?

By removing this line and adding true as a default case, it works. It seems that Z = X is triggering this issue, does fd_put/3, fd_get/5 work with non-variable?

[triska]

It is inadmissible to bind variables in the propagator code: This is because the propagation is invoked from within verify_attributes/3. Therefore, all bindings must be deferred to a later point, using queue_goal//1.

fd_get//3 fails if the first argument is an integer. This means that fd_get//3 can actually also be used to test whether we are reasoning about a variable, this property is used frequently in propagator code. It only succeeds if the first argument is a variable, and in that case the remaining arguments tell us the domain and propagators.

fd_put//3 expects the first argument to be a variable. The sequence is usually fd_get, and then followed by fd_put, and if fd_get succeeds, then fd_put will also succeed, because the variable must not become instantiated between them, since that would violate the property expected by verify_attributes/3: Variables must not become bound (not instantianted, and not aliased) within verify_attributes/3. The way to perform bindings is to delay them for later, this is what the third argument of verify_attributes/3 is for.

[notoria]

So line like this, this is undefined behaviour? Unless it is preceded by a kill(MState) and is the last clause.

[UWN]

?

[triska]

kill//1 is used to truly kill the propagator: It will never again be reactivated after it has been killed. So, use kill//1 only after you are sure that everything the propagator can ever propagate has been (or will be) correctly propagated. Otherwise, you risk instantiations that actually violate the constraints that were stated!

Yes, this is undefined behaviour, use queue_goal(X=Y) for this. Note that you can use (=)/2, which is faster than (#=)/2, because (#=)/2 must also parse the arguments within Prolog.

library(clpz) currently contains several occurrences of just X = Y, which, strictly speaking, is not permitted, but so far seems not to be an issue. To be on the safe side, please use queue_goal//1 for new code of this kind, for the time being, i.e., queue_goal(X=Y). Note that using (=)//2 directly is justified if no CLP(Z) variable is involved, such as for example UY = n(I) etc.