Class Sum
 All Implemented Interfaces:
Lattice
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).

Field Summary

Method Summary
Modifier and Type Method Description boolean
comp(Element x, Element y)
Check whether two elements are comparable usingLattice.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 usingLattice.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.Methods inherited from class it.unimi.dsi.lama4j.AbstractLattice
coveringRelation, ensureElementsInLattice, ensureElementsInLattice, ensureElementsInLattice, pscomp, psdiff, symdiff, valueOfZeroOrOne

Method Details

of
Return the sum of the given distributive lattices. Parameters:
distributiveLattice
 the distributive lattices whose sum has to be computed. Returns:
 the sum of the specified distributive lattices.

of
Return the sum of the given distributive lattices, giving them specified names. Parameters:
distributiveLattice
 the distributive lattices whose sum has to be computed.name
 a parallel list of names for eachdistributiveLattice
. Returns:
 the sum of the specified distributive lattices.

generators
Description copied from interface:Lattice
Return a collection of generators for the lattice. The set will not includezero
orone
. There is no guarantee of freeness or minimality. Returns:
 a collection of generators.

elements
Description copied from class:AbstractLattice
Generate iteratively all elements of this lattice.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.
 Specified by:
elements
in interfaceLattice
 Overrides:
elements
in classAbstractLattice
 Returns:
 the set of elements of this lattice.

valueOf
Description copied from interface:Lattice
Return an element of this lattice, given its name.Certain lattices make it possible to define names for elements. This method returns the element corresponding to the provided name.
 Parameters:
name
 the name of an element of this lattice. Returns:
 the element of this lattice named
name
.

inj
Inject an element of a summand into this sum. Parameters:
k
 the index of a summand.element
 an element of thek
th summand. Returns:
 the corresponding element of this sum.

zero
Description copied from interface:Lattice
Return the zero of this 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.
 Returns:
 the zero of this lattice.

one
Description copied from interface:Lattice
Return the one of this 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.
 Returns:
 the one of this lattice.

meet
Description copied from interface:Lattice
Return the meet of the provided elements. In particular, upon the empty list of arguments returnsone
, and upon a singleton list the only specified element. Parameters:
element
 the elements whose meet has to be computed. Returns:
 the meet of the provided elements.

join
Description copied from interface:Lattice
Return the join of the provided elements. In particular, upon the empty list of arguments returnszero
, and upon a singleton list the only specified element. Parameters:
element
 the elements whose join has to be computed. Returns:
 the join of the provided elements.

toString

comp
Description copied from class:AbstractLattice
Check whether two elements are comparable usingLattice.meet(Element[])
. Specified by:
comp
in interfaceLattice
 Overrides:
comp
in classAbstractLattice
 Parameters:
x
 an element.y
 another element. Returns:
 true iff
x.meet(y)
equalsx
ory
.

leq
Description copied from class:AbstractLattice
Check whether an element is smaller than or equal to another element usingLattice.meet(Element[])
. Specified by:
leq
in interfaceLattice
 Overrides:
leq
in classAbstractLattice
 Parameters:
x
 an element.y
 another element. Returns:
 true iff
x.meet(y)
equalsx
.
