package org.mandarax.reference;

/*
 * Copyright (C) 1999-2004 <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 java.util.*;
import org.mandarax.kernel.*;
import org.mandarax.util.logging.LogCategories;

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

	private List           subNodes      = new java.util.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 = LogicFactory.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.
	 * @see org.mandarax.kernel.DerivationNodeImpl
	 * @return the state, the value is one of the constants defined in org.mandarax.kernel.DerivationNodeImpl
	 */
	public int getState() {
		return isFailed()
			   ? org.mandarax.kernel.DerivationNode.FAILED
			   : org.mandarax.kernel.DerivationNode.SUCCESS;
	}
	/**
     * Indicates whether the result at the given index is supported by this node.
     * @param int 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 int 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.
	 * @return boolean
	 * @param dn a child node
	 */
	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!
	 * @return a term that is the result of applying the unification or a renaming to the original term
	 * @param original a 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.
	 * @return a term
	 * @param original 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,
	 * @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
	 * @param originals an array of terms
	 */
    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 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;
    }
}
