Example of defining a new constraint

The following example demonstrates how to create a new set constraint. To show that set inclusion is not restricted to ground herbrand terms we can take the following constraint which defines lattice inclusion over lattice domains:

S_1 incl S

Assuming that S and S₁ are specific set variables of the form

S `:: {} ..{{a,b,c},{d,e,f}}, ..., S_1 `:: {} ..{{c},{d,f},{g,f}}

we would like to define such a predicate that will be woken as soon as one or both set variables' domains are updated in such a way that would require updating the other variable's domain by propagating the constraint. This constraint definition also shows that if one wants to iterate over a ground set (set of known elements) the transformation to a list is convenient. In fact iterations do not suit sets and benefit much more from a list structure. We define the predicate incl(S,S1) which corresponds to this constraint:

:- use_module(library(conjunto)).
incl(S,S1) :-
          set(S),set(S1),
          !,
          check_incl(S, S1).
incl(S, S1) :-
          set(S),
          set_range(S1, Glb1, Lub1),
          !,
          check_incl(S, Lub1),
          S + Glb1 `= S1NewGlb,
          modify_bound(glb, S1, S1NewGlb).
incl(S, S1) :-
          set(S1),
          set_range(S, Glb, Lub),
          !,
          check_incl(Glb, S1),
          large_inter(S1, Lub, SNewLub),
          modify_bound(lub, S, SNewLub).
incl(S,S1) :-
          set_range(S, Glb, Lub),
          set_range(S1, Glb1, Lub1),
          check_incl(Glb, Lub1),
          Glb \/ Glb1 `= S1NewGlb,
          large_inter(Lub, Lub1, SNewLub),
          modify_bound(glb, S1, S1NewGlb),
          modify_bound(lub, S, SNewLub),
          ( (set(S) ; set(S1)) ->
               true
         ;
               make_suspension(incl(S, S1),2, Susp),
               insert_suspension([S,S1], Susp, del_any of set, set)
          ),
          wake.

large_inter(Lub, Lub1, NewLub) :-
          set2list(Lub, Llub),
          set2list(Lub1, Llub1),
          largeinter(Llub, Llub1, LNewLub),
          list2set(LNewLub, NewLub).

largeinter([], _, []).
largeinter([S | List_set], Lub1, Snew) :-
          largeinter(List_set, Lub1, Snew1),
          ( contained(S, Lub1) ->
                Snew = [S | Snew1]
          ;
                Snew = Snew1
          ).

check_incl({}, _S) :-!.
check_incl(Glb, Lub1) :-
          set2list(Glb, Lsets),
          set2list(Lub1, Lsets1),
          all_union(Lsets, Union),
          all_union(Lsets1, Union1),
          Union `< Union1,!,
          checkincl(Lsets,Lsets1).
checkincl([], _Lsets1).
checkincl([S | Lsets],Lsets1):-
          contained(S, Lsets1),
          checkincl(Lsets,Lsets1).

contained(_S, []) :- fail,!.
contained(S, [Ss | Lsets1]) :-
          (S `< Ss ->
                true
          ;
                contained(S, Lsets1)
          ).

The execution of this constraint is dynamic, i.e., the predicate incl/2 is called and woken following the following steps:

• We check if the two set variables are ground set. If so we just check deterministically if the first one is included (lattice inclusion) in the second one check_incl. This predicate checks that any element of a ground set (which is a set itself in this case) is a subset of at least one element of the second set. If not it fails.
• We check if the first set is ground and the second is a set domain variable. If so, check_incl is called over the first ground set and the upper bound of the second set. If it succeeds then the lower bound of the set variable might not be consistent any more, we compute the new lower bound (i.e., adding elements from the ground set in it (by using the union predicate) and we modify the bound modify_bound. This predicate also wakes all concerned suspension lists and instantiates the set variable if its domain is reduced to a single set (upper bound = lower bound).
• We check if the second set is ground and the first one is a set variable. If so, check_incl is called over the lower bound of the first set and the second ground set. If it succeeds then the upper bound of the set variable might not be consistent any more. The new upper bound is computed by intersecting the first set with the upper bound of the set variable in the lattice acceptation large_inter and is updated modify_bound.
• we check if both set variables are domain variables. If so the lower bound of the first set should be included in the lattice sense in the upper bound of the second one check/incl. If it succeeds, then if the lower bound the second set is no more consistent we compute the new one by making the union with first sec lower bound. In the same way, the upper bound of the first set might not be consistent any more. If so, we compute the new one by intersecting (in the lattice acceptation) the both upper bounds to compute the new upper bound of the first set large_inter. The upper bound of the first set variable is updated as well as the lower bound of the second set modify_bound.
• After checking all these updates, we test if the constraint implies an instanciation of one of the two sets. If this is not the case, we have to suspend the predicate so that it is woken as soon as any bound of either set domain is changed. The predicate make_suspension/3 can be used for any ECLiPSe module based on a meta-term structure. It creates a suspension, and then the predicate insert_suspension/4, puts this suspension into the appropriate lists (woken when any bound is updated) of both set variables.
• the last action wake triggers the execution of all goals that are waiting for the updates we have made. These goals should be woken after inserting the new suspension, otherwise the new updates coming from these woken goals won't be propagated on this constraint !