Pandora.NDRules
Class Substitution

java.lang.Object
  extended by Pandora.NDRules.NDRule
      extended by Pandora.NDRules.Substitution

public class Substitution
extends NDRule

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

Substitution

public Substitution(ProofBox proof)
Constructs a Substitution.

Parameters:
proof - ProofBox representing in which box the rule is being applied
Method Detail

addLine

public void addLine(ProofLine clickedLine)
             throws java.lang.Exception
Adds the extra lines to the rule once the input line has been added.

Specified by:
addLine in class NDRule
Parameters:
clickedLine - ProofLine which has been selected
Throws:
java.lang.Exception

haveAll

public boolean haveAll()
Returns true if the rule has all of the required input lines.

Specified by:
haveAll in class NDRule

check

public void check()
           throws java.lang.Exception
Called by the RuleController to check the input lines to the rule.

Specified by:
check in class NDRule
Throws:
java.lang.Exception

apply

public void apply()
           throws java.lang.Exception
Called by the RuleController to apply the rule.

Specified by:
apply in class NDRule
Throws:
java.lang.Exception

findMatch

public 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.

Parameters:
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.

findMatch

public void findMatch(Term pTerm,
                      Equals pEquals,
                      ProofLine pLine)

findAll

public void findAll(ProofLine pELine,
                    ProofLine pFLine)
             throws java.lang.Exception
This method is only used when the Substitution rule is applied forwards.
It finds all the possible substitution between two passed lines' formulae.

Parameters:
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.
Throws:
java.lang.Exception

showMatch

public void showMatch()