Correct and expand global_cardinality/2 comments

First, a correction to commit message
ffe04e5:

    For two lists Xs and Ys of the same length, Xs = Ys is not the same
    as maplist(=, Xs, Ys).

This is true. In SWI, with Xs=Ys, all elements are unified
simultaneously, whereas with maplist(=, Xs, Ys) successively.

    The former sometimes fails to trigger attr_unify_hook/2 for some
    of the involved variables.

This is not true. SWI's unification mechanism worked correctly in all
tests so far. The commit also did not fix the actual cause (the next
one, 794bea3, did); the cause wasn't
that propagators were forgotten, but rather that the relevant
propagators had not yet had an opportunity to even get queued, let
alone fire. To see what could happen before commit
794bea3, consider for example with
version 85f374c of clpfd.pl:

   ?- tuples_in([[A, C, B]], [[3, 1, 3], [4, 2, 4]]),
      global_cardinality([A, B, D], [3-1, 4-2]),
      A = 4.

A = 4 causes gcc_check and gcc_global to be queued in the fast and
slow queue, respectively. In the fast queue, there is also
rel_tuple/2, which is worked off after gcc_check and instantiates both
C and B (to 2 and 4, respectively). Instantiation of C causes a
do_queue/0 in attr_unify_hook/2 (however, no gcc_check because C does
NOT participate in the global_cardinality/2 constraint), which now
works off the previously scheduled gcc_global. Since B has now been
instantiated and gcc_check has not yet had a chance to run due to the
unification mechanism's first handling C's constraints, gcc_global/1
terminates with an error due to an unexpected instantiation:

   ERROR: put_attr/3: Cannot represent: argument must be unbound (1-st argument)

Critically, tuples_in/2 is capable of instantiating two or more
variables at once WHILE propagators are scheduled in the queue. In the
future, more built-in and user-defined constraints might also have
this property. Therefore, gcc_check/1 must always be called also in
gcc_global/1. I found the above case with:

   :- use_module(library(clpfd)).

   run :- run(_).

   run(L) :-
           length(Vs, L),
           portray_clause(L),
           numlist(1, L, Keys),
           pairs_keys_values(Pairs, Keys, Nums),
           maplist(between(0,L), Nums),
           all_n_tuples(Vs, 3, VsTuples),
           NTuples = [_,_],
           maplist(n_tuple(3,L), NTuples),
           tuples_in(VsTuples, NTuples),
           list_take_rest(Vs, Vs1, Rest),
           Rest ins 1..L,
           global_cardinality(Vs1, Pairs),
           label(Vs),
           false.

   n_tuple(N, L, Ts) :-
           length(Ts, N),
           maplist(between(1, L), Ts).

   all_n_tuples([], _, []) :- !.
   all_n_tuples(Vs, N, Rest) :-
           length(Vs, VL),
           (   VL < N -> Rest = []
           ;   length(Take, N),
               list_take_rest(Vs, Take, Vs1),
               Rest = [Take|Rest1],
               all_n_tuples(Vs1, N, Rest1)
           ).

   list_take_rest([], [], []).
   list_take_rest([L|Ls], [L|Ts], Rest) :-
           list_take_rest(Ls, Ts, Rest).
   list_take_rest([L|Ls], Ts, [L|Rest]) :-
           list_take_rest(Ls, Ts, Rest).

In this concrete case, it is also important that tuples_in/2 is posted
BEFORE global_cardinality/2, because the propagators are scheduled in
reverse order of their posting.

From the above test case, I manually constructed a case where adding a
single gcc_check/1 in gcc_global/1 is not enough:

   ?- E in 0\/4,
      tuples_in([[A, C, B]], [[3, 1, 3], [4, 2, 4]]),
      global_cardinality([A, B, D, E], [0-1,3-1,4-2]),
      A = 4.

A = 4 leads to C = 2, B = 4. When gcc_check processes the key 0, both
D and E can be 0. However, when it reaches 4, it is clear that D and E
cannot be 4, so E becomes 0 and is now an unexpected ground value in
clpfd_gcc_vs of the variable corresponding to key 0, yielding again:

   ERROR: put_attr/3: Cannot represent: argument must be unbound (1-st argument)

   (Notice that the relative order of keys also changes the outcome: If
   key 4 is processed before key 0, there is no problem, as the then
   instantiated variable E is correctly removed from clpfd_gcc_vs:

      ?- E in 0\/4,
         tuples_in([[A, C, B]], [[3, 1, 3], [4, 2, 4]]),
         global_cardinality([A, B, D, E], [4-2,0-1,3-1]),
         A = 4.
      %@ E = 0,
      %@ A = 4,
      %@ C = 2,
      %@ B = 4,
      %@ D = 3.)

Hence, do_queue/0 is indeed necessary after gcc_check/1 in
gcc_global/1 in order to reach a fixpoint (which we do as of commit
794bea3). With the following code,
you can find such cases systematically:

   :- use_module(library(clpfd)).

   neqs([], _) --> [].
   neqs([V|Vs], Vals) --> neqs_(Vals, V), neqs(Vs, Vals).

   neqs_([], _) --> [].
   neqs_([Val|Vals], V) --> ( [] ; [V #\= Val] ), neqs_(Vals, V).

   run :- run(_).

   run(L) :-
           length(Vs, L),
           portray_clause(L),
           numlist(1, L, Keys),
           pairs_keys_values(Pairs, Keys, Nums),
           Nums ins 0..L,
           sum(Nums, #=, LGCC),
           all_n_tuples(Vs, 3, VsTuples),
           NTuples = [T1,T2],
           length(T1, 3),
           length(T2, 3),
           maplist(#\=, T1, T2),
           append(NTuples, TVs),
           TVs ins 1..L,
           label(TVs),
           list_take_rest(Vs, Vs1, Rest),
           length([_|Vs1], LGCC),
           label(Nums),
           include(nonzero, Pairs, Pairs1),
           Rest ins 1..L,
           pairs_keys(Pairs1, Keys1),
           phrase(neqs([X], Keys1), Neqs),
           maplist(call, Neqs),
           tuples_in(VsTuples, NTuples),
           global_cardinality([X|Vs1], Pairs),
           catch(label(Vs),_,portray_clause((maplist(call,Neqs),tuples_in(VsTuples,NTuples),global_cardinality([X|Vs1], Pairs)))),
           false.

   nonzero(N-_) :- N =\= 0.

   all_n_tuples([], _, []) :- !.
   all_n_tuples(Vs, N, Rest) :-
           length(Vs, VL),
           (   VL < N -> Rest = []
           ;   length(Take, N),
               list_take_rest(Vs, Take, Vs1),
               Rest = [Take|Rest1],
               all_n_tuples(Vs1, N, Rest1)
           ).

   list_take_rest([], [], []).
   list_take_rest([L|Ls], [L|Ts], Rest) :-
           list_take_rest(Ls, Ts, Rest).
   list_take_rest([L|Ls], Ts, [L|Rest]) :-
           list_take_rest(Ls, Ts, Rest).

With the current version of clpfd.pl, this kind of "freeness error"
(http://www.complang.tuwien.ac.at/ulrich/iso-prolog/error_k) cannot
arise any more, because only variables are included when constructing
the value graph. To test global_cardinality/2 (old and new), you can
compare the results of posting it and then labeling/2 with those of
first labeling/2 and then posting it. To see that do_queue/0 in
gcc_global/1 is necessary with the current version take for example:

   :- use_module(library(clpfd)).

   neqs([], _) --> [].
   neqs([V|Vs], Vals) --> neqs_(Vals, V), neqs(Vs, Vals).

   neqs_([], _) --> [].
   neqs_([Val|Vals], V) --> ( [] ; [V #\= Val] ), neqs_(Vals, V).

   run :- run(_).

   run(L) :-
           length(Vs, L),
           Vs = [A,C,X|_],
           portray_clause(L),
           numlist(1, L, Keys),
           pairs_keys_values(Pairs, Keys, Nums),
           Nums ins 0..L,
           sum(Nums, #=, L),
           Rel = [[1,1,2],[2,2,3]],
           tuples_in([[A,_,C]], Rel),
           label(Nums),
           phrase(neqs([X], Keys), Neqs),
           maplist(call, Neqs),
           findall(Vs, (Vs ins 1..L,label(Vs),global_cardinality(Vs,Pairs)), Sols2),
           permutation(Vs, Vs1),
           findall(Vs, (global_cardinality(Vs, Pairs),
                           label(Vs1)), Sols1),
           (   sort(Sols1, SSols), sort(Sols2, SSols) -> true
           ;   portray_clause(failed-(Neqs,tuples_in([[A,_,C]],Rel),global_cardinality(Vs,Pairs),label(Vs1)))
           ),
           false.

With said do_queue/0 commented out:

   %?- run.
   %@ 3.
   %@ 4.
   %@ failed- ([C#\=2], tuples_in([[A, _, B]], [[1, 1, 2], [2, 2, 3]]), global_cardinality([A, B, C, D], [1-1, 2-2, 3-1, 4-0]), label([A, B, C, D])).
   %@ failed- ([C#\=2], tuples_in([[A, _, B]], [[1, 1, 2], [2, 2, 3]]), global_cardinality([A, B, C, D], [1-1, 2-2, 3-1, 4-0]), label([A, C, B, D])).
   %@ failed- ([C#\=2], tuples_in([[A, _, B]], [[1, 1, 2], [2, 2, 3]]), global_cardinality([A, B, C, D], [1-1, 2-2, 3-1, 4-0]), label([A, C, D, B])).
   %@ failed- ([C#\=2], tuples_in([[A, _, B]], [[1, 1, 2], [2, 2, 3]]), global_cardinality([A, B, C, D], [1-1, 2-2, 3-1, 4-0]), label([A, B, D, C])).
   %@ etc.

And thus for example the case:

  ?- C#\=2, Vs = [A,B,C,D],
     tuples_in([[A, _, B]], [[1, 1, 2], [2, 2, 3]]),
     global_cardinality(Vs, [1-1, 2-2, 3-1]), label(Vs).
  %@ C = 3,
  %@ Vs = [1, 2, 3, 2],
  %@ A = 1,
  %@ B = 2,
  %@ D = 2 ;
  %@ false.

versus:

  ?- C#\=2, Vs = [A,B,C,D], Vs ins 1..3, label(Vs),
     tuples_in([[A, _, B]], [[1, 1, 2], [2, 2, 3]]),
     global_cardinality(Vs, [1-1, 2-2, 3-1]).
  %@ C = 3,
  %@ Vs = [1, 2, 3, 2],
  %@ A = 1,
  %@ B = 2,
  %@ D = 2 ;
  %@ C = 1,
  %@ Vs = [2, 3, 1, 2],
  %@ A = 2,
  %@ B = 3,
  %@ D = 2 ;
  %@ false.

And now regarding the previous queue comment in gcc_check/1:

   The queue must be disabled when posting constraints
   here, otherwise the stored (new) occurrences can differ
   from the (old) ones used in the following.

It is true that the queue must be disabled here, but for a different
reason. The counts are always correct. However, with enabled queue,
gcc_global/1 can run during an inconsistent state in two cases: In
the goal maplist(=(Key), Os), the variables in Os are unified to Key
successively. And the clpfd_gcc_vs attribute is already removed from
the variable corresponding to Key, denoting that this key is "done".
If now gcc_global is invoked when only *some* of the variables are
instantiated, it can happen that the global propagation algorithm
finds no support for them and thus (wrongly) fails. In addition, in
the current version (since 8c35ed5),
the value graph is constructed differently in that remaining variables
are connected to Target even though all keys are already marked as
done, a situation that can only arise when the queue is kept enabled
in gcc_check, otherwise all variables would then be instantiated. To
see this, leave the queue enabled in gcc_check/1 and run the test:

   :- use_module(library(clpfd)).

   neqs([], _)      --> [].
   neqs([V|Vs], Ns) --> neqs_(Ns, V), neqs(Vs, Ns).

   neqs_([], _) --> [].
   neqs_([N|Ns], V) --> ( [] ; [V #\= N] ), neqs_(Ns, V).

   run :- run(_).

   run(N) :-
           length(Vs, N),
           numlist(1, N, Ns),
           portray_clause(N),
           phrase(neqs(Vs,Ns), Cs),
           Vs ins 1..N,
           maplist(call, Cs),
           length(Values, N),
           length(Xs, N),
           Xs ins 0..N,
           label(Xs),
           pairs_keys_values(Pairs, Ns, Values),
           findall(Vs-Pairs, (Xs=Values,
                                 global_cardinality(Vs, Pairs),
                                 label(Vs)), Sols1),
           findall(Vs-Pairs, (global_cardinality(Vs, Pairs),
                                 Xs=Values,
                                 label(Vs)), Sols2),
           (   Sols1 == Sols2 -> true
           ;   portray_clause(maplist(call, [Values=Xs,global_cardinality(Vs,Pairs)|Cs])),
               portray_clause(Sols1-Sols2),
               halt
           ),
           false.

   ?- run.
   %@ 1.
   %@ 2.
   %@ 3.
   %@ ERROR: uhook/3: Undefined procedure: edges:attr_unify_hook/2
   %@ ^  Exception: (11) setup_call_catcher_cleanup('$bags':'$new_findall_bag'(497957), '$bags':fa_loop([_G9500{clpfd = ...}, _G9503{clpfd = ...}, _G9506{clpfd = ...}]-[1-_G9692, 2-_G9695, 3-_G9698], user: (global_cardinality([_G9500{clpfd = ...}, _G9503{clpfd = ...}, _G9506{clpfd = ...}], [1-_G9692, 2-_G9695, ... - ...]), [0, 0|...]=[_G9692, _G9695|...], label([_G9500{clpfd = ...}, _G9503{clpfd = ...}|...])), 497957, _G10058, []), _G16543, '$bags':'$destroy_findall_bag'(497957)) ? abort
   %@ % Execution Aborted

(See below for a case where this happens.) If you fix this issue with
the following patch to the clpfd.pl version of this commit:

   diff --git a/clpfd.pl b/clpfd.pl
   index d50f8e2..74c9206 100644
   --- a/clpfd.pl
   +++ b/clpfd.pl
   @@ -4930,8 +4930,8 @@ gcc_global(Vs, KNs) :-
            do_queue,
            gcc_arcs(KNs, S, Vals),
            variables_with_num_occurrences(Vs, VNs),
   -        maplist(target_to_v(T), VNs),
            (   get_attr(S, edges, Es) ->
   +            maplist(target_to_v(T), VNs),
                put_attr(S, parent, none), % Mark S as seen to avoid going back to S.
                feasible_flow(Es, S, T),   % First construct a feasible flow (if any)
                maximum_flow(S, T),        % only then, maximize it.

and in addition comment out the disable_queue/0 in line 5171, you get:

   %?- run.
   %@ 1.
   %@ 2.
   %@ 3.
   %@ 4.
   %@ maplist(call, [[A, B, C, D]=[0, 0, 2, 2], global_cardinality([_, _, E, F], [1-A, 2-B, 3-C, 4-D]), E#\=4, F#\=4]).
   %@ [[4, 4, 3, 3]-[1-0, 2-0, 3-2, 4-2]]-[].

In other words:

   ?- E#\=4, F#\=4,
      [A, B, C, D]=[0, 0, 2, 2],
      global_cardinality([X1, X2, E, F], [1-A, 2-B, 3-C, 4-D]),
      label([X1,X2,E,F]).
   %@ E = 3,
   %@ F = 3,
   %@ A = 0,
   %@ B = 0,
   %@ C = 2,
   %@ D = 2,
   %@ X1 = 4,
   %@ X2 = 4.

but (by exchanging only the order of goals):

   ?- E#\=4, F#\=4,
      global_cardinality([X1, X2, E, F], [1-A, 2-B, 3-C, 4-D]),
      [A, B, C, D]=[0, 0, 2, 2],
      label([X1,X2,E,F]).
   %@ false.

   (This specific test case demonstrates the problem also without
   applying the above patch, however, you then have for example:

      ?- global_cardinality([D, E, F], [1-A, 2-B, 3-C]),
         [0, 0, 1]=[A, B, C].
      %@ ERROR: uhook/3: Undefined procedure: edges:attr_unify_hook/2

    Since the variables are part of the value graph but not cleared).

For the "all equal" case, you can fix this in SWI by writing, instead
of maplist(=(Key), Os):

   length(Os, Len),
   length(Ts, Len),
   maplist(=(Key), Ts),
   Os = Ts

This instantiates all variables in Os at the same time, so we do not
need to find a support for them any more. Simultaneous unification
works in SWI, but other systems (and future versions) may handle this
differently, for example by successively instantiating the variables
and working off the queue for each of them in order.

The second case is the "all NOT equal" case in gcc_check. The above
"[0,0,1]=[A,B,C]" example shows this. This could be fixed with the
above patch in gcc_global.

Independently, the queue should be turned off in any case during
gcc_check/1 for efficiency: After we inspected all domains, we want to
put the distilled information to good use, without having nested
invocations going through almost the same computations. This is the
same reason why the queue is disabled in other places.

We have lost one property though that held before the introduction of
global_cardinality/2 in its current form (since it was first
introduced): Previously, turning off the queue was always optional.
Replacing disable_queue with a no-op did not change the correctness of
the solver, it only affected efficiency (disabling the queue could
also make it slower, for example because a nested invocation might
have detected an inconsistency earlier than first posting all derived
restrictions). It is unclear whether this property is very desirable,
especially since retaining it now seems to involve either depending on
the precise internal handling of simultaneous unifications or on other
work-arounds to prevent gcc_global/1 from firing during gcc_check/1.
Luckily, there is an easy and overhead-free solution in this case
which I will apply in the next commit. It seems good that ALL
disable_queue/0 calls can then be replaced by no-ops as opposed to
only some of them.

In summary, when splitting a constraint into two propagators
(slow/fast) with one of them depending on preconditions that are
postconditions of the other, think about:

   * What happens when variables are instantiated simultaneously?
   * Can a propagator be invoked during inconsistent states?
   * Is an essential propagator run in all circumstances?
   * Is it necessary to rerun a propagator to reach a fix-point?
   * How can you test unusual instantiation patterns systematically?

These considerations only concern constraint implementors; users need
not worry about them at all - the point of these tests is to make the
library work flawlessly in all use cases and instantiation patterns.

Author: triska

library/clp/clpfd.pl

@@ -5155,18 +5155,28 @@
 /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
    Simple consistency check, run before global propagation.
    Importantly, it removes all ground values from clpfd_gcc_vs.
-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
 
-gcc_done(Num) :-
-        del_attr(Num, clpfd_gcc_vs),
-        del_attr(Num, clpfd_gcc_num),
-        del_attr(Num, clpfd_gcc_occurred).
+   The pgcc_check/1 propagator in itself would suffice to ensure
+   consistency and could be used in a faster and weaker propagation
+   option for global_cardinality/3.
+
+   The queue must be disabled during gcc_check/1 to prevent
+   gcc_global/1 from running during an inconsistent state. This can
+   happen after a key is marked as "done" (by removing its
+   clpfd_gcc_vs attribute) and before all its variables are
+   instantiated, both in the "all equal" and the "not equal" case.
+- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
 
 gcc_check(Pairs) :-
         disable_queue,
         gcc_check_(Pairs),
         enable_queue.
 
+gcc_done(Num) :-
+        del_attr(Num, clpfd_gcc_vs),
+        del_attr(Num, clpfd_gcc_num),
+        del_attr(Num, clpfd_gcc_occurred).
+
 gcc_check_([]).
 gcc_check_([Key-Num0|KNs]) :-
         (   get_attr(Num0, clpfd_gcc_vs, Vs) ->
@@ -5176,9 +5186,6 @@
             put_attr(Num0, clpfd_gcc_vs, Os),
             put_attr(Num0, clpfd_gcc_occurred, Occ1),
             Occ1 is Occ0 + Min,
-            % The queue must be disabled when posting constraints
-            % here, otherwise the stored (new) occurrences can differ
-            % from the (old) ones used in the following.
             geq(Num, Occ1),
             (   Occ1 == Num -> gcc_done(Num0), all_neq(Os, Key)
             ;   Os == [] -> gcc_done(Num0), Num = Occ1