package JavaAgent.resource.fopl;


import java.util.*;

/** 
** This class represents a quantified Formula that consists of a quantifier,
** some Variables, and a Formulae. Currently the available quantifiers are
** <tt>FORALL</tt> and <tt>EXISTS</tt>.
** @see YYtokentypes
*/

public class QuantFormula extends Formula {

  /**
  ** The constructor for a QuantFormula takes an integer
  ** which represents the quantifier (see YYtokentypes), a list of
  ** Fariables and a Formula.
  ** @param quant an integer representing the quantifier
  ** @param vars a Vector of Variables 
  ** @param form the Formula quantified over
  ** @exception IllegalArgumentException An exception will occur if the 
  ** given integer has an unexpected value, the given Formula is null, or
  ** the given Vector is null, empty, or contains an element that is not 
  ** a Variable.
  */
  public QuantFormula(int quant, Vector vars, Formula form)
      throws IllegalArgumentException {
    theQuant = quant;
    if ((theQuant != allValue) && (theQuant != exValue))
      throw new IllegalArgumentException(
          "Attempt to create QuantFormula with unknown quantifier.");
    theVars = new Vector(vars.size()+1);
    for (Enumeration e=vars.elements(); e.hasMoreElements(); ) {
      Object ne = e.nextElement();
      if (ne instanceof Variable)
	theVars.addElement((Variable)ne);
      else 
	throw new IllegalArgumentException(
            "Attempt to construct QuantFormula quantifying over " + ne + 
            " instead of a variable as expected.");
    }
    if (form == null)
      throw new IllegalArgumentException(
          "Attempt to create QuantFormula with null formula.");
    theForm = form;
  }

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

  /** 
  ** Returns a copy of this QuantFormula 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. Varibales that are mapped to a 
  ** non-VarTerm by the Substitution will be removed from the Vector of
  ** Variables. If the Vector is empty as a result of this the whole
  ** quantification is removed and only the instantiated content Formula
  ** is returned.
  ** @param s the Substitution that tells us how to replace Variables
  ** @return a new Formula that is an instance of this 
  ** QuantFormula; 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 QuantFormula with null Substitution.");
    Vector newVars = new Vector(theVars.size()+1);
    for (Enumeration e=theVars.elements(); e.hasMoreElements(); ) {
      Term t = s.getValue((Variable)e.nextElement());
      if (t instanceof VarTerm)
	newVars.addElement(((VarTerm)t).getVar());
    }
    if (newVars.isEmpty())
      return theForm.clone(s);
    return new QuantFormula(theQuant, newVars, theForm.clone(s));
  }

  /**
  ** This function returns a new Formula which is the skolemized AND/OR form 
  ** of this QuantFormula. 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 Formula 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 {
    if (s == null)
      throw new IllegalArgumentException(
          "Attempt to skolemize QuantFormula with null Substitution.");
    if (allQuantVars == null)
      throw new IllegalArgumentException(
          "Attempt to skolemize QuantFormula with null Vector of Variables.");

    // the resulting quantifier:
    boolean uniQuantRes = 
      (((theQuant == allValue) && (! isNegated)) ||
       ((theQuant == exValue) && (isNegated)));

    // add variables to allQuantVars if necessary:
    if (uniQuantRes)
      for (Enumeration e1=theVars.elements(); e1.hasMoreElements(); )
	allQuantVars.addElement(e1.nextElement());

    // or generate Skolem terms and add them to the substitution:
    else
      for (Enumeration e2=theVars.elements(); e2.hasMoreElements(); )
	try {
          if (! s.unify((Variable)e2.nextElement(), 
		    getSkolemTerm(allQuantVars)))
	  throw new UnknownError("Skolemization problem!");
	} catch (UnificationException ue) {
	  throw new UnknownError("Skolemization problem: " + ue.getMessage());
	}

    // compute the vector of conditions:
    Vector conds = new Vector(theVars.size());
    for (Enumeration e3=theVars.elements(); e3.hasMoreElements(); ) {
      Variable v = (Variable)e3.nextElement();
      Symbol tType = v.getType();
      if (tType != null)
	conds.addElement(new Literal(uniQuantRes, InstanceOfSy, 
            new VarTerm(v), new ConstTerm(tType)));
    }

    // compute the formula to be returned:
    Formula result;
    if (! conds.isEmpty()) {
      MultiConFormula mcf = new MultiConFormula((uniQuantRes) ?
	  YYtokentypes.OR.intValue() : YYtokentypes.AND.intValue(), 
          conds.size()+4);
      for (Enumeration e4=conds.elements(); e4.hasMoreElements(); ) {
	Literal nL = (Literal)e4.nextElement();
	mcf.addFormula(nL);
      }
      mcf.addFormula(theForm.
          toSkolemizedAndOrForm(s, allQuantVars, isNegated));
      mcf.liftSameConnective();
      result = mcf;
    }
    else
      result = theForm.toSkolemizedAndOrForm(s, allQuantVars, isNegated);

    // remove the variables from allQuantVars if necessary:
    if (uniQuantRes) {
      int lastToRemove = allQuantVars.size()-theVars.size();
      for (int i=allQuantVars.size()-1; i>=lastToRemove; i--)
	allQuantVars.removeElementAt(i);
    }

    // return the result:
    return result;
  }

  private Term getSkolemTerm(Vector vars) {
    if (vars.isEmpty())
      return new ConstTerm(new UnnamedSymbol("SkC"));
    Vector args = new Vector(vars.size()+1);
    for (Enumeration e=vars.elements(); e.hasMoreElements(); )
      args.addElement(new VarTerm((Variable)e.nextElement()));
    return new FunctTerm(new UnnamedSymbol("SkF"), args);
  }

  /**
  ** A QuantFormula is printed as ((&lt;quantifier&gt; &lt;var-spec&gt;) 
  ** &lt;quantifier&gt;). A &lt;var-spec&gt; can be either 
  ** &lt;variable&gt; or (&lt;varibale&gt; &lt;constant&gt;).
  ** @return the String that represents this QuantFormula
  */
  public String toString() {
    String res = "((" + YYtokentypes.tokenname(theQuant) + ' ';
    Enumeration e = theVars.elements();
    if (e.hasMoreElements())
      res += varSpecToString((Variable)e.nextElement());
    while (e.hasMoreElements()) {
      res += " " + varSpecToString((Variable)e.nextElement());
    }
    return res + ") " + theForm.toString() + ')';
  }
  
  private String varSpecToString(Variable v) {
    Symbol vType = v.getType();
    if (vType == null)
      return v.toString();
    return "(" + v.toString() + ' ' + vType.toString() + ')';
  }
    

  /** 
  ** This function tests whether this and the given Object are equal. In
  ** general, two QuantFormulae are equal if they have the same 
  ** quantifier, quantify over the same variables in the same order, and 
  ** quantify over equal formulae.
  ** @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 QuantFormula))
      return false;
    QuantFormula oqf = (QuantFormula)otherForm;
    if ((theQuant != oqf.theQuant) || (theVars.size() != oqf.theVars.size()))
      return false;
    Enumeration e2=oqf.theVars.elements();
    for (Enumeration e1=theVars.elements(); e1.hasMoreElements(); )
      if (e1.nextElement() != e2.nextElement())
	return false;
    return theForm.equals(oqf.theForm);
  }

  /**
  ** the quantifyer as defined in YYtokentypes
  */
  private int theQuant;

  /**
  ** the Vector of Variables quantified over; type information is stored 
  ** in the Variable itself
  */
  private Vector theVars;

  /**
  ** the Formula quantified over
  */
  private Formula theForm;


  /** 
  ** for quicker access these values are stored locally
  */
  private static int allValue = YYtokentypes.FORALL.intValue();
  private static int exValue = YYtokentypes.EXISTS.intValue();
  private static Symbol InstanceOfSy = Symbol.get("InstanceOf");
}
