public class ReplaceInfo extends DBInfo
Constructor and Description |
---|
ReplaceInfo(EquivalenceInfo eqInfo,
ImplicationInfo implInfo,
java.util.List<Assrt> assrtList,
TrOutput output,
boolean dbg) |
Modifier and Type | Method and Description |
---|---|
GenProofStepStmt |
createReplaceStep(mmj.transforms.WorksheetInfo info,
ParseNode prevVersion,
int i,
ParseNode newSubTree,
GenProofStepStmt childTrStmt)
Creates replace step (e.g.
|
boolean[] |
getPossibleReplaces(Stmt stmt,
mmj.transforms.WorksheetInfo info) |
boolean |
isFullReplaceStatement(Stmt stmt) |
public ReplaceInfo(EquivalenceInfo eqInfo, ImplicationInfo implInfo, java.util.List<Assrt> assrtList, TrOutput output, boolean dbg)
public boolean isFullReplaceStatement(Stmt stmt)
stmt
- the statementpublic GenProofStepStmt createReplaceStep(mmj.transforms.WorksheetInfo info, ParseNode prevVersion, int i, ParseNode newSubTree, GenProofStepStmt childTrStmt)
info
- the work sheet infoprevVersion
- the source node (e.g. g(A, B, C) )i
- the position for replace (e.g. 1 (second))newSubTree
- the new child (e.g. B')childTrStmt
- the equivalence of children (e.g. B = B' )public boolean[] getPossibleReplaces(Stmt stmt, mmj.transforms.WorksheetInfo info)