public class LogHyp extends Hyp
Note: there is no rule stipulating that the "Logical Hypothesis" have a Type Code of "|-" or its equivalent in the LogicalSystem under such discussion. In other words, a "syntax hypothesis" could be "snuck in".
DESC_NBR_PROOF_REFS, exprParseTree, LABEL, logHypsL1HiLoKey, logHypsMaxDepth, nbrProofRefs
chapterNbr, description, isTempObject, SECTION_AND_MOBJ_NBR, sectionMObjNbr, sectionNbr, seq, SEQ
Modifier | Constructor and Description |
---|---|
|
LogHyp(int seq,
java.util.Map<java.lang.String,Sym> symTbl,
java.util.Map<java.lang.String,Stmt> stmtTbl,
java.util.List<java.lang.String> symList,
java.lang.String labelS,
java.lang.String typS)
Construct LogHyp using sequence number plus label, Type Code and Sym list
Strings.
|
protected |
LogHyp(int tempLogHypSeq,
java.lang.String tempLogHypLabel,
Formula tempLogHypFormula,
VarHyp[] tempVarHypArray,
ParseTree tempLogHypParseTree)
Construct temp LogHyp using precomputed values and doing no validation.
|
Modifier and Type | Method and Description |
---|---|
static LogHyp |
BuildTempLogHypObject(int tempLogHypSeq,
java.lang.String tempLogHypLabel,
Formula tempLogHypFormula,
Hyp[] tempHypArray,
ParseTree tempLogHypParseTree)
Construct a LogHyp object that is temporary, in the sense that it will
not be added to the Logical System Statement Table or participate in
other features of mmj2.
|
int |
getMandHypArrayLength()
Return the mandatory Hyp array length.
|
VarHyp[] |
getMandVarHypArray()
Return the mandatory VarHyp array for this VarHyp.
|
int |
renderParsedSubExpr(java.lang.StringBuilder sb,
int maxDepth,
int maxLength,
ParseNode[] child)
Throws an IllegalArgumentException because a ParseTree for a parsed
sub-expression should contain only VarHyp and Syntax Axiom nodes.
|
void |
setMandVarHypArray(VarHyp[] varHypArray)
Set the VarHyp array for this VarHyp (they're all "mandatory").
|
equals, getExprParseTree, getExprRPN, getFormula, getLabel, getNbrProofRefs, getTyp, hashCode, incrementNbrProofRefs, initNbrProofRefs, resetLogHypsL1HiLoKey, resetLogHypsMaxDepth, setExprParseTree, setExprRPN, setLogHypsL1HiLoKey, setLogHypsMaxDepth, setTyp, toJSONString, toString
getChapterNbr, getDescription, getDescriptionForSearch, getIsTempObject, getOrigSectionNbr, getSectionMObjNbr, getSectionNbr, getSeq, setChapterNbr, setDescription, setIsTempObject, setSectionMObjNbr, setSectionNbr
public LogHyp(int seq, java.util.Map<java.lang.String,Sym> symTbl, java.util.Map<java.lang.String,Stmt> stmtTbl, java.util.List<java.lang.String> symList, java.lang.String labelS, java.lang.String typS) throws LangException
seq
- MObj.seq numbersymTbl
- Symbol Table (Map)stmtTbl
- Statement Table (Map)symList
- list of Syms comprising ExpressionlabelS
- Statement label String.typS
- Type Code id String.LangException
- if duplicate, etc.protected LogHyp(int tempLogHypSeq, java.lang.String tempLogHypLabel, Formula tempLogHypFormula, VarHyp[] tempVarHypArray, ParseTree tempLogHypParseTree)
tempLogHypSeq
- MObj.seqtempLogHypLabel
- Stmt.labeltempLogHypFormula
- Stmt.formulatempVarHypArray
- LogHyp.varHypArraytempLogHypParseTree
- Stmt.exprParseTreepublic static LogHyp BuildTempLogHypObject(int tempLogHypSeq, java.lang.String tempLogHypLabel, Formula tempLogHypFormula, Hyp[] tempHypArray, ParseTree tempLogHypParseTree)
Beware: no real validation is performed, except that bogus input may generate IllegalArgumentException or ArrayOutOfBoundsException!
tempLogHypSeq
- MObj.seqtempLogHypLabel
- Stmt.labeltempLogHypFormula
- Stmt.formulatempHypArray
- array containing VarHyps for formula but perhaps
other Hyps as welltempLogHypParseTree
- Stmt.exprParseTreepublic VarHyp[] getMandVarHypArray()
Simply return varHypArray, the VarHyp's used in the LogHyp's Formula.
getMandVarHypArray
in class Stmt
public int getMandHypArrayLength()
getMandHypArrayLength
in class Stmt
public void setMandVarHypArray(VarHyp[] varHypArray)
varHypArray
- array of VarHyp's used in Formula.public int renderParsedSubExpr(java.lang.StringBuilder sb, int maxDepth, int maxLength, ParseNode[] child)
renderParsedSubExpr
in class Stmt
sb
- StringBuilder already initialized for appending characters.maxDepth
- maximum depth of Notation Syntax axioms in sub-tree to be
printed. Set to Integer.MAX_VALUE to turn off depth checking.maxLength
- maximum length of output sub-expression. Set to
Integer.MAX_VALUE to turn off depth checking.child
- array of ParseNode, corresponding to VarHyp nodes to be
substituted into the Stmt.java.lang.IllegalArgumentException
- always