Raptor.LogicParser.Formula
Class Exists

java.lang.Object
  Raptor.LogicParser.Formula.Formula
      Raptor.LogicParser.Formula.Quantifier
          Raptor.LogicParser.Formula.Exists

All Implemented Interfaces:

java.io.Serializable

public class Exists
extends Quantifier

The There Exists quantifier formula.
Extends abstract class Quantifier.

See Also:

Serialized Form

Constructor Summary

Exists(Var pVar, Formula pFormula)
Constructs a There Exists Formula.

Method Summary

void	addToSignature(PanSignature pSignature) This method adds this Formula to the passed PanSignature's 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 the occurrences of Term x by Term y.
java.lang.String	display() Returns the a String to display the There Exists Formula.
Formula	getFormula() Returns the Formula which is bound by the quantifier.
Var	getVar() Returns the bound variable of the quantifier formula.
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() Adds this atom to the list of atoms for the formula. The list of atoms is found in Formula class.
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.
Formula	subBoolRes(java.lang.String display)

Methods inherited from class Raptor.LogicParser.Formula.Quantifier

clashes, getAllTerms, getPrecedence, getTerms

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

Exists

public Exists(Var pVar,
              Formula pFormula)

Constructs a There Exists Formula.

Parameters:

pVar - Var represents the variable of the There Exists Formula.

pFormula - Formula represents the Formula the quantifier is applied on.

Method Detail

getVar

public Var getVar()

Returns the bound variable of the quantifier formula.

Specified by:

getVar in class Quantifier

getFormula

public Formula getFormula()

Returns the Formula which is bound by the quantifier.

Specified by:

getFormula in class Quantifier

display

public java.lang.String display()

Returns the a String to display the There Exists Formula.

Specified by:

display in class Quantifier

setAtoms

public void setAtoms()

Adds this atom to the list of atoms for the formula.
The list of atoms is found in Formula class.

Specified by:

setAtoms in class Formula

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.

checkSub

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

Specified by:

checkSub in class Formula

Parameters:

pTermX - Term represents the Term to be substituted.

pTermY - Term represents the Term to substituted 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.

Specified by:

subAll in class Formula

Parameters:

pTermX - Term represents the Term to be substituted.

pTermY - Term represents the Term to substitute Term x.

addToSignature

public void addToSignature(PanSignature pSignature)

This method adds this Formula to the passed PanSignature's 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.

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

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