package JavaAgent.resource.fopl;


import java.util.*;
import java.io.*;

/**
** An RTProver is a resolution theorem prover. Currently it maintains two
** Vectors of Clauses, the open and closed Clauses. Clauses can be added to
** either Vector with the appropriate add-functions. Once the RTProver is 
** set up in this way the function <tt>resolve()</tt> can be called to start 
** the reasoning process.
** <p> The basic strategy is very simple. The RTProver takes the first Clause
** from the Vector of open Clauses and generates all resolvents with Clauses 
** from the Vector of closed Clauses over only one of the Literals in the 
** former Clause (the one that generates the fewest successors). The first 
** Clause in the Vector of open Clauses is then moved to the Vector of closed 
** Clausesand the new Clauses are added to the Vector of open Clauses. This
** process is repeated with the first Clause in the Vector of open Clauses 
** until either the empty Clause has been generated, or until the Vector
** of open Clauses is empty.
** @see Clause
*/

public class RTProver {

  /**
  ** This constructor creates an RTProver.
  */
  public RTProver() {
    open = new Vector(1000, 200);
    closed = new Vector(1000, 200);
    containsEmptyClause = false;
  }

  /** 
  ** This function can be used to add Clauses to the Vector of open Clauses.
  ** @param aClause the Clause to be added
  ** @exception IllegalArgumentException An exception will occur if the given 
  ** Clause is null.
  */
  public void addOpenClause(Clause aClause) throws IllegalArgumentException {
    if (aClause == null)
      throw new IllegalArgumentException(
          "Attempt to add null Clause to open Clauses.");
    if (aClause.isEmpty())
      containsEmptyClause = true;
    if (! aClause.isTautology())
      open.addElement(aClause);
  } 

  /** 
  ** This function can be used to add Clauses to the Vector of closed Clauses.
  ** @param aClause the Clause to be added
  ** @exception IllegalArgumentException An exception will occur if the given 
  ** Clause is null.
  */
  public void addClosedClause(Clause aClause) throws IllegalArgumentException {
    if (aClause == null)
      throw new IllegalArgumentException(
          "Attempt to add null Clause to closed Clauses.");
    if (aClause.isEmpty())
      containsEmptyClause = true;
    if (! aClause.isTautology())
      closed.addElement(aClause);
  } 

  /**
  ** This function executes the resolution theorem proving process. The basic
  ** strategy is outlined above. The process stops when there are no more open
  ** Clauses and returns <tt>true</tt> indicating satisfyability. If it stops 
  ** because the empty Clause has been generated it will return <tt>false</tt> 
  ** indicating inconsistency.
  ** @return <tt>false</tt> if the given Clauses were inconsistent
  ** @exception IOException An exception can occur if writing to the given 
  ** OutputStream for tracing fails.
  */
  public boolean resolve() throws IOException {

    // writing out the initial clauses for tracing:
    if (traceStream != null) {
      traceStream.write((new String("Clauses in Closed:\n")).getBytes());
      for (Enumeration cce=closed.elements(); cce.hasMoreElements(); ) {
	traceStream.write(((Clause)cce.nextElement()).toString().getBytes());
	traceStream.write((int)'\n');
      }
      traceStream.write((new String("Clauses in Open:\n")).getBytes());
      for (Enumeration oce=open.elements(); oce.hasMoreElements(); ) {
	traceStream.write(((Clause)oce.nextElement()).toString().getBytes());
	traceStream.write((int)'\n');
      }
      traceStream.write((new String("New Clauses:\n")).getBytes());
    }

    if (containsEmptyClause)
      return false;

    // now generating new clauses:
    while ((! open.isEmpty()) && (closed.size() < searchLimit)) {
      Clause nextCl = (Clause)open.firstElement();
      open.removeElementAt(0);
      addClosedClause(nextCl);
      Vector newCls = nextCl.getResolvents(closed);
      for (Enumeration en=newCls.elements(); en.hasMoreElements(); ) {
	Clause newCl = (Clause)en.nextElement();
	if (traceStream != null) {
	  traceStream.write(newCl.toString().getBytes());
	  traceStream.write((int)'\n');
	}
	addOpenClause(newCl);
	if (newCl.isEmpty()) {
	  lastRefute = extractRefutation();
	  return false;
	}
      }
    }
    lastRefute = null;
    return true;
  }

  /**
  ** This function extracts a proof from the Clauses currently in the closed
  ** and open sets. The last open Clause should be the empty Clause. The
  ** result is a Vector that contains all those Clauses that were involved 
  ** in the proof (in the order they were generated).
  ** @return A vector with all Clauses involved in the proof
  */
  protected Vector extractRefutation() {
    Vector pClauses = new Vector();
    pClauses.addElement(open.elementAt(open.size()-1));
    extractRefutation(pClauses, open);
    extractRefutation(pClauses, closed);
    return reverse(pClauses);
  }

  private void extractRefutation(Vector pClauses, Vector allClauses) {
    for (int i=allClauses.size()-1; i>=0; i--) {
      Clause nextCl = (Clause)allClauses.elementAt(i);
      for (Enumeration ce=pClauses.elements(); ce.hasMoreElements(); )
	if (((Clause)ce.nextElement()).hasParent(nextCl)) {
	  pClauses.addElement(nextCl);
	  break;
	}
    }
  }

  static private Vector reverse(Vector v) {
    Vector res = new Vector();
    for (int i=v.size()-1; i>=0; i--)
      res.addElement(v.elementAt(i));
    return res;
  }

  /**
  ** This function extracts the values for the given Variables from the
  ** last refutation. It returns a Hashtable in which Variables are mapped
  ** to Terms. It cannot be guaranteed that given Variables will occor in the
  ** Hashtable or that they will be mapped to a value.
  ** @param vars a Vector of Variables
  ** @return a Hashtable containing the Terms the given Variables were
  ** mapped to.
  */
  public Hashtable extractValues(Vector vars) {
    Hashtable clausesAndMaps = new Hashtable();
    for (Enumeration ce=lastRefute.elements(); ce.hasMoreElements(); ) {
      Clause cl = (Clause)ce.nextElement();
      //System.out.println("Current clause: " + cl);
      if (cl.hasAncestorClauses())
	clausesAndMaps.put(cl, combineMappings(cl, clausesAndMaps));
      else 
	clausesAndMaps.put(cl, getNewMapping(vars, cl));
      //System.out.println("Mapping: " + clausesAndMaps.get(cl));
      if (cl.isEmpty())
	return (Hashtable)clausesAndMaps.get(cl);
    }
    return null;
  }

  private Hashtable getNewMapping(Vector vars, Clause cl) {
    Hashtable res = new Hashtable();
    Vector clVars = cl.getVars();
    //System.out.println("Vars in clause: " + clVars);
    for (Enumeration ve=vars.elements(); ve.hasMoreElements(); ) {
      Variable nv = (Variable)ve.nextElement();
      Variable cv = Variable.get(nv.getName(), clVars);
      //System.out.println("Mapping: " + nv + " to " + cv);
      if (cv != null)
	res.put(nv, new VarTerm(cv));
    }
    return res;
  }

  private Hashtable combineMappings(Clause cl, Hashtable clausesAndMaps) {
    Hashtable res = new Hashtable();
    Vector parents = cl.getParents();
    //System.out.println("Parents: " + parents);
    Substitution s = cl.getParentSubstitution();
    for (Enumeration ce=parents.elements(); ce.hasMoreElements(); ) {
      Clause pCl = (Clause)ce.nextElement();
      Hashtable pMap = (Hashtable)clausesAndMaps.get(pCl);
      for (Enumeration ve=pMap.keys(); ve.hasMoreElements(); ) {
	Variable v = (Variable)ve.nextElement();
	if (! res.containsKey(v))
	  res.put(v, ((Term)pMap.get(v)).clone(s));
      }
    }
    return res;
  }

  /**
  ** This function tests whether the given KRSentence was used in the last
  ** derivation.
  ** @param krs the KRSentence to be tested
  ** @return true iff it was used in the derivation
  */
  public boolean usedInProof(JavaAgent.resource.cdl.KRSentence krs) {
    for (Enumeration ce=lastRefute.elements(); ce.hasMoreElements(); ) {
      Clause cl = (Clause)ce.nextElement();
      if (cl.hasParent(krs))
	return true;
    }
    return false;
  }

  /**
  ** This function can be used to set the search limit for this RTProver.
  ** Effectively, this limits the number of Clauses that can be in the set
  ** of closed nodes. Note that this set is not empty to start with.
  ** @param limit the search limit
  */
  public void setSearchLimit(int limit) {
    searchLimit = limit;
  }

  /** 
  ** This function can be used create a trace of the function 
  ** <tt>resolve()</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;
  }

  /**
  ** the maximum number of Clauses that will be explored
  */
  static protected int searchLimit = 500;

  /**
  ** a Vector of Clauses that represent the last refutation by this RTProver
  */
  protected Vector lastRefute;

  /** 
  ** the Vector of open Clauses
  */
  protected Vector open;

  /** 
  ** the Vector of closed Clauses
  */
  protected Vector closed;

  /**
  ** this boolean indicates whether the open or closed Clauses contain the 
  ** empty Clause
  */
  protected boolean containsEmptyClause;

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