%
% A ZDD constraint implementing
% https://www.metalevel.at/prolog/attributedvariables#minatotask
% Author: Joachim Schimpf, this code is in the public domain.
%
% ?- zdd_constraint(X -> b(true) ; Y -> b(true) ; b(false)), [X,Y] = [1,1].
% No (0.00s cpu)
% 
% ?- zdd_constraint(X -> b(true) ; Y -> b(true) ; b(false)), X=1.
% X = 1
% Y = 0
% Yes (0.00s cpu)
% 
% ?- zdd_constraint(X -> b(true) ; Y -> b(true) ; b(false)), X=0.
% X = 0
% Y = Y
% There is 1 delayed goal.
% Yes (0.00s cpu)
%

:- lib(hash).

zdd_constraint(Desc) :-
        term_variables(Desc, Xs),
        copy_term(Xs-Desc, Ids-ZDD),
        ( foreach(Id,Ids), count(Id,1,_) do true ),
        Xz =.. [[]|Xs],
        suspend(zdd_propagate(Xz, Ids-ZDD), 0, Xz->inst).


zdd_propagate(Xz, Ids-ZDD) :-
        hash_create(Flags),
        zdd_simplify(Xz, ZDD, ZDD1, Flags),
        ZDD1 \= b(false),
        ( foreach(Id,Ids), fromto(Ids1,Ids2,Ids3,[]), param(Xz,Flags) do
            ( hash_get(Flags, Id, Flag) ->
                ( Flag=kept -> Ids2=[Id|Ids3]   % still in ZDD
                ; Flag=seen -> Ids2=Ids3        % simplified away
                )
            ;
                Ids2=Ids3, arg(Id, Xz, 0)       % eliminated, set to 0
            )
        ),
        ( ground(Xz) -> true
        ; suspend(zdd_propagate(Xz, Ids1-ZDD1), 0, Xz->inst)
        ).


zdd_simplify(_Xz, b(T), b(T), _).
zdd_simplify(Xz, (Id->ZDDL;ZDDR), ZDD, Flags) :-
        arg(Id, Xz, Val),
        ( var(Val) ->
            hash_set(Flags, Id, kept),
            ZDD = (Id->ZDDL1;ZDDR1),
            zdd_simplify(Xz, ZDDL, ZDDL1, Flags),
            zdd_simplify(Xz, ZDDR, ZDDR1, Flags)
        ; Val==1,
            hash_set(Flags, Id, seen),
            zdd_simplify(Xz, ZDDL, ZDD, Flags)
        ; Val==0,
            hash_set(Flags, Id, seen),
            zdd_simplify(Xz, ZDDR, ZDD, Flags)
        ).