package ws.prova.reference;

/*
 * Copyright (C) 1999-2005 <a href="mailto:mandarax@jbdietrich.com">Jens Dietrich</a>
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

import org.mandarax.kernel.*;
import org.mandarax.reference.SemanticEvaluationPolicy;
import org.mandarax.util.logging.LogCategories;

import java.util.*;

/**
 * Derivation nodes represent application of a single rule.
 *
 * @author <A HREF="mailto:mandarax@jbdietrich.com">Jens Dietrich</A>
 * @author <A HREF="mailto:a.kozlenkov@city.ac.uk">Alex Kozlenkov</A>
 * @version 3.3.1 <9 August 2004>
 * @since 1.0
 *        Prova re-integration modifications
 */
public class DerivationNodeImpl implements DerivationNode, LogCategories {

	private List subNodes = new Vector();
	private boolean failed = false;
	private Unification unification = null;
	private Clause appliedClause = null;
	private Clause query = null;
	private DerivationNodeImpl parent = null;
	private SemanticEvaluationPolicy semanticEvaluationPolicy = null;
	private static LogicFactory lfactory = DefaultLogicFactory.getDefaultFactory();
	Map varRenamings = new HashMap();
	private int id = 0;
	private boolean isLastNode = false;
	private boolean isResultNode = false;
	private boolean isCut = false;
	// 2.2
	// Further corrections 28/04/03
	private Object cutPredicate = null;

	private BitSet supportedSolutions = null;

	/**
	 * Cache the string representation for optimized debugging.
	 */
	private transient String cachedToString = null;

	/**
	 * Constructor.
	 */
	public DerivationNodeImpl() {
		super();
	}

	/**
	 * Add a subnode.
	 *
	 * @param dn a child node
	 */
	public void addSubNode(DerivationNodeImpl dn) {
		subNodes.add(dn);
		dn.parent = this;
	}

	/**
	 * Get the applied clause.
	 *
	 * @return the applied clause
	 */
	public Clause getAppliedClause() {
		return appliedClause;
	}

	/**
	 * Get the parent derivation node.
	 *
	 * @return the parent node
	 */
	public DerivationNodeImpl getParent() {
		return parent;
	}

	/**
	 * Get the query.
	 *
	 * @return the query
	 */
	public Clause getQuery() {
		return query;
	}

	/**
	 * Get the state of this node.
	 *
	 * @return the state, the value is one of the constants defined in org.mandarax.kernel.DerivationNodeImpl
	 * @see org.mandarax.reference.DerivationNodeImpl
	 */
	public int getState() {
		return isFailed()
				? DerivationNode.FAILED
				: DerivationNode.SUCCESS;
	}

	/**
	 * Indicates whether the result at the given index is supported by this node.
	 *
	 * @param resultNumber - the number of the result in the result set indexing starts with 0
	 * @return boolean
	 */
	public boolean isSupported(int resultNumber) {
		return supportedSolutions != null && supportedSolutions.get(resultNumber);
	}

	/**
	 * Set the result number as supported.
	 *
	 * @param resultNumber - the number of the result in the result set indexing starts with 0
	 */
	public void setSupported(int resultNumber) {
		if (supportedSolutions == null) supportedSolutions = new BitSet();
		supportedSolutions.set(resultNumber);
	}

	/**
	 * Get the sub nodes.
	 *
	 * @return a list containing the child nodes
	 */
	public List getSubNodes() {
		return subNodes;
	}

	/**
	 * Get the unification.
	 *
	 * @return the unification applied
	 */
	public Unification getUnification() {
		return unification;
	}

	/**
	 * Indicates whether this derivation step has failed.
	 *
	 * @return true if this proof step has failed, false otherwise
	 */
	public boolean isFailed() {
		return failed;
	}

	/**
	 * Remove a subnode.
	 *
	 * @param dn a child node
	 * @return boolean
	 */
	public boolean removeSubNode(DerivationNodeImpl dn) {
		dn.parent = null;
		return subNodes.remove(dn);
	}

	/**
	 * Replace a term. Check unification and renamings - do not traverse children.
	 * Method has been changed in 1.9.2 to support complex terms!
	 *
	 * @param original a term
	 * @return a term that is the result of applying the unification or a renaming to the original term
	 */
	private Term replaceByUnificationOrRenaming(Term original) {

		boolean debug = LOG_IE_RESULT.isDebugEnabled();
		Term replacedHere = original;

		if (debug) LOG_IE_RESULT.debug("Replace " + original + " in node " + this);

		Replacement r = null;

		// first check the unification
		if (getUnification() != null) {
			Collection uni = getUnification().replacements;

			for (Iterator it = uni.iterator(); it.hasNext();) {
				r = (Replacement) it.next();
				replacedHere = replacedHere.apply(r);
				if (debug) LOG_IE_RESULT.debug("Replaced by unification " + original + " -> " + replacedHere);
			}
		}

		// apply renamings
		if (replacedHere instanceof VariableTerm) {
			// more effective for variable terms
			Object rp = varRenamings.get(replacedHere);
			if (rp != null) {
				replacedHere = (Term) rp;
				if (debug) LOG_IE_RESULT.debug("Replaced by var renaming " + original + " -> " + replacedHere);
			}

		} else {
			// general, in particular for complex terms
			for (Iterator iter = varRenamings.keySet().iterator(); iter.hasNext();) {
				Term nextKey = (Term) iter.next();
				r = new Replacement();
				r.original = nextKey;
				r.replacement = (Term) varRenamings.get(nextKey);
				replacedHere = replacedHere.apply(r);
				if (debug) LOG_IE_RESULT.debug("Replaced by var renaming " + original + " -> " + replacedHere);
			}
		}

		// try to simplify terms - only necessary for complex terms
		if (replacedHere instanceof ComplexTerm) {
			// TODO pass session !
			replacedHere = getSemanticEvaluationPolicy().evaluate((ComplexTerm) replacedHere, appliedClause, null, debug);
		}

		return replacedHere;

	}

	/**
	 * Replace a term.
	 *
	 * @param original a term
	 * @return a term
	 */
	Term replace(Term original) {

		Term replacedHere = replaceByUnificationOrRenaming(original);

		// the following code has been replace as from version 1.8 !!
		// now we check whether there are more subnodes. In this case we must continue replacing !!
		/*
		if(getSubNodes ().isEmpty ()) return replacedHere;
		else {
			List sn = getSubNodes ();
			DerivationNodeImpl nextNode = (DerivationNodeImpl) sn.get(sn.size () - 1);
			return nextNode.replace (replacedHere);
		}
		*/

		// new code: look for the first successful node
		for (Iterator iter = getSubNodes().iterator(); iter.hasNext();) {
			DerivationNodeImpl nextNode = (DerivationNodeImpl) iter.next();
			if (!nextNode.isFailed()) return nextNode.replace(replacedHere);
		}
		return replacedHere;
	}

	/**
	 * Replace a term and add any replacements found to the list,
	 *
	 * @param originals an array of terms
	 * @return an array of lists, each containing a list of terms representing the
	 *         solution for the variable at the respective position
	 *         [Prova] Made public to be callable from ws.prova.reference.ProvaResultSetImpl2
	 */
//	public void replace(List[] replacements, Term[] originals) {
//		boolean logOn = LOG_IE_RESULT.isDebugEnabled();
//		Term[] replacedHere = new Term[originals.length];
//		for (int i = 0; i < originals.length; i++) {
//			replacedHere[i] = replaceByUnificationOrRenaming(originals[i]);
//		}
//		if (logOn) {
//			LOG_IE_RESULT.debug("Replaced in derivation node " + this);
//			boolean somethingReplaced = false;
//			for (int i = 0; i < originals.length; i++) {
//				if (originals[i] != replacedHere[i]) {
//					LOG_IE_RESULT.debug(originals[i] + " -> " + replacedHere[i]);
//					somethingReplaced = true;
//				}
//				if (!somethingReplaced) LOG_IE_RESULT.debug("<nothing replaced>");
//			}
//		}
//		//boolean finalNode = true;
//		for (Iterator iter = getSubNodes().iterator(); iter.hasNext();) {
//			DerivationNodeImpl nextNode = (DerivationNodeImpl) iter.next();
//			//finalNode = false;
//			if (!nextNode.isFailed()) nextNode.replace(replacements, replacedHere);
//		}
//		if (isResultNode) {
//			if (logOn) LOG_IE_RESULT.debug("Add solution in node " + this);
//			for (int i = 0; i < originals.length; i++) {
//				replacements[i].add(replacedHere[i]);
//			}
//		}
//	}

	/**
	 * Set the applied clause.
	 *
	 * @param c the applied clause
	 */
	public void setAppliedClause(Clause c) {
		cachedToString = null;
		appliedClause = c;
	}

	/**
	 * Set the failed flag.
	 *
	 * @param f true if this node has failed, false otherwise
	 */
	public void setFailed(boolean f) {
		cachedToString = null;
		failed = f;
	}
	
	/**
	 * Set the partent node.
	 *
	 * @param n a node
	 */
	public void setParent(DerivationNodeImpl n) {
		parent = n;
	}

	/**
	 * Set the query.
	 *
	 * @param f a query
	 */
	public void setQuery(Clause f) {
		query = f;
	}

	/**
	 * Set the subnodes.
	 *
	 * @param sn a list of subnodes
	 */
	public void setSubNodes(List sn) {
		subNodes = sn;

		for (Iterator it = sn.iterator(); it.hasNext();) {
			((DerivationNodeImpl) it.next()).parent = this;
		}
	}

	/**
	 * Set the unification.
	 *
	 * @param u a unification
	 */
	public void setUnification(Unification u) {
		unification = u;
	}

	/**
	 * Convert the derivation node to a string.
	 *
	 * @return the string representation of this object
	 */
	public String toString() {
		if (cachedToString == null) {
			StringBuffer buf = new StringBuffer();
			buf.append("NODE ");
			buf.append(id);
			buf.append(" : CLAUSE: \"");
			if (getAppliedClause() == null) {
				buf.append("<NONE>");
			} else
				buf.append(getAppliedClause().toString());
			buf.append("\" FAILED: ");
			buf.append(isFailed());
			buf.append(" IS_LAST_NODE: ");
			buf.append(this.isLastNode);
			cachedToString = buf.toString();
		}
		return cachedToString;
	}

	/**
	 * Dump the derivation node and the subtree having this node as a root to the print writer.
	 * This method is for developer support only.
	 *
	 * @param out a print stream
	 */
	public void dump(java.io.PrintStream out) {
		dump(out, 0);
	}

	/**
	 * Dump the derivation node and the subtree having this node as a root to the print writer.
	 * This method is for developer support only.
	 *
	 * @param out        a print stream
	 * @param childLevel the child level (visualized by an indent)
	 */
	private void dump(java.io.PrintStream out, int childLevel) {
		startLine(out, childLevel);
		out.println(this);
		// recursion
		List subNodes = getSubNodes();
		for (Iterator iter = subNodes.iterator(); iter.hasNext();) {
			((DerivationNodeImpl) iter.next()).dump(out, childLevel + 1);
		}
	}

	/**
	 * Start a line. Support method for dump.
	 * out a print stream
	 *
	 * @param childLevel the child level
	 */
	private void startLine(java.io.PrintStream out, int childLevel) {
		out.print(childLevel);
		int maxIndent = 10;
		int indent = 1 + Math.min(childLevel, maxIndent);
		char indentChar = '.';
		for (int i = 0; i < indent; i++) out.print(indentChar);

	}

	/**
	 * Returns the semantic evaluation policy.
	 *
	 * @return the policy
	 */
	SemanticEvaluationPolicy getSemanticEvaluationPolicy() {
		return semanticEvaluationPolicy == null ? this.parent.getSemanticEvaluationPolicy() : semanticEvaluationPolicy;
	}

	/**
	 * Propagate supported solutions to the parent node.
	 * [Prova] Changed to public to allow out of package inference engines.
	 */
	public void propagateSupportedSolutions() {
		if (supportedSolutions != null && parent != null) {
			for (int i = 0; i < supportedSolutions.length(); i++) {
				if (supportedSolutions.get(i)) {
					parent.setSupported(i);
					if (LOG_IE_STEP.isDebugEnabled()) LOG_IE_STEP.debug("propagate supported result index " + i + " in " + this);
				}
			}
			parent.propagateSupportedSolutions();
		}
	}

	/**
	 * Sets the semantic evaluation policy.
	 * [Prova] Changed to public to allow out of package inference engines.
	 *
	 * @param policy The semantic evaluation policy to set
	 */
	public void setSemanticEvaluationPolicy(SemanticEvaluationPolicy policy) {
		this.semanticEvaluationPolicy = policy;
	}

	/**
	 * Get an array of integers containing the indexes of all solutions supported.
	 *
	 * @return an array of integer
	 */
	public int[] getSupportedResults() {
		if (supportedSolutions == null) return new int[]{};
		int[] resultIndexes = new int[supportedSolutions.length()];
		int i, j = 0;
		for (i = 0; i < supportedSolutions.length(); i++) {
			if (supportedSolutions.get(i)) {
				resultIndexes[j] = i;
				j = j + 1;
			}
		}
		int[] array = new int[j];
		for (i = 0; i < j; i++) array[i] = resultIndexes[i];
		return array;
	}

	public boolean isCut() {
		return isCut;
	}

	public void setCut(boolean cut) {
		isCut = cut;
	}

	public int getId() {
		return id;
	}

	public void setId(int id) {
		this.id = id;
	}

	public Object getCutPredicate() {
		return cutPredicate;
	}

	public void setCutPredicate(Object cutPredicate) {
		this.cutPredicate = cutPredicate;
	}

	public boolean isLastNode() {
		return isLastNode;
	}

	public void setLastNode(boolean lastNode) {
		isLastNode = lastNode;
	}

	public boolean isResultNode() {
		return isResultNode;
	}

	public void setResultNode(boolean resultNode) {
		isResultNode = resultNode;
	}
}
