de.uka.ilkd.key.axiom_abstraction.predicateabstraction

Class SimplePredicateAbstractionDomainElement

java.lang.Object

de.uka.ilkd.key.axiom_abstraction.AbstractDomainElement

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

de.uka.ilkd.key.axiom_abstraction.predicateabstraction.SimplePredicateAbstractionDomainElement

All Implemented Interfaces:

Named

public class SimplePredicateAbstractionDomainElement
extends AbstractPredicateAbstractionDomainElement

An abstract domain element for a predicate abstraction lattice encapsulating exactly one abstraction predicate.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
static SimplePredicateAbstractionDomainElement	BOTTOM The bottom element of any predicate abstraction lattice.
static SimplePredicateAbstractionDomainElement	TOP The top element of any predicate abstraction lattice.

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method and Description
protected Term	combinePredicates(Term preds, Term newPred, Services services) Combines the given predicate terms (classically using AND or OR).
boolean	equals(java.lang.Object obj)
java.lang.String	getPredicateNameCombinationString() NOTE: This method should be defined in accordance with AbstractPredicateAbstractionLattice.getPredicateNameCombinationString() .
int	hashCode()

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

getDefiningAxiom, getPredicates, isTopElem, name, setPredicates, toParseableString, toString

Methods inherited from class java.lang.Object

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

Field Detail

BOTTOM

public static final SimplePredicateAbstractionDomainElement BOTTOM

The bottom element of any predicate abstraction lattice.

TOP

public static final SimplePredicateAbstractionDomainElement TOP

The top element of any predicate abstraction lattice.

Constructor Detail

SimplePredicateAbstractionDomainElement

public SimplePredicateAbstractionDomainElement(ImmutableSet<AbstractionPredicate> predicates)

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

SimplePredicateAbstractionDomainElement

private SimplePredicateAbstractionDomainElement(boolean isTopElem)

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

Method Detail

combinePredicates

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

Description copied from class: AbstractPredicateAbstractionDomainElement

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

Specified by:

combinePredicates in class AbstractPredicateAbstractionDomainElement

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 java.lang.String getPredicateNameCombinationString()

Description copied from class: AbstractPredicateAbstractionDomainElement

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.

Specified by:

getPredicateNameCombinationString in class AbstractPredicateAbstractionDomainElement

Returns:

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

equals

public boolean equals(java.lang.Object obj)

Specified by:

equals in class AbstractPredicateAbstractionDomainElement

hashCode

public int hashCode()

Specified by:

hashCode in class AbstractPredicateAbstractionDomainElement