de.uka.ilkd.key.axiom_abstraction.predicateabstraction

Class AbstractPredicateAbstractionDomainElement

java.lang.Object

de.uka.ilkd.key.axiom_abstraction.AbstractDomainElement

de.uka.ilkd.key.axiom_abstraction.predicateabstraction.AbstractPredicateAbstractionDomainElement

All Implemented Interfaces:

Named

Direct Known Subclasses:

ConjunctivePredicateAbstractionDomainElement, DisjunctivePredicateAbstractionDomainElement, SimplePredicateAbstractionDomainElement

public abstract class AbstractPredicateAbstractionDomainElement
extends AbstractDomainElement

A base class for abstract domain elements in a predicate abstraction lattice.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableSet<AbstractionPredicate>	predicates
private boolean	topElem

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AbstractPredicateAbstractionDomainElement(boolean isTopElem) Constructs a new AbstractPredicateAbstractionDomainElement that is a top element if isTopElem is set to true; otherwise, it is a bottom element.
	AbstractPredicateAbstractionDomainElement(ImmutableSet<AbstractionPredicate> predicates) Constructs a new AbstractPredicateAbstractionDomainElement from a given list of abstraction predicates.

Method Summary

Modifier and Type	Method and Description
protected abstract Term	combinePredicates(Term preds, Term newPred, Services services) Combines the given predicate terms (classically using AND or OR).
abstract boolean	equals(java.lang.Object obj)
Term	getDefiningAxiom(Term varOrConst, Services services) Return the defining axiom, instantiated for a given Term (skolem constant or logical / program variable).
abstract java.lang.String	getPredicateNameCombinationString() NOTE: This method should be defined in accordance with AbstractPredicateAbstractionLattice.getPredicateNameCombinationString() .
ImmutableSet<AbstractionPredicate>	getPredicates()
abstract int	hashCode()
protected boolean	isTopElem()
Name	name() returns the name of this element
void	setPredicates(ImmutableSet<AbstractionPredicate> predicates)
java.lang.String	toParseableString(Services services) Returns a parseable String representation of this AbstractDomainElement.
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

predicates

private ImmutableSet<AbstractionPredicate> predicates

topElem

private boolean topElem

Constructor Detail

AbstractPredicateAbstractionDomainElement

public AbstractPredicateAbstractionDomainElement(ImmutableSet<AbstractionPredicate> predicates)

Constructs a new AbstractPredicateAbstractionDomainElement from a given list of abstraction predicates.

AbstractPredicateAbstractionDomainElement

protected AbstractPredicateAbstractionDomainElement(boolean isTopElem)

Constructs a new AbstractPredicateAbstractionDomainElement that is a top element if isTopElem is set to true; otherwise, it is a bottom element.

Method Detail

isTopElem

protected boolean isTopElem()

Returns:

Whether this element is the top element of the lattice (the axiom of which is true for every input).

getPredicates

public ImmutableSet<AbstractionPredicate> getPredicates()

Returns:

The abstraction predicates for this domain element.

setPredicates

public void setPredicates(ImmutableSet<AbstractionPredicate> predicates)

Parameters:

predicates - the abstraction predicates for this domain element to set.

name

public Name name()

Description copied from interface: Named

returns the name of this element

Returns:

the name of the element

toString

public java.lang.String toString()

Overrides:

toString in class AbstractDomainElement

getDefiningAxiom

public Term getDefiningAxiom(Term varOrConst,
                             Services services)

Description copied from class: AbstractDomainElement

Return the defining axiom, instantiated for a given Term (skolem constant or logical / program variable). The term can be seen as a representative of this abstract domain element; the returned formula must formally specify this.

If this element describes, for instance, all numbers divisible by 2, the method could return the formula "varOrConst % 2 == 0".

Specified by:

getDefiningAxiom in class AbstractDomainElement

Parameters:

varOrConst - The logical / program variable or skolem constant representing an instance of this abstract domain element.

services - A services object.

Returns:

A JavaDL formula expressing that the given variable or constant represents an instance of this abstract domain element.

combinePredicates

protected abstract Term combinePredicates(Term preds,
                                          Term newPred,
                                          Services services)

Combines the given predicate terms (classically using AND or OR).

Parameters:

preds - Term with all previous predicates.

newPred - The new predicate to combine preds with.

services - The services object.

Returns:

The combination of preds with newPred.

getPredicateNameCombinationString

public abstract java.lang.String getPredicateNameCombinationString()

NOTE: This method should be defined in accordance with AbstractPredicateAbstractionLattice.getPredicateNameCombinationString() . This is probably bad design, but a substitute of the Java shortcoming that there are no abstract static methods.

Returns:

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

toParseableString

public java.lang.String toParseableString(Services services)

Description copied from class: AbstractDomainElement

Returns a parseable String representation of this AbstractDomainElement. It should always hold that, for an AbstractDomainElement e and the corresponding AbstractDomainLattice l, that l.fromString(e.toParseableString(), services).equals(e).

Specified by:

toParseableString in class AbstractDomainElement

Parameters:

services - The services object.

Returns:

A parseable String representation of this domain element.

equals

public abstract boolean equals(java.lang.Object obj)

Overrides:

equals in class java.lang.Object

hashCode

public abstract int hashCode()

Overrides:

hashCode in class java.lang.Object