public class ClosureInfo extends DBInfo
Modifier and Type | Class and Description |
---|---|
static class |
ClosureInfo.ClosureResult |
class |
ClosureInfo.ResultClosureInfo |
static class |
ClosureInfo.TemplDetectRes |
Constructor and Description |
---|
ClosureInfo(ImplicationInfo implInfo,
ConjunctionInfo conjInfo,
java.util.List<Assrt> assrtList,
TrOutput output,
boolean dbg) |
Modifier and Type | Method and Description |
---|---|
GenProofStepStmt |
closureProperty(mmj.transforms.WorksheetInfo info,
PropertyTemplate template,
ParseNode node,
boolean finishStatement,
boolean searchWithPrefix)
Creates closure rule applying generalized statement for the the node
recursively.
|
static PropertyTemplate |
createTemplateFromHyp(Assrt assrt) |
ClosureInfo.ResultClosureInfo |
extractImplClosureInfo(Assrt assrt)
Parses rules in implication form
|
ClosureInfo.ClosureResult |
getClosurePossibility(mmj.transforms.WorksheetInfo info,
ParseNode node,
PropertyTemplate template,
boolean searchWithPrefix) |
static ClosureInfo.TemplDetectRes |
getTemplateAndVarHyps(Assrt assrt) |
boolean |
hasClosureAssert(Stmt stmt,
ConstSubst constSubst,
PropertyTemplate template) |
static ClosureInfo.ClosureResult |
mergeSearchResults(ClosureInfo.ClosureResult preferred,
ClosureInfo.ClosureResult other) |
boolean |
performClosureTransformation(mmj.transforms.WorksheetInfo info) |
boolean |
performClosureTransformationInternal(mmj.transforms.WorksheetInfo info,
ParseNode input) |
public ClosureInfo(ImplicationInfo implInfo, ConjunctionInfo conjInfo, java.util.List<Assrt> assrtList, TrOutput output, boolean dbg)
public ClosureInfo.ResultClosureInfo extractImplClosureInfo(Assrt assrt)
assrt
- input assertionpublic static ClosureInfo.TemplDetectRes getTemplateAndVarHyps(Assrt assrt)
public static PropertyTemplate createTemplateFromHyp(Assrt assrt)
public GenProofStepStmt closureProperty(mmj.transforms.WorksheetInfo info, PropertyTemplate template, ParseNode node, boolean finishStatement, boolean searchWithPrefix)
info
- the work sheet infotemplate
- template (" _ e. CC" in the example)node
- the input node ("( sin ` A )" in the example)finishStatement
- true if the result statement is a target statementsearchWithPrefix
- true if we could search closure rules with
implication prefixpublic static ClosureInfo.ClosureResult mergeSearchResults(ClosureInfo.ClosureResult preferred, ClosureInfo.ClosureResult other)
public ClosureInfo.ClosureResult getClosurePossibility(mmj.transforms.WorksheetInfo info, ParseNode node, PropertyTemplate template, boolean searchWithPrefix)
public boolean performClosureTransformationInternal(mmj.transforms.WorksheetInfo info, ParseNode input)
public boolean performClosureTransformation(mmj.transforms.WorksheetInfo info)
public boolean hasClosureAssert(Stmt stmt, ConstSubst constSubst, PropertyTemplate template)