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

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>)

 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.

 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

 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

 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

 public String toString()

A NegFormula is printed as (NOT <formula>)

Returns:

the String that represents this NegFormula

Overrides:

toString in class Object

 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