finite set select intersection

[Raphael Collet]

Hi Irene,

Here is a slightly improved definition for SelectPartition.  Your
definition with FD.reified.sum is too weak.  It does not enforce mutual
disjunction between sets in the partition, for instance.  Notice that I
use FD.sumCN in order to avoid the plethora of FD.conj in your
definition.


proc {SelectPartition Sets SelectorSet ResultSet}
   UB Selector Ones
   fun {ListWise Xs Ys} {List.zip Xs Ys fun {$ X Y} [X Y] end} end
in
   %% UB is the union of all upper bounds in Sets
   UB={FS.value.make {Flatten {Map Sets FS.reflect.upperBound}}}
   ResultSet={FS.var.upperBound {FS.reflect.upperBound UB}}
   
   %% Selector reifies the presence of each set
   SelectorSet={FS.var.upperBound 1#{Length Sets}}
   Selector={FS.reified.areIn 1#{Length Sets} SelectorSet}
   
   %% I is in ResultSet iff I is in exactly one of the selected Sets
   Ones={Map Sets fun {$ _} 1 end}
   {FS.forAllIn UB
    proc {$ I}
       InResultSet={FS.reified.isIn I ResultSet}
       InSets={Map Sets fun {$ S} {FS.reified.isIn I S} end}
    in
       {FD.sumCN Ones {ListWise Selector InSets} '=:' InResultSet}
    end}
   
   %% selected sets must be non-empty
   for S in Sets  Sel in Selector do Sel =<: {FS.card S} end
   
   %% cardinalities
   {FD.sumCN Ones {ListWise Selector {Map Sets FS.card}}
    '=:' {FS.card ResultSet}}
end


Cheers,

raph