001: package org.mandarax.reference;
002:
003: /*
004: * Copyright (C) 1999-2004 <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</a>
005: *
006: * This library is free software; you can redistribute it and/or
007: * modify it under the terms of the GNU Lesser General Public
008: * License as published by the Free Software Foundation; either
009: * version 2 of the License, or (at your option) any later version.
010: *
011: * This library is distributed in the hope that it will be useful,
012: * but WITHOUT ANY WARRANTY; without even the implied warranty of
013: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
014: * Lesser General Public License for more details.
015: *
016: * You should have received a copy of the GNU Lesser General Public
017: * License along with this library; if not, write to the Free Software
018: * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
019: */
020: import java.util.List;
021: import org.mandarax.kernel.*;
022:
023: /**
024: * Helper class to retrieve resolution steps. Instances are created
025: * using the static method <code>resolver(..)</code>.
026: * The created resolution has the following structure:
027: * <ul>
028: * <li> position1 is the position of the resolved fact in clause 1
029: * <li> position1 is the position of the resolved fact in clause 2
030: * <li> unification is the unification computed
031: * <li> order is true if a negative literal from clause 1 has been unified with a positive
032: * literal from clause 2 and false if it is the other way around.
033: * </ul>
034: * @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
035: * @version 3.4 <7 March 05>
036: * @since 1.0
037: * Prova re-integration modifications
038: * @author <A HREF="mailto:a.kozlenkov@city.ac.uk">Alex Kozlenkov</A>
039: * @version 3.4 <7 March 05>
040: */
041: public class Resolution extends org.mandarax.kernel.LObject {
042:
043: public int position1;
044: public int position2;
045: public Unification unification = null;
046:
047: /**
048: * Constructor.
049: * @param p1 position 1
050: * @param p2 position 2
051: * @param u the unification
052: */
053: private Resolution(int p1, int p2, Unification u) {
054: super ();
055:
056: position1 = p1;
057: position2 = p2;
058: unification = u;
059: }
060:
061: /**
062: * Indicate whether this resolution has failed.
063: * @return true if the resolution has failed, false otherwise
064: */
065: public boolean hasFailed() {
066: return (unification == null) || unification.hasFailed();
067: }
068:
069: /**
070: * Resolve the two clauses.
071: * @return the resolution
072: * @param c the clause
073: * @param goal the goal
074: * @param ua the unification algorithm used
075: * @param sp the selection policy used
076: * @param session a session
077: */
078: public static Resolution resolve(Clause c, Clause goal,
079: UnificationAlgorithm ua, SelectionPolicy sp, Session session) {
080: int i, j = 0;
081: Fact f1, f2 = null;
082: Unification u = null;
083: List negLitFromGoal = goal.getNegativeLiterals();
084: List posLit = c.getPositiveLiterals();
085: int[] selection = sp.getOrderedPositions(goal, c);
086:
087: for (i = 0; i < selection.length; i++) {
088: f1 = (Fact) negLitFromGoal.get(selection[i]);
089:
090: for (j = 0; j < posLit.size(); j++) {
091: f2 = (Fact) posLit.get(j);
092:
093: // Corrected in 2.2.1 - take NAF into account
094: // by Hans-Henning Wiesner (Hans-Henning.Wiesner@bauer-partner.com)
095: String p1 = f1.getPredicate().getName();
096: String p2 = f2.getPredicate().getName();
097:
098: if (!p1.equals(p2)
099: || f1.isNegatedAF() != f2.isNegatedAF()) {
100: u = Unification.noUnificationPossible;
101: } else {
102: u = ua.unify(f1.getTerms(), f2.getTerms(), session);
103: }
104: if (!u.hasFailed()) {
105: // in this case, build and return a resolution
106: return new Resolution(selection[i], j, u);
107: }
108: }
109: }
110:
111: return null;
112: }
113:
114: /**
115: * Prova version.
116: * Resolve the two clauses.
117: * @return the resolution
118: * @param c the clause
119: * @param goal the goal
120: * @param ua the unification algorithm used
121: * @param sp the selection policy used
122: */
123: public static Resolution resolve(Clause c, Clause goal,
124: UnificationAlgorithm ua, SelectionPolicy sp, boolean isRule) {
125: int i, j = 0;
126: Fact f1, f2 = null;
127: Unification u = null;
128: List negLitFromGoal = goal.getNegativeLiterals();
129: List posLit = c.getPositiveLiterals();
130: int[] selection = sp.getOrderedPositions(goal, c);
131:
132: for (i = 0; i < selection.length; i++) {
133: f1 = (Fact) negLitFromGoal.get(selection[i]);
134:
135: for (j = 0; j < posLit.size(); j++) {
136: f2 = (Fact) posLit.get(j);
137:
138: // Corrected in 2.2
139: String p1 = f1.getPredicate().getName();
140: String p2 = f2.getPredicate().getName();
141: if (!p1.equals(p2)) {
142: u = Unification.noUnificationPossible;
143: } else {
144: u = ua.unify(f1.getTerms(), f2.getTerms(), isRule);
145: }
146: if (!u.hasFailed()) {
147: // in this case, build and return a resolution
148: return new Resolution(selection[i], j, u);
149: }
150: }
151: }
152:
153: return null;
154: }
155: }
|