public class ConjunctivePredicateAbstractionLattice extends AbstractPredicateAbstractionLattice
It may happen that certain elements of the lattice are equivalent to the bottom element, since the respective combinations of predicates are unsatisfiable. It should however not happen that combinations of predicates are valid, that is they equal the top element. For efficiency reasons, the lattice is only lazily generated on-demand by the iterator. Therefore, the unsatisfiable combinations cannot be removed at generation time.
Modifier and Type | Class and Description |
---|---|
private class |
ConjunctivePredicateAbstractionLattice.PredicateLatticeIterator |
AbstractPredicateAbstractionLattice.AbstractPredicateLatticeIterator
PartialComparator.PartialComparisonResult
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
PREDICATE_NAME_CONBINATION_STRING |
private java.util.List<AbstractionPredicate> |
predicates |
Constructor and Description |
---|
ConjunctivePredicateAbstractionLattice(java.util.List<AbstractionPredicate> applicablePredicates)
Constructs a new
ConjunctivePredicateAbstractionLattice for the
given list of applicable predicates. |
Modifier and Type | Method and Description |
---|---|
boolean |
equals(java.lang.Object obj) |
protected AbstractPredicateAbstractionDomainElement |
getBottomElem() |
java.lang.String |
getPredicateNameCombinationString() |
protected AbstractPredicateAbstractionDomainElement |
getTopElem() |
int |
hashCode() |
java.util.Iterator<AbstractDomainElement> |
iterator()
The iterator for this lattice will first return the bottom element, then
all conjunctions of length n of the predicates, then all conjunctions of
length n-1, and so on, until finally the top element is returned.
|
AbstractDomainElement |
join(AbstractDomainElement a,
AbstractDomainElement b)
A lattice join operation; finds an abstract element that is the least
upper bound of the set consisting of the elements a and b.
|
int |
size() |
java.lang.String |
toString() |
join
abstractFrom, compare, fromString, getSideConditionForAxiom
public static final java.lang.String PREDICATE_NAME_CONBINATION_STRING
private java.util.List<AbstractionPredicate> predicates
public ConjunctivePredicateAbstractionLattice(java.util.List<AbstractionPredicate> applicablePredicates)
ConjunctivePredicateAbstractionLattice
for the
given list of applicable predicates. The caller is responsible for making
sure that none of the predicates is valid.applicablePredicates
- The predicates to generate the lattice from.public AbstractDomainElement join(AbstractDomainElement a, AbstractDomainElement b)
AbstractDomainLattice
join
in class AbstractDomainLattice
a
- First element to find the least upper bound for.b
- Second element to find the least upper bound for.public java.util.Iterator<AbstractDomainElement> iterator()
iterator
in interface java.lang.Iterable<AbstractDomainElement>
iterator
in class AbstractDomainLattice
public int size()
public boolean equals(java.lang.Object obj)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public java.lang.String toString()
toString
in class java.lang.Object
protected AbstractPredicateAbstractionDomainElement getTopElem()
getTopElem
in class AbstractPredicateAbstractionLattice
protected AbstractPredicateAbstractionDomainElement getBottomElem()
getBottomElem
in class AbstractPredicateAbstractionLattice
public java.lang.String getPredicateNameCombinationString()
getPredicateNameCombinationString
in class AbstractPredicateAbstractionLattice