|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectPandora.NDRules.NDRule
Pandora.NDRules.Substitution
public class Substitution
Implements the Substitution rule.
Extends abstract class NDRule.
Field Summary |
---|
Fields inherited from class Pandora.NDRules.NDRule |
---|
firstLine |
Constructor Summary | |
---|---|
Substitution(ProofBox proof)
Constructs a Substitution. |
Method Summary | |
---|---|
void |
addLine(ProofLine clickedLine)
Adds the extra lines to the rule once the input line has been added. |
void |
apply()
Called by the RuleController to apply the rule. |
void |
check()
Called by the RuleController to check the input lines to the rule. |
void |
findAll(ProofLine pELine,
ProofLine pFLine)
This method is only used when the Substitution rule is applied forwards. It finds all the possible substitution between two passed lines' formulae. |
void |
findMatch(Formula f,
Equals e,
ProofLine p)
This is a helper method called by the findAll method, to check if the passed Term is cotained in the passed Equals Formula's left or right hand side. |
void |
findMatch(Term pTerm,
Equals pEquals,
ProofLine pLine)
|
boolean |
haveAll()
Returns true if the rule has all of the required input lines. |
void |
showMatch()
|
Methods inherited from class Pandora.NDRules.NDRule |
---|
addInputLine, checkSignature, getNewFormula |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
---|
public Substitution(ProofBox proof)
proof
- ProofBox representing in which box the rule is being appliedMethod Detail |
---|
public void addLine(ProofLine clickedLine) throws java.lang.Exception
addLine
in class NDRule
clickedLine
- ProofLine which has been selected
java.lang.Exception
public boolean haveAll()
haveAll
in class NDRule
public void check() throws java.lang.Exception
check
in class NDRule
java.lang.Exception
public void apply() throws java.lang.Exception
apply
in class NDRule
java.lang.Exception
public void findMatch(Formula f, Equals e, ProofLine p)
t
- Term represents the Term to look for in the passed Equals formula.e
- Equals represents the Equals formula to look for the passed Term in.line
- ProofLine represents the proof line containing the passed Term.public void findMatch(Term pTerm, Equals pEquals, ProofLine pLine)
public void findAll(ProofLine pELine, ProofLine pFLine) throws java.lang.Exception
eLine
- ProofLine represents the proof line which includes the Equals Formula.fLine
- ProofLine represents the proof line which is to be looked for the possible substitutions.
java.lang.Exception
public void showMatch()
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |