    All Packages  Class Hierarchy  This Package  Previous  Next  Index

# Class JavaAgent.resource.fopl.MultiConFormula

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

public class MultiConFormula
extends Formula

This class represents a Formula that consists of a connective that connects a number (at least two) of sub-Formulae. The connective must be associative, i.e. `AND` or `OR` at the moment.

See Also:
  YYtokentypes

##

MultiConFormula(int, Formula, Formula)
  This constructor for a MultiConFormula takes an integer which represents the connective (see YYtokentypes) and two Formulae that are to be connected in this MultiConFormula.
MultiConFormula(int, int)
  This protected constructor creates an empty Formula for the given connective type.
MultiConFormula(int, Vector)
  This constructor for a MultiConFormula takes an integer which represents the connective (see YYtokentypes) and a Vector of Formulae which are the Formulae that are connected by this connective.

##

addFormula(Formula)
  This function adds a new conjunct/disjunct to this Formula if it is not already in there.
clone()
  This function generates a copy of this MultiConFormula.
clone(Substitution)
  Returns a copy of this MultiConFormula with Variables replaced according to the given Substitution.
elements()
  This function returns an enumerator for the sub-Formulae in this Formula.
equals(Object)
  This function tests whether this and the given Object are equal.
isConjunction()
  This function tests whether this Formula is a conjunction.
isDisjunction()
  This function tests whether this Formula is a disjunction.
liftSameConnective()
  This function checks whether any of the direct sub-Formulae of this Formula are a MultiConFormula with the same connective (AND or OR) and lifts those that do up to this level.
toSkolemizedAndOrForm(Substitution, Vector, boolean)
  This function returns a new Formula which is the skolemized AND/OR form of this MultiConFormula.
toString()
  A MultiConFormula is printed as ( <connective> <formula>+ ).

##

MultiConFormula

     public MultiConFormula(int con,
                            Vector someForms) throws IllegalArgumentException

  This constructor for a MultiConFormula takes an integer which represents the connective (see YYtokentypes) and a Vector of Formulae which are the Formulae that are connected by this connective. All elements of the given Vector must be Formulae. Formulae occuring more than once in the Vector are only added once. Sub-Formulae that are MultiConFormulas of the same type are lifted to create just one flat Formula.

  Parameters:
    con - an integer representing the connective
    someForms - the Formulae to be connected here
  Throws: IllegalArgumentException
    An exception will occur if the given integer has an unexpected value, the given Vector is null or empty, or one of the elements of the Vector is not a Formula.

MultiConFormula

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

  This constructor for a MultiConFormula takes an integer which represents the connective (see YYtokentypes) and two Formulae that are to be connected in this MultiConFormula. If the two Formulae are equal then only the first will be added. Sub-Formulae that are MultiConFormulas of the same type are lifted to create just one flat Formula.

  Parameters:
    con - an integer representing the connective
    f1 - the first Formula to be connected here
    f2 - the second Formula to be connected here
  Throws: IllegalArgumentException
    An exception will occur if the given integer has an unexpected value or either of the given Formulae is null.

MultiConFormula

     protected MultiConFormula(int con,
                               int size) throws IllegalArgumentException

  This protected constructor creates an empty Formula for the given connective type. Sub-Formulae should be added to this Formula before anything is done with it.

  Parameters:
    con - an integer representing the connective
    size - the expected number of sub-formulae
  Throws: IllegalArgumentException
    An exception will occur if the given connective (integer) has an unexpected value.

##

clone

     public Object clone()

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

  Returns:
    an equal copy of this MultiConFormula
  Overrides:
    clone in class Formula

clone

     public Formula clone(Substitution s) throws IllegalArgumentException

  Returns a copy of this MultiConFormula 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. If two of the sub-Formulae become equal in this process only one will occur in the result.

  Parameters:
    s - the Substitution that tells us how to replace Variables
  Returns:
    a new MultiConFormula that is an instance of this MultiConFormula; 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

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

addFormula

     public void addFormula(Formula f) throws IllegalArgumentException

  This function adds a new conjunct/disjunct to this Formula if it is not already in there.

  Parameters:
    f - the new Formula to be appended
  Throws: IllegalArgumentException
    An exception will occur if the given Formula is null.

liftSameConnective

     public void liftSameConnective()

  This function checks whether any of the direct sub-Formulae of this Formula are a MultiConFormula with the same connective (AND or OR) and lifts those that do up to this level. E.g., `(AND P (AND Q R))` will be converted to `(AND P Q R)`. Multiply occuring Formulae will only be in the result once.

isConjunction

     public boolean isConjunction()

  This function tests whether this Formula is a conjunction.

  Returns:
    whether this Formula is a conjunction

isDisjunction

     public boolean isDisjunction()

  This function tests whether this Formula is a disjunction.

  Returns:
    whether this Formula is a disjunction

elements

     public Enumeration elements()

  This function returns an enumerator for the sub-Formulae in this Formula.

  Returns:
    an Enumeration over the sub-Formulae

toString

     public String toString()

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

  Returns:
    the String that represents this MultiConFormula
  Overrides:
    toString in class Object

equals

     public boolean equals(Object otherForm)

  This function tests whether this and the given Object are equal. In general, two MultiConFormulae are equal if they have the same connective and all the 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

    All Packages  Class Hierarchy  This Package  Previous  Next  Index