All Packages  Class Hierarchy  This Package  Previous  Next  Index

Class JavaAgent.resource.fopl.QuantFormula 

java.lang.Object
   |
   +----JavaAgent.resource.fopl.Formula
           |
           +----JavaAgent.resource.fopl.QuantFormula
public class QuantFormula
extends Formula
This class represents a quantified Formula that consists of a quantifier, some Variables, and a Formulae. Currently the available quantifiers are FORALL and EXISTS.

See Also:
YYtokentypes

Constructor Index

o QuantFormula(int, Vector, Formula)
The constructor for a QuantFormula takes an integer which represents the quantifier (see YYtokentypes), a list of Fariables and a Formula.

Method Index

o clone()
This function generates a copy of this QuantFormula.
o clone(Substitution)
Returns a copy of this QuantFormula with Variables replaced according to the given Substitution.
o equals(Object)
This function tests whether this and the given Object are equal.
o toSkolemizedAndOrForm(Substitution, Vector, boolean)
This function returns a new Formula which is the skolemized AND/OR form of this QuantFormula.
o toString()
A QuantFormula is printed as ((<quantifier> <var-spec>) <quantifier>).

Constructors

o QuantFormula 
 public QuantFormula(int quant,
                     Vector vars,
                     Formula form) throws IllegalArgumentException
The constructor for a QuantFormula takes an integer which represents the quantifier (see YYtokentypes), a list of Fariables and a Formula.

Parameters:
quant - an integer representing the quantifier
vars - a Vector of Variables
form - the Formula quantified over
Throws: IllegalArgumentException
An exception will occur if the given integer has an unexpected value, the given Formula is null, or the given Vector is null, empty, or contains an element that is not a Variable.

Methods

o clone 
 public Object clone()
This function generates a copy of this QuantFormula. The copy will contain the same Variables and Symbols as the original.

Returns:
an equal copy of this QuantFormula
Overrides:
clone in class Formula
o clone 
 public Formula clone(Substitution s) throws IllegalArgumentException
Returns a copy of this QuantFormula with Variables replaced according to the given Substitution. Symbols in the copy will be the same as the original ones but Variables will be repalced by the respective Terms in the given Substitution. A Variable not occurring in the Substitution will be replaced by a new (different) Variable with the same name. The given Substitution will be extended to include the mappings of old Variables to new ones. Varibales that are mapped to a non-VarTerm by the Substitution will be removed from the Vector of Variables. If the Vector is empty as a result of this the whole quantification is removed and only the instantiated content Formula is returned.

Parameters:
s - the Substitution that tells us how to replace Variables
Returns:
a new Formula that is an instance of this QuantFormula; the Substitution s will be extended with any new Variable replacements introduced
Throws: IllegalArgumentException
An exception can occur if the given Substitution is null. In this case clone() (above) should be used.
Overrides:
clone in class Formula
o toSkolemizedAndOrForm 
 protected Formula toSkolemizedAndOrForm(Substitution s,
                                         Vector allQuantVars,
                                         boolean isNegated) throws IllegalArgumentException
This function returns a new Formula which is the skolemized AND/OR form of this QuantFormula. The given Substitution will be extended with new Variable to Skolem term (ConstTerm or FunctTerm) mappings. The given Vector of Variables is used to keep track of any Variables that are universally quantified at this point. Finally, the given boolean indicates whether the Formula is to be treated as negated at this point.

Parameters:
s - the Substitution that tells us how to replace Variables
allQuantVars - the Vector of universally quantified Variables
isNegated - whether the Formula is negated
Returns:
a new Formula which is the skolemized AND/OR form of this Formula; the Substitution s will be extended with any new Variable replacements introduced
Throws: IllegalArgumentException
An exception can occur if the given Substitution or Vector are null.
Overrides:
toSkolemizedAndOrForm in class Formula
o toString 
 public String toString()
A QuantFormula is printed as ((<quantifier> <var-spec>) <quantifier>). A <var-spec> can be either <variable> or (<varibale> <constant>).

Returns:
the String that represents this QuantFormula
Overrides:
toString in class Object
o equals 
 public boolean equals(Object otherForm)
This function tests whether this and the given Object are equal. In general, two QuantFormulae are equal if they have the same quantifier, quantify over the same variables in the same order, and quantify over equal formulae.

Parameters:
otherForm - the Formula this one is to be compared to
Returns:
whether the given Object is equal to this one
Overrides:
equals in class Formula 
All Packages  Class Hierarchy  This Package  Previous  Next  Index