Raptor.LogicParser.Formula
Class Implies

java.lang.Object
  Raptor.LogicParser.Formula.Formula
      Raptor.LogicParser.Formula.Implies

All Implemented Interfaces:

java.io.Serializable

public class Implies
extends Formula

The Implies formula.
Extends abstract class Formula.

See Also:

Serialized Form

Constructor Summary

Implies(Formula pLeft, Formula pRight)
Constructs an Implies Formula.

Method Summary

void	addToSignature(PanSignature pSignature) This method adds the Atoms and Terms of this Formula to the passed PanSignature IF it is not already in the signature.
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 a String containing an Error character if this Formula clashes with the passed PanSignature, Otherwise it will return an Empty String "" An Implies Formula clashes with a signature if any of its left or right sub-Formulae clashes with the signature.
java.lang.String	display() Returns the a String to display the Implies formula.
Formula	getLeft() Returns the left side formula.
int	getPrecedence() Returns an integer representing the precedence of this formula according to binding conventions
Formula	getRight() Returns the right side formula.
java.util.List<Term>	getTerms() This method returns a list of all the Terms this Formula contain.
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 VVar 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	setLeft(Formula pLeft) Sets the left formula of the implication
void	setRight(Formula pRight) Sets the right formula of the implication
void	setVars(Var pVar) This method adds Var v to the list of variables this formula is bound to.
Term	ST()
Formula	subAll(PTerm left, PTerm right)
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.
Formula	subBoolRes(java.lang.String display)

Methods inherited from class Raptor.LogicParser.Formula.Formula

check, concatNoDup, getAtoms, getTuples, getVars, higher, map, setTuples, showTuples, sub, subBool

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Implies

public Implies(Formula pLeft,
               Formula pRight)

Constructs an Implies Formula.

Parameters:

pLeft - Formula of left side of implication

pRight - Formula of right side of cimplication

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

getLeft

public Formula getLeft()

Returns the left side formula.

Overrides:

getLeft in class Formula

getRight

public Formula getRight()

Returns the right side formula.

Overrides:

getRight in class Formula

setLeft

public void setLeft(Formula pLeft)

Sets the left formula of the implication

Overrides:

setLeft in class Formula

setRight

public void setRight(Formula pRight)

Sets the right formula of the implication

Overrides:

setRight in class Formula

display

public java.lang.String display()

Returns the a String to display the Implies formula.

Specified by:

display in class Formula

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.

Specified by:

checkSub in class Formula

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.

Specified by:

subAll in class Formula

Parameters:

pTermX - Term represents the Term to be substituted.

pTermY - Term represents the Term to substitute Term x.

setVars

public void setVars(Var pVar)

This method adds Var v to the list of variables this formula is bound to.

Specified by:

setVars in class Formula

Parameters:

pVar - Var represents the Var to be added to the list of this formula's variables.

clashes

public java.lang.String clashes(PanSignature pSignature)

Returns a String containing an Error character if this Formula clashes with the passed PanSignature, Otherwise it will return an Empty String ""
An Implies Formula clashes with a signature if any of its left or right sub-Formulae clashes with the signature.

Specified by:

clashes in class Formula

Parameters:

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

addToSignature

public void addToSignature(PanSignature pSignature)

This method adds the Atoms and Terms of this Formula to the passed PanSignature IF it is not already in the signature.

Specified by:

addToSignature in class Formula

Parameters:

pSignature - PanSignature represents the signature to add this Formula to.

getTerms

public java.util.List<Term> getTerms()

This method returns a list of all the Terms this Formula contain.

Specified by:

getTerms in class Formula

s

public Formula s()

Creates VVar 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

getPrecedence

public int getPrecedence()

Returns an integer representing the precedence of this formula according to binding conventions

Specified by:

getPrecedence in class Formula

ST

public Term ST()

Specified by:

ST in class Formula

subAll

public Formula subAll(PTerm left,
                      PTerm right)

Specified by:

subAll in class Formula

subBoolRes

public Formula subBoolRes(java.lang.String display)

Specified by:

subBoolRes in class Formula