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.List;

import org.mandarax.kernel.Clause;
import org.mandarax.kernel.Fact;
import org.mandarax.kernel.SelectionPolicy;

/**
 * Selection policy that orders literals from the left to the right, 
 * but moves all negated literals to the right.<br>
 * Using this selection policy can proof R(a) from -P(x),Q(x) -> R(x),Q(a) , using 
 * 'left most selection' would only be able to do this with prerequisites 
 * being in a different position.
 * @author <A HREF="mailto:mandarax@jbdietrich.com">Jens Dietrich</A>
 * @version 3.3.1 <9 August 2004>
 * @since 2.0
 */
public final class DefaultSelectionPolicy implements SelectionPolicy {

	/**
	 * Return an array of integers specifying in which order the inference engine
	 * should attempt to unify the literals with the candidate.
	 * @return int[] the indices
	 * @param goal the goal
	 * @param appliedClause the clause that should be used to prove the goal
	 */
	public int[] getOrderedPositions(Clause goal, Clause appliedClause) {
		
		List literals = goal.getNegativeLiterals ();
		int l = literals.size ();
		int[] positions = new int[l];
		int[] nafPositions = new int[l];
		int i=0;
		int j=0;
		int k=0;

		for(i=0; i < l; i++) {
			if (((Fact)literals.get(i)).isNegatedAF()) {
				nafPositions[k] = i;
				k=k+1;
			}
			else {
				positions[j] = i;
				j=j+1;
			}
		}
		if (k>0) {
			for (i=0;i<k;i++) {
				positions[j] = nafPositions[i];
				j=j+1;
			} 
		}

		return positions;
	}
}
