Raptor.LogicParser.Formula
Class True

java.lang.Object
  Raptor.LogicParser.Formula.Formula
      Raptor.LogicParser.Formula.Atom
          Raptor.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 pTermX, Term pTermY, Formula pFormula) 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 pSignature) 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 pTermX, Term pTermY) Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula.

Methods inherited from class Raptor.LogicParser.Formula.Atom

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

Methods inherited from class Raptor.LogicParser.Formula.Formula

check, concatNoDup, getAtoms, getLeft, getRight, getTuples, getVars, higher, map, setLeft, setRight, setTuples, showTuples, sub, subBool

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 pTermX,
                        Term pTermY,
                        Formula pFormula)

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:

pTermX - Term represents the Term to be substituted.

pTermY - Term represents the Term to substitute Term x.

pFormula - Formula represents the Formula to check if it can be reached after substitution.

subAll

public Formula subAll(Term pTermX,
                      Term pTermY)

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:

pTermX - Term represents the Term to be substituted.

pTermY - Term represents the Term to substitute Term x.

clashes

public java.lang.String clashes(PanSignature pSignature)

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

Overrides:

clashes in class Atom

Parameters:

pSignature - 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