    All Packages  Class Hierarchy  This Package  Previous  Next  Index

# Class JavaAgent.resource.fopl.NegFormula

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

public class NegFormula
extends Formula

This class represents a negated Formula.

##

NegFormula(Formula)
  The constructor for a NegFormula takes just a Formula.

##

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

##

NegFormula

     public NegFormula(Formula aForm) throws IllegalArgumentException

  The constructor for a NegFormula takes just a Formula.

  Parameters:
    aForm - the Formula to be negated
  Throws: IllegalArgumentException
    An exception will occur if the given Formula is null.

##

clone

     public Object clone()

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

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

clone

     public Formula clone(Substitution s) throws IllegalArgumentException

  Returns a copy of this NegFormula 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 NegFormula that is an instance of this NegFormula; 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 allQVars,
                                             boolean isNegated) throws IllegalArgumentException

  This function returns a new Formula which is the skolemized AND/OR form of this Formula. The only change that takes place here is that the negation will be pulled into the Formula.

  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 (either a MultiConFormula or a Literal) 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

toString

     public String toString()

  A NegFormula is printed as (NOT <formula>)

  Returns:
    the String that represents this NegFormula
  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 NegFormulas are equal if they contain an equal negated Formula.

  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