de.uka.ilkd.key.axiom_abstraction.predicateabstraction

Class ConjunctivePredicateAbstractionLattice

java.lang.Object

de.uka.ilkd.key.axiom_abstraction.AbstractDomainLattice

de.uka.ilkd.key.axiom_abstraction.predicateabstraction.AbstractPredicateAbstractionLattice

de.uka.ilkd.key.axiom_abstraction.predicateabstraction.ConjunctivePredicateAbstractionLattice

All Implemented Interfaces:

PartialComparator<AbstractDomainElement>, java.lang.Iterable<AbstractDomainElement>

public class ConjunctivePredicateAbstractionLattice
extends AbstractPredicateAbstractionLattice

A lattice for all predicates accepting the given sort. This lattice consists of 2^n + 1 elements, where n is the number of applicable predicates. Each element is a conjunction of the given predicates. The last element is a top element which is true for all inputs.

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.

Author:

Dominic Scheurer

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	ConjunctivePredicateAbstractionLattice.PredicateLatticeIterator

Nested classes/interfaces inherited from class de.uka.ilkd.key.axiom_abstraction.predicateabstraction.AbstractPredicateAbstractionLattice

AbstractPredicateAbstractionLattice.AbstractPredicateLatticeIterator

Nested classes/interfaces inherited from interface de.uka.ilkd.key.axiom_abstraction.PartialComparator

PartialComparator.PartialComparisonResult

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	PREDICATE_NAME_CONBINATION_STRING
private java.util.List<AbstractionPredicate>	predicates

Constructor Summary

Constructors

Constructor and Description
ConjunctivePredicateAbstractionLattice(java.util.List<AbstractionPredicate> applicablePredicates) Constructs a new ConjunctivePredicateAbstractionLattice for the given list of applicable predicates.

Method Summary

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()

Methods inherited from class de.uka.ilkd.key.axiom_abstraction.predicateabstraction.AbstractPredicateAbstractionLattice

join

Methods inherited from class de.uka.ilkd.key.axiom_abstraction.AbstractDomainLattice

abstractFrom, compare, fromString, getSideConditionForAxiom

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Field Detail

PREDICATE_NAME_CONBINATION_STRING

public static final java.lang.String PREDICATE_NAME_CONBINATION_STRING

See Also:

Constant Field Values

predicates

private java.util.List<AbstractionPredicate> predicates

Constructor Detail

ConjunctivePredicateAbstractionLattice

public ConjunctivePredicateAbstractionLattice(java.util.List<AbstractionPredicate> applicablePredicates)

Constructs a new ConjunctivePredicateAbstractionLattice for the given list of applicable predicates. The caller is responsible for making sure that none of the predicates is valid.

Parameters:

applicablePredicates - The predicates to generate the lattice from.

Method Detail

join

public AbstractDomainElement join(AbstractDomainElement a,
                                  AbstractDomainElement b)

Description copied from class: AbstractDomainLattice

A lattice join operation; finds an abstract element that is the least upper bound of the set consisting of the elements a and b.

Specified by:

join in class AbstractDomainLattice

Parameters:

a - First element to find the least upper bound for.

b - Second element to find the least upper bound for.

Returns:

The least upper bound of the set consisting of the elements a and b.

iterator

public 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.

Specified by:

iterator in interface java.lang.Iterable<AbstractDomainElement>

Specified by:

iterator in class AbstractDomainLattice

size

public int size()

Returns:

The number of elements in this lattice.

equals

public boolean equals(java.lang.Object obj)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getTopElem

protected AbstractPredicateAbstractionDomainElement getTopElem()

Specified by:

getTopElem in class AbstractPredicateAbstractionLattice

Returns:

The top element of the lattice.

getBottomElem

protected AbstractPredicateAbstractionDomainElement getBottomElem()

Specified by:

getBottomElem in class AbstractPredicateAbstractionLattice

Returns:

The bottom element of the lattice.

getPredicateNameCombinationString

public java.lang.String getPredicateNameCombinationString()

Specified by:

getPredicateNameCombinationString in class AbstractPredicateAbstractionLattice

Returns:

The String which is used for combining the names of predicates for lattice types where multiple predicates determine an abstract element.