public abstract class AbstractDomainElement extends java.lang.Object implements Named
Constructor and Description |
---|
AbstractDomainElement() |
Modifier and Type | Method and Description |
---|---|
abstract 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 |
toParseableString(Services services)
Returns a parseable String representation of this
AbstractDomainElement . |
java.lang.String |
toString() |
public abstract Term getDefiningAxiom(Term varOrConst, Services services)
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".
varOrConst
- The logical / program variable or skolem constant representing
an instance of this abstract domain element.services
- A services object.public abstract java.lang.String toParseableString(Services services)
AbstractDomainElement
. It should always hold that, for an
AbstractDomainElement
e and the corresponding
AbstractDomainLattice
l, that
l.fromString(e.toParseableString(),
services).equals(e)
.services
- The services object.public java.lang.String toString()
toString
in class java.lang.Object