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 ClauseSet is a set of Clauses. ClauseSets can be constructed from a 
** Formula or a FormulaSet and then tested for inconsistency. They will
** construct a resolution theorem prover to do so.
** @see Clause
** @see RTProver
*/

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

  /**
  ** This constructor creates an empty ClauseSet.
  */
  public ClauseSet() {
    theClauses = new Vector(30, 50);
    containsEmptyClause = false;
  }

  /**
  ** This constructor for a ClauseSet takes a single Clause as its
  ** argument. 
  ** @param aCl the single Clause this set will contain initially
  ** @exception IllegalArgumentException An exception will occur if the given
  ** Clause is null. In this case the constructor for an empty ClauseSet 
  ** (above) should be used.
  */
  public ClauseSet(Clause aCl) throws IllegalArgumentException {
    containsEmptyClause = false;
    theClauses = new Vector(30, 50);
    try {
      assert(aCl);
    } catch (FormalismException fe) {
      throw new UnknownError("Cannot create ClauseSet: " + fe.getMessage());
    }
  }

  /**
  ** This constructor creates a ClauseSet that contains the Skolemized
  ** clause form version of the given Formula.
  ** @param aForm the Formula for which the Clauses are to be created
  ** @exception IllegalArgumentException An exception will occur if the given
  ** Formula is null.
  */
  public ClauseSet (Formula aForm) throws IllegalArgumentException {
    if (aForm == null)
      throw new IllegalArgumentException(
          "Attempt to create clause set with null formula");
    theClauses = new Vector(30, 50);
    containsEmptyClause = false;

    // generating the Clauses and separating the Variables apart:
    Formula SkForm = aForm.toSkolemizedAndOrForm();
    Vector cls = getSkClauses(SkForm);
    for (Enumeration e=cls.elements(); e.hasMoreElements(); ) {
      try {
	Clause newCl = (Clause)e.nextElement();
	if (! newCl.isTautology()) {
	  Substitution s = new Substitution();
	  Clause addCl = newCl.clone(s);
	  addCl.setParent(aForm, s);
	  assert(addCl);
	}
      } catch (FormalismException fe) {
	throw new UnknownError("Cannot create ClauseSet: " + fe.getMessage());
      }
    }
  }

  /**
  ** This constructor creates a ClauseSet that contains the Skolemized
  ** clause form version of the given Formulae in the given FormulaSet.
  ** @param forms the FormulaSet for which the Clauses are to be created
  ** @exception IllegalArgumentException An exception will occur if the given
  ** FormulaSet is null.
  */
  public ClauseSet (FormulaSet forms) throws IllegalArgumentException {
    if (forms == null)
      throw new IllegalArgumentException(
          "Attempt to create clause set with null formula set");
    theClauses = new Vector(90, 100);
    containsEmptyClause = false;

    for (Enumeration f=forms.sentences(); f.hasMoreElements(); ) {
      // genarating the Clauses and separating the Variables apart:
      Formula nextForm = (Formula)f.nextElement();
      Formula SkForm = nextForm.toSkolemizedAndOrForm();
      Vector cls = getSkClauses(SkForm);
      for (Enumeration e=cls.elements(); e.hasMoreElements(); ) {
	try {
	  Clause newCl = (Clause)e.nextElement();
	  if (! newCl.isTautology()) {
	    Substitution s = new Substitution();
	    Clause addCl = newCl.clone(s);
	    addCl.setParent(nextForm, s);
	    assert(addCl);
	  }
	} catch (FormalismException fe) {
	  throw new UnknownError(
              "Cannot create ClauseSet: " + fe.getMessage());
	}
      }
    }
  }

  /** 
  ** This function takes a Formula in Skolemized AND/OR form and returns a 
  ** Vector of Clauses that represent the Skolemized clause Form of this 
  ** Formula. Variables are not standardized apart here.
  ** @param SkForm the Formula in Skolemized AND/OR form to be converted
  ** @return a Vector of Clauses
  */
  private Vector getSkClauses(Formula SkForm) {
    Vector cls;
    if (SkForm instanceof Literal) {
      cls = new Vector(10, 10);
      cls.addElement(new Clause((Literal)SkForm));
      return cls;
    }
    Enumeration e = ((MultiConFormula)SkForm).elements();
    cls = getSkClauses((Formula)e.nextElement());
    while (e.hasMoreElements()) {
      Vector addCls = getSkClauses((Formula)e.nextElement());
      if (((MultiConFormula)SkForm).isConjunction())
	conjoin(cls, addCls);
      else
	disjoin(cls, addCls);
    }
    return cls;
  }

  /**
  ** This function adds the Clauses in the second Vector to the Clauses
  ** in the first Vector.
  ** @param c1 a Vector of Clauses; Clauses from the other Vector will be 
  ** added to this one
  ** @param c2 a Vector of Clauses to be added to the first Vector
  */
  private void conjoin(Vector c1, Vector c2) {
    for (Enumeration e=c2.elements(); e.hasMoreElements(); )
      c1.addElement(e.nextElement());
  }

  /**
  ** This function takes two Vectors of Clauses and modifies the first
  ** Vector to contain the disjunction of the two sets of Clauses. The
  ** resulting first Vector will contain c1.size()*c2.size(), each containing 
  ** one possible combination of a Clause from c1 and one from c2.
  ** @param c1 a Vector of Clauses; this Vector will also contain the result
  ** @param c2 a Vector of Clauses
  */
  private void disjoin(Vector c1, Vector c2) {
    int c1size = c1.size();
    int c2size = c2.size();
    
    // append c2size-1 copies of c1 to c1:
    for (int i=1; i<c2size; i++)
      for (int j=0; j<c1size; j++)
	c1.addElement(((Clause)c1.elementAt(j)).clone());

    // now add copies of clauses in c2 to c1:
    Enumeration e1 = c1.elements();
    for (Enumeration e2 = c2.elements(); e2.hasMoreElements(); ) {
      Clause ac = (Clause)e2.nextElement();
      for (int k=0; k<c1size; k++)
	((Clause)e1.nextElement()).disjoin((Clause)ac.clone());
    }
  }

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

  /**
  ** This function can be used to add knowledge to this KnowledgeBase. The 
  ** asserted KRSentence must be a Clause.
  ** @param sent the Clause 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 Clause.
  */
  public void assert(KRSentence sent) 
      throws IllegalArgumentException, FormalismException {
    if (sent == null)
      throw new IllegalArgumentException(
          "Attempt to assert null clause in clause set.");
    if (! (sent instanceof Clause))
      throw new FormalismException(
          "Attempt to assert " + sent + " in clause set.");
    theClauses.addElement(sent);
    containsEmptyClause = ((Clause)sent).isEmpty();
  }

  /**
  ** This function can be used to add knowledge to this KnowledgeBase. It will
  ** add all the Clauses in the given ClauseSet to this ClauseSet.
  ** @param cls the ClauseSet containing the new Clauses
  ** @exception IllegalArgumentException An exception will occur if the given
  ** ClauseSet is null.
  */
  public void assert(ClauseSet cls) throws IllegalArgumentException {
    if (cls == null)
      throw new IllegalArgumentException(
          "Attempt to assert null ClauseSet.");
    for (Enumeration cl=cls.sentences(); cl.hasMoreElements(); ) {
      try {
	assert((Clause)cl.nextElement());
      } catch (FormalismException fe) {
	throw new UnknownError("Error in asserting ClauseSet.");
      }
    }
  }

  /**
  ** This function tests whether this KnowledgeBase 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 {
    if (containsEmptyClause)
      return true;
    RTProver rtp = new RTProver();
    rtp.setTraceStream(traceStream);
    for (Enumeration ce=theClauses.elements(); ce.hasMoreElements(); )
      rtp.addOpenClause((Clause)ce.nextElement());
    return (! rtp.resolve());
  }

  /**
  ** This function takes a Clause and evaluates it against this
  ** ClauseSet. It returns whether the given Clause is entailed by this 
  ** ClauseSet.
  ** @param sent the Clause to be evaluated
  ** @return <tt>true</tt> iff the given Clause could be derived from 
  ** the ClauseSet
  ** @exception IllegalArgumentException An exception will occur if the given
  ** Clause is null.
  ** @exception FormalismException An exception will occur if the given
  ** KRSentence is not a Clause.
  ** @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 clause set.");
    if (! (sent instanceof Clause))
      throw new FormalismException(
          "Attempt to evaluate " + sent + " in clause set.");
    if (containsEmptyClause)
      return true;
    if (((Clause)sent).isEmpty())
      return isInconsistent();
    RTProver rtp = new RTProver();
    rtp.setTraceStream(traceStream);
    for (Enumeration ce1=theClauses.elements(); ce1.hasMoreElements(); )
      rtp.addClosedClause((Clause)ce1.nextElement());
    for (Enumeration ce2=((Clause)sent).literals(); ce2.hasMoreElements(); ) {
      Literal nLit = (Literal)((Literal)ce2.nextElement()).clone();
      nLit.negate();
      rtp.addOpenClause(new Clause(nLit));
    }
    return (! rtp.resolve());
  }

  /**
  ** This function returns an Enumerator for the Clauses in this
  ** ClauseSet.
  ** @return an Enumeration for the KRSentences in this KnowledgeBase
  */
  public Enumeration sentences() {
    return theClauses.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 Clauses are 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 clauses to null output stream");
    for (Enumeration c=sentences(); c.hasMoreElements(); ) {
      String cl = c.nextElement().toString();
      os.write(cl.getBytes());
      os.write((int)'\n');
    }
  }

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

  /**
  ** the Clauses in this ClauseSet
  */
  private Vector theClauses;

  /** 
  ** this variable indicates whether this ClauseSet contains the empty Clause
  */
  private boolean containsEmptyClause;

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