Raptor.LogicParser.Formula
Class Formula

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

All Implemented Interfaces:

java.io.Serializable

Direct Known Subclasses:

And, ArrayWrapper, Atom, BExp, Blah, Bool, Iff, Implies, Not, NotBlah, NotBool, Or, PBExp, Quantifier, Unknown

public abstract class Formula
extends java.lang.Object
implements java.io.Serializable

Abstract Formula class.
Extended by each of the Formula classes.

See Also:

Serialized Form

Constructor Summary

Formula()

Method Summary

abstract void	addToSignature(PanSignature pSignature) This method adds this Formula to the passed PanSignature's Predicate list IF it is not already in the signature.
Formula	check(Term pTermX, Term pTermY, Formula pFormula) Returns true if the passed formula f can be reached by substituting the occurrences of Term x by Term y.
abstract boolean	checkSub(Term pTermX, Term pTermY, Formula pFormula) Returns true if the passed formula f can be reached by substituting the occurrences of Term x by Term y.
abstract 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 "".
java.util.List<Term>	concatNoDup(java.util.List<Term> pTerms) This method removes the duplicates from the Formula's Term list.
abstract java.lang.String	display() Returns the a String to display the Formula.
java.util.List<Atom>	getAtoms() Returns the list of atoms contained in a Formula tree.
Formula	getLeft() Default getLeft() method for when a Formula has no left Formula.
abstract int	getPrecedence() Returns an integer representing the precedence of this formula according to binding conventions
Formula	getRight() Default getRight() method for when a Formula has no right Formula.
abstract java.util.List<Term>	getTerms() This method returns a list of all the Terms this formula contain.
java.util.List<Tuple>	getTuples() Returns the list of tuples in a Formula.
java.util.List<Var>	getVars() This method returns the list of all the variables this Formula is bound to.
boolean	higher(Formula pFormula)
Term	map(Term pTerm, java.util.List<Tuple> pTuples) Checks if the passed Term is equal to the first element of any of the Tuples in the passed List.
abstract Formula	regenerate() Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
abstract Formula	s() Creates VVar to replace PVar in the formula where necessary.
abstract void	setAtoms() Adds the list of Atoms in a given tree to the list of Atoms.
void	setLeft(Formula pLeft) Default setLeft() method for when a Formula has no left Formula.
void	setRight(Formula pRight) Default setRight() method for when a Formula has no right Formula.
void	setTuples(java.util.List<Tuple> pTuples) Set the tuples in a Formula.
abstract void	setVars(Var pVar) This method adds Var v to the list of variables this Formula is bound to.
void	showTuples() Prints to the console the list of tuples in a formula.
abstract Term	ST()
Formula	sub(Term pTermX, Term pTermY, Formula pFormula) Returns the Formula that can be reached by substituting the occurrences of Term x by Term y.
abstract Formula	subAll(PTerm left, PTerm right)
abstract Formula	subAll(Term pTermX, Term pTermY) Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y.
Formula	subBool(PTerm left, PTerm right)
abstract Formula	subBoolRes(java.lang.String display)

Methods inherited from class java.lang.Object

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

Constructor Detail

Formula

public Formula()

Method Detail

map

public Term map(Term pTerm,
                java.util.List<Tuple> pTuples)

Checks if the passed Term is equal to the first element of any of the Tuples in the passed List.

Parameters:

pTerm - Term represents the Term to search the List for.

pTuples - List the tuple list to search the passed Term in.

display

public abstract java.lang.String display()

Returns the a String to display the Formula.

getAtoms

public java.util.List<Atom> getAtoms()

Returns the list of atoms contained in a Formula tree.

getVars

public java.util.List<Var> getVars()

This method returns the list of all the variables this Formula is bound to.

setAtoms

public abstract void setAtoms()

Adds the list of Atoms in a given tree to the list of Atoms.

setVars

public abstract void setVars(Var pVar)

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

Parameters:

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

sub

public Formula sub(Term pTermX,
                   Term pTermY,
                   Formula pFormula)
            throws java.lang.Exception

Returns the Formula that can be reached by substituting the occurrences of Term x by Term y.

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. If the passed formula is null it will call the subAll method to substitute all the occurrences of Term x by Term y. Otherwise it will call the checkSub method to check if formula f can be reached by substitution.

Throws:

java.lang.Exception

check

public Formula check(Term pTermX,
                     Term pTermY,
                     Formula pFormula)
              throws java.lang.Exception

Returns true if the passed formula f can be reached by substituting the occurrences of Term x by Term y.

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. If the formula cannot be reached it will throw an Exception.

Throws:

java.lang.Exception

checkSub

public abstract boolean checkSub(Term pTermX,
                                 Term pTermY,
                                 Formula pFormula)

Returns true if the passed formula f can be reached by substituting the occurrences of Term x by Term y.

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 abstract Formula subAll(Term pTermX,
                               Term pTermY)

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

Parameters:

pTermX - Term represents the Term to be substituted.

pTermY - Term represents the Term to substitute Term x.

clashes

public abstract 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 "".

Parameters:

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

addToSignature

public abstract void addToSignature(PanSignature pSignature)

This method adds this Formula to the passed PanSignature's Predicate list IF it is not already in the signature.

Parameters:

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

getTerms

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

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

concatNoDup

public java.util.List<Term> concatNoDup(java.util.List<Term> pTerms)

This method removes the duplicates from the Formula's Term list.

showTuples

public void showTuples()

Prints to the console the list of tuples in a formula.

setTuples

public void setTuples(java.util.List<Tuple> pTuples)

Set the tuples in a Formula.

Parameters:

pTuples - the list of tuples in a Formula

getTuples

public java.util.List<Tuple> getTuples()

Returns the list of tuples in a Formula.

regenerate

public abstract Formula regenerate()

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

s

public abstract Formula s()

Creates VVar to replace PVar in the formula where necessary.

setLeft

public void setLeft(Formula pLeft)

Default setLeft() method for when a Formula has no left Formula.

getLeft

public Formula getLeft()

Default getLeft() method for when a Formula has no left Formula.

setRight

public void setRight(Formula pRight)

Default setRight() method for when a Formula has no right Formula.

getRight

public Formula getRight()

Default getRight() method for when a Formula has no right Formula.

getPrecedence

public abstract int getPrecedence()

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

higher

public boolean higher(Formula pFormula)

ST

public abstract Term ST()

subBool

public Formula subBool(PTerm left,
                       PTerm right)

subAll

public abstract Formula subAll(PTerm left,
                               PTerm right)

subBoolRes

public abstract Formula subBoolRes(java.lang.String display)