public class LogicFormula extends Formula
Constructor and Description |
---|
LogicFormula(int workCnt,
Sym[] workFormula)
Construct using count and Sym array.
|
LogicFormula(java.util.Map<java.lang.String,Sym> symTbl,
java.lang.String typS,
java.util.List<java.lang.String> symList,
java.util.List<Hyp> exprHypList)
Construct using String Type Code and Sym List.
|
Modifier and Type | Method and Description |
---|---|
void |
verifyExprSymsDefAndActive(java.util.Map<java.lang.String,Sym> symTbl,
java.util.List<java.lang.String> symList,
java.util.List<Hyp> hypList)
Verifies that each Sym id in Expression is active and accumulates the
matching VarHyp's in the input exprHypList param.
|
accumHypInList, buildMandVarHypArray, buildRuleFormatExpr, collectConstFrequenceAndInitConstList, computeWidthOfWidestExprCnst, constructTempDummyFormula, equals, exprEquals, exprToString, getCnt, getExpr, getParseNodeHolderExpr, getParseNodeHolderExpr, getSym, getTyp, hashCode, preunificationCheck, setTyp, setTyp, sortConstList, srcStmtEquals, toProofWorksheetStringBuilder, toString, toStringBuilderLineList
public LogicFormula(int workCnt, Sym[] workFormula)
workCnt
- length of formula.workFormula
- Formula Sym array.public LogicFormula(java.util.Map<java.lang.String,Sym> symTbl, java.lang.String typS, java.util.List<java.lang.String> symList, java.util.List<Hyp> exprHypList) throws LangException
Verifies that each Sym id in Expression is active and accumulates the matching VarHyp's in the input exprHypList param.
symTbl
- Symbol Table (map).typS
- Formula Type Code String.symList
- Formula Expression as List of Sym id StringsexprHypList
- List of Hyps, updated in function.LangException
- if an error occurredpublic void verifyExprSymsDefAndActive(java.util.Map<java.lang.String,Sym> symTbl, java.util.List<java.lang.String> symList, java.util.List<Hyp> hypList) throws LangException
symTbl
- Map containing Cnst and Var definitions.symList
- expression's symbol character stringshypList
- List of Hyp's. Is updated with unique variable hypotheses
in the expression. Because the list is maintained in database
statement sequence order, hypList should either be empty (new)
before the call, or already be in that order (see
accumHypInList
.LangException
- if duplicate symbol, etc. (see
mmj.lang.LangConstants.java
)