public abstract class AbstractDomainElement extends 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).
|
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.