package JavaAgent.resource.fopl;


import java.util.*;

/** 
** A Propostion represents a sentence that can be either true or false.
** It is represented by a Symbol.
** @see Symbol
*/

public class Proposition extends Literal {

  /**
  ** The constructor for a Proposition takes just a Symbol.
  ** @exception IllegalArgumentException An exception will occur if the 
  ** given Symbol is null.
  */
  public Proposition(Symbol aSy) throws IllegalArgumentException {
    theTerms = new Vector(2);
    theTerms.addElement(new ConstTerm(aSy));
  }

  /**
  ** Cloning a Proposition returns a new Proposition of the same Symbol.
  ** @return an equal copy of this Literal
  */
  public Object clone() {
    Proposition p = new Proposition(
        ((ConstTerm)theTerms.firstElement()).getSymbol());
    p.negated = negated;
    return p;
  }

  /**
  ** Cloning a Proposition returns a new Proposition of the same Symbol. The
  ** given Substitution can be ignored as Propositions do not contain 
  ** Variables.
  ** @param s the Substitution that tells us how to replace Variables (will 
  ** be ignored)
  ** @return a new Proposition containing the same Symbol
  */
  public Formula clone(Substitution s) {
    Proposition p = new Proposition(
        ((ConstTerm)theTerms.firstElement()).getSymbol());
    p.negated = negated;
    return p;
  }

  /**
  ** This function returns a new Proposition which is an equal copy of
  ** this Proposition. The given Substitution and the given Vector of 
  ** Variables will be ignored here. Finally, the given boolean indicates 
  ** whether the Proposition is to be negated, i.e. its sign to be reversed.
  ** @param s a Substitution (will be ignored)
  ** @param allQuantVars the Vector of universally quantified Variables 
  ** (will be ignored)
  ** @param isNegated whether the Literal has to be negated
  ** @return an equal copy of this Proposition
  */
  protected Formula toSkolemizedAndOrForm(
      Substitution s, Vector allQuantVars, boolean isNegated) {
    Proposition p = new Proposition(
        ((ConstTerm)theTerms.firstElement()).getSymbol());
    p.negated = (negated && !isNegated) || (!negated && isNegated);
    return p;
  }

  /**
  ** A Proposition is printed as &lt;constant&gt; or (NOT &lt;constant&gt;)
  ** if it is negated.
  ** @return the String that represents this Proposition
  */
  public String toString() {
    if (negated)
      return "(NOT " + theTerms.firstElement().toString() + ')';
    else
      return theTerms.firstElement().toString();
  }

  /** 
  ** A Proposition is equal to any other Proposition that consists of the
  ** same symbol and sign.
  ** @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 Proposition))
      return false;
    Proposition p = (Proposition)otherForm;
    if ((negated == p.negated) &&
        (theTerms.firstElement().equals(p.theTerms.firstElement())))
      return true;
    return false;
  }

}
