apply existential quantification sooner when building counter networks
further simplification of counter_network/3 and related predicates

I am also considering the following patch (relative to the previous revision):

   diff --git a/library/clp/clpb.pl b/library/clp/clpb.pl
   index 79c2faf..2c20e91 100644
   --- a/library/clp/clpb.pl
   +++ b/library/clp/clpb.pl
   @@ -463,32 +463,29 @@ existential(V, BDD, Node) :-
    counter_network(Cs, Fs, Node) :-
            same_length([_|Fs], Indicators),
            fill_indicators(Indicators, 0, Cs),
   -        same_length(Fs, Vars0),
   -        % enumerate variables in reverse order so that they appear
   -        % in the correct order in the resulting BDD
   -        maplist(enumerate_variable, Vars0),
   -        reverse(Vars0, Vars),
   -        counter_network(Fs, Indicators, Vars, Node0),
   -        maplist(var_index_root, Vars, _, Roots),
   -        maplist(=(Root), Roots),
   -        root_put_formula_bdd(Root, card(Cs,Fs), Node),
   -        eq_and(Vars, Fs, Node0, Node),
   -        % remove attributes to avoid residual goals for these variables,
   -        % which are only used temporarily to build the counter network.
   -        maplist(del_attrs, Vars).
   -
   -eq_and([], [], Node, Node).
   -eq_and([X|Xs], [Y|Ys], Node0, Node) :-
   -        sat_rewrite(v(X) =:= Y, Sat),
   -        sat_bdd(Sat, B),
   -        apply(*, B, Node0, Node1),
   -        existential(X, Node1, Node2),
   -        eq_and(Xs, Ys, Node2, Node).
   -
   -counter_network([], [Node], [], Node).
   -counter_network([_|Fs], [I|Is0], [Var|Vars], Node) :-
   +        maplist(formula_var_bdd_existential, Fs, Vars0, BDDs, Exs),
   +        variables_in_index_order(Vars0, Vars1),
   +        % The counter network is built bottom-up, so variables with
   +        % highest index must be processed first.
   +        reverse(Vars1, Vars),
   +        counter_network_(Vars, Indicators, Node0),
   +        writeln(BDDs),
   +        foldl(bdd_and, BDDs, Node0, Node1),
   +        foldl(remove_existential, Exs, Node1, Node).
   +
   +% Introduce fresh variables for expressions that are not variables.
   +% These variables are later existentially quantified to remove them.
   +
   +formula_var_bdd_existential(v(Var), Var, 1, none) :- !.
   +formula_var_bdd_existential(F, Var, BDD, v(Var)) :-
   +        enumerate_variable(Var),
   +        sat_rewrite(v(Var) =:= F, Sat),
   +        sat_bdd(Sat, BDD).
   +
   +counter_network_([], [Node], Node).
   +counter_network_([Var|Vars], [I|Is0], Node) :-
            indicators_pairing(Is0, I, Var, Is),
   -        counter_network(Fs, Is, Vars, Node).
   +        counter_network_(Vars, Is, Node).

    indicators_pairing([], _, _, []).
    indicators_pairing([I|Is], Prev, Var, [Node|Nodes]) :-
   @@ -504,6 +501,13 @@ fill_indicators([I|Is], Index0, Cs) :-
            Index1 is Index0 + 1,
            fill_indicators(Is, Index1, Cs).

   +remove_existential(none, Node, Node).
   +remove_existential(v(Var), Node0, Node) :-
   +        existential(Var, Node0, Node),
   +        % remove attributes to avoid residual goals for these variables,
   +        % which are only used temporarily to build the counter network.
   +        del_attrs(Var).
   +
    /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
       Compute F(NA, NB).

   @@ -754,10 +758,13 @@ node_ite(Node, Node-ite(Var,High,Low)) :-

    labeling(Vs0) :-
            must_be(list, Vs0),
   +        variables_in_index_order(Vs0, Vs),
   +        maplist(indomain, Vs).
   +
   +variables_in_index_order(Vs0, Vs) :-
            maplist(var_with_index, Vs0, IVs0),
            keysort(IVs0, IVs),
   -        pairs_values(IVs, Vs),
   -        maplist(indomain, Vs).
   +        pairs_values(IVs, Vs).

    var_with_index(V, I-V) :-
            (   var_index_root(V, I, _) -> true

This prevents auxiliary variables when existing variables can be used.
It makes the whole predicate a bit harder to understand and has so far
shown only negligible benefits, even where card/2 constraints dominate,
such as Project Euler Problem 172.