|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectPandora.LogicParser.Formula.Formula
Pandora.LogicParser.Formula.Quantifier
Pandora.LogicParser.Formula.Exists
public class Exists
The There Exists quantifier formula.
Extends abstract class Formula.
Constructor Summary | |
---|---|
Exists(Var var,
Formula formula)
Constructs a There Exists Formula. |
Method Summary | |
---|---|
void |
addToSignature(PanSignature signature)
This method adds this Formula to the passed PanSignature's IF it is not already in the signature. |
boolean |
checkSub(Term x,
Term y,
Formula f)
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 SVar 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 |
setVar(Var v)
|
void |
setVars(Var v)
This method adds Var v to the list of variables this Formula is bound to. |
Formula |
subAll(Term x,
Term y)
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y. |
Methods inherited from class Pandora.LogicParser.Formula.Quantifier |
---|
clashes, getAllTerms, getPrecedence, getTerms |
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 |
---|
public Exists(Var var, Formula formula)
var
- Var represents the variable of the There Exists Formula.formula
- Formula represents the Formula the quantifier is applied on.Method Detail |
---|
public Var getVar()
getVar
in class Quantifier
public void setVar(Var v)
public Formula getFormula()
getFormula
in class Quantifier
public java.lang.String display()
display
in class Quantifier
public void setAtoms()
setAtoms
in class Formula
public void setVars(Var v)
setVars
in class Formula
v
- Var represents the Var to be added to the list of this Formula's variables.public boolean checkSub(Term x, Term y, Formula f)
checkSub
in class Formula
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.public Formula subAll(Term x, Term y)
subAll
in class Formula
x
- Term represents the Term to be substituted.y
- Term represents the Term to substitute Term x.public void addToSignature(PanSignature signature)
addToSignature
in class Formula
signature
- PanSignature represents the signature to add this Formula to.public Formula s()
s
in class Formula
public Formula regenerate()
regenerate
in class Formula
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |