Modifier and Type | Field and Description |
---|---|
static java.lang.String |
BEFORE_ID_SEPARATOR
Separator between multiple before IDs.
|
private java.lang.String |
beforeIds
The optional previous IDs of the label this one is derived from separated by ";".
|
private int |
majorId
The unique major ID of this term label in the
Sequent . |
private int |
minorId
The per major ID unique minor ID of this term label in the
Sequent . |
static Name |
NAME
The unique name of this label.
|
static java.lang.String |
PROOF_COUNTER_NAME
The name used in
Services.getCounter(String) to keep track
of the already used IDs. |
static java.lang.String |
PROOF_COUNTER_SUB_PREFIX
The prefix of the name used in
Services.getCounter(String) to
keep track of the already used sub IDs. |
Constructor and Description |
---|
FormulaTermLabel(int majorId,
int minorId)
Constructor.
|
FormulaTermLabel(int majorId,
int minorId,
java.util.Collection<java.lang.String> beforeIds)
Constructor.
|
FormulaTermLabel(java.lang.String id)
Constructor.
|
FormulaTermLabel(java.lang.String id,
java.lang.String beforeIds)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
boolean |
equals(java.lang.Object o) |
java.lang.String[] |
getBeforeIds()
Returns the optional previous IDs of the label this one is derived from.
|
private static java.lang.String[] |
getBeforeIds(java.lang.String beforeIds)
Returns the optional previous IDs of the label this one is derived from.
|
java.lang.Object |
getChild(int i)
Retrieves the i-th parameter object of this term label.
|
int |
getChildCount()
Gets the number of parameters of this term label.
|
java.lang.String |
getId()
Returns the unique ID of this label in the
Sequent . |
int |
getMajorId()
Returns the major part of the unique ID.
|
static int |
getMajorId(java.lang.String id)
Returns the major part of the given ID.
|
int |
getMinorId()
Returns the minor part of the unique ID.
|
static int |
getMinorId(java.lang.String id)
Returns the minor part of the given ID.
|
static java.util.List<java.lang.String> |
getValidBeforeIds(java.lang.String beforeIds)
Returns the optional previous IDs if they are all valid.
|
Name |
name()
returns the name of this element
|
static int |
newLabelSubID(Services services,
FormulaTermLabel label)
Creates a new label sub ID.
|
static int |
newLabelSubID(Services services,
int labelId)
Creates a new label sub ID.
|
java.lang.String |
toString() |
public static final Name NAME
public static final java.lang.String PROOF_COUNTER_NAME
Services.getCounter(String)
to keep track
of the already used IDs.public static final java.lang.String PROOF_COUNTER_SUB_PREFIX
Services.getCounter(String)
to
keep track of the already used sub IDs.public static final java.lang.String BEFORE_ID_SEPARATOR
private final int majorId
Sequent
.private final int minorId
Sequent
.private final java.lang.String beforeIds
public FormulaTermLabel(java.lang.String id) throws TermLabelException
id
- The unique ID of this term label in the Sequent
.TermLabelException
- Occurred Exception in case that the given ID is not valid.public FormulaTermLabel(java.lang.String id, java.lang.String beforeIds) throws TermLabelException
id
- The unique ID of this term label in the Sequent
.beforeIds
- The optional previous IDs of the label this one is derived from separated by ";".TermLabelException
- Occurred Exception in case that the given IDs are not valid.public FormulaTermLabel(int majorId, int minorId)
majorId
- The major part of the unique ID.minorId
- The minor part of the unique ID.public FormulaTermLabel(int majorId, int minorId, java.util.Collection<java.lang.String> beforeIds)
majorId
- The major part of the unique ID.minorId
- The minor part of the unique ID.beforeIds
- The optional previous ID of the label this one is derived from.public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public java.lang.String toString()
toString
in class java.lang.Object
public java.lang.Object getChild(int i)
A term label may have structure, i.e. can be parameterized.
public int getChildCount()
getChildCount
in interface TermLabel
public java.lang.String getId()
Sequent
.Sequent
.public int getMajorId()
public static int getMajorId(java.lang.String id) throws TermLabelException
id
- The ID to extract its major part.TermLabelException
- Occurred Exception in case that the given ID is not valid.public int getMinorId()
public static int getMinorId(java.lang.String id) throws TermLabelException
id
- The ID to extract its minor part.TermLabelException
- Occurred Exception in case that the given ID is not valid.public java.lang.String[] getBeforeIds()
private static java.lang.String[] getBeforeIds(java.lang.String beforeIds)
beforeIds
- The String
with the before IDs.public static java.util.List<java.lang.String> getValidBeforeIds(java.lang.String beforeIds) throws TermLabelException
beforeIds
- The String
with the before IDs to analyze.TermLabelException
- Occurred Exception in case that the given IDs are not valid.public Name name()
public static int newLabelSubID(Services services, FormulaTermLabel label)
services
- The Services
to use.label
- The parent FormulaTermLabel
which provides the major ID.public static int newLabelSubID(Services services, int labelId)
services
- The Services
to use.labelId
- The parent FormulaTermLabel
which provides the major ID.