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:
021: import java.util.*;
022: import org.mandarax.kernel.*;
023:
024: /**
025: * Default policy to do semantic evaluation: if predicates / functions are semantic,
026: * always try to evaluate the respective clauses / complex terms.
027: * @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
028: * @version 3.4 <7 March 05>
029: * @since 2.0
030: */
031: public class DefaultSemanticEvaluationPolicy implements
032: SemanticEvaluationPolicy {
033:
034: protected LogicFactory lfactory = LogicFactory.getDefaultFactory();
035:
036: /**
037: * Try to execute literals in the clause, and remove those literals if the
038: * result ist true. E.g., the result of performing +[]-[L1,L2,2<4,L3]
039: * would be +[]-[L1,L2,2<4,L3]. If the parameter was +[]-[L1,L2,2>4,L3],
040: * null would be returned.
041: * <p>
042: * @todo: Check whether we should use the selection policy here, right now we
043: * use a from the left to the right policy.
044: * <p>
045: * A rather sensible question is how to handle exceptions that occur when
046: * evaluating literals. The approach taken here is that an exception will render
047: * the literal as "false".
048: * <p>
049: * New in 3.3: ground complex terms are evaluated even if the predicate is not a "semantic" predicate.
050: * This is important to run simple recursive programs like the following implementing factorial:
051: * <code>
052: * factorial(1,1)<br>
053: * IF factorial(n-1,k) THEN factorial(n,n*k)<br>
054: * ?factorial(5,x)<br>
055: * </code>
056: * @param c a clause
057: * @param session a session object
058: * @param logOn indicates whether we should log
059: * @return another clause
060: */
061: public Clause evaluate(Clause c, Session session, boolean logOn) {
062: Fact literal = null;
063: List literals = new ArrayList();
064: for (Iterator it = c.getNegativeLiterals().iterator(); it
065: .hasNext();) {
066: literal = (Fact) it.next();
067:
068: // Added in version 3.3 by Jens STARTS HERE
069: // first simplify facts by resolving complex terms which are ground (do not contain variables)
070: Term terms[] = literal.getTerms();
071: for (int i = 0; i < terms.length; i++) {
072: if (terms[i] instanceof ComplexTerm) {
073: try {
074: Object obj = terms[i].resolve(session);
075: Term newTerm = lfactory.createConstantTerm(obj,
076: terms[i].getType());
077: if (logOn) {
078: LOG_IE_STEP.debug("Resolved term "
079: + terms[i] + " -> " + newTerm);
080: }
081: terms[i] = newTerm;
082: } catch (Exception x) {
083: // may throw runtime exception - in this case we carry on
084: // with the old term. Could just indicate that the term is not ground
085: if (logOn) {
086: LOG_IE_STEP.debug("Cannot evaluate "
087: + literal);
088: }
089: }
090: }
091: }
092: // Added code in version 3.3 by Jens ENDS HERE
093:
094: if (literal.isExecutable()) {
095: if (logOn) {
096: LOG_IE_STEP.debug("Evaluate literal " + literal);
097: }
098:
099: Boolean result = null;
100:
101: try {
102: result = (Boolean) literal.resolve(session);
103: // changed in version 2.0: support for NAF
104: result = (result.booleanValue() == literal
105: .isNegatedAF()) ? Boolean.FALSE
106: : Boolean.TRUE;
107: } catch (Exception x) {
108: LOG_IE_STEP.warn("Error evaluating literal "
109: + literal + " assume it is false");
110: LOG_IE_STEP.error("Error evaluating literal "
111: + literal, x);
112: result = Boolean.FALSE;
113: }
114: // if true, do not add
115: if (result.booleanValue()) {
116: if (logOn) {
117: LOG_IE_STEP
118: .debug("The following statement is true and therefore removed from the goal: "
119: + literal);
120: }
121: }
122: // if false, return null
123: else {
124: if (logOn) {
125: LOG_IE_STEP
126: .debug("The following statement is false and makes the goal unprovable: "
127: + literal);
128: }
129: return null;
130: }
131: } else {
132: if (logOn) {
133: LOG_IE_STEP.debug("Don't evaluate literal "
134: + literal);
135: }
136: literals.add(literal);
137: }
138: }
139: // build a new instance only some literals have been removed
140: if (c.getNegativeLiterals().size() > literals.size()) {
141: List posLit = new ArrayList();
142: posLit.addAll(c.getPositiveLiterals());
143: Clause result = new TmpClause(posLit, literals);
144: return result;
145: } else {
146: return c;
147: }
148: }
149:
150: /**
151: * Try to evaluate (simplify) a complex term.
152: * @param ct a complex term
153: * @param cs the clause set (context object)
154: * @param session a session object
155: * @param logOn indicates whether we should log
156: * @return a term
157: */
158: public Term evaluate(ComplexTerm ct, ClauseSet cs, Session session,
159: boolean logOn) {
160:
161: try {
162: if (!ct.containsVariables()) {
163: Term t = lfactory.createConstantTerm(ct
164: .resolve(session), ct.getType());
165: if (logOn)
166: LOG_IE_RESULT.debug("Replaced by simplification "
167: + ct + " -> " + t);
168: return t;
169: } else {
170: // Added in version 3.3 by Jens STARTS HERE
171: // replace ground branches, e.g. x+(5+1) -> x+6
172: // @TODO Not very efficient, should be improved (e.g. we check sub
173: // branches again for groundness
174: Term[] terms = ct.getTerms();
175: for (int i = 0; i < terms.length; i++) {
176: if (terms[i] instanceof ComplexTerm)
177: terms[i] = evaluate((ComplexTerm) terms[i], cs,
178: session, logOn);
179: }
180: // Added in version 3.3 by Jens ENDS HERE
181: }
182: } catch (Exception x) {
183: LOG_IE_RESULT.warn(
184: "Replacing term by simplification failed", x);
185: }
186: return ct;
187: }
188:
189: /**
190: * Try to unify two terms by evaluating them and comparing the results.
191: * @param t1 the first term
192: * @param t2 the second term
193: * @param session a session object
194: * @param logOn indicates whether we should log
195: * @return a boolean - true if the terms represent the same object
196: */
197: public boolean evaluateAndCompare(Term t1, Term t2,
198: Session session, boolean logOn) {
199: // if ((t1.isCompound() && !t2.containsVariables()) || (t2.isCompound() && !t2.containsVariables())) {
200: // replaced in 3.2.1 by the following lines - thanks to Hans-Henning Wiesner:
201: if (!t1.containsVariables() && !t2.containsVariables()) {
202: Object obj1 = t1.resolve(session);
203: Object obj2 = t2.resolve(session);
204: return (obj1 == obj2)
205: || (obj1 != null && obj2 != null && obj1
206: .equals(obj2));
207: }
208: return false;
209: }
210:
211: }
|