public class SimplePredicateAbstractionLattice extends AbstractPredicateAbstractionLattice
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 |
---|
SimplePredicateAbstractionLattice(java.util.List<AbstractionPredicate> applicablePredicates)
Constructs a new
SimplePredicateAbstractionLattice 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
the given predicates in the order in which they have been initially
supplied, and finally the top element.
|
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 SimplePredicateAbstractionLattice(java.util.List<AbstractionPredicate> applicablePredicates)
SimplePredicateAbstractionLattice
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