public class StepUnifier
extends java.lang.Object
It is customized for mmj2's needs as discussed in
mmj2/doc/StepUnifier.html
.
StepUnifier has much in common with the unification algorithm in ProofUnifier. These are the main differences:
Modifier and Type | Field and Description |
---|---|
static int |
F_LEVEL_NBR
Proof Step Formula assigned number -1 while logical hypotheses have
indexes 0 -> n.
|
Constructor and Description |
---|
StepUnifier(WorkVarManager workVarManager)
Constructor for StepUnifier.
|
Modifier and Type | Method and Description |
---|---|
void |
backoutFLevelApplieds()
Backout Proof Step Formula applied substitutions.
|
ParseNode[] |
finalizeAndLoadAssrtSubst()
Resolve chained substitutions into Work Variables and load the assrtSubst
array with the substitutions generated by successful Unification.
|
int[] |
getDerivAssrtXRef()
Returns an int array of indexes that cross references to the unifying
assertion logical hypothesis index.
|
void |
startProofWorksheet()
Initialization for handling unification of an entire Proof Worksheet.
|
ParseNode[] |
unifyAndMergeHypsSorted(LogHyp[] assrtLogHypArray,
ProofStepStmt[] derivStepHypArray)
Unifies sorted proof step logical hypotheses against a sorted array of
assertion logical hypotheses.
|
ParseNode[] |
unifyAndMergeHypsUnsorted(ProofStepStmt[] derivStepHypArray)
Unifies proof step logical hypotheses against an assertion's array of
logical hypotheses.
|
boolean |
unifyAndMergeStepFormula(boolean commit,
Assrt assrt,
ParseNode stepRoot)
Initialize for start of new Proof Step unification.
|
public static int F_LEVEL_NBR
public StepUnifier(WorkVarManager workVarManager)
workVarManager
- instance of WorkVarManager.public void startProofWorksheet()
NOTE: This function is vitally important -- it must be invoked at the start of Proof Worksheet processing in ProofUnifier.java (or whatever.) Its function is to prepare the Work Variables for use in the ProofWorksheet, including initializing their values and making sure that none are still allocated from previous usages. THEREFORE --
public ParseNode[] finalizeAndLoadAssrtSubst()
NOTE: This is an especially important part of the zany scheme to hold Work Variable substitution values inside the actual VarHyp instances (oy...) The resolution of chained substitutions into Work Variables does two vital things:
public int[] getDerivAssrtXRef()
Note that derivAssrtXRef index numbers correspond to the sorted arrays of Logical Hypotheses input to unifyAndMergeHypsSorted(). For example, if derivAssrtXRef[0] = 2 that means that the first (sorted) element of derivStepHypArray unifies with the 3rd (sorted) element of assrtLogHypArray.
public void backoutFLevelApplieds()
This function would need to be used if the full sequence of calls is not performed:
If unification succeeds for (1) but (2) and (3) are not called, or, if (1) succeeds and (2) fails, but (3) is not called, then backoutFLevelApplieds() would be necessary to tidy up...
But, in normal ProofUnifier processing this function is not needed because it does perform the full sequence of calls.
public boolean unifyAndMergeStepFormula(boolean commit, Assrt assrt, ParseNode stepRoot) throws VerifyException
Then unify/merge the proof step formula but not, yet, the logical hypotheses.
commit
- see commit
assrt
- the AssrtstepRoot
- the root of the step's formula ParseTreeVerifyException
- if an error occurspublic ParseNode[] unifyAndMergeHypsUnsorted(ProofStepStmt[] derivStepHypArray)
The derivation step hypothesis order used ought to be the order input by the user -- only if that order is wrong should unifyAndMergeHypsSorted() be used.
derivStepHypArray
- the hypArray for the derivation steppublic ParseNode[] unifyAndMergeHypsSorted(LogHyp[] assrtLogHypArray, ProofStepStmt[] derivStepHypArray)
This function ought to be called after first attempting unifyAndMergeHypsUnsorted() because the user's hypothesis order may be significant: there can be more than one valid, consistent unification if work variables are present in a proof step and its hypotheses. Therefore, this function ought to be used as a last resort (especially since it is slow.....)
The sort order of the input assrtLogHypArray and derivStepHypArray is particularly important due to the potential problem of combinatorial explosion requiring n-factorial hypothesis-pair unification attempts if the sort order is precisely wrong :-) ProofUnifier uses sortAssrtLogHypArray() and sortDerivStepHypArray() to order the hypotheses in order by descending formula length -- and if two formulas have equal length, then if one has a variable in common with the derivation step's main formula, then that hypothesis is placed ahead of the other. This sort order is based on empirical observation -- and seems to work ok.
assrtLogHypArray
- the logHypArrayderivStepHypArray
- the hypArray for the derivation step