package org.mandarax.reference;

/*
 * Copyright (C) 1999-2004 <a href="mailto:mandarax@jbdietrich.com">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="mailto:mandarax@jbdietrich.com">Jens Dietrich</A>
 * @version 3.3.1 <9 August 2004>
 * @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&lt4,L3]
	 * would be +[]-[L1,L2,2&lt4,L3]. If  the parameter was +[]-[L1,L2,2&gt4,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;
	}
		
}
