package JavaAgent.resource.fopl;


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

import JavaAgent.resource.cdl.KRSentence;

/**
** A Clause is a set of Literals (or Propositions). Implicitely, the 
** Literals in a Clause are disjunctively connected.
** @see Literal
*/

public class Clause implements JavaAgent.resource.cdl.Parsable, 
    JavaAgent.resource.cdl.KRSentence {

  /**
  ** This constructor is for the empty clause.
  */
  public Clause() {
    tautology = false;
    theLits = new Vector(5, 4);
    ancestors = null;
  }

  /**
  ** This constructor for a Clause takes a single Literal as
  ** argument for this unit clause. 
  ** @param aLit the Literal in this Clause
  ** @exception IllegalArgumentException An exception will occur if the given
  ** Literal is null. In this case the constructor for an empty Clause (above)
  ** should be used.
  */
  public Clause(Literal aLit) throws IllegalArgumentException {
    tautology = false;
    theLits = new Vector(3, 4);
    addLiteral(aLit);
    ancestors = null;
  }

  /**
  ** This constructor for a Clause takes a Vector of Literals.
  ** All elements of the Vector must be Literals! Literals occuring twice
  ** in the Vector will only be added once. 
  ** @param someLits the Vector of Literals in this Clause
  ** @exception IllegalArgumentException An exception will occur if the given
  ** Vector is null or one of its elements is not a Literal.
  */
  public Clause(Vector someLits) throws IllegalArgumentException {
    tautology = false;
    if (someLits == null)
      throw new IllegalArgumentException(
          "Attempt to create clause with null Vector of Literals");
    theLits = new Vector(someLits.size()+1, 4);
    for (Enumeration e=someLits.elements(); e.hasMoreElements(); ) {
      Object ne = e.nextElement();
      if (ne instanceof Literal)
	addLiteral((Literal)ne);
      else 
	throw new IllegalArgumentException(
            "Attempt to create Clause with " + ne + 
            " and not a Literal as expected.");
    }
    ancestors = null;
  }

  /** 
  ** Cloning a Clause returns a new Clause consisting of
  ** clones of the Literals in the original Clause. The new Clause
  ** comes with the same Variables as the original.
  ** @return a new Clause with equal Literals
  */
  public Object clone() {
    Clause newCl = new Clause();
    newCl.tautology = tautology;
    newCl.ancestors = ancestors;
    for (Enumeration e=theLits.elements(); e.hasMoreElements(); )
      newCl.theLits.addElement((Literal)((Literal)e.nextElement()).clone());
    return newCl;
  }

  /** 
  ** Returns a copy of this Clause 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. If two of the Literals
  ** become equal in this process only one will occur in the result.
  ** <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 Clause.
  ** @param s the Substitution that tells us how to replace Variables
  ** @return a new Clause that is an instance of this 
  ** Clause; 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 Clause clone(Substitution s) throws IllegalArgumentException {
    if (s == null)
      throw new IllegalArgumentException(
          "Attempt to clone Clause with null Substitution.");
    Clause newCl = new Clause();
    newCl.tautology = tautology;
    newCl.ancestors = ancestors; /* not quite true! */
    for (Enumeration e=theLits.elements(); e.hasMoreElements(); )
      newCl.addLiteral((Literal)((Literal)e.nextElement()).clone(s));
    return newCl;
  }

  /**
  ** This function returns the Variables in this Clause in a Vector. No
  ** Variable is in the Vector twice though, i.e. it is like a set of
  ** Variables.
  ** @return a Vector of Variables in this Clause
  */
  public Vector getVars() {
    Vector vars = new Vector();
    for (Enumeration e=theLits.elements(); e.hasMoreElements(); )
      ((Literal)e.nextElement()).getVars(vars);
    return vars;
  }

  /** 
  ** This function test whether this Clause is the empty Cluase.
  ** @return <tt>true</tt> iff this clause contains no Literals
  */
  public boolean isEmpty() {
    return theLits.isEmpty();
  }

  /** 
  ** This function test whether this Clause is a tautology. This will be
  ** true if it contains two complementary Literal.
  ** @return <tt>true</tt> iff this clause is a tautology
  */
  public boolean isTautology() {
    return tautology;
  }

  /**
  ** This function adds a new Literal to this Clause. If it is already 
  ** in the Clause or is an inequality between two equal Terms it won't be
  ** added. This function uses the <tt>equals()</tt> test to determine this.
  ** @param aLit the new Literal to be appended
  ** @exception IllegalArgumentException An exception will occur if the given
  ** Literal is null.
  */
  public void addLiteral(Literal aLit) throws IllegalArgumentException {
    if (aLit == null)
      throw new IllegalArgumentException(
          "Attempt to add null Literal to Clause.");
    if ((aLit.isEquality()) && 
	(aLit.nthArgument(1).equals(aLit.nthArgument(2)))) {
      if (aLit.negated)
	return;
      else
	tautology = true;
    }
    for (Enumeration e=theLits.elements(); e.hasMoreElements(); ) {
      Literal neL = (Literal)e.nextElement();
      if (aLit.equals(neL))
	return;
      if (aLit.complements(neL))
	tautology = true;
    }
    theLits.addElement(aLit);
  }

  /**
  ** This function adds the Literals (not clones) in the given Clause to 
  ** this Clause. Duplicates are eliminated.
  ** @param c the Clause to be appended
  ** @exception IllegalArgumentException An exception will occur if the given
  ** Clause is null.
  */
  public void disjoin(Clause c) throws IllegalArgumentException {
    if (c == null)
      throw new IllegalArgumentException(
          "Attempt to disjoin null Clause to Clause.");
    for (Enumeration e=c.theLits.elements(); e.hasMoreElements(); )
      addLiteral((Literal)e.nextElement());
  }

  /** 
  ** This function generates all possible resolvents from this and the 
  ** given Vector of Clauses over one of this Clauses' Literals. For this 
  ** purpose it will first generate all resolvents over all Literals in this 
  ** Clause. It will then select the Literal which generated the smallest 
  ** number of resolvents and return the resolvents of this Literal.
  ** @param a Vector of Clauses this one is to be resolved with
  ** @return a Vector of Clauses which are all possible resolvents over only
  ** one of the Literals in this Clause and all given Clauses with 
  ** complementary Literals
  ** @exception IllegalArgumentException An exception will occur if the given
  ** Vector is null.
  */
  public Vector getResolvents(Vector clauses) throws IllegalArgumentException {
    if (clauses == null)
      throw new IllegalArgumentException(
          "Attempt to Clause with null Vector of Clauses.");
    Vector bestR = null;
    for (Enumeration e1=theLits.elements(); e1.hasMoreElements(); ) {
      Literal curLit = (Literal)e1.nextElement();
      Vector resolvents = new Vector();
      testInequality(resolvents, curLit);
      for (Enumeration e2=clauses.elements(); e2.hasMoreElements(); )
	getResolvents(curLit, (Clause)e2.nextElement(), resolvents);
      if ((bestR == null) || (bestR.size() > resolvents.size()))
	bestR = resolvents;
    }
    return bestR;
  }

  /**
  ** This function tests whether the given Literal in this Clause is
  ** an inequality and adds a new derived Clause to the given Vector
  ** if possible. The added Clause is basically the result of a 
  ** resolution step with the Literal (= ?x ?x).
  ** @param resolvents the Vector to which the result may be added
  ** @param lit a Literal in this Clause
  */
  protected void testInequality(Vector resolvents, Literal lit) {
    if ((! lit.isPositive()) && (lit.isEquality())) {
      try {
	Substitution s = new Substitution();
	if (lit.nthArgument(1).unify(lit.nthArgument(2), s)) {
	  Clause newCl = new Clause();
	  for (Enumeration le=literals(); le.hasMoreElements(); ) {
	    Literal l = (Literal)le.nextElement();
	    if (l != lit)
	      newCl.addLiteral((Literal)l.clone(s));
	  }
	  newCl.ancestors = new InEqStep(this, lit, s);
	  resolvents.addElement(newCl);
	}
      } catch (UnificationException ue) {
	throw new UnknownError("Resolution problem: " + ue.getMessage());
      }
    }
  }

  /** 
  ** This function generates all possible resolvents from this and the 
  ** given Clause over the given Literal in this Clause and adds them
  ** to the given Vector.
  ** @param lit a Literal in this Clause
  ** @param other the Clause this one is to be resolved with
  ** @param res A Vector of Clauses; new resolvents generated here will be
  ** added to this Vector
  ** @exception IllegalArgumentException An exception will occur if the given 
  ** Clause or the given Vector are null
  */
  protected void getResolvents(Literal lit, Clause other, Vector res) 
      throws IllegalArgumentException {
    if (other == null)
      throw new IllegalArgumentException(
          "Attempt to generate resolvents for null clause.");
    for (Enumeration e2=other.theLits.elements(); e2.hasMoreElements(); ) {
      Literal oLit = (Literal)e2.nextElement();
      try {
	Substitution s = new Substitution();
	if (lit.complements(oLit, s))
	  res.addElement(getResolvent(lit, other, oLit, s));
      } catch (UnificationException ue) {
	throw new UnknownError("Resolution problem: " + ue.getMessage());
      }
      if (oLit.isPositive() && oLit.isEquality())
	addParamodulants(lit, other, oLit, res);
    }
  }

  /**
  ** This function generates a new Clause that is the resolvent of this
  ** Clause and the given Clause over the first given Literal in this Clause
  ** and the second given Literal in the given Clause where the given 
  ** Substitution must be a unifying Substitution over these two Literals.
  ** The resolvent Clause will contain a new set of Variables and no
  ** duplicate Literals will be in this Clause.
  ** <p> If the two Literals are not members of the respective Clauses or
  ** if they are not complementary under the given Substitution then the
  ** behaviour of this function is undefined. It may cause exceptions or
  ** just generate a meaningless Clause.
  ** @param myLit a Literal in this Clause
  ** @param otherCl the second Clause that will be used to generate the
  ** resolvent
  ** @param otherLit a Literal in <tt>otherCl</tt> that must be complementary
  ** to <tt>myLit</tt>
  ** @param s a unifying Substitution for <tt>myLit</tt> and <tt>otherLit</tt>
  ** @return a new Clause that is the resolvent of this and the given Clause
  ** over the given Literals; the given Substitution will be extended to
  ** keep track of Variable mappings
  ** @exception IllegalArgumentException An exception may occur if the given
  ** Clause or Substitution are null.
  */
  protected Clause getResolvent(
      Literal myLit, Clause otherCl, Literal otherLit, Substitution s) 
      throws IllegalArgumentException {
    Clause res = new Clause();
    for (Enumeration e1=theLits.elements(); e1.hasMoreElements(); ) {
      Literal l1 = (Literal)e1.nextElement();
      if (l1 != myLit)
	res.addLiteral((Literal)l1.clone(s));
    }
    if (otherCl == null)
      throw new IllegalArgumentException(
          "Attempt to generate resolvent for null clause.");
    for (Enumeration e2=otherCl.theLits.elements(); e2.hasMoreElements(); ) {
      Literal l2 = (Literal)e2.nextElement();
      if (l2 != otherLit)
	res.addLiteral((Literal)l2.clone(s));
    }
    res.ancestors = new RStep(this, myLit, otherCl, otherLit, s);
    return res;
  }

  /**
  ** This function adds certain paramodulants to the given Vector. Only
  ** FunctTerms in the first given Literal which must be in this Clause will
  ** be replaced. Replacements are determined solely by the given Literal 
  ** which should be an equality in the other Clause. 
  ** @param lit a Literal in this Clause
  ** @param other another Clause
  ** @param eqLit an equality in the other Clause
  ** @param res the Vector new Clauses are to be added to
  */
  protected void addParamodulants(
      Literal lit, Clause other, Literal eqLit, Vector res) {
    Term eqTerm1 = eqLit.nthArgument(1);
    Term eqTerm2 = eqLit.nthArgument(2);
    if ((eqTerm1 instanceof VarTerm) && (eqTerm2 instanceof VarTerm))
      return;
    for (Enumeration ste=lit.allSubTerms(); ste.hasMoreElements(); ) {
      Term st = (Term)ste.nextElement();
      if (! (st instanceof VarTerm)) {
	getParamod(lit, st, other, eqLit, eqTerm1, eqTerm2, res);
	getParamod(lit, st, other, eqLit, eqTerm2, eqTerm1, res);
      }
    }
  }

  /**
  ** This function may add a paramodulant to the given Vector. The
  ** paramodulant will replace the first given Term in the given Literal in 
  ** this Clause which must unify with the second given Term for this
  ** purpose. It will be replaced by the third given Term and the 
  ** paramodulant will be construted from this CLause and the given Clause
  ** which should contain the given equality.
  ** @param lit a Literal in this Clause
  ** @param sTerm a sub-Term in this Literal
  ** @param eqCl another Clause
  ** @param eqLit an equality in this Clause
  ** @param eqTerm1 one side of this equality
  ** @param eqTerm2 the other side of this equality
  ** @param res the Vector the paramodulant may be added to
  */
  private void getParamod(
      Literal lit, Term sTerm, Clause eqCl, Literal eqLit, 
      Term eqTerm1, Term eqTerm2, Vector res) {
    if (eqTerm1 instanceof VarTerm)
      return;
    try {
      Substitution s1 = new Substitution();
      if (eqTerm1.unify(sTerm, s1)) {
	Clause newCl = new Clause();

	// adding all Literals from this Clause (with the replaced Term):
	for (Enumeration le1=literals(); le1.hasMoreElements(); ) {
	  Literal l1 = (Literal)le1.nextElement();
	  if (l1 == lit)
	    newCl.addLiteral(l1.clone(s1, sTerm, eqTerm2));
	  else 
	    newCl.addLiteral((Literal)l1.clone(s1));
	}

	// adding the Literals form the other Clause except for the eqality:
	for (Enumeration le2=eqCl.literals(); le2.hasMoreElements(); ) {
	  Literal l2 = (Literal)le2.nextElement();
	  if (l2 != eqLit)
	    newCl.addLiteral((Literal)l2.clone(s1));
	}

	newCl.ancestors = new PStep(
            this, lit, sTerm, eqCl, eqLit, eqTerm2, s1);
	res.addElement(newCl);
      }
    } catch (UnificationException ue) {
      throw new UnknownError("Paramodulation problem: " + ue.getMessage());
    }
  }

  /**
  ** This function can be used to set the ancestor of this Clause to the
  ** given KRSentence.
  ** @param krs the parent KRSentence
  */
  protected void setParent(KRSentence krs, Substitution s) {
    ancestors = new Instantiation(krs, s);
  }

  /**
  ** This function tests whether this Clause has the given Clause as a
  ** (direct) parent clause.
  ** @param cl the potential parent Clause 
  ** @return <tt>true</tt> iff the given Clause is a parent of this Clause
  */
  protected boolean hasParent(KRSentence cl) {
    if (ancestors == null)
      return false;
    return ancestors.parent(cl);
  }

  /**
  ** This function returns a Vector that contains all the direct parent
  ** Clauses to this Clause. It returns null if no parents are known.
  ** @return a Vector that contains all the direct parent Clauses to 
  ** this Clause
  */
  protected Vector getParents() {
    if (ancestors == null)
      return null;
    return ancestors.getParents();
  }

  /**
  ** This function returns the Substitution that was used to derive this
  ** Clause. It returns null if no parents are known.
  ** @return the Substitution that was used to derive this Clause
  */
  protected Substitution getParentSubstitution() {
    if (ancestors == null)
      return null;
    return ancestors.subst;
  }

  /**
  ** This funtion tests whether this Clause has an associated ancestry 
  ** record of Clauses.
  ** @return <tt>true</tt> iff the are known ancestors to this Clause
  */
  protected boolean hasAncestorClauses() {
    return ((ancestors != null) && 
       (! (ancestors instanceof JavaAgent.resource.fopl.Instantiation)));
  }

  /**
  ** This function returns an Enumeration over the Literals in this Clause.
  ** @return an Enumeration over the Literals in this Clause
  */ 
  public Enumeration literals() {
    return theLits.elements();
  }

  /**
  ** A Clause is printed as ( &lt;literal&gt;* ).
  ** @return the String that represents this Clause
  */
  public String toString() {
    String res = "(";
    if (theLits.size() > 0) {
      res += theLits.elementAt(0).toString();
      for (int i=1; i<theLits.size(); i++)
	res += " " + theLits.elementAt(i).toString();
    }
    return res + ")";
  }

  /**
  ** This function tests whether this and the given Object are equal. In
  ** general, two Clauses are equal if they contain equal Literals in the 
  ** same order. This is not a test for logical equivalence or unifyability!
  ** @param otherForm the Clause this one is to be compared to
  ** @return whether the given Object is equal to this one
  */
  public boolean equals(Object otherCl) {
    if (otherCl == null)
      return false;
    if (! (otherCl instanceof Clause))
      return false;
    return theLits.equals(((Clause)otherCl).theLits);
  }

  /**
  ** This function can be used to parse a given String that represents a 
  ** Clause. The syntax in BNF is as follows:
  ** <pre>
  ** &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 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 Clause parse(String s) 
      throws IllegalArgumentException, ParseException {
    if ((s == null) || s.equals(""))
      throw new IllegalArgumentException("Attempt to parse empty String!");
    try {
      YYparse parser = new YYparse("clause " + s);
      return (Clause)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 Clause " + s + 
          " (" + e.getMessage() + ')', 0);
    }
  }

  /**
  ** This function can be used to parse a given InputStream that represents
  ** a Clause. The syntax in BNF is as above except that the first token
  ** should be the word <tt>CLAUSE</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 Clause 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 (Clause)parser.parseResult;
    } catch (IOException ioe) {
      throw ioe;
    } catch (Exception e) {
      throw new ParseException("Parse error in Clause: (" + 
          e.getMessage() + ')', 0);
    }
  }

  /**
  ** the Literals in this Clause
  */
  private Vector theLits;

  /** 
  ** indicates whether this Clause represents a tautology
  */
  private boolean tautology;

  /**
  ** how this Clause has been derived
  */
  private Ancestry ancestors = null;
}

abstract class Ancestry {
  abstract boolean parent(KRSentence cl);
  abstract Vector getParents();
  Substitution subst;
}

class Instantiation extends Ancestry {
  Instantiation(KRSentence krs, Substitution s) {
    parent1 = krs;
    subst = s;
  }
  boolean parent(KRSentence cl) {
    return cl.equals(parent1);
  }
  Vector getParents() {
    Vector res = new Vector(2);
    //res.addElement(parent1);
    return res;
  }
  KRSentence parent1;
}

class InEqStep extends Ancestry {
  InEqStep(Clause cl, Literal lit, Substitution s) {
    parent1 = cl;
    lit1 = lit;
    subst = s;
  }
  boolean parent(KRSentence cl) {
    return (cl==parent1);
  }
  Vector getParents() {
    Vector res = new Vector(2);
    res.addElement(parent1);
    return res;
  }
  Clause parent1;
  Literal lit1;
}

class RStep extends Ancestry {
  RStep(Clause cl1, Literal l1, Clause cl2, Literal l2, Substitution s) {
    parent1 = cl1;
    lit1 = l1;
    parent2 = cl2;
    lit2 = l2;
    subst = s;
  }
  boolean parent(KRSentence cl) {
    return ((cl==parent1) || (cl==parent2));
  }
  Vector getParents() {
    Vector res = new Vector(3);
    res.addElement(parent1);
    res.addElement(parent2);
    return res;
  }
  Clause parent1, parent2;
  Literal lit1, lit2;
}

class PStep extends Ancestry {
  PStep(Clause cl1, Literal l1, Term t1, Clause cl2, Literal l2, Term t2, 
      Substitution s) {
    parent1 = cl1;
    lit1 = l1;
    term1 = t1;
    parentEq = cl2;
    litEq = l2;
    termEq = t2;
    subst = s;
  }
  boolean parent(KRSentence cl) {
    return ((cl==parent1) || (cl==parentEq));
  }
  Vector getParents() {
    Vector res = new Vector(3);
    res.addElement(parent1);
    res.addElement(parentEq);
    return res;
  }
  Clause parent1, parentEq;
  Literal lit1, litEq;
  Term term1, termEq;
}
