package JavaAgent.resource.fopl;


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

import JavaAgent.resource.cdl.KRSentence;
import JavaAgent.resource.cdl.FormalismException;

/**
** A FormulaSet is a set of Formulae. This is the most general knowledge 
** representation in the fopl package. When evaluating a Formula against
** a FormulaSet, the Formula and FormulaSet will be converted to clause form 
** and a resolution theorem prover will be used to test whether the negated
** Formula and the FormulaSet give rise to an inconsistency.
** @see Formula
** @see ClauseSet
** @see RTProver
*/

public class FormulaSet implements JavaAgent.resource.cdl.Parsable, 
    JavaAgent.resource.cdl.KnowledgeBase {

  /**
  ** This constructor creates an empty FormulaSet.
  */
  public FormulaSet() {
    theForms = new Vector(30, 20);
    theClauses = new ClauseSet();
  }

  /**
  ** This constructor creates a FormulaSet that contains just the given 
  ** Formula.
  ** @param aFrom the Formula in this FormulaSet
  ** @exception IllegalArgumentException An exception will occur if the given
  ** FormulaSet is null. In this case the constructor for an empty FormulaSet 
  ** (above) should be used.
  */
  public FormulaSet(Formula aFrom) throws IllegalArgumentException {
    theForms = new Vector(10, 20);
    theClauses = new ClauseSet();
    try {
      assert(aFrom);
    } catch (FormalismException fe) {
      throw new UnknownError("Cannot create FormulaSet: " + fe.getMessage());
    }
  }

  /** 
  ** Cloning a FormulaSet returns a new FormulaSet consisting of
  ** clones of the Formulae in the original FormulaSet.
  ** @return a copy of this ClauseSet
  */
  public Object clone() {
    FormulaSet newForms = new FormulaSet();
    for (Enumeration e=sentences(); e.hasMoreElements(); ) {
      try {
	newForms.assert(((Formula)e.nextElement()).clone(new Substitution()));
      } catch (FormalismException fe) {
	throw new UnknownError(
            "Cannot create FormulaSet: " + fe.getMessage());
      }
    }
    return newForms;
  }

  /**
  ** This function can be used to add knowledge to this FormulaSet.
  ** @param sent the KRSentence holding the new knowledge
  ** @exception IllegalArgumentException An exception will occur if the given
  ** KRSentence is null.
  ** @exception FormalismException An exception will occur if the given
  ** KRSentence is not a Formula.
  */
  public void assert(KRSentence sent)
       throws IllegalArgumentException, FormalismException {
    if (sent == null)
      throw new IllegalArgumentException(
          "Attempt to assert null formula in formula set.");
    FOPLFormula ff = getFOPLFormula(sent);
    theForms.addElement(ff);
    theClauses.assert(new ClauseSet(ff.getFormula()));
  }

  /**
  ** This function converts the given KRSentence into a FOPLFormula. It
  ** trivially succeeds if the given KRSentence already is a FOPLFormula.
  ** Otherwise it tries to use the function <tt>getFOPLFormula()</tt> of
  ** the given KRSentence to get the FOPLFormula. If this fails a
  ** FormalismException will be thrown.
  ** @param sent the KRSentence to be converted into a FOPLFormula
  ** @return a FOPLFormula representing the given KRSentence
  ** @exception FormalismException An exception will be thrown if the
  ** given KRSentence cannot be converted in to a FOPLFormula for 
  ** some reason.
  */
  static protected FOPLFormula getFOPLFormula(KRSentence sent) 
      throws FormalismException {
    if (sent instanceof FOPLFormula)
      return (FOPLFormula)sent;
    try {
      return (FOPLFormula)sent.getClass().
	  getMethod("getFOPLFormula", new Class[]{}).
          invoke(sent, new Object[]{});
    } catch (Exception e) {
      throw new FormalismException(
          "Failed to convert " + sent + " to FOPLFormula!");
    }
  }

  /**
  ** This function tests whether this FormulaSet is inconsistent.
  ** @return <tt>true</tt> iff this KnowledgeBase is inconsistent
  ** @exception IOException An exception can occur if writing to the given 
  ** OutputStream for tracing fails.
  */
  public boolean isInconsistent() throws IOException {
    rtp = new RTProver();
    rtp.setTraceStream(traceStream);
    for (Enumeration ce=theClauses.sentences(); ce.hasMoreElements(); )
      rtp.addOpenClause((Clause)ce.nextElement());
    return (! rtp.resolve());
  }

  /**
  ** This function takes a Formula and evaluates it against this
  ** FormulaSet.
  ** @param sent the KRSentence to be evaluated
  ** @return <tt>true</tt> iff the given KRSentence could be derived from 
  ** the KnowledgeBase
  ** @exception IllegalArgumentException An exception will occur if the given
  ** KRSentence is null.
  ** @exception FormalismException An exception will occur if the given
  ** KRSentence is not a Formula.
  ** @exception IOException An exception can occur if writing to the given 
  ** OutputStream for tracing fails.
  */
  public boolean evaluate(KRSentence sent)
       throws IllegalArgumentException, FormalismException, IOException {
    if (sent == null)
      throw new IllegalArgumentException(
          "Attempt to evaluate null sentence in formula set.");
    FOPLFormula ff = getFOPLFormula(sent);
    rtp = new RTProver();
    //traceStream = new FileOutputStream("trace.txt");
    rtp.setTraceStream(traceStream);
    for (Enumeration ce1=theClauses.sentences(); ce1.hasMoreElements(); )
      rtp.addClosedClause((Clause)ce1.nextElement());
    ClauseSet qClauses = new ClauseSet(new NegFormula(ff.getFormula()));
    for (Enumeration ce2=qClauses.sentences(); ce2.hasMoreElements(); )
      rtp.addOpenClause((Clause)ce2.nextElement());
    return (! rtp.resolve());
  }

  /**
  ** This function tries to find values for the Variables in the given Vector
  ** such that the given KRSentence follows from this FormulaSet. The values
  ** will be returned in a HashTable. If no such values can be found the
  ** result will be null.
  ** @param sent the KRSentence to be evaluated
  ** @param vars The Vector of Variables
  ** @return a HashTable containing the Variable value assignments found
  ** or null if no assignments were found.
  ** @exception IllegalArgumentException An exception will occur if the given
  ** KRSentence is null.
  ** @exception FormalismException An exception will occur if the given
  ** KRSentence is not a Formula.
  ** @exception IOException An exception can occur if writing to the given 
  ** OutputStream for tracing fails.
  */
  public Hashtable evaluate(KRSentence sent, Vector vars)
       throws IllegalArgumentException, FormalismException, IOException {
    if (sent == null)
      throw new IllegalArgumentException(
          "Attempt to evaluate null sentence in formula set.");
    if (! evaluate(sent))
      return null;
    return rtp.extractValues(vars);
  }

  /**
  ** This function tests whether the given KRSentence was used in the last
  ** derivation or whether it could have been deleted from this FormulaSet
  ** without changing the derivability of the last query.
  ** @param krs the KRSentence to be tested
  ** @return true iff it was used in the derivation
  */
  public boolean usedInProof(JavaAgent.resource.cdl.KRSentence krs) {
    return rtp.usedInProof(krs);
  }

  /**
  ** This function returns an enumerator for the Formulae in this
  ** FormulaSet.
  ** @return an Enumeration for the KRSentences in this KnowledgeBase
  */
  public Enumeration sentences() {
    return theForms.elements();
  }

  /** 
  ** This function can be used create a trace of the functions 
  ** <tt>isInconsistent()</tt> and <tt>evaluate()</tt>. If the given 
  ** value is null no trace will be generated. Otherwise the trace will
  ** be written to the given OutputStream.
  ** @param ost the OutputStream the trace is to be written to
  */
  public void setTraceStream(OutputStream ost) {
    traceStream = ost;
  }

  /**
  ** This function writes the content of this KnowledgeBase to the given
  ** OutputStream.
  ** @param os theOutputStream the KRSentences is to be written to
  ** @exception IllegalArgumentException An exception will occur if the given
  ** OutputStream is null.
  ** @exception IOException An exception will occur if writing to the given
  ** OutputStream failed for some reason.
  */
  public void writeToStream(OutputStream os)
       throws IllegalArgumentException, IOException {
    if (os == null)
      throw new IllegalArgumentException(
          "Attempt to write formulae to null output stream");
    for (Enumeration fe=sentences(); fe.hasMoreElements(); ) {
      String form = fe.nextElement().toString();
      os.write(form.getBytes());
      os.write((int)'\n');
    }
  }

  /**
  ** This function can be used to parse a given InputStream that represents a 
  ** FormulaSet. The syntax in BNF is as follows:
  ** <pre>
  ** &lt;formulaset&gt;::= FORMS &lt;formula&gt;*
  ** &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 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 FormulaSet 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 (FormulaSet)parser.parseResult;
    } catch (IOException ioe) {
      throw ioe;
    } catch (Exception e) {
      throw new ParseException("Parse error in FormulaSet: (" + 
          e.getMessage() + ')', 0);
    }
  }

  /**
  ** the Formulae in this FormulaSet
  */
  private Vector theForms;

  /**
  ** the Skolemized clause form version of the Formulae
  */
  private ClauseSet theClauses;

  /** 
  ** the OutputStream to which traces of calls to <tt>isInconsistent()</tt> and
  ** <tt>evaluate()</tt> can be written
  */
  private OutputStream traceStream = null;

  /**
  ** the last RTProver used
  */
  private RTProver rtp;
}    
