public class TransformationManager
extends java.lang.Object
Canonical form for the parse node is a parse node with sorted commutative/associative transformations.
The functions in this class are separated into 4 parts:
Modifier and Type | Field and Description |
---|---|
AssociativeInfo |
assocInfo |
ClosureInfo |
clInfo
The information about closure rules
|
CommutativeInfo |
comInfo |
ConjunctionInfo |
conjInfo |
boolean |
dbg |
EquivalenceInfo |
eqInfo
The information about equivalence rules
|
ImplicationInfo |
implInfo |
TrOutput |
output |
ProofAsst |
proofAsst |
Cnst |
provableLogicStmtTyp
The symbol like |- in set.mm
|
java.util.List<Prover> |
provers |
ReplaceInfo |
replInfo
The information about replace rules
|
boolean |
supportImplicationPrefix
This constant indicates whether we should try to indicate implication
prefix and perform auto-transformations with it.
|
VerifyProofs |
verifyProofs
It is necessary for formula construction
|
Constructor and Description |
---|
TransformationManager(ProofAsst proofAsst,
java.util.List<Assrt> assrtList,
Cnst provableLogicStmtTyp,
Messages messages,
VerifyProofs verifyProofs,
boolean supportPrefix,
boolean debugOutput)
Note: Here will be performed a lot of work during the construction of
this class!
|
Modifier and Type | Method and Description |
---|---|
void |
buildUWPProvers(java.util.List<Assrt> assrtList,
java.util.function.Predicate<Assrt> isLegal)
Create
Provers.UseWhenPossible provers for eligible assrts in the
database. |
Transformation |
createTransformation(ParseNode node,
mmj.transforms.WorksheetInfo info)
The main function to create transformation.
|
ProofStepStmt |
findReverseTransformations(mmj.transforms.WorksheetInfo info,
ParseNode root,
boolean finish) |
ParseNode |
getCanonicalForm(ParseNode originalNode,
mmj.transforms.WorksheetInfo info) |
protected Formula |
getFormula(ParseNode node)
This function is needed for debug
|
java.util.List<DerivationStep> |
tryToFindTransformations(ProofWorksheet proofWorksheet,
DerivationStep derivStep)
The main entry point transformation function.
|
public final boolean supportImplicationPrefix
public final boolean dbg
public final TrOutput output
public final VerifyProofs verifyProofs
public final Cnst provableLogicStmtTyp
public final EquivalenceInfo eqInfo
public final ImplicationInfo implInfo
public final ConjunctionInfo conjInfo
public final ReplaceInfo replInfo
public final ClosureInfo clInfo
public final AssociativeInfo assocInfo
public final CommutativeInfo comInfo
public final java.util.List<Prover> provers
public final ProofAsst proofAsst
public TransformationManager(ProofAsst proofAsst, java.util.List<Assrt> assrtList, Cnst provableLogicStmtTyp, Messages messages, VerifyProofs verifyProofs, boolean supportPrefix, boolean debugOutput)
assrtList
- the list all library assertsprovableLogicStmtTyp
- this constant indicates "provable logic
statement type"messages
- the message managerverifyProofs
- the proof verification is needed for some actionsproofAsst
- The proof asstsupportPrefix
- when it is true auto-transformation component will
try to use implication prefix in transformationsdebugOutput
- when it is true auto-transformation component will
produce a lot of debug outputpublic void buildUWPProvers(java.util.List<Assrt> assrtList, java.util.function.Predicate<Assrt> isLegal)
Provers.UseWhenPossible
provers for eligible assrts in the
database.assrtList
- The list of available assrts, sorted by number of
loghypsisLegal
- A filter for the assrtList: any illegal assrts will not be
used to build proverspublic Transformation createTransformation(ParseNode node, mmj.transforms.WorksheetInfo info)
node
- the source nodeinfo
- the information about previous stepspublic ParseNode getCanonicalForm(ParseNode originalNode, mmj.transforms.WorksheetInfo info)
public ProofStepStmt findReverseTransformations(mmj.transforms.WorksheetInfo info, ParseNode root, boolean finish)
public java.util.List<DerivationStep> tryToFindTransformations(ProofWorksheet proofWorksheet, DerivationStep derivStep)
proofWorksheet
- the proof work sheetderivStep
- the