public class AssociativeInfo extends DBInfo
Note: the current implementation contains some stub implementations!
Constructor and Description |
---|
AssociativeInfo(EquivalenceInfo eqInfo,
ClosureInfo clInfo,
ReplaceInfo replInfo,
java.util.List<Assrt> assrtList,
TrOutput output,
boolean dbg) |
Modifier and Type | Method and Description |
---|---|
GenProofStepStmt |
createAssociativeStep(mmj.transforms.WorksheetInfo info,
mmj.transforms.GeneralizedStmt assocProp,
int from,
ParseNode firstNode,
ParseNode secondNode)
Creates f(f(a, b), c) = f(a, f(b, c)) or f(a, f(b, c)) = f(f(a, b), c)
statement.
|
mmj.transforms.GeneralizedStmt |
getGenStmtForAssocNode(ParseNode node,
mmj.transforms.WorksheetInfo info)
This function searches generalized statement for node which is considered
to be the root of some associative actions
|
static boolean |
isAssociativeWithProp(ParseNode node,
mmj.transforms.GeneralizedStmt assocProp,
mmj.transforms.WorksheetInfo info) |
public AssociativeInfo(EquivalenceInfo eqInfo, ClosureInfo clInfo, ReplaceInfo replInfo, java.util.List<Assrt> assrtList, TrOutput output, boolean dbg)
public static boolean isAssociativeWithProp(ParseNode node, mmj.transforms.GeneralizedStmt assocProp, mmj.transforms.WorksheetInfo info)
public mmj.transforms.GeneralizedStmt getGenStmtForAssocNode(ParseNode node, mmj.transforms.WorksheetInfo info)
node
- the input nodeinfo
- the work sheet infopublic GenProofStepStmt createAssociativeStep(mmj.transforms.WorksheetInfo info, mmj.transforms.GeneralizedStmt assocProp, int from, ParseNode firstNode, ParseNode secondNode)
info
- the work sheet infoassocProp
- the generalized associative statementfrom
- 0 if we should use f(f(a, b), c) = f(a, f(b, c)) form and 1
if we should use f(a, f(b, c)) = f(f(a, b), c)firstNode
- the first node (f(f(a, b), c) or f(a, f(b, c)))secondNode
- the second node (f(a, f(b, c)) or f(f(a, b), c))