package JavaAgent.resource.fopl;


import java.util.*;
import java.io.*;
import java.text.ParseException;

/**
** A Formula is an abstraction. A Formula is usually used in logic to 
** represent a proposition or sentence that is either true or false.
** Currently, there are several kinds of Formulae implemented.
** @see Literal
** @see NegFormula
** @see MultiConFormula
** @see BinConFormula
** @see QuantFormula
*/

public abstract class Formula implements JavaAgent.resource.cdl.Parsable, 
    JavaAgent.resource.cdl.KRSentence {

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

  /** 
  ** Returns a copy of this Formula 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.
  ** <p> This function can also be used to generate a copy of this 
  ** Formula that contains a new set of Variables. The given Substitution 
  ** should be a new, empty Substitution in this case. Otherwise cloning
  ** can be seen as instantiating the Formula.
  ** @param s the Substitution that tells us how to replace Variables
  ** @return a new Formula that is an instance 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 is null. In this case <tt>clone()</tt> (above) should be
  ** used.
  */
  abstract public Formula clone(Substitution s) 
      throws IllegalArgumentException;

  /** 
  ** This function returns a new Formula which is the skolemized version 
  ** of this Formula in which the only connectives are AND and OR and only
  ** literals may be negated. This is done by:
  ** <ol>
  ** <li> adding information about Variable types in the quantfication to the
  **   Formula itself;
  ** <li> replacing the connectives IMPLIES, IFF, and XOR by their equivalent
  **   combinations of AND and OR; this may lead to a multiplication of 
  **   sub-formuae;
  ** <li> pulling the negations into the Formula using mainly de Morgan's law; 
  **   this may also reverse quantifiers;
  ** <li> replacing Variables that are existentially quantified at this point 
  **   by appropriate Skolem symbols and functions;
  ** <li> dropping the quantifiers;
  ** </ol>
  ** @return a new Formula which is the skolemized AND/OR form of this 
  ** Formula
  */
  public Formula toSkolemizedAndOrForm() {
    try {
      Substitution s = new Substitution();
      Formula SkForm = toSkolemizedAndOrForm(s, new Vector(), false);
      return SkForm.clone(s);
    } catch (IllegalArgumentException iae) {
      throw new UnknownError(
          "Problem in toSkolemizedAndOrForm(): " + iae.getMessage());
    }
  }

  /** 
  ** This function returns a new Formula which is the skolemized AND/OR form 
  ** of this Formula. The returned Substitution indicates how Variables are
  ** to be replaced; either by copies of the Variable or a Skolem symbol 
  ** (ConstTerm) or function. The Variables to be replaced will still be in
  ** the Formula though! 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 (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.
  */
  abstract protected Formula toSkolemizedAndOrForm(
      Substitution s, Vector allQuantVars, boolean isNegated)
      throws IllegalArgumentException;

  /**
  ** This function tests whether this and the given Object are equal. In
  ** general, two Formulae are equal if they have the same structure and
  ** consist of the same Symbols and Variables. This is not a test for 
  ** logical equivalence or unifyability!
  ** @param otherForm the Formula this one is to be compared to
  ** @return whether the given Object is equal to this one
  */
  abstract public boolean equals(Object otherForm);

  /**
  ** This function can be used to parse a given String that represents a 
  ** Formula. The syntax in BNF is as follows:
  ** <pre>
  ** &lt;formula&gt;    ::= ( &lt;quant&gt; &lt;c-from&gt; ) | &lt;c-from&gt;
  **
  ** &lt;quant&gt;      ::= ( &lt;quantifier&gt; &lt;varspec&gt;+ )
  ** &lt;quantifier&gt; ::= forall | exists
  ** &lt;varspec&gt;    ::= &lt;variable&gt; | 
  **                  ( &lt;variable&gt; &lt;constant&gt; )
  ** 
  ** &lt;c-from&gt;     ::= &lt;literal&gt; |
  **                  ( not &lt;formula&gt; ) | 
  **                  ( and &lt;formula&gt; &lt;formula&gt;+ ) | 
  **                  ( or &lt;formula&gt; &lt;formula&gt;+ ) | 
  **                  ( implies &lt;formula&gt; &lt;formula&gt; ) | 
  **                  ( iff &lt;formula&gt; &lt;formula&gt; ) | 
  **                  ( xor &lt;formula&gt; &lt;formula&gt; ) | 
  ** 
  ** &lt;literal&gt;    ::= &lt;constant&gt; | 
  **                  ( = &lt;term&gt; &lt;term&gt; )
  **                  ( &lt;constant&gt; &lt;term&gt;+ )
  **
  ** &lt;term&gt;       ::= &lt;constant&gt; | &lt;variable&gt; | 
  **                  ( &lt;constant&gt; &lt;term&gt;+ ) |
  ** &lt;variable&gt;   ::= ?&lt;name&gt;
  ** &lt;constant&gt;   ::= &lt;name&gt;
  ** </pre>
  ** @exception IllegalArgumentException An exception will occur if the 
  ** supplied String is empty or null.
  ** @exception ParseException An exception can occur if parsing failed.
  ** Potential reasons include a syntax error or an I/O problem.
  */
  public static Formula parse(String s) 
      throws IllegalArgumentException, ParseException {
    if ((s == null) || s.equals(""))
      throw new IllegalArgumentException("Attempt to parse empty String!");
    try {
      YYparse parser = new YYparse("formula " + s);
      return (Formula)parser.parseResult;
    } catch (IOException ioe) {
      throw new ParseException("I/O problem while parsing (" + 
          ioe.getMessage() + ')', 0);
    } catch (Exception e) {
      throw new ParseException("Parse error in Formula " + s + 
          " (" + e.getMessage() + ')', 0);
    }
  }

  /**
  ** This function can be used to parse a given InputStream that represents 
  ** a Formula. The syntax in BNF is as above except that the first token
  ** should be the word <tt>FORMULA</tt> so that the generic parser knows what
  ** it has to expect. This is added automatically when parsing a String.
  ** @exception IllegalArgumentException An exception will occur if the 
  ** supplied InputStream is null.
  ** @exception IOException An exception can occur if there are problems 
  ** reading from the given InputStream.
  ** @exception ParseException An exception can occur if parsing failed.
  ** Potential reasons include a syntax error.
  */
  public static Formula parse(InputStream ist) 
      throws IllegalArgumentException, IOException, ParseException {
    if (ist == null)
      throw new IllegalArgumentException("Attempt to parse null Stream!");
    try {
      YYparse parser = new YYparse(ist);
      return (Formula)parser.parseResult;
    } catch (IOException ioe) {
      throw ioe;
    } catch (Exception e) {
      throw new ParseException("Parse error in Formula: (" + 
          e.getMessage() + ')', 0);
    }
  }
}
