package JavaAgent.resource.fopl;


import java.util.*;

/** 
** This class represents a Formula that consists of a exactly two 
** sub-Formulae that are connected by a binary connective. Currently there
** are the connectives <tt>IMPLIES</tt>, <tt>IFF</tt>, and <tt>XOR</tt>.
** @see YYtokentypes
*/

public class BinConFormula extends Formula {

  /**
  ** This constructor for a BinConFormula takes an integer
  ** which represents the connective (see YYtokentypes) and two 
  ** Formulae. The first Formula is taken to be the left hand side where 
  ** that matters.
  ** @param con an integer representing the connective
  ** @param f1 the left hand side Formula
  ** @param f2 the right hand side Formula
  ** @exception IllegalArgumentException An exception will occur if the 
  ** given integer has an unexpected value or either of the given Formulae 
  ** is null.
  */
  public BinConFormula(int con, Formula f1, Formula f2)
      throws IllegalArgumentException {
    theCon = con;
    if ((theCon != implValue) && (theCon != iffValue)&& (theCon != xorValue))
      throw new IllegalArgumentException(
          "Attempt to create BinConFormula with unknown connective.");
    if ((f1 == null) || (f2 == null))
      throw new IllegalArgumentException(
          "Attempt to create BinConFormula with null sub-formula.");
    theLHS = f1;
    theRHS = f2;
  }

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

  /** 
  ** Returns a copy of this BinConFormula 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 BinConFormula that is an instance of this 
  ** BinConFormula; 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 BinConFormula with null Substitution.");
    return new BinConFormula(
        theCon, (Formula)theLHS.clone(s), (Formula)theRHS.clone(s));
  }

  /**
  ** This function returns a new Formula which is the skolemized AND/OR form 
  ** of this BinConFormula. 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 aQVars, boolean isNegated) 
      throws IllegalArgumentException {
    if (((theCon == iffValue) && (! isNegated)) ||
	((theCon == xorValue) && (isNegated))) {
      return new MultiConFormula(andValue,
          new MultiConFormula(orValue,
              theLHS.toSkolemizedAndOrForm(s, aQVars, true),
              theRHS.toSkolemizedAndOrForm(s, aQVars, false)),
          new MultiConFormula(orValue,
              theLHS.toSkolemizedAndOrForm(s, aQVars, false),
              theRHS.toSkolemizedAndOrForm(s, aQVars, true)));
    }
    if (((theCon == xorValue) && (! isNegated)) ||
	((theCon == iffValue) && (isNegated))) {
      return new MultiConFormula(andValue,
          new MultiConFormula(orValue,
              theLHS.toSkolemizedAndOrForm(s, aQVars, true),
              theRHS.toSkolemizedAndOrForm(s, aQVars, true)),
          new MultiConFormula(orValue,
              theLHS.toSkolemizedAndOrForm(s, aQVars, false),
              theRHS.toSkolemizedAndOrForm(s, aQVars, false)));
    }
    // it is a possibly negated implication:
    if (isNegated) {
      return new MultiConFormula(andValue,
          theLHS.toSkolemizedAndOrForm(s, aQVars, false),
          theRHS.toSkolemizedAndOrForm(s, aQVars, true));
    }
    return new MultiConFormula(orValue,
        theLHS.toSkolemizedAndOrForm(s, aQVars, true),
        theRHS.toSkolemizedAndOrForm(s, aQVars, false));
  }

  /**
  ** A MultiConFormula is printed as ( &lt;connective&gt; &lt;formula&gt; 
  ** &lt;formula&gt; ).
  ** @return the String that represents this MultiConFormula
  */
  public String toString() {
    return "(" + YYtokentypes.tokenname(theCon) + ' ' + theLHS.toString() + 
        ' ' + theRHS.toString() + ')';
  }

  /** 
  ** This function tests whether this and the given Object are equal. In
  ** general, two BinConFormulae are equal if they have the same 
  ** connective and both 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 BinConFormula))
      return false;
    BinConFormula obcf = (BinConFormula)otherForm;
    return (theCon == obcf.theCon) && 
        (theLHS.equals(obcf.theLHS)) && (theRHS.equals(obcf.theRHS));
  }

  /**
  ** This function returns the premise of this implication.
  */
  public Formula getPremise() {
    return theLHS;
  }

  /**
  ** This function returns the conclusion of this implication.
  */
  public Formula getConclusion() {
    return theRHS;
  }

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

  /**
  ** the sub-Formulae
  */
  private Formula theLHS, theRHS;

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