Pandora.LogicParser.Formula
Class Unknown

java.lang.Object
  extended by Pandora.LogicParser.Formula.Formula
      extended by Pandora.LogicParser.Formula.Unknown
All Implemented Interfaces:
java.io.Serializable

public class Unknown
extends Formula

The unknown item.
Extends abstract class Formula.
Respresents the ?P formulae that are necessary in the proof.

See Also:
Serialized Form

Constructor Summary
Unknown(java.lang.String name)
          Constructs a new unknown.
 
Method Summary
 void addToSignature(PanSignature signature)
          This method adds this Formula to the passed PanSignature's Predicate list IF it is not already in the signature
If this Formula is an instance of Predicate, its Parameters will be added to the signature as well
 boolean checkSub(Term x, Term y, Formula f)
          Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Unknown.
 java.lang.String clashes(PanSignature signature)
          Returns a String containing an Error character if this Unknown clashes with the passed PanSignature, Otherwise it will return an Empty String ""
An Atom clashes with a signature if it clashes with any of its Predicates/Functions/Constants/Variables.
 java.lang.String display()
          Returns a String to display the var term.
 int getPrecedence()
          Returns an integer representing the precedence of this formula according to binding conventions
 java.util.List<Term> getTerms()
          This method returns a list of all the Terms this formula contains.
i.e.
 Formula regenerate()
          Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
 Formula s()
          Creates SVar to replace PVar in the formula where necessary.
 void setAtoms()
          Obtains the atoms in the formula and adds them to the list of atoms for the tree which contains this formula.
 void setVars(Var v)
          This method adds Var v to the list of variables this Formula is bound to.
 Formula subAll(Term a, Term b)
          Returns the Formula that is derived after substituting ALL the occurrences of Term a with Term b in this Unknown.
 
Methods inherited from class Pandora.LogicParser.Formula.Formula
check, concatNoDup, getAtoms, getLeft, getRight, getTuples, getVars, higher, isBracketed, map, setLeft, setRight, setTuples, showTuples, sub
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

Unknown

public Unknown(java.lang.String name)
Constructs a new unknown.

Parameters:
name - the name of the unknown
Method Detail

setAtoms

public void setAtoms()
Obtains the atoms in the formula and adds them to the list of atoms for the tree which contains this formula.
The list of atoms is found in Formula class.

Specified by:
setAtoms in class Formula

display

public java.lang.String display()
Returns a String to display the var term.

Specified by:
display in class Formula

subAll

public Formula subAll(Term a,
                      Term b)
Returns the Formula that is derived after substituting ALL the occurrences of Term a with Term b in this Unknown.

Specified by:
subAll in class Formula
Parameters:
a - Term represents the Term to be substituted.
b - Term represents the Term to substitute Term a.

checkSub

public boolean checkSub(Term x,
                        Term y,
                        Formula f)
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Unknown.

Specified by:
checkSub in class Formula
Parameters:
x - Term represents the Term to be substituted.
y - Term represents the Term to substitute Term x.
f - Formula represents the Formula to check if it can be reached after substitution.

s

public Formula s()
Creates SVar to replace PVar in the formula where necessary. Used in Raptor.

Specified by:
s in class Formula

regenerate

public Formula regenerate()
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.

Specified by:
regenerate in class Formula

clashes

public java.lang.String clashes(PanSignature signature)
Returns a String containing an Error character if this Unknown clashes with the passed PanSignature, Otherwise it will return an Empty String ""
An Atom clashes with a signature if it clashes with any of its Predicates/Functions/Constants/Variables.

Specified by:
clashes in class Formula
Parameters:
signature - PanSignature represents the PanSignature to be checked if this Atom clashes with.

getTerms

public java.util.List<Term> getTerms()
This method returns a list of all the Terms this formula contains.
i.e. it returns an empty list as an Atom does not contain any Terms.

Specified by:
getTerms in class Formula

addToSignature

public void addToSignature(PanSignature signature)
This method adds this Formula to the passed PanSignature's Predicate list IF it is not already in the signature
If this Formula is an instance of Predicate, its Parameters will be added to the signature as well

Specified by:
addToSignature in class Formula
Parameters:
signature - PanSignature represents the signature to add this Formula to.

setVars

public void setVars(Var v)
This method adds Var v to the list of variables this Formula is bound to.

Specified by:
setVars in class Formula
Parameters:
v - Var represents the Var to be added to the list of this Formula's variables.

getPrecedence

public int getPrecedence()
Returns an integer representing the precedence of this formula according to binding conventions

Specified by:
getPrecedence in class Formula