package JavaAgent.resource.fopl;


import java.util.*;

/** 
** 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. <tt>AND</tt> or <tt>OR</tt> at the moment.
** @see YYtokentypes
*/

public class MultiConFormula extends Formula {

  /**
  ** 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.
  ** @param con an integer representing the connective
  ** @param someForms the Formulae to be connected here
  ** @exception 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.
  */
  public MultiConFormula(int con, Vector someForms) 
      throws IllegalArgumentException {
    theCon = con;
    if ((theCon != andValue) && (theCon != orValue))
      throw new IllegalArgumentException(
          "Attempt to create MultiConFormula with unknown connective.");
    if ((someForms == null) || someForms.isEmpty())
      throw new IllegalArgumentException(
          "Attempt to create MultiConFormula without sub-formulae.");
    theForms = new Vector(someForms.size()+3, 4);
    for (Enumeration e=someForms.elements(); e.hasMoreElements(); ) {
      Object ne = e.nextElement();
      if (ne instanceof Formula)
	addFormula((Formula)ne);
      else 
	throw new IllegalArgumentException(
            "MultiConFormula argument " + ne + 
            " is not a Formula as expected.");
    }
    liftSameConnective();
  }

  /** 
  ** 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.
  ** @param con an integer representing the connective
  ** @param f1 the first Formula to be connected here
  ** @param f2 the second Formula to be connected here
  ** @exception IllegalArgumentException An exception will occur if the 
  ** given integer has an unexpected value or either
  ** of the given Formulae is null.
  */
  public MultiConFormula(int con, Formula f1, Formula f2)
      throws IllegalArgumentException {
    theCon = con;
    if ((theCon != andValue) && (theCon != orValue))
      throw new IllegalArgumentException(
          "Attempt to create MultiConFormula with unknown connective.");
    theForms = new Vector(3, 4);
    if ((f1 == null) || (f2 == null))
      throw new IllegalArgumentException(
          "Attempt to create MultiConFormula with null argument.");
    theForms.addElement(f1);
    if (! f1.equals(f2))
      theForms.addElement(f2);
    liftSameConnective();
  }

  /** 
  ** 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.
  ** @param con an integer representing the connective
  ** @param size the expected number of sub-formulae
  ** @exception IllegalArgumentException An exception will occur if the 
  ** given connective (integer) has an unexpected value.
  */
  protected MultiConFormula(int con, int size) 
      throws IllegalArgumentException {
    theCon = con;
    if ((theCon != andValue) && (theCon != orValue))
      throw new IllegalArgumentException(
          "Attempt to create MultiConFormula with unknown connective.");
    theForms = new Vector(size, 4);
  }
  
  /** 
  ** This function generates a copy of this MultiConFormula. The copy will 
  ** contain the same Variables and Symbols as the original.
  ** @return an equal copy of this MultiConFormula
  */
  public Object clone() {
    MultiConFormula mcf = new MultiConFormula(theCon, theForms.size()+3);
    for (Enumeration e=theForms.elements(); e.hasMoreElements(); )
      mcf.theForms.addElement(((Formula)e.nextElement()).clone());
    return mcf;
  }

  /** 
  ** 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.
  ** @param s the Substitution that tells us how to replace Variables
  ** @return a new MultiConFormula that is an instance of this 
  ** MultiConFormula; 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 {
    if (s == null)
      throw new IllegalArgumentException(
          "Attempt to clone MultiConFormula with null Substitution.");
    MultiConFormula mcf = new MultiConFormula(theCon, theForms.size()+3);
    for (Enumeration e=theForms.elements(); e.hasMoreElements(); )
      mcf.addFormula(((Formula)e.nextElement()).clone(s));
    return mcf;
  }

  /**
  ** 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.
  ** @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 MultiConFormula 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 allQuantVars, boolean isNegated) 
      throws IllegalArgumentException {
    MultiConFormula mcf = new MultiConFormula(theCon, theForms.size()+3);
    if (isNegated)
      mcf.theCon = (theCon == andValue) ? orValue : andValue;
    for (Enumeration e=theForms.elements(); e.hasMoreElements(); )
      mcf.addFormula(((Formula)e.nextElement()).
          toSkolemizedAndOrForm(s, allQuantVars, isNegated));
    mcf.liftSameConnective();
    return mcf;
  }

  /** 
  ** This function adds a new conjunct/disjunct to this Formula if it is not
  ** already in there. 
  ** @param f the new Formula to be appended
  ** @exception IllegalArgumentException An exception will occur if the given
  ** Formula is null.
  */
  public void addFormula(Formula f) throws IllegalArgumentException {
    if (f == null)
      throw new IllegalArgumentException(
          "Attempt to add null Formula to MultiConFormula.");
    for (Enumeration e=theForms.elements(); e.hasMoreElements(); )
      if (f.equals((Formula)e.nextElement()))
	return;
    theForms.addElement(f);
  }

  /** 
  ** This function adds a new conjunct/disjunct to the given Vector of 
  ** Formulae if it is not already in there. 
  ** @param fv a Vector of Formulae
  ** @param f the new Formula to be appended
  */
  private void addFormula(Vector fv, Formula f) {
    for (Enumeration e=fv.elements(); e.hasMoreElements(); )
      if (f.equals((Formula)e.nextElement()))
	return;
    fv.addElement(f);
  }

  /**
  ** 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., <tt>(AND P (AND Q R))</tt> 
  ** will be converted to <tt>(AND P Q R)</tt>. Multiply occuring Formulae
  ** will only be in the result once.
  */
  public void liftSameConnective() {
    Vector newForms = new Vector(theForms.size()+3, 4);
    for (Enumeration sf=theForms.elements(); sf.hasMoreElements(); ) {
      Formula f = (Formula)sf.nextElement();
      if ((f instanceof MultiConFormula) && 
          (((MultiConFormula)f).theCon == theCon)) {
	Enumeration es = ((MultiConFormula)f).theForms.elements();
	while (es.hasMoreElements())
	  addFormula(newForms, (Formula)es.nextElement());
      }
      else 
	newForms.addElement(f);
    }
    theForms = newForms;
  }

  /**
  ** This function tests whether this Formula is a conjunction.
  ** @return whether this Formula is a conjunction
  */
  public boolean isConjunction() {
    return (theCon == andValue);
  }

  /**
  ** This function tests whether this Formula is a disjunction.
  ** @return whether this Formula is a disjunction
  */
  public boolean isDisjunction() {
    return (theCon == orValue);
  }

  /**
  ** This function returns an enumerator for the sub-Formulae in this Formula.
  ** @return an Enumeration over the sub-Formulae
  */
  public Enumeration elements() {
    return theForms.elements();
  }

  /**
  ** A MultiConFormula is printed as ( &lt;connective&gt; &lt;formula&gt;+ ).
  ** @return the String that represents this MultiConFormula
  */
  public String toString() {
    String result = "(" + YYtokentypes.tokenname(theCon) + ' ';
    Enumeration e = theForms.elements();
    if (e.hasMoreElements())
      result += ((Formula)e.nextElement()).toString();
    while (e.hasMoreElements())
      result += " " + ((Formula)e.nextElement()).toString();
    return result + ')';
  }

  /** 
  ** 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.
  ** @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 MultiConFormula))
      return false;
    MultiConFormula mcf = (MultiConFormula)otherForm;
    if ((mcf.theCon != theCon) || (mcf.theForms.size() != theForms.size()))
      return false;
    Enumeration e2 = mcf.theForms.elements();
    for (Enumeration e1=theForms.elements(); e1.hasMoreElements(); )
      if (! e1.nextElement().equals(e2.nextElement()))
	return false;
    return true;
  }

  /**
  ** the connective as defined in YYtokentypes
  */
  private int theCon;

  /**
  ** a Vector of Formulae
  */
  private Vector theForms;

  /** 
  ** for quicker access these values are stored locally
  */
  private static int andValue = YYtokentypes.AND.intValue();
  private static int orValue = YYtokentypes.OR.intValue();
}
