public abstract class AbstractPredicateAbstractionDomainElement extends AbstractDomainElement
Modifier and Type | Field and Description |
---|---|
private ImmutableSet<AbstractionPredicate> |
predicates |
private boolean |
topElem |
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. |
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() |
private ImmutableSet<AbstractionPredicate> predicates
private boolean topElem
public AbstractPredicateAbstractionDomainElement(ImmutableSet<AbstractionPredicate> predicates)
AbstractPredicateAbstractionDomainElement
from a
given list of abstraction predicates.protected AbstractPredicateAbstractionDomainElement(boolean isTopElem)
AbstractPredicateAbstractionDomainElement
that
is a top element if isTopElem is set to true; otherwise, it is a bottom
element.protected boolean isTopElem()
public ImmutableSet<AbstractionPredicate> getPredicates()
public void setPredicates(ImmutableSet<AbstractionPredicate> predicates)
predicates
- the abstraction predicates for this domain element to set.public Name name()
Named
public java.lang.String toString()
toString
in class AbstractDomainElement
public Term getDefiningAxiom(Term varOrConst, Services services)
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".
getDefiningAxiom
in class AbstractDomainElement
varOrConst
- The logical / program variable or skolem constant representing
an instance of this abstract domain element.services
- A services object.protected abstract Term combinePredicates(Term preds, Term newPred, Services services)
preds
- Term with all previous predicates.newPred
- The new predicate to combine preds with.services
- The services object.public abstract java.lang.String getPredicateNameCombinationString()
AbstractPredicateAbstractionLattice.getPredicateNameCombinationString()
. This is probably bad design, but a substitute of the Java shortcoming
that there are no abstract static methods.public java.lang.String toParseableString(Services services)
AbstractDomainElement
AbstractDomainElement
. It should always hold that, for an
AbstractDomainElement
e and the corresponding
AbstractDomainLattice
l, that
l.fromString(e.toParseableString(),
services).equals(e)
.toParseableString
in class AbstractDomainElement
services
- The services object.public abstract boolean equals(java.lang.Object obj)
equals
in class java.lang.Object
public abstract int hashCode()
hashCode
in class java.lang.Object