public class Neg extends SignAnalysisDomainElem
Modifier | Constructor and Description |
---|---|
private |
Neg() |
Modifier and Type | Method and Description |
---|---|
Term |
getDefiningAxiom(Term varOrConst,
Services services)
Return the defining axiom, instantiated for a given Term (skolem constant
or logical / program variable).
|
static Neg |
getInstance() |
Name |
name()
returns the name of this element
|
java.lang.String |
toParseableString(Services services)
Returns a parseable String representation of this
AbstractDomainElement . |
isBottom, isGeq, isLeq, isNeg, isPos, isTop, isZero
toString
private static final Neg INSTANCE
public static Neg getInstance()
public Name name()
Named
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.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.