/*
 * 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
 */
package org.mandarax.util;


import java.util.Collection;
import java.util.Iterator;
import java.util.List;
import java.util.Vector;
import org.apache.commons.collections.Predicate;
import org.mandarax.kernel.Derivation;
import org.mandarax.kernel.DerivationNode;

/**
 * This class implements some useful in order to analyze proofs.
 * @author <A HREF="mailto:mandarax@jbdietrich.com">Jens Dietrich</A>
 * @version 3.3.1 <9 August 2004>
 * @since 1.2
 */
public class ProofAnalyzer {

    /**
     * Collect all applied clauses meeting a certain condition.
     * @param node a derivation node
     * @param condition a condition
     * @param coll a collection of clauses
     */
    private static void collectClauses(DerivationNode node, org.apache.commons.collections.Predicate condition,Collection coll) {
        if(node == null) {
            return;
        }
        if(condition.evaluate(node)) {
            coll.add (node.getAppliedClause ());
        }
        List subNodes = node.getSubNodes ();
        DerivationNode nextNode = null;
        for(Iterator it = subNodes.iterator (); it.hasNext (); ) {
            nextNode = (DerivationNode) it.next ();
            collectClauses (nextNode, condition, coll);
        }
    }

    /**
     * Collect and return all clauses which have applied used in 
     * the given proof.
     * @return a collection of clauses
     * @param proof a derivation
     */
    public static Collection getAppliedClauses(Derivation proof) {
		org.apache.commons.collections.Predicate condition = new org.apache.commons.collections.Predicate() {
			public boolean evaluate(Object obj) {
				if (obj!=null && obj instanceof DerivationNode) {
					DerivationNode node = (DerivationNode)obj;
					return !node.isFailed();
				}
				return false;
			}
		};
        return getClauses (proof.getRoot (), condition);
    }
	/**
	 * Collect and return all clauses which have been
	 * tried in the given proof.
	 * @return a collection of clauses
	 * @param proof a derivation
	 */
	public static Collection getUsedClauses(Derivation proof) {
		org.apache.commons.collections.Predicate condition = new org.apache.commons.collections.Predicate() {
			public boolean evaluate(Object obj) {
				return true;
			}
		};
		return getClauses (proof.getRoot (), condition);
	}
	/**
	 * Collect and return all clauses which have been
	 * used in the proof of the result with the given number.
	 * @return a collection of clauses
	 * @param proof a derivation
	 */
	public static Collection getAppliedClauses(Derivation proof,final int resultNumber) {
		org.apache.commons.collections.Predicate condition = new org.apache.commons.collections.Predicate() {
			public boolean evaluate(Object obj) {
				if (obj!=null && obj instanceof DerivationNode) {
					DerivationNode node = (DerivationNode)obj;
					return node.isSupported(resultNumber);
				}
				return false;
			}
		};
		return getClauses (proof.getRoot (), condition);
	}

	/**
	 * Collect and return all clauses which occur in a derivations
	 * and meet a certain condition.
	 * @return a collection of clauses
	 * @param node a derivation node
	 * @param condition a condition
	 */
	public static Collection getClauses(DerivationNode node, org.apache.commons.collections.Predicate condition) {
		Collection coll = new Vector ();
		collectClauses (node, condition, coll);
		return coll;
	}
}
