Pandora.LogicParser.Formula
Class True

java.lang.Object
  Pandora.LogicParser.Formula.Formula
      Pandora.LogicParser.Formula.Atom
          Pandora.LogicParser.Formula.True

All Implemented Interfaces:

java.io.Serializable

public class True
extends Atom

The Top formula.
Extends abstract class Formula.

See Also:

Serialized Form

Constructor Summary

True()
Constructs a Top Formula.

Method Summary

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 Formula.
java.lang.String	clashes(PanSignature signature) Returns an Empty String "" as a top formula never clashes with a signature.
java.lang.String	display() Returns the a String to display the Implies formula.
Formula	regenerate() Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
Formula	subAll(Term x, Term y) Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula.

Methods inherited from class Pandora.LogicParser.Formula.Atom

addToSignature, clashes, clashes, equals, getArity, getName, getPrecedence, getTerms, isIn, s, setAtoms, setVars

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

True

public True()

Constructs a Top Formula.

Method Detail

display

public java.lang.String display()

Returns the a String to display the Implies formula.

Overrides:

display in class Atom

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

Overrides:

checkSub in class Atom

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.

subAll

public Formula subAll(Term x,
                      Term y)

Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula.

Overrides:

subAll in class Atom

Parameters:

x - Term represents the Term to be substituted.

y - Term represents the Term to substitute Term x.

clashes

public java.lang.String clashes(PanSignature signature)

Returns an Empty String "" as a top formula never clashes with a signature.

Overrides:

clashes in class Atom

Parameters:

signature - PanSignature represents the PanSignature to be checked if this Formula clashes with.

regenerate

public Formula regenerate()

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

Overrides:

regenerate in class Atom