de.uka.ilkd.key.axiom_abstraction.predicateabstraction

Class ConjunctivePredicateAbstractionDomainElement

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

All Implemented Interfaces:

Named

public class ConjunctivePredicateAbstractionDomainElement
extends AbstractPredicateAbstractionDomainElement

An abstract domain element for a predicate abstraction lattice based on the conjunction of predicates.

Author:

Dominic Scheurer

Field Summary

Fields

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

Constructor Summary

Constructors

Modifier	Constructor and Description
private	ConjunctivePredicateAbstractionDomainElement(boolean isTopElem) Constructs a new ConjunctivePredicateAbstractionDomainElement that is a top element if isTopElem is set to true; otherwise, it is a bottom element.
	ConjunctivePredicateAbstractionDomainElement(ImmutableSet<AbstractionPredicate> predicates) Constructs a new ConjunctivePredicateAbstractionDomainElement 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 ConjunctivePredicateAbstractionDomainElement BOTTOM

The bottom element of any predicate abstraction lattice.

TOP

public static final ConjunctivePredicateAbstractionDomainElement TOP

The top element of any predicate abstraction lattice.

Constructor Detail

ConjunctivePredicateAbstractionDomainElement

public ConjunctivePredicateAbstractionDomainElement(ImmutableSet<AbstractionPredicate> predicates)

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

ConjunctivePredicateAbstractionDomainElement

private ConjunctivePredicateAbstractionDomainElement(boolean isTopElem)

Constructs a new ConjunctivePredicateAbstractionDomainElement 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