01: package org.mandarax.reference;
02:
03: /*
04: * Copyright (C) 1999-2004 <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</a>
05: *
06: * This library is free software; you can redistribute it and/or
07: * modify it under the terms of the GNU Lesser General Public
08: * License as published by the Free Software Foundation; either
09: * version 2 of the License, or (at your option) any later version.
10: *
11: * This library is distributed in the hope that it will be useful,
12: * but WITHOUT ANY WARRANTY; without even the implied warranty of
13: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14: * Lesser General Public License for more details.
15: *
16: * You should have received a copy of the GNU Lesser General Public
17: * License along with this library; if not, write to the Free Software
18: * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
19: */
20: import java.util.List;
21:
22: import org.mandarax.kernel.Clause;
23: import org.mandarax.kernel.Fact;
24: import org.mandarax.kernel.SelectionPolicy;
25:
26: /**
27: * Selection policy that orders literals from the left to the right,
28: * but moves all negated literals to the right.<br>
29: * Using this selection policy can proof R(a) from -P(x),Q(x) -> R(x),Q(a) , using
30: * 'left most selection' would only be able to do this with prerequisites
31: * being in a different position.
32: * @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
33: * @version 3.4 <7 March 05>
34: * @since 2.0
35: */
36: public final class DefaultSelectionPolicy implements SelectionPolicy {
37:
38: /**
39: * Return an array of integers specifying in which order the inference engine
40: * should attempt to unify the literals with the candidate.
41: * @return int[] the indices
42: * @param goal the goal
43: * @param appliedClause the clause that should be used to prove the goal
44: */
45: public int[] getOrderedPositions(Clause goal, Clause appliedClause) {
46:
47: List literals = goal.getNegativeLiterals();
48: int l = literals.size();
49: int[] positions = new int[l];
50: int[] nafPositions = new int[l];
51: int i = 0;
52: int j = 0;
53: int k = 0;
54:
55: for (i = 0; i < l; i++) {
56: if (((Fact) literals.get(i)).isNegatedAF()) {
57: nafPositions[k] = i;
58: k = k + 1;
59: } else {
60: positions[j] = i;
61: j = j + 1;
62: }
63: }
64: if (k > 0) {
65: for (i = 0; i < k; i++) {
66: positions[j] = nafPositions[i];
67: j = j + 1;
68: }
69: }
70:
71: return positions;
72: }
73: }
|