de.uka.ilkd.key.axiom_abstraction.predicateabstraction

Class AbstractPredicateAbstractionLattice

java.lang.Object

de.uka.ilkd.key.axiom_abstraction.AbstractDomainLattice

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

All Implemented Interfaces:

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

Direct Known Subclasses:

ConjunctivePredicateAbstractionLattice, DisjunctivePredicateAbstractionLattice, SimplePredicateAbstractionLattice

public abstract class AbstractPredicateAbstractionLattice
extends AbstractDomainLattice

A super class for predicates abstraction lattices. Implements basic join functionality and a template for an iterator initializing ImmutableFixedLengthBitSets.

Author:

Dominic Scheurer

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected class	AbstractPredicateAbstractionLattice.AbstractPredicateLatticeIterator An abstract iterator which basically only sets up the bit sets used for building up complex iterators.

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

PartialComparator.PartialComparisonResult

Constructor Summary

Constructors

Constructor and Description
AbstractPredicateAbstractionLattice()

Method Summary

Modifier and Type	Method and Description
protected abstract AbstractPredicateAbstractionDomainElement	getBottomElem()
abstract java.lang.String	getPredicateNameCombinationString()
protected abstract AbstractPredicateAbstractionDomainElement	getTopElem()
protected AbstractPredicateAbstractionDomainElement	join(AbstractDomainElement a, AbstractDomainElement b, java.util.function.BiFunction<ImmutableSet<AbstractionPredicate>,ImmutableSet<AbstractionPredicate>,ImmutableSet<AbstractionPredicate>> combiner, java.util.function.Function<ImmutableSet<AbstractionPredicate>,AbstractPredicateAbstractionDomainElement> abstrElemConstructor) Joins to abstract elements in the lattice.

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

abstractFrom, compare, fromString, getSideConditionForAxiom, iterator, join

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Constructor Detail

AbstractPredicateAbstractionLattice

public AbstractPredicateAbstractionLattice()

Method Detail

join

protected AbstractPredicateAbstractionDomainElement join(AbstractDomainElement a,
                                                         AbstractDomainElement b,
                                                         java.util.function.BiFunction<ImmutableSet<AbstractionPredicate>,ImmutableSet<AbstractionPredicate>,ImmutableSet<AbstractionPredicate>> combiner,
                                                         java.util.function.Function<ImmutableSet<AbstractionPredicate>,AbstractPredicateAbstractionDomainElement> abstrElemConstructor)

Joins to abstract elements in the lattice.

Parameters:

a - First domain element for the join.

b - Second domain element for the join.

combiner - The combination function (e.g., "AND") for the respective predicates of the inputs..

abstrElemConstructor - A function constructing abstract domain elements from predicates.

Returns:

The joined abstract domain element.

getTopElem

protected abstract AbstractPredicateAbstractionDomainElement getTopElem()

Returns:

The top element of the lattice.

getBottomElem

protected abstract AbstractPredicateAbstractionDomainElement getBottomElem()

Returns:

The bottom element of the lattice.

getPredicateNameCombinationString

public abstract java.lang.String getPredicateNameCombinationString()

Returns:

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