public class SimplePredicateAbstractionDomainElement extends AbstractPredicateAbstractionDomainElement
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.
|
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. |
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() |
getDefiningAxiom, getPredicates, isTopElem, name, setPredicates, toParseableString, toString
public static final SimplePredicateAbstractionDomainElement BOTTOM
public static final SimplePredicateAbstractionDomainElement TOP
public SimplePredicateAbstractionDomainElement(ImmutableSet<AbstractionPredicate> predicates)
SimplePredicateAbstractionDomainElement
from a
given list of abstraction predicates.private SimplePredicateAbstractionDomainElement(boolean isTopElem)
SimplePredicateAbstractionDomainElement
that is
a top element if isTopElem is set to true; otherwise, it is a bottom
element.protected Term combinePredicates(Term preds, Term newPred, Services services)
AbstractPredicateAbstractionDomainElement
combinePredicates
in class AbstractPredicateAbstractionDomainElement
preds
- Term with all previous predicates.newPred
- The new predicate to combine preds with.services
- The services object.public java.lang.String getPredicateNameCombinationString()
AbstractPredicateAbstractionDomainElement
AbstractPredicateAbstractionLattice.getPredicateNameCombinationString()
. This is probably bad design, but a substitute of the Java shortcoming
that there are no abstract static methods.getPredicateNameCombinationString
in class AbstractPredicateAbstractionDomainElement
public boolean equals(java.lang.Object obj)
equals
in class AbstractPredicateAbstractionDomainElement
public int hashCode()
hashCode
in class AbstractPredicateAbstractionDomainElement