package JavaAgent.resource.fopl;


import java.util.*;

/** 
** This class represents a negated Formula. 
*/

public class NegFormula extends Formula {

  /**
  ** The constructor for a NegFormula takes just a Formula.
  ** @param aForm the Formula to be negated
  ** @exception IllegalArgumentException An exception will occur if the 
  ** given Formula is null.
  */
  public NegFormula(Formula aForm) throws IllegalArgumentException {
    if (aForm == null)
      throw new IllegalArgumentException(
          "Attempt to construct NegFormula without Formula.");
    theForm = aForm;
  }

  /**
  ** This function generates a copy of this NegFormula. The copy will 
  ** contain the same Variables and Symbols as the original.
  ** @return an equal copy of this Formula
  */
  public Object clone() {
    return new NegFormula((Formula)theForm.clone());
  }

  /**
  ** 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.
  ** @param s the Substitution that tells us how to replace Variables
  ** @return a new NegFormula that is an instance of this NegFormula; the 
  ** Substitution <tt>s</tt> will be extended with any new Variable 
  ** replacements introduced
  ** @exception IllegalArgumentException An exception can occur if the given
  ** Substitution is null. In this case <tt>clone()</tt> (above) should be
  ** used.
  */
  public Formula clone(Substitution s) throws IllegalArgumentException {
    return new NegFormula((Formula)theForm.clone(s));
  }

  /**
  ** 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.
  ** @param s the Substitution that tells us how to replace Variables
  ** @param allQuantVars the Vector of universally quantified Variables
  ** @param isNegated whether the Formula is negated
  ** @return a new Formula (either a MultiConFormula or a Literal) which is 
  ** the skolemized AND/OR form of this Formula; the Substitution <tt>s</tt> 
  ** will be extended with any new Variable replacements introduced
  ** @exception IllegalArgumentException An exception can occur if the given
  ** Substitution or Vector are null.
  */
  protected Formula toSkolemizedAndOrForm(
      Substitution s, Vector allQVars, boolean isNegated) 
      throws IllegalArgumentException {
    return theForm.toSkolemizedAndOrForm(s, allQVars, (! isNegated));
  }

  /**
  ** A NegFormula is printed as (NOT &lt;formula&gt;)
  ** @return the String that represents this NegFormula
  */
  public String toString() {
    return "(NOT " + theForm.toString() + ')';
  }

  /** 
  ** This function tests whether this and the given Object are equal. In
  ** general, two NegFormulas are equal if they contain an equal negated
  ** Formula.
  ** @param otherForm the Formula this one is to be compared to
  ** @return whether the given Object is equal to this one
  */
  public boolean equals(Object otherForm) {
    if (otherForm == null)
      return false;
    if (! (otherForm instanceof NegFormula))
      return false;
    return theForm.equals(((NegFormula)otherForm).theForm);
  }

  /**
  ** the content Formula that is negated
  */
  private Formula theForm;
}
