All Packages  Class Hierarchy  This Package  Previous  Next  Index

Class JavaAgent.resource.fopl.BinConFormula

java.lang.Object
   |
   +----JavaAgent.resource.fopl.Formula
           |
           +----JavaAgent.resource.fopl.BinConFormula

public class BinConFormula

extends Formula

See Also:

YYtokentypes

BinConFormula(int, Formula, Formula)

This constructor for a BinConFormula takes an integer which represents the connective (see YYtokentypes) and two Formulae.

clone()

This function generates a copy of this BinConFormula.

clone(Substitution)

Returns a copy of this BinConFormula with Variables replaced according to the given Substitution.

equals(Object)

This function tests whether this and the given Object are equal.

getConclusion()

This function returns the conclusion of this implication.

getPremise()

This function returns the premise of this implication.

toSkolemizedAndOrForm(Substitution, Vector, boolean)

This function returns a new Formula which is the skolemized AND/OR form of this BinConFormula.

toString()

A MultiConFormula is printed as ( <connective> <formula> <formula> ).

 public BinConFormula(int con,
                      Formula f1,
                      Formula f2) throws IllegalArgumentException

This constructor for a BinConFormula takes an integer which represents the connective (see YYtokentypes) and two Formulae. The first Formula is taken to be the left hand side where that matters.

Parameters:

con - an integer representing the connective

f1 - the left hand side Formula

f2 - the right hand side Formula

Throws: IllegalArgumentException

An exception will occur if the given integer has an unexpected value or either of the given Formulae is null.

 public Object clone()

This function generates a copy of this BinConFormula. The copy will contain the same Variables and Symbols as the original.

Returns:

an equal copy of this BinConFormula

Overrides:

clone in class Formula

 public Formula clone(Substitution s) throws IllegalArgumentException

Returns a copy of this BinConFormula 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.

Parameters:

s - the Substitution that tells us how to replace Variables

Returns:

a new BinConFormula that is an instance of this BinConFormula; 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

 protected Formula toSkolemizedAndOrForm(Substitution s,
                                         Vector aQVars,
                                         boolean isNegated) throws IllegalArgumentException

This function returns a new Formula which is the skolemized AND/OR form of this BinConFormula. 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 MultiConFormula 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

 public String toString()

A MultiConFormula is printed as ( <connective> <formula> <formula> ).

Returns:

the String that represents this MultiConFormula

Overrides:

toString in class Object

 public boolean equals(Object otherForm)

This function tests whether this and the given Object are equal. In general, two BinConFormulae are equal if they have the same connective and both sub-Formulae are in the same order and equal.

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

 public Formula getPremise()

This function returns the premise of this implication.

 public Formula getConclusion()

This function returns the conclusion of this implication.

All Packages  Class Hierarchy  This Package  Previous  Next  Index