Raptor.NDRules
Class Instantiate

java.lang.Object
  Raptor.NDRules.NDRule
      Raptor.NDRules.Instantiate

public class Instantiate
extends NDRule

Implements the instantiate rule.
Extends abstract class NDRule.

Constructor Summary

Instantiate(ProofBox pProof)
Constructs an Instantiate rule instance.

Method Summary

void	addLine(ProofLine pClickedLine) Adds the extra lines to the rule once the input line has been added.
void	apply() Called by the controller to apply the instantiate rule.
void	check() Called by the RuleController to check the input lines to the rule.
boolean	haveAll() Returns true if the rule has all of the required input lines.

Methods inherited from class Raptor.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

Instantiate

public Instantiate(ProofBox pProof)

Constructs an Instantiate rule instance.

Parameters:

pProof - the ProofBox representing the box in which the rule is being applied

Method Detail

addLine

public void addLine(ProofLine pClickedLine)
             throws java.lang.Exception

Adds the extra lines to the rule once the input line has been added.
Throws an exception if the line selected is not correct for the rule.

Specified by:

addLine in class NDRule

Parameters:

pClickedLine - 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.
Only one line required for this rule so this function returns true.

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 controller to apply the instantiate rule.

Specified by:

apply in class NDRule

Throws:

java.lang.Exception