📄 defaultsemanticevaluationpolicy.java
字号:
package org.mandarax.reference;
/*
* Copyright (C) 1999-2004 <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">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.*;
import org.mandarax.kernel.*;
/**
* Default policy to do semantic evaluation: if predicates / functions are semantic,
* always try to evaluate the respective clauses / complex terms.
* @author <A href="http://www-ist.massey.ac.nz/JBDietrich" target="_top">Jens Dietrich</A>
* @version 3.4 <7 March 05>
* @since 2.0
*/
public class DefaultSemanticEvaluationPolicy implements SemanticEvaluationPolicy {
protected LogicFactory lfactory = LogicFactory.getDefaultFactory();
/**
* Try to execute literals in the clause, and remove those literals if the
* result ist true. E.g., the result of performing +[]-[L1,L2,2<4,L3]
* would be +[]-[L1,L2,2<4,L3]. If the parameter was +[]-[L1,L2,2>4,L3],
* null would be returned.
* <p>
* @todo: Check whether we should use the selection policy here, right now we
* use a from the left to the right policy.
* <p>
* A rather sensible question is how to handle exceptions that occur when
* evaluating literals. The approach taken here is that an exception will render
* the literal as "false".
* <p>
* New in 3.3: ground complex terms are evaluated even if the predicate is not a "semantic" predicate.
* This is important to run simple recursive programs like the following implementing factorial:
* <code>
* factorial(1,1)<br>
* IF factorial(n-1,k) THEN factorial(n,n*k)<br>
* ?factorial(5,x)<br>
* </code>
* @param c a clause
* @param session a session object
* @param logOn indicates whether we should log
* @return another clause
*/
public Clause evaluate(Clause c,Session session,boolean logOn) {
Fact literal = null;
List literals = new ArrayList();
for (Iterator it = c.getNegativeLiterals().iterator(); it.hasNext();) {
literal = (Fact) it.next();
// Added in version 3.3 by Jens STARTS HERE
// first simplify facts by resolving complex terms which are ground (do not contain variables)
Term terms[] = literal.getTerms();
for (int i=0;i<terms.length;i++) {
if (terms[i] instanceof ComplexTerm) {
try {
Object obj = terms[i].resolve(session);
Term newTerm = lfactory.createConstantTerm(obj,terms[i].getType());
if (logOn) {
LOG_IE_STEP.debug("Resolved term " + terms[i] + " -> " + newTerm);
}
terms[i] = newTerm;
}
catch (Exception x) {
// may throw runtime exception - in this case we carry on
// with the old term. Could just indicate that the term is not ground
if (logOn) {
LOG_IE_STEP.debug("Cannot evaluate " + literal);
}
}
}
}
// Added code in version 3.3 by Jens ENDS HERE
if (literal.isExecutable()) {
if (logOn) {
LOG_IE_STEP.debug("Evaluate literal " + literal);
}
Boolean result = null;
try {
result = (Boolean) literal.resolve(session);
// changed in version 2.0: support for NAF
result = (result.booleanValue()==literal.isNegatedAF())?Boolean.FALSE:Boolean.TRUE;
}
catch (Exception x) {
LOG_IE_STEP.warn("Error evaluating literal " + literal + " assume it is false");
LOG_IE_STEP.error("Error evaluating literal " + literal, x);
result = Boolean.FALSE;
}
// if true, do not add
if (result.booleanValue()) {
if (logOn) {
LOG_IE_STEP.debug("The following statement is true and therefore removed from the goal: " + literal);
}
}
// if false, return null
else {
if (logOn) {
LOG_IE_STEP.debug("The following statement is false and makes the goal unprovable: " + literal);
}
return null;
}
}
else {
if (logOn) {
LOG_IE_STEP.debug("Don't evaluate literal " + literal);
}
literals.add(literal);
}
}
// build a new instance only some literals have been removed
if (c.getNegativeLiterals().size() > literals.size()) {
List posLit = new ArrayList();
posLit.addAll(c.getPositiveLiterals());
Clause result = new TmpClause(posLit, literals);
return result;
}
else {
return c;
}
}
/**
* Try to evaluate (simplify) a complex term.
* @param ct a complex term
* @param cs the clause set (context object)
* @param session a session object
* @param logOn indicates whether we should log
* @return a term
*/
public Term evaluate(ComplexTerm ct,ClauseSet cs,Session session, boolean logOn){
try {
if (!ct.containsVariables()) {
Term t = lfactory.createConstantTerm(ct.resolve(session),ct.getType());
if (logOn) LOG_IE_RESULT.debug("Replaced by simplification " + ct + " -> " + t);
return t;
}
else {
// Added in version 3.3 by Jens STARTS HERE
// replace ground branches, e.g. x+(5+1) -> x+6
// @TODO Not very efficient, should be improved (e.g. we check sub
// branches again for groundness
Term[] terms = ct.getTerms();
for (int i=0;i<terms.length;i++) {
if (terms[i] instanceof ComplexTerm)
terms[i] = evaluate((ComplexTerm)terms[i],cs,session,logOn);
}
// Added in version 3.3 by Jens ENDS HERE
}
}
catch (Exception x) {
LOG_IE_RESULT.warn("Replacing term by simplification failed",x);
}
return ct;
}
/**
* Try to unify two terms by evaluating them and comparing the results.
* @param t1 the first term
* @param t2 the second term
* @param session a session object
* @param logOn indicates whether we should log
* @return a boolean - true if the terms represent the same object
*/
public boolean evaluateAndCompare(Term t1,Term t2, Session session,boolean logOn) {
// if ((t1.isCompound() && !t2.containsVariables()) || (t2.isCompound() && !t2.containsVariables())) {
// replaced in 3.2.1 by the following lines - thanks to Hans-Henning Wiesner:
if (!t1.containsVariables() && !t2.containsVariables()) {
Object obj1 = t1.resolve(session);
Object obj2 = t2.resolve(session);
return (obj1==obj2) || (obj1!=null && obj2!=null && obj1.equals(obj2));
}
return false;
}
}
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -