public class Sum extends AbstractDistributiveLattice
As for every algebraic theory, elements are terms built from the elements of the two lattices, and quotiented w.r.t. all equations of the theory and all equations that are true in either summand. Each element of a summand is thus identified with an element of the sum, which can be obtained by injection.
In this implementation, to avoid equivalence classes and make the sum computable we restrict to distributive lattices and use Grätzer–Lakser's (disjunctive) canonical representatives (see “Chain conditions in the distributive free product of lattices”, Trans. Amer. Math. Soc., 144:301−312, 1969) described in clausal form.
A clause is a set of elements from the summands. A reduced clause is a clause containing at most one element from each summand. A (clausal) formula is a set of clauses.
Formulae can be interpreted in a disjunctive or conjunctive way (i.e., as a join of meets or a meet of joins), and both intepretations are used during computations. A (disjunctive or conjunctive) reduced formula is a set of reduced clauses in which no clause can be eliminated without affecting the formula's value. Elements of a sum are stored as disjunctive reduced formulae.
Warning: if one of the summands is trivial (just one element)
it will not annihilate the sum (as it should happen) but
rather it will behave like a neutral element (a rôle actually
played by the twoelement Boolean lattice). This unfortunate restriction
is caused by the difficulty of detecting whether one of the summands is trivial (as
Lattice.elements()
is optional).
Modifier and Type  Method and Description 

boolean 
comp(Element x,
Element y)
Check whether two elements are comparable using
Lattice.meet(Element[]) . 
Collection<Element> 
elements()
Generate iteratively all elements of this lattice.

Collection<Element> 
generators()
Return a collection of generators for the lattice.

Element 
inj(int k,
Element element)
Inject an element of a summand into this sum.

Element 
join(Element... element)
Return the join of the provided elements.

boolean 
leq(Element x,
Element y)
Check whether an element is smaller than or equal to another element using
Lattice.meet(Element[]) . 
Element 
meet(Element... element)
Return the meet of the provided elements.

static Lattice 
of(Lattice... distributiveLattice)
Return the sum of the given distributive lattices.

static Lattice 
of(Lattice[] distributiveLattice,
String[] name)
Return the sum of the given distributive lattices, giving them specified names.

Element 
one()
Return the one of this lattice.

String 
toString() 
Element 
valueOf(String name)
Return an element of this lattice, given its name.

Element 
zero()
Return the zero of this lattice.

isDistributive
coveringRelation, ensureElementsInLattice, ensureElementsInLattice, ensureElementsInLattice, pscomp, psdiff, symdiff, valueOfZeroOrOne
public static Lattice of(Lattice... distributiveLattice)
distributiveLattice
 the distributive lattices whose sum has to be computed.public static Lattice of(Lattice[] distributiveLattice, String[] name)
distributiveLattice
 the distributive lattices whose sum has to be computed.name
 a parallel list of names for each distributiveLattice
.public Collection<Element> generators()
Lattice
zero
or
one
. There is no guarantee of freeness or minimality.public Collection<Element> elements()
AbstractLattice
This methods uses Lattice.generators()
to obtain an initial set of elements,
and then computes joins and meets of all available elements until no new elements
are generated.
It is expected that concrete subclasses will override this method
with an ad hoc, more efficient implementation.
It is strongly suggested that concrete subclasses that do not override this method cache its result internally.
elements
in interface Lattice
elements
in class AbstractLattice
public Element valueOf(String name)
Lattice
Certain lattices make it possible to define names for elements. This method returns the element corresponding to the provided name.
name
 the name of an element of this lattice.name
.public Element inj(int k, Element element)
k
 the index of a summand.element
 an element of the k
th summand.public Element zero()
Lattice
Note that there is no guarantee that the returned element is the only element representing zero in this lattice. Other zeroes may arise from computations, but they will always be equal to the element returned by this method.
public Element one()
Lattice
Note that there is no guarantee that the returned element is the only element representing one in this lattice. Other ones may arise from computations, but they will always be equal to the element returned by this method.
public Element meet(Element... element)
Lattice
one
, and upon a singleton list the only specified element.element
 the elements whose meet has to be computed.public Element join(Element... element)
Lattice
zero
, and upon a singleton list the only specified element.element
 the elements whose join has to be computed.public boolean comp(Element x, Element y)
AbstractLattice
Lattice.meet(Element[])
.comp
in interface Lattice
comp
in class AbstractLattice
x
 an element.y
 another element.x.meet(y)
equals x
or y
.public boolean leq(Element x, Element y)
AbstractLattice
Lattice.meet(Element[])
.leq
in interface Lattice
leq
in class AbstractLattice
x
 an element.y
 another element.x.meet(y)
equals x
.