public class DisjunctivePredicateAbstractionLattice extends AbstractPredicateAbstractionLattice
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 predicates cannot be removed at generation time.
Modifier and Type | Class and Description |
---|---|
private class |
DisjunctivePredicateAbstractionLattice.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 |
---|
DisjunctivePredicateAbstractionLattice(java.util.List<AbstractionPredicate> applicablePredicates)
Constructs a new
DisjunctivePredicateAbstractionLattice 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 DisjunctivePredicateAbstractionLattice(java.util.List<AbstractionPredicate> applicablePredicates)
DisjunctivePredicateAbstractionLattice
for the
given list of applicable predicates. The caller is responsible for making
sure that no combinations of predicates are 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