001: package org.mandarax.reference;
002:
003: /*
004: * Copyright (C) 2002-2004 <a href="mailto:a.kozlenkov@city.ac.uk">Alex Kozlenkov</a>
005: * Copyright (C) 1999-2004 <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</a>
006: *
007: * This library is free software; you can redistribute it and/or
008: * modify it under the terms of the GNU Lesser General Public
009: * License as published by the Free Software Foundation; either
010: * version 2 of the License, or (at your option) any later version.
011: *
012: * This library is distributed in the hope that it will be useful,
013: * but WITHOUT ANY WARRANTY; without even the implied warranty of
014: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
015: * Lesser General Public License for more details.
016: *
017: * You should have received a copy of the GNU Lesser General Public
018: * License along with this library; if not, write to the Free Software
019: * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
020: */
021:
022: import java.util.ArrayList;
023: import java.util.Iterator;
024: import java.util.List;
025: import org.mandarax.kernel.*;
026: import org.mandarax.util.StringUtils;
027: import org.mandarax.util.logging.LogCategories;
028:
029: /**
030: * Reference implementation of Robinson's unification algorithm.
031: * @author <A HREF="mailto:a.kozlenkov@city.ac.uk">Alex Kozlenkov</A>
032: * @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
033: * @version 3.4 <7 March 05>
034: * @since 1.2
035: * [Prova] Most methods made inheritable as the class is overridden
036: * by ws.prova.reference.ProvaRobinsonUnificationAlgorithm
037: * @author <A HREF="mailto:a.kozlenkov@city.ac.uk">Alex Kozlenkov</A>
038: * @version 3.4 <7 March 05>
039: */
040: public class RobinsonsUnificationAlgorithm implements
041: ExtendedUnificationAlgorithm, LogCategories {
042:
043: private SemanticEvaluationPolicy semanticEvaluationPolicy = new DefaultSemanticEvaluationPolicy();
044:
045: /**
046: * Constructor.
047: */
048: public RobinsonsUnificationAlgorithm() {
049: super ();
050: }
051:
052: /**
053: * Apply a replacement to an array of terms.
054: * @return an array containing the results of applying the replacement
055: * @param t an array of terms
056: * @param r a replacement
057: */
058: protected Term[] apply(Term[] t, Replacement r) {
059: Term[] tn = new Term[t.length];
060:
061: for (int i = 0; i < t.length; i++) {
062: tn[i] = t[i].apply(r);
063: }
064:
065: return tn;
066: }
067:
068: /**
069: * Get an array of all subterms of an array of terms.
070: * @return an array containing all subterms of all terms of the inpute array
071: * @param terms an array of terms
072: */
073: protected Term[] getAllSubterms(Term[] terms) {
074: int i, l = 0;
075: Term[] st = null;
076:
077: // compute the length and set up collected
078: for (i = 0; i < terms.length; i++) {
079: l = l + terms[i].getAllSubterms().length;
080: }
081:
082: Term[] collected = new Term[l];
083:
084: // populate collected
085: int j = 0;
086:
087: for (i = 0; i < terms.length; i++) {
088:
089: // inject all subterms for each term
090: st = terms[i].getAllSubterms();
091:
092: for (int k = 0; k < st.length; k++) {
093: collected[j] = st[k];
094: j = j + 1;
095: }
096: }
097:
098: return collected;
099: }
100:
101: /**
102: * Unify the two arrays of terms. Return <code>Unification.noUnificationPossible</code> if unifiction fails.
103: * @see org.mandarax.kernel.Unification#noUnificationPossible
104: * @return the computed unification
105: * @param t1 the first array of terms
106: * @param t2 the second array of terms
107: * @param session a session
108: */
109: public Unification unify(Term[] t1, Term[] t2, Session session) {
110: List substitutions = new ArrayList();
111: boolean logOn = LOG_IE_UNIFICATION.isDebugEnabled();
112:
113: if (logOn) {
114: LOG_IE_UNIFICATION.debug("Trying to unify: "
115: + StringUtils.toString(t1) + " and "
116: + StringUtils.toString(t2));
117: }
118:
119: return unify(t1, t2, substitutions, 0, session, logOn);
120: }
121:
122: public Unification unify(Term[] t1, Term[] t2, boolean isRule) {
123: return null; //To change body of implemented methods use File | Settings | File Templates.
124: }
125:
126: /**
127: * Unify two arrays of terms.
128: * @return org.mandarax.kernel.Unification
129: * @param t1 the first array of terms
130: * @param t2 the second array of terms
131: * @param subst the list of replavements
132: * @param start start investigation at this index
133: * @param session a session
134: * @param logOn if true then we log
135: */
136: protected org.mandarax.kernel.Unification unify(Term[] t1,
137: Term[] t2, List subst, int start, Session session,
138: boolean logOn) {
139: Term[] subTerms1 = getAllSubterms(t1);
140: Term[] subTerms2 = getAllSubterms(t2);
141: int maxIdx = Math.min(subTerms1.length, subTerms2.length);
142: Term subTerm1, subTerm2, original, replace;
143:
144: for (int i = start; i < maxIdx; i++) {
145: original = null;
146: replace = null;
147: subTerm1 = subTerms1[i];
148: subTerm2 = subTerms2[i];
149:
150: // find the first index to unify
151: if (!subTerm1.sameAs(subTerm2)) {
152:
153: // check whether there is a variable
154: if (subTerm1.isVariable()) {
155: original = subTerm1;
156: replace = subTerm2;
157: } else if (subTerm2.isVariable()) {
158: original = subTerm2;
159: replace = subTerm1;
160: }
161:
162: // test code to solve bug 1086990 - by jens
163: // not yet released - do not uncomment !!
164: // handle case if one term is complex variable -- test version starts
165: /*
166: if (original==null) {
167: if(subTerm1.containsVariables()) {
168: original = subTerm1;
169: replace = subTerm2;
170: } else if(subTerm2.containsVariables()) {
171: original = subTerm2;
172: replace = subTerm1;
173: }
174: }
175: */
176: // handle case if one term is complex variable -- test version ends
177: // no unification possible if there is no variable
178: if (original == null) {
179: if (semanticEvaluationPolicy != null
180: && semanticEvaluationPolicy
181: .evaluateAndCompare(subTerm1,
182: subTerm2, session, logOn))
183: continue;
184: else
185: return Unification.noUnificationPossible;
186: }
187:
188: // otherwise continue and enter recursion .. keep track of the index in order to not to waste time
189: // investigating the same terms twice
190: Replacement r = new Replacement(original, replace);
191: subst.add(r);
192: return unify(apply(t1, r), apply(t2, r), subst, i + 1,
193: session, logOn);
194: }
195: }
196:
197: // if the algorithm is here, both terms have been unified (are equal)
198: if (logOn) {
199: LOG_IE_UNIFICATION.debug("Unified: "
200: + StringUtils.toString(t1) + " and "
201: + StringUtils.toString(t2));
202: LOG_IE_UNIFICATION.debug("Substitutions:");
203:
204: for (Iterator it = subst.iterator(); it.hasNext();) {
205: LOG_IE_UNIFICATION.debug(it.next().toString());
206: }
207: }
208:
209: return new Unification(subst, t1, t2);
210: }
211:
212: /**
213: * Returns the semantic evaluation policy.
214: * @return the semantic evaluation policy
215: */
216: public SemanticEvaluationPolicy getSemanticEvaluationPolicy() {
217: return semanticEvaluationPolicy;
218: }
219:
220: /**
221: * Sets the semantic evaluation policy.
222: * @param semanticEvaluationPolicy The semantic evaluation policy to set
223: */
224: public void setSemanticEvaluationPolicy(
225: SemanticEvaluationPolicy semanticEvaluationPolicy) {
226: this.semanticEvaluationPolicy = semanticEvaluationPolicy;
227: }
228:
229: }
|