public class DistinctVariablesStmt extends ProofWorkStmt
A proof may contain 0 -> n DistinctVariablesStmt's. They are used during Unification as *additions* to whatever $d statements are contained in the database for the theorem being proved.
Constructor and Description |
---|
DistinctVariablesStmt(ProofWorksheet w)
Default Constructor.
|
DistinctVariablesStmt(ProofWorksheet w,
java.util.List<Var> dvGroup)
Constructor with a group of distinct variables as input.
|
Modifier and Type | Method and Description |
---|---|
int |
computeFieldIdCol(int fieldId)
Function used for cursor positioning.
|
static java.util.List<java.util.List<Var>> |
eliminateDvGroupsAlreadyPresent(DistinctVariablesStmt[] dvStmtArray,
java.util.List<java.util.List<Var>> dvGroupsIn)
Returns a dvGroup ArrayList of elements of the input dvGroup1 ArrayList
which are not already specified by the contents of the input array of
DistinctVariableStmt.
|
Var[] |
getDv() |
java.lang.String |
load(java.lang.String firstToken)
Load Distinct Variable Statement.
|
boolean |
stmtIsIncomplete()
Returns false, DistinctVariablesStmt never "incomplete" in ProofWorksheet
terms.
|
void |
tmffReformat()
Reformats Derivation Step using TMFF.
|
appendToProofText, getLineCnt, getProofWorksheet, getStmtDiagnosticInfo, getStmtText, hasMatchingRefLabel, hasMatchingStepNbr, loadAllStmtTextGetNextStmt, loadStmtTextGetNextStmt, loadStmtTextGetOptionalToken, loadStmtTextGetRequiredToken, setStmtCursorToCurrLineColumn, updateLineCntUsingTokenizer
public DistinctVariablesStmt(ProofWorksheet w)
w
- ProofWorksheet objectpublic DistinctVariablesStmt(ProofWorksheet w, java.util.List<Var> dvGroup)
w
- ProofWorksheet objectdvGroup
- List of Var which are distinct.public static java.util.List<java.util.List<Var>> eliminateDvGroupsAlreadyPresent(DistinctVariablesStmt[] dvStmtArray, java.util.List<java.util.List<Var>> dvGroupsIn)
For example, if the input dvGroup has an element
dvStmtArray
- array of DistinctVariablesStmtdvGroupsIn
- List of List of Varpublic boolean stmtIsIncomplete()
stmtIsIncomplete
in class ProofWorkStmt
public int computeFieldIdCol(int fieldId)
computeFieldIdCol
in class ProofWorkStmt
fieldId
- value identify ProofWorkStmt field for cursor positioning,
as defined in PaConstants.FIELD_ID_*.public void tmffReformat()
Does nothing as there is no formula to reformat.
tmffReformat
in class ProofWorkStmt
public Var[] getDv()
public java.lang.String load(java.lang.String firstToken) throws java.io.IOException, MMIOException, ProofAsstException
Distinct Variable group of variables must satisfy these edits:
Output/Updates
load
in class ProofWorkStmt
firstToken
- first token of the statementjava.io.IOException
- if IO errorMMIOException
- if an error occurredProofAsstException
- if an error occurred