|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectPandora.NDRules.NDRule
public abstract class NDRule
Abstract Rule class.
Extended by each of the rule classes.
Field Summary | |
---|---|
ProofLine |
firstLine
|
Constructor Summary | |
---|---|
NDRule(ProofBox pProof)
|
Method Summary | |
---|---|
void |
addInputLine(ProofLine line)
Adds the input line to the rule. |
abstract void |
addLine(ProofLine line)
Adds the extra lines to the rule once the input line has been added. |
abstract void |
apply()
Called by the controller to apply the rule. |
abstract void |
check()
Called by the controller to check the input lines to the rule. |
boolean |
checkSignature(Formula formula)
Returns true if the given formula contains only predicates/terms/functions already in the signature of the proof and if it does not clash with any of the previously declared predicates/functions and constants. |
protected Formula |
getNewFormula(java.lang.String oldFormula,
java.lang.String message)
Takes as input a formula that was rejected because its atoms were not in the signature of the proof. |
abstract boolean |
haveAll()
Returns true if the rule ahs all of the required input lines. |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
---|
public ProofLine firstLine
Constructor Detail |
---|
public NDRule(ProofBox pProof)
Method Detail |
---|
public void addInputLine(ProofLine line) throws java.lang.Exception
line
- ProofLine which is the first line selected
java.lang.Exception
public abstract boolean haveAll()
public abstract void addLine(ProofLine line) throws java.lang.Exception
line
- ProofLine which has been selected
java.lang.Exception
public abstract void check() throws java.lang.Exception
java.lang.Exception
public abstract void apply() throws java.lang.Exception
java.lang.Exception
public boolean checkSignature(Formula formula)
formula
- the formula to be checked against the signatureprotected Formula getNewFormula(java.lang.String oldFormula, java.lang.String message) throws java.lang.Exception
oldFormula
- the formula with atoms that are not in the signature of the proof
java.lang.Exception
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |